Documentation

LeanPool.RegtsSevenster.RS.Classical.Deligne.PointMonoidal.Calculus

A point-free calculus for the two tensor products #

The laws of the comparison are proved by evaluating both sides on generators. This module collects the evaluations: the structural morphisms of the category of super modules over a super-commutative algebra, and of RS.SuperVect, applied to a generator of a tensor product, together with the extensionality principles that reduce an identity of maps out of a twofold or threefold graded tensor product to its values on generators. The comparison itself is defined in Comparison.lean and its laws are proved in Coherence.lean.

Contents #

One-step computations on generators #

The whiskerings, the associator and the unitors of the super modules, and the whiskerings and associator of the super vector spaces, evaluated on the generators of a tensor product. Each is an instance of a computation lemma of the construction; they are collected here so that the coherence proofs below rewrite with concrete equations only.

source
theorem RS.modComp_evenMap_apply {S : SuperCommAlgebra} {X Y Z : S.Mod} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.even) :
(CategoryTheory.CategoryStruct.comp f g).evenMap x = g.evenMap (f.evenMap x)

Composition of super module morphisms, even degree, on an element.

source
theorem RS.modComp_oddMap_apply {S : SuperCommAlgebra} {X Y Z : S.Mod} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X.odd) :
(CategoryTheory.CategoryStruct.comp f g).oddMap x = g.oddMap (f.oddMap x)

Composition of super module morphisms, odd degree, on an element.

source
theorem RS.whiskerRight_evenMap_tmulEE {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (x : X.even) (c : C.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f C).evenMap (((X.tmulEE C) x) c) = ((Y.tmulEE C) (f.evenMap x)) c

Right whiskering on an even-even generator.

source
theorem RS.whiskerRight_evenMap_tmulOO {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (x : X.odd) (c : C.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f C).evenMap (((X.tmulOO C) x) c) = ((Y.tmulOO C) (f.oddMap x)) c

Right whiskering on an odd-odd generator.

source
theorem RS.whiskerRight_oddMap_tmulEO {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (x : X.even) (c : C.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f C).oddMap (((X.tmulEO C) x) c) = ((Y.tmulEO C) (f.evenMap x)) c

Right whiskering on an even-odd generator.

source
theorem RS.whiskerRight_oddMap_tmulOE {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (x : X.odd) (c : C.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f C).oddMap (((X.tmulOE C) x) c) = ((Y.tmulOE C) (f.oddMap x)) c

Right whiskering on an odd-even generator.

source
theorem RS.whiskerLeft_evenMap_tmulEE {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (a : C.even) (x : X.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f).evenMap (((C.tmulEE X) a) x) = ((C.tmulEE Y) a) (f.evenMap x)

Left whiskering on an even-even generator.

source
theorem RS.whiskerLeft_evenMap_tmulOO {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (a : C.odd) (x : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f).evenMap (((C.tmulOO X) a) x) = ((C.tmulOO Y) a) (f.oddMap x)

Left whiskering on an odd-odd generator.

source
theorem RS.whiskerLeft_oddMap_tmulEO {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (a : C.even) (x : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f).oddMap (((C.tmulEO X) a) x) = ((C.tmulEO Y) a) (f.oddMap x)

Left whiskering on an even-odd generator.

source
theorem RS.whiskerLeft_oddMap_tmulOE {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (C : S.Mod) (a : C.odd) (x : X.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft C f).oddMap (((C.tmulOE X) a) x) = ((C.tmulOE Y) a) (f.evenMap x)

Left whiskering on an odd-even generator.

source
theorem RS.actEE_span_one {S : SuperCommAlgebra} {X : S.Mod} (r : ℂ) (z : X.even) :
(X.actEE ((LinearMap.toSpanSingleton ℂ S.even S.one) r)) z = r • z

A scalar multiple of the unit acts by that scalar, in even degree.

source
theorem RS.actEO_span_one {S : SuperCommAlgebra} {X : S.Mod} (r : ℂ) (z : X.odd) :
(X.actEO ((LinearMap.toSpanSingleton ℂ S.even S.one) r)) z = r • z

A scalar multiple of the unit acts by that scalar, in odd degree.

source
theorem RS.mcTensorHom_evenMap_tmulEE {S : SuperCommAlgebra} {X Y X' Y' : S.Mod} (f : X ⟶ Y) (g : X' ⟶ Y') (m : X.even) (n : X'.even) :
(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).evenMap (((X.tmulEE X') m) n) = ((Y.tmulEE Y') (f.evenMap m)) (g.evenMap n)

The monoidal tensor of two morphisms on an even-even generator.

source
theorem RS.mcTensorHom_evenMap_tmulOO {S : SuperCommAlgebra} {X Y X' Y' : S.Mod} (f : X ⟶ Y) (g : X' ⟶ Y') (m : X.odd) (n : X'.odd) :
(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).evenMap (((X.tmulOO X') m) n) = ((Y.tmulOO Y') (f.oddMap m)) (g.oddMap n)

The monoidal tensor of two morphisms on an odd-odd generator.

source
theorem RS.mcTensorHom_oddMap_tmulEO {S : SuperCommAlgebra} {X Y X' Y' : S.Mod} (f : X ⟶ Y) (g : X' ⟶ Y') (m : X.even) (n : X'.odd) :
(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).oddMap (((X.tmulEO X') m) n) = ((Y.tmulEO Y') (f.evenMap m)) (g.oddMap n)

The monoidal tensor of two morphisms on an even-odd generator.

source
theorem RS.mcTensorHom_oddMap_tmulOE {S : SuperCommAlgebra} {X Y X' Y' : S.Mod} (f : X ⟶ Y) (g : X' ⟶ Y') (m : X.odd) (n : X'.even) :
(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).oddMap (((X.tmulOE X') m) n) = ((Y.tmulOE Y') (f.oddMap m)) (g.evenMap n)

The monoidal tensor of two morphisms on an odd-even generator.

source
theorem RS.modAssoc_evenMap_ee {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.even) (n : N.even) (q : Q.even) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.evenMap ((((M.tensor N).tmulEE Q) (((M.tmulEE N) m) n)) q) = ((M.tmulEE (N.tensor Q)) m) (((N.tmulEE Q) n) q)

The associator on the even-even-even generators.

source
theorem RS.modAssoc_evenMap_oo {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.odd) (n : N.odd) (q : Q.even) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.evenMap ((((M.tensor N).tmulEE Q) (((M.tmulOO N) m) n)) q) = ((M.tmulOO (N.tensor Q)) m) (((N.tmulOE Q) n) q)

The associator on the odd-odd-even generators.

source
theorem RS.modAssoc_evenMap_eo {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.even) (n : N.odd) (q : Q.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.evenMap ((((M.tensor N).tmulOO Q) (((M.tmulEO N) m) n)) q) = ((M.tmulEE (N.tensor Q)) m) (((N.tmulOO Q) n) q)

The associator on the even-odd-odd generators.

source
theorem RS.modAssoc_evenMap_oe {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.odd) (n : N.even) (q : Q.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.evenMap ((((M.tensor N).tmulOO Q) (((M.tmulOE N) m) n)) q) = ((M.tmulOO (N.tensor Q)) m) (((N.tmulEO Q) n) q)

The associator on the odd-even-odd generators.

source
theorem RS.modAssoc_oddMap_ee {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.even) (n : N.even) (q : Q.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.oddMap ((((M.tensor N).tmulEO Q) (((M.tmulEE N) m) n)) q) = ((M.tmulEO (N.tensor Q)) m) (((N.tmulEO Q) n) q)

The associator on the even-even-odd generators.

source
theorem RS.modAssoc_oddMap_oo {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.odd) (n : N.odd) (q : Q.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.oddMap ((((M.tensor N).tmulEO Q) (((M.tmulOO N) m) n)) q) = ((M.tmulOE (N.tensor Q)) m) (((N.tmulOO Q) n) q)

The associator on the odd-odd-odd generators.

source
theorem RS.modAssoc_oddMap_eo {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.even) (n : N.odd) (q : Q.even) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.oddMap ((((M.tensor N).tmulOE Q) (((M.tmulEO N) m) n)) q) = ((M.tmulEO (N.tensor Q)) m) (((N.tmulOE Q) n) q)

The associator on the even-odd-even generators.

source
theorem RS.modAssoc_oddMap_oe {S : SuperCommAlgebra} (M N Q : S.Mod) (m : M.odd) (n : N.even) (q : Q.even) :
(CategoryTheory.MonoidalCategoryStruct.associator M N Q).hom.oddMap ((((M.tensor N).tmulOE Q) (((M.tmulOE N) m) n)) q) = ((M.tmulOE (N.tensor Q)) m) (((N.tmulEE Q) n) q)

The associator on the odd-even-even generators.

source
theorem RS.svWhiskerRight_evenMap_inl {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (v : V.even) (x : X.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).evenMap (svEvenInl (v ⊗ₜ[ℂ] x)) = svEvenInl (f.evenMap v ⊗ₜ[ℂ] x)

Right whiskering of super vector spaces, first summand.

source
theorem RS.svWhiskerRight_evenMap_inr {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (v : V.odd) (x : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).evenMap (svEvenInr (v ⊗ₜ[ℂ] x)) = svEvenInr (f.oddMap v ⊗ₜ[ℂ] x)

Right whiskering of super vector spaces, second summand.

source
theorem RS.svWhiskerRight_oddMap_inl {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (v : V.even) (x : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).oddMap (svOddInl (v ⊗ₜ[ℂ] x)) = svOddInl (f.evenMap v ⊗ₜ[ℂ] x)

Right whiskering of super vector spaces, odd degree, first summand.

source
theorem RS.svWhiskerRight_oddMap_inr {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (v : V.odd) (x : X.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).oddMap (svOddInr (v ⊗ₜ[ℂ] x)) = svOddInr (f.oddMap v ⊗ₜ[ℂ] x)

Right whiskering of super vector spaces, odd degree, second summand.

source
theorem RS.svWhiskerLeft_evenMap_inl {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (x : X.even) (v : V.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).evenMap (svEvenInl (x ⊗ₜ[ℂ] v)) = svEvenInl (x ⊗ₜ[ℂ] f.evenMap v)

Left whiskering of super vector spaces, first summand.

source
theorem RS.svWhiskerLeft_evenMap_inr {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (x : X.odd) (v : V.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).evenMap (svEvenInr (x ⊗ₜ[ℂ] v)) = svEvenInr (x ⊗ₜ[ℂ] f.oddMap v)

Left whiskering of super vector spaces, second summand.

source
theorem RS.svWhiskerLeft_oddMap_inl {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (x : X.even) (v : V.odd) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).oddMap (svOddInl (x ⊗ₜ[ℂ] v)) = svOddInl (x ⊗ₜ[ℂ] f.oddMap v)

Left whiskering of super vector spaces, odd degree, first summand.

source
theorem RS.svWhiskerLeft_oddMap_inr {V W : SuperVect} (f : V ⟶ W) (X : SuperVect) (x : X.odd) (v : V.even) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).oddMap (svOddInr (x ⊗ₜ[ℂ] v)) = svOddInr (x ⊗ₜ[ℂ] f.evenMap v)

Left whiskering of super vector spaces, odd degree, second summand.

source
theorem RS.svComp_evenMap_apply {V W Y : SuperVect} (f : V ⟶ W) (g : W ⟶ Y) (x : V.even) :
(CategoryTheory.CategoryStruct.comp f g).evenMap x = g.evenMap (f.evenMap x)

Composition of super vector space morphisms, even degree, on an element.

source
theorem RS.svComp_oddMap_apply {V W Y : SuperVect} (f : V ⟶ W) (g : W ⟶ Y) (x : V.odd) :
(CategoryTheory.CategoryStruct.comp f g).oddMap x = g.oddMap (f.oddMap x)

Composition of super vector space morphisms, odd degree, on an element.

source
theorem RS.svBraiding_evenMap_inl (V W : SuperVect) (x : V.even) (y : W.even) :
(β_ V W).hom.evenMap (svEvenInl (x ⊗ₜ[ℂ] y)) = svEvenInl (y ⊗ₜ[ℂ] x)

The Koszul braiding on an even-even generator.

source
theorem RS.svBraiding_evenMap_inr (V W : SuperVect) (x : V.odd) (y : W.odd) :
(β_ V W).hom.evenMap (svEvenInr (x ⊗ₜ[ℂ] y)) = -svEvenInr (y ⊗ₜ[ℂ] x)

The Koszul braiding on an odd-odd generator: this is where the sign lives.

source
theorem RS.svBraiding_oddMap_inl (V W : SuperVect) (x : V.even) (y : W.odd) :
(β_ V W).hom.oddMap (svOddInl (x ⊗ₜ[ℂ] y)) = svOddInr (y ⊗ₜ[ℂ] x)

The Koszul braiding on an even-odd generator.

source
theorem RS.svBraiding_oddMap_inr (V W : SuperVect) (x : V.odd) (y : W.even) :
(β_ V W).hom.oddMap (svOddInr (x ⊗ₜ[ℂ] y)) = svOddInl (y ⊗ₜ[ℂ] x)

The Koszul braiding on an odd-even generator.

source
theorem RS.svAssoc_evenMap_ee (V W X : SuperVect) (a : V.even) (b : W.even) (c : X.even) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.evenMap (svEvenInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svEvenInl (a ⊗ₜ[ℂ] svEvenInl (b ⊗ₜ[ℂ] c))

The associator of super vector spaces on an even-even-even generator.

source
theorem RS.svAssoc_evenMap_oo (V W X : SuperVect) (a : V.odd) (b : W.odd) (c : X.even) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.evenMap (svEvenInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svEvenInr (a ⊗ₜ[ℂ] svOddInr (b ⊗ₜ[ℂ] c))

The associator on an odd-odd-even generator.

source
theorem RS.svAssoc_evenMap_eo (V W X : SuperVect) (a : V.even) (b : W.odd) (c : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.evenMap (svEvenInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svEvenInl (a ⊗ₜ[ℂ] svEvenInr (b ⊗ₜ[ℂ] c))

The associator on an even-odd-odd generator.

source
theorem RS.svAssoc_evenMap_oe (V W X : SuperVect) (a : V.odd) (b : W.even) (c : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.evenMap (svEvenInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svEvenInr (a ⊗ₜ[ℂ] svOddInl (b ⊗ₜ[ℂ] c))

The associator on an odd-even-odd generator.

source
theorem RS.svAssoc_oddMap_ee (V W X : SuperVect) (a : V.even) (b : W.even) (c : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.oddMap (svOddInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svOddInl (a ⊗ₜ[ℂ] svOddInl (b ⊗ₜ[ℂ] c))

The associator on an even-even-odd generator.

source
theorem RS.svAssoc_oddMap_oo (V W X : SuperVect) (a : V.odd) (b : W.odd) (c : X.odd) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.oddMap (svOddInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svOddInr (a ⊗ₜ[ℂ] svEvenInr (b ⊗ₜ[ℂ] c))

The associator on an odd-odd-odd generator.

source
theorem RS.svAssoc_oddMap_eo (V W X : SuperVect) (a : V.even) (b : W.odd) (c : X.even) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.oddMap (svOddInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svOddInl (a ⊗ₜ[ℂ] svOddInr (b ⊗ₜ[ℂ] c))

The associator on an even-odd-even generator.

source
theorem RS.svAssoc_oddMap_oe (V W X : SuperVect) (a : V.odd) (b : W.even) (c : X.even) :
(CategoryTheory.MonoidalCategoryStruct.associator V W X).hom.oddMap (svOddInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = svOddInr (a ⊗ₜ[ℂ] svEvenInl (b ⊗ₜ[ℂ] c))

The associator on an odd-even-even generator.

source
theorem RS.svLeftUnitor_evenMap_inl (V : SuperVect) (r : ℂ) (x : V.even) :
(CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom.evenMap (svEvenInl (r ⊗ₜ[ℂ] x)) = r • x

The left unitor of super vector spaces on the first summand.

source
theorem RS.svLeftUnitor_oddMap_inl (V : SuperVect) (r : ℂ) (y : V.odd) :
(CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom.oddMap (svOddInl (r ⊗ₜ[ℂ] y)) = r • y

The left unitor in odd degree, on the first summand.

source
theorem RS.svRightUnitor_evenMap_inl (V : SuperVect) (x : V.even) (r : ℂ) :
(CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom.evenMap (svEvenInl (x ⊗ₜ[ℂ] r)) = r • x

The right unitor of super vector spaces on the first summand.

source
theorem RS.svRightUnitor_oddMap_inr (V : SuperVect) (y : V.odd) (r : ℂ) :
(CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom.oddMap (svOddInr (y ⊗ₜ[ℂ] r)) = r • y

The right unitor in odd degree, on the second summand.

source
theorem RS.superVectHom_evenMap_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] (u : M ⟶ N) (y : (toSuperVect P M).even) :
(superVectHom P u).evenMap y = (toSuperVectEvenEquiv P N) ((CategoryTheory.MonoidalCategoryStruct.whiskerRight u (SuperCommAlgebra.pointMod P)).evenMap ((toSuperVectEvenEquiv P M).symm y))

Base change of a morphism, in even degree, on an element.

source
theorem RS.superVectHom_oddMap_apply {S : SuperCommAlgebra} (P : SuperPoint S) {M N : S.Mod} [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (M.tensor (SuperCommAlgebra.pointMod P)).odd] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).even] [FiniteDimensional ℂ (N.tensor (SuperCommAlgebra.pointMod P)).odd] (u : M ⟶ N) (y : (toSuperVect P M).odd) :
(superVectHom P u).oddMap y = (toSuperVectOddEquiv P N) ((CategoryTheory.MonoidalCategoryStruct.whiskerRight u (SuperCommAlgebra.pointMod P)).oddMap ((toSuperVectOddEquiv P M).symm y))

Base change of a morphism, in odd degree, on an element.

Extensionality for a threefold graded tensor product #

source
theorem RS.gradedTriple_ext {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {C₁ : Type u_5} {C₂ : Type u_6} [AddCommGroup A₁] [Module ℂ A₁] [AddCommGroup A₂] [Module ℂ A₂] [AddCommGroup B₁] [Module ℂ B₁] [AddCommGroup B₂] [Module ℂ B₂] [AddCommGroup C₁] [Module ℂ C₁] [AddCommGroup C₂] [Module ℂ C₂] {Z : Type u_7} [AddCommGroup Z] [Module ℂ Z] {f g : TensorProduct ℂ (TensorProduct ℂ A₁ B₁ × TensorProduct ℂ A₂ B₂) C₁ × TensorProduct ℂ (TensorProduct ℂ A₁ B₂ × TensorProduct ℂ A₂ B₁) C₂ →ₗ[ℂ] Z} (h₁ : ∀ (a : A₁) (b : B₁) (c : C₁), f ((a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c, 0) = g ((a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c, 0)) (h₂ : ∀ (a : A₂) (b : B₂) (c : C₁), f ((0, a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c, 0) = g ((0, a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c, 0)) (h₃ : ∀ (a : A₁) (b : B₂) (c : C₂), f (0, (a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c) = g (0, (a ⊗ₜ[ℂ] b, 0) ⊗ₜ[ℂ] c)) (h₄ : ∀ (a : A₂) (b : B₁) (c : C₂), f (0, (0, a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c) = g (0, (0, a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) :
f = g

Two linear maps out of a threefold graded tensor product agree as soon as they agree on the four families of generators. Both components of a threefold product of super vector spaces are of this shape, the two C-slots taken in the two orders.

source
theorem RS.superVectTripleEven_ext {V W X : SuperVect} {Z : Type u_1} [AddCommGroup Z] [Module ℂ Z] {f g : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) X).even →ₗ[ℂ] Z} (h₁ : ∀ (a : V.even) (b : W.even) (c : X.even), f (svEvenInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svEvenInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₂ : ∀ (a : V.odd) (b : W.odd) (c : X.even), f (svEvenInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svEvenInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₃ : ∀ (a : V.even) (b : W.odd) (c : X.odd), f (svEvenInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svEvenInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₄ : ∀ (a : V.odd) (b : W.even) (c : X.odd), f (svEvenInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svEvenInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) :
f = g

Extensionality for the even part of a threefold product of super vector spaces.

source
theorem RS.superVectTripleOdd_ext {V W X : SuperVect} {Z : Type u_1} [AddCommGroup Z] [Module ℂ Z] {f g : (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) X).odd →ₗ[ℂ] Z} (h₁ : ∀ (a : V.even) (b : W.even) (c : X.odd), f (svOddInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svOddInl (svEvenInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₂ : ∀ (a : V.odd) (b : W.odd) (c : X.odd), f (svOddInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svOddInl (svEvenInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₃ : ∀ (a : V.even) (b : W.odd) (c : X.even), f (svOddInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svOddInr (svOddInl (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) (h₄ : ∀ (a : V.odd) (b : W.even) (c : X.even), f (svOddInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c)) = g (svOddInr (svOddInr (a ⊗ₜ[ℂ] b) ⊗ₜ[ℂ] c))) :
f = g

Extensionality for the odd part of a threefold product of super vector spaces.

source
theorem RS.superVectPairEven_ext {V W : SuperVect} {Z : Type u_1} [AddCommGroup Z] [Module ℂ Z] {f g : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).even →ₗ[ℂ] Z} (h₁ : ∀ (a : V.even) (b : W.even), f (svEvenInl (a ⊗ₜ[ℂ] b)) = g (svEvenInl (a ⊗ₜ[ℂ] b))) (h₂ : ∀ (a : V.odd) (b : W.odd), f (svEvenInr (a ⊗ₜ[ℂ] b)) = g (svEvenInr (a ⊗ₜ[ℂ] b))) :
f = g

Extensionality for the even part of a product of super vector spaces.

source
theorem RS.superVectPairOdd_ext {V W : SuperVect} {Z : Type u_1} [AddCommGroup Z] [Module ℂ Z] {f g : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).odd →ₗ[ℂ] Z} (h₁ : ∀ (a : V.even) (b : W.odd), f (svOddInl (a ⊗ₜ[ℂ] b)) = g (svOddInl (a ⊗ₜ[ℂ] b))) (h₂ : ∀ (a : V.odd) (b : W.even), f (svOddInr (a ⊗ₜ[ℂ] b)) = g (svOddInr (a ⊗ₜ[ℂ] b))) :
f = g

Extensionality for the odd part of a product of super vector spaces.