The symmetric monoidal structure on super modules

For a super-commutative ℂ-algebra S the category S.Mod of modules over it carries a symmetric monoidal structure, built throughout from the universal property of RS.SuperCommAlgebra.Mod.tensor established in RS.Classical.Deligne.SuperModTensor.

Every map out of a tensor product is produced by liftEven and liftOdd, and every identity between two such maps is proved by liftEven_unique and liftOdd_unique, packaged here as the extensionality principles hom_ext, hom_ext₃ and hom_ext₄ for morphisms out of a two-, three- and four-fold tensor product.

Contents

• RS.bicomp: the composite (a, a') ↦ f a ∘ₗ g a' of two bilinear maps, used to feed a lift into a lift.
• RS.SuperCommAlgebra.Mod.mkHom: a morphism out of a tensor product from four bilinear maps, eight balancing laws and eight action laws.
• RS.SuperCommAlgebra.Mod.hom_ext, hom_ext₃, hom_ext₄: extensionality for morphisms out of iterated tensor products.
• RS.SuperCommAlgebra.Mod.tensorHom, with tensorHom_id and tensorHom_comp.
• RS.SuperCommAlgebra.Mod.unitMod: the algebra as a module over itself, the tensor unit.
• RS.SuperCommAlgebra.Mod.leftUnitor, rightUnitor, associator, braiding, with their naturality.
• The pentagon and triangle identities, and the resulting MonoidalCategory and SymmetricCategory instances.

Composing bilinear maps

noncomputable def RS.bicomp {A : Type u_1} {A' : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup A'] [Module ℂ A'] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (f : A →ₗ[ℂ] B →ₗ[ℂ] C) (g : A' →ₗ[ℂ] D →ₗ[ℂ] B) : A →ₗ[ℂ] A' →ₗ[ℂ] D →ₗ[ℂ] C

The composite of two bilinear maps, (a, a') ↦ f a ∘ₗ g a', again bilinear. This is the shape in which a lift out of a tensor product is fed into a second lift: the value of the outer lift is itself a linear map.

Equations

• RS.bicomp f g = (LinearMap.llcomp ℂ D B C).compl₁₂ f g

@[simp]

theorem RS.bicomp_apply {A : Type u_1} {A' : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup A'] [Module ℂ A'] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (f : A →ₗ[ℂ] B →ₗ[ℂ] C) (g : A' →ₗ[ℂ] D →ₗ[ℂ] B) (a : A) (a' : A') (d : D) : (((bicomp f g) a) a') d = (f a) ((g a') d)

noncomputable def RS.bicompFlip {A : Type u_1} {A' : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup A'] [Module ℂ A'] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (f : B →ₗ[ℂ] C →ₗ[ℂ] A') (g : A →ₗ[ℂ] D →ₗ[ℂ] B) : D →ₗ[ℂ] C →ₗ[ℂ] A →ₗ[ℂ] A'

The composite of two bilinear maps in which the first argument is the one held back: (a', d) ↦ (a ↦ f (g a a') d). This is the shape needed when the inner lift is taken in the second factor of a tensor product.

Equations

• RS.bicompFlip f g = (RS.bicomp f.flip g.flip).flip

@[simp]

theorem RS.bicompFlip_apply {A : Type u_1} {A' : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup A'] [Module ℂ A'] [AddCommGroup B] [Module ℂ B] [AddCommGroup C] [Module ℂ C] [AddCommGroup D] [Module ℂ D] (f : B →ₗ[ℂ] C →ₗ[ℂ] A') (g : A →ₗ[ℂ] D →ₗ[ℂ] B) (d : D) (c : C) (a : A) : (((bicompFlip f g) d) c) a = (f ((g a) d)) c

Extensionality for maps out of a tensor product

theorem RS.SuperCommAlgebra.Mod.hom_ext {S : SuperCommAlgebra} {M N P : S.Mod} {f g : M.tensor N ⟶ P} (hEE : ∀ (m : M.even) (n : N.even), f.evenMap (((M.tmulEE N) m) n) = g.evenMap (((M.tmulEE N) m) n)) (hOO : ∀ (m : M.odd) (n : N.odd), f.evenMap (((M.tmulOO N) m) n) = g.evenMap (((M.tmulOO N) m) n)) (hEO : ∀ (m : M.even) (n : N.odd), f.oddMap (((M.tmulEO N) m) n) = g.oddMap (((M.tmulEO N) m) n)) (hOE : ∀ (m : M.odd) (n : N.even), f.oddMap (((M.tmulOE N) m) n) = g.oddMap (((M.tmulOE N) m) n)) : f = g

Extensionality for a morphism out of a tensor product: two morphisms agreeing on all four families of products agree.

theorem RS.SuperCommAlgebra.Mod.liftEven₃_unique {S : SuperCommAlgebra} {M N P : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : ((M.tensor N).tensor P).even →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even), g ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p) = g' ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even), g ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p) = g' ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd), g ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p) = g' ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd), g ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p) = g' ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) : g = g'

Uniqueness in even degree for a threefold tensor product: the even part of (M ⊗ N) ⊗ P is generated by the four families of triple products of even total degree.

theorem RS.SuperCommAlgebra.Mod.liftOdd₃_unique {S : SuperCommAlgebra} {M N P : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : ((M.tensor N).tensor P).odd →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.odd), g ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p) = g' ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.odd), g ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p) = g' ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.even), g ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p) = g' ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.even), g ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p) = g' ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) : g = g'

Uniqueness in odd degree for a threefold tensor product.

theorem RS.SuperCommAlgebra.Mod.hom_ext₃ {S : SuperCommAlgebra} {M N P Q : S.Mod} {f g : (M.tensor N).tensor P ⟶ Q} (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even), f.evenMap ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p) = g.evenMap ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even), f.evenMap ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p) = g.evenMap ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd), f.evenMap ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p) = g.evenMap ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd), f.evenMap ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p) = g.evenMap ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) (h₅ : ∀ (m : M.even) (n : N.even) (p : P.odd), f.oddMap ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p) = g.oddMap ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) (h₆ : ∀ (m : M.odd) (n : N.odd) (p : P.odd), f.oddMap ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p) = g.oddMap ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) (h₇ : ∀ (m : M.even) (n : N.odd) (p : P.even), f.oddMap ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p) = g.oddMap ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) (h₈ : ∀ (m : M.odd) (n : N.even) (p : P.even), f.oddMap ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p) = g.oddMap ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) : f = g

Extensionality for a morphism out of a threefold tensor product: two morphisms out of (M ⊗ N) ⊗ P agreeing on all eight families of triple products agree.

theorem RS.SuperCommAlgebra.Mod.liftEven₃'_unique {S : SuperCommAlgebra} {M N P : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : (M.tensor (N.tensor P)).even →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even), g (((M.tmulEE (N.tensor P)) m) (((N.tmulEE P) n) p)) = g' (((M.tmulEE (N.tensor P)) m) (((N.tmulEE P) n) p))) (h₂ : ∀ (m : M.even) (n : N.odd) (p : P.odd), g (((M.tmulEE (N.tensor P)) m) (((N.tmulOO P) n) p)) = g' (((M.tmulEE (N.tensor P)) m) (((N.tmulOO P) n) p))) (h₃ : ∀ (m : M.odd) (n : N.even) (p : P.odd), g (((M.tmulOO (N.tensor P)) m) (((N.tmulEO P) n) p)) = g' (((M.tmulOO (N.tensor P)) m) (((N.tmulEO P) n) p))) (h₄ : ∀ (m : M.odd) (n : N.odd) (p : P.even), g (((M.tmulOO (N.tensor P)) m) (((N.tmulOE P) n) p)) = g' (((M.tmulOO (N.tensor P)) m) (((N.tmulOE P) n) p))) : g = g'

Uniqueness in even degree for a right-nested threefold tensor product.

theorem RS.SuperCommAlgebra.Mod.liftOdd₃'_unique {S : SuperCommAlgebra} {M N P : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : (M.tensor (N.tensor P)).odd →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.odd), g (((M.tmulEO (N.tensor P)) m) (((N.tmulEO P) n) p)) = g' (((M.tmulEO (N.tensor P)) m) (((N.tmulEO P) n) p))) (h₂ : ∀ (m : M.even) (n : N.odd) (p : P.even), g (((M.tmulEO (N.tensor P)) m) (((N.tmulOE P) n) p)) = g' (((M.tmulEO (N.tensor P)) m) (((N.tmulOE P) n) p))) (h₃ : ∀ (m : M.odd) (n : N.even) (p : P.even), g (((M.tmulOE (N.tensor P)) m) (((N.tmulEE P) n) p)) = g' (((M.tmulOE (N.tensor P)) m) (((N.tmulEE P) n) p))) (h₄ : ∀ (m : M.odd) (n : N.odd) (p : P.odd), g (((M.tmulOE (N.tensor P)) m) (((N.tmulOO P) n) p)) = g' (((M.tmulOE (N.tensor P)) m) (((N.tmulOO P) n) p))) : g = g'

Uniqueness in odd degree for a right-nested threefold tensor product.

theorem RS.SuperCommAlgebra.Mod.hom_ext₃' {S : SuperCommAlgebra} {M N P Q : S.Mod} {f g : M.tensor (N.tensor P) ⟶ Q} (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even), f.evenMap (((M.tmulEE (N.tensor P)) m) (((N.tmulEE P) n) p)) = g.evenMap (((M.tmulEE (N.tensor P)) m) (((N.tmulEE P) n) p))) (h₂ : ∀ (m : M.even) (n : N.odd) (p : P.odd), f.evenMap (((M.tmulEE (N.tensor P)) m) (((N.tmulOO P) n) p)) = g.evenMap (((M.tmulEE (N.tensor P)) m) (((N.tmulOO P) n) p))) (h₃ : ∀ (m : M.odd) (n : N.even) (p : P.odd), f.evenMap (((M.tmulOO (N.tensor P)) m) (((N.tmulEO P) n) p)) = g.evenMap (((M.tmulOO (N.tensor P)) m) (((N.tmulEO P) n) p))) (h₄ : ∀ (m : M.odd) (n : N.odd) (p : P.even), f.evenMap (((M.tmulOO (N.tensor P)) m) (((N.tmulOE P) n) p)) = g.evenMap (((M.tmulOO (N.tensor P)) m) (((N.tmulOE P) n) p))) (h₅ : ∀ (m : M.even) (n : N.even) (p : P.odd), f.oddMap (((M.tmulEO (N.tensor P)) m) (((N.tmulEO P) n) p)) = g.oddMap (((M.tmulEO (N.tensor P)) m) (((N.tmulEO P) n) p))) (h₆ : ∀ (m : M.even) (n : N.odd) (p : P.even), f.oddMap (((M.tmulEO (N.tensor P)) m) (((N.tmulOE P) n) p)) = g.oddMap (((M.tmulEO (N.tensor P)) m) (((N.tmulOE P) n) p))) (h₇ : ∀ (m : M.odd) (n : N.even) (p : P.even), f.oddMap (((M.tmulOE (N.tensor P)) m) (((N.tmulEE P) n) p)) = g.oddMap (((M.tmulOE (N.tensor P)) m) (((N.tmulEE P) n) p))) (h₈ : ∀ (m : M.odd) (n : N.odd) (p : P.odd), f.oddMap (((M.tmulOE (N.tensor P)) m) (((N.tmulOO P) n) p)) = g.oddMap (((M.tmulOE (N.tensor P)) m) (((N.tmulOO P) n) p))) : f = g

Extensionality for a morphism out of a right-nested threefold tensor product.

theorem RS.SuperCommAlgebra.Mod.liftEven₄_unique {S : SuperCommAlgebra} {M N P Q : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : (((M.tensor N).tensor P).tensor Q).even →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even) (q : Q.even), g (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even) (q : Q.even), g (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd) (q : Q.even), g (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd) (q : Q.even), g (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q)) (h₅ : ∀ (m : M.even) (n : N.even) (p : P.odd) (q : Q.odd), g (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q)) (h₆ : ∀ (m : M.odd) (n : N.odd) (p : P.odd) (q : Q.odd), g (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q)) (h₇ : ∀ (m : M.even) (n : N.odd) (p : P.even) (q : Q.odd), g (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q)) (h₈ : ∀ (m : M.odd) (n : N.even) (p : P.even) (q : Q.odd), g (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q)) : g = g'

Uniqueness in even degree for a fourfold tensor product, left-nested.

theorem RS.SuperCommAlgebra.Mod.liftOdd₄_unique {S : SuperCommAlgebra} {M N P Q : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (g g' : (((M.tensor N).tensor P).tensor Q).odd →ₗ[ℂ] T) (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even) (q : Q.odd), g (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even) (q : Q.odd), g (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd) (q : Q.odd), g (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd) (q : Q.odd), g (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q)) (h₅ : ∀ (m : M.even) (n : N.even) (p : P.odd) (q : Q.even), g (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q)) (h₆ : ∀ (m : M.odd) (n : N.odd) (p : P.odd) (q : Q.even), g (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q)) (h₇ : ∀ (m : M.even) (n : N.odd) (p : P.even) (q : Q.even), g (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q)) (h₈ : ∀ (m : M.odd) (n : N.even) (p : P.even) (q : Q.even), g (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q) = g' (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q)) : g = g'

Uniqueness in odd degree for a fourfold tensor product, left-nested.

theorem RS.SuperCommAlgebra.Mod.hom_ext₄ {S : SuperCommAlgebra} {M N P Q R : S.Mod} {f g : ((M.tensor N).tensor P).tensor Q ⟶ R} (h₁ : ∀ (m : M.even) (n : N.even) (p : P.even) (q : Q.even), f.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q)) (h₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even) (q : Q.even), f.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q)) (h₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd) (q : Q.even), f.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q)) (h₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd) (q : Q.even), f.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulEE Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q)) (h₅ : ∀ (m : M.even) (n : N.even) (p : P.odd) (q : Q.odd), f.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q)) (h₆ : ∀ (m : M.odd) (n : N.odd) (p : P.odd) (q : Q.odd), f.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q)) (h₇ : ∀ (m : M.even) (n : N.odd) (p : P.even) (q : Q.odd), f.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q)) (h₈ : ∀ (m : M.odd) (n : N.even) (p : P.even) (q : Q.odd), f.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q) = g.evenMap (((((M.tensor N).tensor P).tmulOO Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q)) (k₁ : ∀ (m : M.even) (n : N.even) (p : P.even) (q : Q.odd), f.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p)) q)) (k₂ : ∀ (m : M.odd) (n : N.odd) (p : P.even) (q : Q.odd), f.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p)) q)) (k₃ : ∀ (m : M.even) (n : N.odd) (p : P.odd) (q : Q.odd), f.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p)) q)) (k₄ : ∀ (m : M.odd) (n : N.even) (p : P.odd) (q : Q.odd), f.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulEO Q) ((((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p)) q)) (k₅ : ∀ (m : M.even) (n : N.even) (p : P.odd) (q : Q.even), f.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p)) q)) (k₆ : ∀ (m : M.odd) (n : N.odd) (p : P.odd) (q : Q.even), f.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p)) q)) (k₇ : ∀ (m : M.even) (n : N.odd) (p : P.even) (q : Q.even), f.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p)) q)) (k₈ : ∀ (m : M.odd) (n : N.even) (p : P.even) (q : Q.even), f.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q) = g.oddMap (((((M.tensor N).tensor P).tmulOE Q) ((((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p)) q)) : f = g

Extensionality for a morphism out of a fourfold tensor product: two morphisms out of ((M ⊗ N) ⊗ P) ⊗ Q agreeing on all sixteen families of quadruple products agree.

Building a morphism out of a tensor product

structure RS.SuperCommAlgebra.Mod.TensorData {S : SuperCommAlgebra} (M N Q : S.Mod) : Type u

The data of a morphism out of a tensor product: four degreewise bilinear maps, balanced against the eight relator families and compatible with the four action blocks.

The eight balancing laws are exactly the hypotheses of liftEven and liftOdd. The eight action laws say that each bilinear map intertwines the action on the left factor of the source with the action on the target, one for each pair of a scalar parity and a block.

• fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] Q.even

  The even-even block.

• foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] Q.even

  The odd-odd block.

• feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] Q.odd

  The even-odd block.

• foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] Q.odd

  The odd-even block.

• hee (b : S.even) (m : M.even) (n : N.even) : (self.fee ((M.actEE b) m)) n = (self.fee m) ((N.actEE b) n)

  Balancing at parity pattern even-even-even.

• hoo (b : S.even) (m : M.odd) (n : N.odd) : (self.foo ((M.actEO b) m)) n = (self.foo m) ((N.actEO b) n)

  Balancing at parity pattern even-odd-odd.

• hoeo (c : S.odd) (m : M.even) (n : N.odd) : (self.foo ((M.actOE c) m)) n = (self.fee m) ((N.actOO c) n)

  Balancing at parity pattern odd-even-odd.

• hooe (c : S.odd) (m : M.odd) (n : N.even) : (self.fee ((M.actOO c) m)) n = -(self.foo m) ((N.actOE c) n)

  Balancing at parity pattern odd-odd-even.

• heeo (b : S.even) (m : M.even) (n : N.odd) : (self.feo ((M.actEE b) m)) n = (self.feo m) ((N.actEO b) n)

  Balancing at parity pattern even-even-odd.

• heoe (b : S.even) (m : M.odd) (n : N.even) : (self.foe ((M.actEO b) m)) n = (self.foe m) ((N.actEE b) n)

  Balancing at parity pattern even-odd-even.

• hoee (c : S.odd) (m : M.even) (n : N.even) : (self.foe ((M.actOE c) m)) n = (self.feo m) ((N.actOE c) n)

  Balancing at parity pattern odd-even-even.

• hooo (c : S.odd) (m : M.odd) (n : N.odd) : (self.feo ((M.actOO c) m)) n = -(self.foe m) ((N.actOO c) n)

  Balancing at parity pattern odd-odd-odd.

• aee (a : S.even) (m : M.even) (n : N.even) : (self.fee ((M.actEE a) m)) n = (Q.actEE a) ((self.fee m) n)

  An even scalar passes through the even-even block.

• aoo (a : S.even) (m : M.odd) (n : N.odd) : (self.foo ((M.actEO a) m)) n = (Q.actEE a) ((self.foo m) n)

  An even scalar passes through the odd-odd block.

• aeo (a : S.even) (m : M.even) (n : N.odd) : (self.feo ((M.actEE a) m)) n = (Q.actEO a) ((self.feo m) n)

  An even scalar passes through the even-odd block.

• aoe (a : S.even) (m : M.odd) (n : N.even) : (self.foe ((M.actEO a) m)) n = (Q.actEO a) ((self.foe m) n)

  An even scalar passes through the odd-even block.

• cee (c : S.odd) (m : M.even) (n : N.even) : (self.foe ((M.actOE c) m)) n = (Q.actOE c) ((self.fee m) n)

  An odd scalar passes through the even-even block.

• coo (c : S.odd) (m : M.odd) (n : N.odd) : (self.feo ((M.actOO c) m)) n = (Q.actOE c) ((self.foo m) n)

  An odd scalar passes through the odd-odd block.

• ceo (c : S.odd) (m : M.even) (n : N.odd) : (self.foo ((M.actOE c) m)) n = (Q.actOO c) ((self.feo m) n)

  An odd scalar passes through the even-odd block.

• coe (c : S.odd) (m : M.odd) (n : N.even) : (self.fee ((M.actOO c) m)) n = (Q.actOO c) ((self.foe m) n)

  An odd scalar passes through the odd-even block.

noncomputable def RS.SuperCommAlgebra.Mod.mkHom {S : SuperCommAlgebra} {M N Q : S.Mod} (d : M.TensorData N Q) : M.tensor N ⟶ Q

A morphism out of a tensor product: the two lifts of the four blocks of a TensorData, assembled into a morphism of super modules out of M ⊗ N.

Equations

• RS.SuperCommAlgebra.Mod.mkHom d = { evenMap := M.liftEven N d.fee d.foo ⋯ ⋯ ⋯ ⋯, oddMap := M.liftOdd N d.feo d.foe ⋯ ⋯ ⋯ ⋯, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

@[simp]

theorem RS.SuperCommAlgebra.Mod.mkHom_evenMap_tmulEE {S : SuperCommAlgebra} {M N Q : S.Mod} (d : M.TensorData N Q) (m : M.even) (n : N.even) : (mkHom d).evenMap (((M.tmulEE N) m) n) = (d.fee m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.mkHom_evenMap_tmulOO {S : SuperCommAlgebra} {M N Q : S.Mod} (d : M.TensorData N Q) (m : M.odd) (n : N.odd) : (mkHom d).evenMap (((M.tmulOO N) m) n) = (d.foo m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.mkHom_oddMap_tmulEO {S : SuperCommAlgebra} {M N Q : S.Mod} (d : M.TensorData N Q) (m : M.even) (n : N.odd) : (mkHom d).oddMap (((M.tmulEO N) m) n) = (d.feo m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.mkHom_oddMap_tmulOE {S : SuperCommAlgebra} {M N Q : S.Mod} (d : M.TensorData N Q) (m : M.odd) (n : N.even) : (mkHom d).oddMap (((M.tmulOE N) m) n) = (d.foe m) n

Functoriality of the tensor product

noncomputable def RS.SuperCommAlgebra.Mod.tensorHomData {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') : M.TensorData N (M'.tensor N')

The data of the tensor product of two morphisms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.tensorHom {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') : M.tensor N ⟶ M'.tensor N'

The tensor product of two morphisms: apply each morphism in its own factor, degreewise.

Equations

• RS.SuperCommAlgebra.Mod.tensorHom f g = RS.SuperCommAlgebra.Mod.mkHom (RS.SuperCommAlgebra.Mod.tensorHomData f g)

@[simp]

theorem RS.SuperCommAlgebra.Mod.tensorHom_evenMap_tmulEE {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') (m : M.even) (n : N.even) : (tensorHom f g).evenMap (((M.tmulEE N) m) n) = ((M'.tmulEE N') (f.evenMap m)) (g.evenMap n)

@[simp]

theorem RS.SuperCommAlgebra.Mod.tensorHom_evenMap_tmulOO {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') (m : M.odd) (n : N.odd) : (tensorHom f g).evenMap (((M.tmulOO N) m) n) = ((M'.tmulOO N') (f.oddMap m)) (g.oddMap n)

@[simp]

theorem RS.SuperCommAlgebra.Mod.tensorHom_oddMap_tmulEO {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') (m : M.even) (n : N.odd) : (tensorHom f g).oddMap (((M.tmulEO N) m) n) = ((M'.tmulEO N') (f.evenMap m)) (g.oddMap n)

@[simp]

theorem RS.SuperCommAlgebra.Mod.tensorHom_oddMap_tmulOE {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') (m : M.odd) (n : N.even) : (tensorHom f g).oddMap (((M.tmulOE N) m) n) = ((M'.tmulOE N') (f.oddMap m)) (g.evenMap n)

theorem RS.SuperCommAlgebra.Mod.tensorHom_id {S : SuperCommAlgebra} (M N : S.Mod) : tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (M.tensor N)

The tensor product preserves identities.

theorem RS.SuperCommAlgebra.Mod.tensorHom_comp {S : SuperCommAlgebra} {M M' M'' N N' N'' : S.Mod} (f : M ⟶ M') (f' : M' ⟶ M'') (g : N ⟶ N') (g' : N' ⟶ N'') : tensorHom (CategoryTheory.CategoryStruct.comp f f') (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (tensorHom f g) (tensorHom f' g')

The tensor product preserves composition.

The tensor unit

@[reducible]

def RS.SuperCommAlgebra.unitMod (S : SuperCommAlgebra) : S.Mod

The tensor unit: the algebra regarded as a module over itself, the four action blocks being the four multiplication blocks. The ten module axioms are the algebra's own unit and associativity laws.

It is reducible so that the identification of its components with those of S is transparent to unification and to rw.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.SuperCommAlgebra.Mod.unitMod_actEE {S : SuperCommAlgebra} (x y : S.even) : (S.unitMod.actEE x) y = (S.mulEE x) y

@[simp]

theorem RS.SuperCommAlgebra.Mod.unitMod_actEO {S : SuperCommAlgebra} (x : S.even) (u : S.odd) : (S.unitMod.actEO x) u = (S.mulEO x) u

@[simp]

theorem RS.SuperCommAlgebra.Mod.unitMod_actOE {S : SuperCommAlgebra} (u : S.odd) (x : S.even) : (S.unitMod.actOE u) x = (S.mulOE u) x

@[simp]

theorem RS.SuperCommAlgebra.Mod.unitMod_actOO {S : SuperCommAlgebra} (u v : S.odd) : (S.unitMod.actOO u) v = (S.mulOO u) v

theorem RS.SuperCommAlgebra.Mod.unitMod_actEE_one {S : SuperCommAlgebra} (x : S.even) : (S.unitMod.actEE x) S.one = x

Acting by an even scalar on the unit returns the scalar.

theorem RS.SuperCommAlgebra.Mod.unitMod_actOE_one {S : SuperCommAlgebra} (u : S.odd) : (S.unitMod.actOE u) S.one = u

Acting by an odd scalar on the unit returns the scalar.

The left unitor

def RS.SuperCommAlgebra.Mod.leftUnitorData {S : SuperCommAlgebra} (M : S.Mod) : S.unitMod.TensorData M M

The data of the left unitor: the unit factor acts on the module. Every law is one of the module axioms, conjugated where needed by the commutativity of S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.leftUnitorHom {S : SuperCommAlgebra} (M : S.Mod) : S.unitMod.tensor M ⟶ M

The structure map of the left unitor.

Equations

• M.leftUnitorHom = RS.SuperCommAlgebra.Mod.mkHom M.leftUnitorData

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorHom_evenMap_tmulEE {S : SuperCommAlgebra} (M : S.Mod) (x : S.even) (m : M.even) : M.leftUnitorHom.evenMap (((S.unitMod.tmulEE M) x) m) = (M.actEE x) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorHom_evenMap_tmulOO {S : SuperCommAlgebra} (M : S.Mod) (u : S.odd) (m : M.odd) : M.leftUnitorHom.evenMap (((S.unitMod.tmulOO M) u) m) = (M.actOO u) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorHom_oddMap_tmulEO {S : SuperCommAlgebra} (M : S.Mod) (x : S.even) (m : M.odd) : M.leftUnitorHom.oddMap (((S.unitMod.tmulEO M) x) m) = (M.actEO x) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorHom_oddMap_tmulOE {S : SuperCommAlgebra} (M : S.Mod) (u : S.odd) (m : M.even) : M.leftUnitorHom.oddMap (((S.unitMod.tmulOE M) u) m) = (M.actOE u) m

noncomputable def RS.SuperCommAlgebra.Mod.leftUnitorInv {S : SuperCommAlgebra} (M : S.Mod) : M ⟶ S.unitMod.tensor M

The inverse of the left unitor: tensor with the algebra unit.

Equations

• M.leftUnitorInv = { evenMap := (S.unitMod.tmulEE M) S.one, oddMap := (S.unitMod.tmulEO M) S.one, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorInv_evenMap {S : SuperCommAlgebra} (M : S.Mod) (m : M.even) : M.leftUnitorInv.evenMap m = ((S.unitMod.tmulEE M) S.one) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.leftUnitorInv_oddMap {S : SuperCommAlgebra} (M : S.Mod) (m : M.odd) : M.leftUnitorInv.oddMap m = ((S.unitMod.tmulEO M) S.one) m

noncomputable def RS.SuperCommAlgebra.Mod.leftUnitor {S : SuperCommAlgebra} (M : S.Mod) : S.unitMod.tensor M ≅ M

The left unitor: tensoring with the unit on the left changes nothing.

Equations

• M.leftUnitor = { hom := M.leftUnitorHom, inv := M.leftUnitorInv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

The right unitor

noncomputable def RS.SuperCommAlgebra.Mod.rightUnitorData {S : SuperCommAlgebra} (M : S.Mod) : M.TensorData S.unitMod M

The data of the right unitor: the unit factor acts on the module, with the Koszul sign when both factors are odd.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.rightUnitorHom {S : SuperCommAlgebra} (M : S.Mod) : M.tensor S.unitMod ⟶ M

The structure map of the right unitor.

Equations

• M.rightUnitorHom = RS.SuperCommAlgebra.Mod.mkHom M.rightUnitorData

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorHom_evenMap_tmulEE {S : SuperCommAlgebra} (M : S.Mod) (m : M.even) (x : S.even) : M.rightUnitorHom.evenMap (((M.tmulEE S.unitMod) m) x) = (M.actEE x) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorHom_evenMap_tmulOO {S : SuperCommAlgebra} (M : S.Mod) (m : M.odd) (u : S.odd) : M.rightUnitorHom.evenMap (((M.tmulOO S.unitMod) m) u) = -(M.actOO u) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorHom_oddMap_tmulEO {S : SuperCommAlgebra} (M : S.Mod) (m : M.even) (u : S.odd) : M.rightUnitorHom.oddMap (((M.tmulEO S.unitMod) m) u) = (M.actOE u) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorHom_oddMap_tmulOE {S : SuperCommAlgebra} (M : S.Mod) (m : M.odd) (x : S.even) : M.rightUnitorHom.oddMap (((M.tmulOE S.unitMod) m) x) = (M.actEO x) m

noncomputable def RS.SuperCommAlgebra.Mod.rightUnitorInv {S : SuperCommAlgebra} (M : S.Mod) : M ⟶ M.tensor S.unitMod

The inverse of the right unitor: tensor with the algebra unit on the right.

Equations

• M.rightUnitorInv = { evenMap := (M.tmulEE S.unitMod).flip S.one, oddMap := (M.tmulOE S.unitMod).flip S.one, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorInv_evenMap {S : SuperCommAlgebra} (M : S.Mod) (m : M.even) : M.rightUnitorInv.evenMap m = ((M.tmulEE S.unitMod) m) S.one

@[simp]

theorem RS.SuperCommAlgebra.Mod.rightUnitorInv_oddMap {S : SuperCommAlgebra} (M : S.Mod) (m : M.odd) : M.rightUnitorInv.oddMap m = ((M.tmulOE S.unitMod) m) S.one

noncomputable def RS.SuperCommAlgebra.Mod.rightUnitor {S : SuperCommAlgebra} (M : S.Mod) : M.tensor S.unitMod ≅ M

The right unitor: tensoring with the unit on the right changes nothing.

Equations

• M.rightUnitor = { hom := M.rightUnitorHom, inv := M.rightUnitorInv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Naturality of the unitors

theorem RS.SuperCommAlgebra.Mod.leftUnitor_naturality {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id S.unitMod) f) N.leftUnitorHom = CategoryTheory.CategoryStruct.comp M.leftUnitorHom f

The left unitor is natural.

theorem RS.SuperCommAlgebra.Mod.rightUnitor_naturality {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (tensorHom f (CategoryTheory.CategoryStruct.id S.unitMod)) N.rightUnitorHom = CategoryTheory.CategoryStruct.comp M.rightUnitorHom f

The right unitor is natural.

The braiding

noncomputable def RS.SuperCommAlgebra.Mod.braidingData {S : SuperCommAlgebra} (M N : S.Mod) : M.TensorData N (N.tensor M)

The data of the Koszul swap: interchange the two factors, with a sign when both are odd.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.braidingHom {S : SuperCommAlgebra} (M N : S.Mod) : M.tensor N ⟶ N.tensor M

The structure map of the braiding.

Equations

• M.braidingHom N = RS.SuperCommAlgebra.Mod.mkHom (M.braidingData N)

@[simp]

theorem RS.SuperCommAlgebra.Mod.braidingHom_evenMap_tmulEE {S : SuperCommAlgebra} (M N : S.Mod) (m : M.even) (n : N.even) : (M.braidingHom N).evenMap (((M.tmulEE N) m) n) = ((N.tmulEE M) n) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.braidingHom_evenMap_tmulOO {S : SuperCommAlgebra} (M N : S.Mod) (m : M.odd) (n : N.odd) : (M.braidingHom N).evenMap (((M.tmulOO N) m) n) = -((N.tmulOO M) n) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.braidingHom_oddMap_tmulEO {S : SuperCommAlgebra} (M N : S.Mod) (m : M.even) (n : N.odd) : (M.braidingHom N).oddMap (((M.tmulEO N) m) n) = ((N.tmulOE M) n) m

@[simp]

theorem RS.SuperCommAlgebra.Mod.braidingHom_oddMap_tmulOE {S : SuperCommAlgebra} (M N : S.Mod) (m : M.odd) (n : N.even) : (M.braidingHom N).oddMap (((M.tmulOE N) m) n) = ((N.tmulEO M) n) m

theorem RS.SuperCommAlgebra.Mod.braidingHom_braidingHom {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.braidingHom N) (N.braidingHom M) = CategoryTheory.CategoryStruct.id (M.tensor N)

The Koszul swap is an involution: swapping twice restores the original order, the two signs cancelling.

noncomputable def RS.SuperCommAlgebra.Mod.braiding {S : SuperCommAlgebra} (M N : S.Mod) : M.tensor N ≅ N.tensor M

The braiding: the Koszul swap of the two factors.

Equations

• M.braiding N = { hom := M.braidingHom N, inv := N.braidingHom M, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Lifting one degree at a time

structure RS.SuperCommAlgebra.Mod.LiftEvenData {S : SuperCommAlgebra} (M N : S.Mod) (T : Type u) [AddCommGroup T] [Module ℂ T] : Type u

The data of a linear map out of the even part of a tensor product: two balanced bilinear blocks.

• fee : M.even →ₗ[ℂ] N.even →ₗ[ℂ] T

  The even-even block.

• foo : M.odd →ₗ[ℂ] N.odd →ₗ[ℂ] T

  The odd-odd block.

• hee (b : S.even) (m : M.even) (n : N.even) : (self.fee ((M.actEE b) m)) n = (self.fee m) ((N.actEE b) n)

  Balancing at parity pattern even-even-even.

• hoo (b : S.even) (m : M.odd) (n : N.odd) : (self.foo ((M.actEO b) m)) n = (self.foo m) ((N.actEO b) n)

  Balancing at parity pattern even-odd-odd.

• hoeo (c : S.odd) (m : M.even) (n : N.odd) : (self.foo ((M.actOE c) m)) n = (self.fee m) ((N.actOO c) n)

  Balancing at parity pattern odd-even-odd.

• hooe (c : S.odd) (m : M.odd) (n : N.even) : (self.fee ((M.actOO c) m)) n = -(self.foo m) ((N.actOE c) n)

  Balancing at parity pattern odd-odd-even.

structure RS.SuperCommAlgebra.Mod.LiftOddData {S : SuperCommAlgebra} (M N : S.Mod) (T : Type u) [AddCommGroup T] [Module ℂ T] : Type u

The data of a linear map out of the odd part of a tensor product: two balanced bilinear blocks.

• feo : M.even →ₗ[ℂ] N.odd →ₗ[ℂ] T

  The even-odd block.

• foe : M.odd →ₗ[ℂ] N.even →ₗ[ℂ] T

  The odd-even block.

• heeo (b : S.even) (m : M.even) (n : N.odd) : (self.feo ((M.actEE b) m)) n = (self.feo m) ((N.actEO b) n)

  Balancing at parity pattern even-even-odd.

• heoe (b : S.even) (m : M.odd) (n : N.even) : (self.foe ((M.actEO b) m)) n = (self.foe m) ((N.actEE b) n)

  Balancing at parity pattern even-odd-even.

• hoee (c : S.odd) (m : M.even) (n : N.even) : (self.foe ((M.actOE c) m)) n = (self.feo m) ((N.actOE c) n)

  Balancing at parity pattern odd-even-even.

• hooo (c : S.odd) (m : M.odd) (n : N.odd) : (self.feo ((M.actOO c) m)) n = -(self.foe m) ((N.actOO c) n)

  Balancing at parity pattern odd-odd-odd.

noncomputable def RS.SuperCommAlgebra.Mod.liftE {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftEvenData N T) : (M.tensor N).even →ₗ[ℂ] T

The even-degree lift of a LiftEvenData.

Equations

• RS.SuperCommAlgebra.Mod.liftE d = M.liftEven N d.fee d.foo ⋯ ⋯ ⋯ ⋯

noncomputable def RS.SuperCommAlgebra.Mod.liftO {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftOddData N T) : (M.tensor N).odd →ₗ[ℂ] T

The odd-degree lift of a LiftOddData.

Equations

• RS.SuperCommAlgebra.Mod.liftO d = M.liftOdd N d.feo d.foe ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftE_tmulEE {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftEvenData N T) (m : M.even) (n : N.even) : (liftE d) (((M.tmulEE N) m) n) = (d.fee m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftE_tmulOO {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftEvenData N T) (m : M.odd) (n : N.odd) : (liftE d) (((M.tmulOO N) m) n) = (d.foo m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftO_tmulEO {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftOddData N T) (m : M.even) (n : N.odd) : (liftO d) (((M.tmulEO N) m) n) = (d.feo m) n

@[simp]

theorem RS.SuperCommAlgebra.Mod.liftO_tmulOE {S : SuperCommAlgebra} {M N : S.Mod} {T : Type u} [AddCommGroup T] [Module ℂ T] (d : M.LiftOddData N T) (m : M.odd) (n : N.even) : (liftO d) (((M.tmulOE N) m) n) = (d.foe m) n

The associator

noncomputable def RS.SuperCommAlgebra.Mod.assocFeeData {S : SuperCommAlgebra} (M N P : S.Mod) : M.LiftEvenData N (P.even →ₗ[ℂ] (M.tensor (N.tensor P)).even)

The even-even and odd-odd blocks of the associator in even total degree.

Equations

• M.assocFeeData N P = { fee := RS.bicomp (M.tmulEE (N.tensor P)) (N.tmulEE P), foo := RS.bicomp (M.tmulOO (N.tensor P)) (N.tmulOE P), hee := ⋯, hoo := ⋯, hoeo := ⋯, hooe := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocFooData {S : SuperCommAlgebra} (M N P : S.Mod) : M.LiftOddData N (P.odd →ₗ[ℂ] (M.tensor (N.tensor P)).even)

The even-odd and odd-even blocks of the associator in even total degree.

Equations

• M.assocFooData N P = { feo := RS.bicomp (M.tmulEE (N.tensor P)) (N.tmulOO P), foe := RS.bicomp (M.tmulOO (N.tensor P)) (N.tmulEO P), heeo := ⋯, heoe := ⋯, hoee := ⋯, hooo := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocFeoData {S : SuperCommAlgebra} (M N P : S.Mod) : M.LiftEvenData N (P.odd →ₗ[ℂ] (M.tensor (N.tensor P)).odd)

The even-even and odd-odd blocks of the associator in odd total degree.

Equations

• M.assocFeoData N P = { fee := RS.bicomp (M.tmulEO (N.tensor P)) (N.tmulEO P), foo := RS.bicomp (M.tmulOE (N.tensor P)) (N.tmulOO P), hee := ⋯, hoo := ⋯, hoeo := ⋯, hooe := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocFoeData {S : SuperCommAlgebra} (M N P : S.Mod) : M.LiftOddData N (P.even →ₗ[ℂ] (M.tensor (N.tensor P)).odd)

The even-odd and odd-even blocks of the associator in odd total degree.

Equations

• M.assocFoeData N P = { feo := RS.bicomp (M.tmulEO (N.tensor P)) (N.tmulOE P), foe := RS.bicomp (M.tmulOE (N.tensor P)) (N.tmulEE P), heeo := ⋯, heoe := ⋯, hoee := ⋯, hooo := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocFee {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).even →ₗ[ℂ] P.even →ₗ[ℂ] (M.tensor (N.tensor P)).even

The even-degree block of the associator, in the first two factors.

Equations

• M.assocFee N P = RS.SuperCommAlgebra.Mod.liftE (M.assocFeeData N P)

noncomputable def RS.SuperCommAlgebra.Mod.assocFoo {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).odd →ₗ[ℂ] P.odd →ₗ[ℂ] (M.tensor (N.tensor P)).even

The odd-degree block of the associator taking an odd third factor to an even value.

Equations

• M.assocFoo N P = RS.SuperCommAlgebra.Mod.liftO (M.assocFooData N P)

noncomputable def RS.SuperCommAlgebra.Mod.assocFeo {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).even →ₗ[ℂ] P.odd →ₗ[ℂ] (M.tensor (N.tensor P)).odd

The even-degree block of the associator taking an odd third factor to an odd value.

Equations

• M.assocFeo N P = RS.SuperCommAlgebra.Mod.liftE (M.assocFeoData N P)

noncomputable def RS.SuperCommAlgebra.Mod.assocFoe {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).odd →ₗ[ℂ] P.even →ₗ[ℂ] (M.tensor (N.tensor P)).odd

The odd-degree block of the associator taking an even third factor to an odd value.

Equations

• M.assocFoe N P = RS.SuperCommAlgebra.Mod.liftO (M.assocFoeData N P)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFee_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.even) (p : P.even) : ((M.assocFee N P) (((M.tmulEE N) m) n)) p = ((M.tmulEE (N.tensor P)) m) (((N.tmulEE P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFee_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.odd) (p : P.even) : ((M.assocFee N P) (((M.tmulOO N) m) n)) p = ((M.tmulOO (N.tensor P)) m) (((N.tmulOE P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFoo_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.odd) (p : P.odd) : ((M.assocFoo N P) (((M.tmulEO N) m) n)) p = ((M.tmulEE (N.tensor P)) m) (((N.tmulOO P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFoo_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.even) (p : P.odd) : ((M.assocFoo N P) (((M.tmulOE N) m) n)) p = ((M.tmulOO (N.tensor P)) m) (((N.tmulEO P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFeo_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.even) (p : P.odd) : ((M.assocFeo N P) (((M.tmulEE N) m) n)) p = ((M.tmulEO (N.tensor P)) m) (((N.tmulEO P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFeo_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.odd) (p : P.odd) : ((M.assocFeo N P) (((M.tmulOO N) m) n)) p = ((M.tmulOE (N.tensor P)) m) (((N.tmulOO P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFoe_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.odd) (p : P.even) : ((M.assocFoe N P) (((M.tmulEO N) m) n)) p = ((M.tmulEO (N.tensor P)) m) (((N.tmulOE P) n) p)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocFoe_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.even) (p : P.even) : ((M.assocFoe N P) (((M.tmulOE N) m) n)) p = ((M.tmulOE (N.tensor P)) m) (((N.tmulEE P) n) p)

noncomputable def RS.SuperCommAlgebra.Mod.assocHomData {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).TensorData P (M.tensor (N.tensor P))

The data of the associator: reassociate a triple product. There is no sign; every law is an instance of the balancing and action laws of the two inner tensor products.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.assocHom {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).tensor P ⟶ M.tensor (N.tensor P)

The structure map of the associator.

Equations

• M.assocHom N P = RS.SuperCommAlgebra.Mod.mkHom (M.assocHomData N P)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocHom_evenMap_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (t : (M.tensor N).even) (p : P.even) : (M.assocHom N P).evenMap ((((M.tensor N).tmulEE P) t) p) = ((M.assocFee N P) t) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocHom_evenMap_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (t : (M.tensor N).odd) (p : P.odd) : (M.assocHom N P).evenMap ((((M.tensor N).tmulOO P) t) p) = ((M.assocFoo N P) t) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocHom_oddMap_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (t : (M.tensor N).even) (p : P.odd) : (M.assocHom N P).oddMap ((((M.tensor N).tmulEO P) t) p) = ((M.assocFeo N P) t) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocHom_oddMap_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (t : (M.tensor N).odd) (p : P.even) : (M.assocHom N P).oddMap ((((M.tensor N).tmulOE P) t) p) = ((M.assocFoe N P) t) p

The inverse of the associator

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFeeData {S : SuperCommAlgebra} (M N P : S.Mod) : N.LiftEvenData P (M.even →ₗ[ℂ] ((M.tensor N).tensor P).even)

The even-even and odd-odd blocks of the inverse associator in even total degree, lifted in the last two factors.

Equations

• M.assocInvFeeData N P = { fee := RS.bicompFlip ((M.tensor N).tmulEE P) (M.tmulEE N), foo := RS.bicompFlip ((M.tensor N).tmulOO P) (M.tmulEO N), hee := ⋯, hoo := ⋯, hoeo := ⋯, hooe := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFooData {S : SuperCommAlgebra} (M N P : S.Mod) : N.LiftOddData P (M.odd →ₗ[ℂ] ((M.tensor N).tensor P).even)

The even-odd and odd-even blocks of the inverse associator in even total degree.

Equations

• M.assocInvFooData N P = { feo := RS.bicompFlip ((M.tensor N).tmulOO P) (M.tmulOE N), foe := RS.bicompFlip ((M.tensor N).tmulEE P) (M.tmulOO N), heeo := ⋯, heoe := ⋯, hoee := ⋯, hooo := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFeoData {S : SuperCommAlgebra} (M N P : S.Mod) : N.LiftOddData P (M.even →ₗ[ℂ] ((M.tensor N).tensor P).odd)

The even-odd and odd-even blocks of the inverse associator in odd total degree.

Equations

• M.assocInvFeoData N P = { feo := RS.bicompFlip ((M.tensor N).tmulEO P) (M.tmulEE N), foe := RS.bicompFlip ((M.tensor N).tmulOE P) (M.tmulEO N), heeo := ⋯, heoe := ⋯, hoee := ⋯, hooo := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFoeData {S : SuperCommAlgebra} (M N P : S.Mod) : N.LiftEvenData P (M.odd →ₗ[ℂ] ((M.tensor N).tensor P).odd)

The even-even and odd-odd blocks of the inverse associator in odd total degree.

Equations

• M.assocInvFoeData N P = { fee := RS.bicompFlip ((M.tensor N).tmulOE P) (M.tmulOE N), foo := RS.bicompFlip ((M.tensor N).tmulEO P) (M.tmulOO N), hee := ⋯, hoo := ⋯, hoeo := ⋯, hooe := ⋯ }

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFee {S : SuperCommAlgebra} (M N P : S.Mod) : M.even →ₗ[ℂ] (N.tensor P).even →ₗ[ℂ] ((M.tensor N).tensor P).even

The even-degree block of the inverse associator.

Equations

• M.assocInvFee N P = (RS.SuperCommAlgebra.Mod.liftE (M.assocInvFeeData N P)).flip

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFoo {S : SuperCommAlgebra} (M N P : S.Mod) : M.odd →ₗ[ℂ] (N.tensor P).odd →ₗ[ℂ] ((M.tensor N).tensor P).even

The block of the inverse associator on an odd second factor with an odd first factor.

Equations

• M.assocInvFoo N P = (RS.SuperCommAlgebra.Mod.liftO (M.assocInvFooData N P)).flip

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFeo {S : SuperCommAlgebra} (M N P : S.Mod) : M.even →ₗ[ℂ] (N.tensor P).odd →ₗ[ℂ] ((M.tensor N).tensor P).odd

The block of the inverse associator on an odd second factor with an even first factor.

Equations

• M.assocInvFeo N P = (RS.SuperCommAlgebra.Mod.liftO (M.assocInvFeoData N P)).flip

noncomputable def RS.SuperCommAlgebra.Mod.assocInvFoe {S : SuperCommAlgebra} (M N P : S.Mod) : M.odd →ₗ[ℂ] (N.tensor P).even →ₗ[ℂ] ((M.tensor N).tensor P).odd

The block of the inverse associator on an even second factor with an odd first factor.

Equations

• M.assocInvFoe N P = (RS.SuperCommAlgebra.Mod.liftE (M.assocInvFoeData N P)).flip

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFee_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.even) (p : P.even) : ((M.assocInvFee N P) m) (((N.tmulEE P) n) p) = (((M.tensor N).tmulEE P) (((M.tmulEE N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFee_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.odd) (p : P.odd) : ((M.assocInvFee N P) m) (((N.tmulOO P) n) p) = (((M.tensor N).tmulOO P) (((M.tmulEO N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFoo_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.even) (p : P.odd) : ((M.assocInvFoo N P) m) (((N.tmulEO P) n) p) = (((M.tensor N).tmulOO P) (((M.tmulOE N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFoo_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.odd) (p : P.even) : ((M.assocInvFoo N P) m) (((N.tmulOE P) n) p) = (((M.tensor N).tmulEE P) (((M.tmulOO N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFeo_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.even) (p : P.odd) : ((M.assocInvFeo N P) m) (((N.tmulEO P) n) p) = (((M.tensor N).tmulEO P) (((M.tmulEE N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFeo_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (n : N.odd) (p : P.even) : ((M.assocInvFeo N P) m) (((N.tmulOE P) n) p) = (((M.tensor N).tmulOE P) (((M.tmulEO N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFoe_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.even) (p : P.even) : ((M.assocInvFoe N P) m) (((N.tmulEE P) n) p) = (((M.tensor N).tmulOE P) (((M.tmulOE N) m) n)) p

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInvFoe_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (n : N.odd) (p : P.odd) : ((M.assocInvFoe N P) m) (((N.tmulOO P) n) p) = (((M.tensor N).tmulEO P) (((M.tmulOO N) m) n)) p

noncomputable def RS.SuperCommAlgebra.Mod.assocInvData {S : SuperCommAlgebra} (M N P : S.Mod) : M.TensorData (N.tensor P) ((M.tensor N).tensor P)

The data of the inverse associator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.SuperCommAlgebra.Mod.assocInv {S : SuperCommAlgebra} (M N P : S.Mod) : M.tensor (N.tensor P) ⟶ (M.tensor N).tensor P

The structure map of the inverse associator.

Equations

• M.assocInv N P = RS.SuperCommAlgebra.Mod.mkHom (M.assocInvData N P)

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInv_evenMap_tmulEE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (w : (N.tensor P).even) : (M.assocInv N P).evenMap (((M.tmulEE (N.tensor P)) m) w) = ((M.assocInvFee N P) m) w

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInv_evenMap_tmulOO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (w : (N.tensor P).odd) : (M.assocInv N P).evenMap (((M.tmulOO (N.tensor P)) m) w) = ((M.assocInvFoo N P) m) w

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInv_oddMap_tmulEO {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.even) (w : (N.tensor P).odd) : (M.assocInv N P).oddMap (((M.tmulEO (N.tensor P)) m) w) = ((M.assocInvFeo N P) m) w

@[simp]

theorem RS.SuperCommAlgebra.Mod.assocInv_oddMap_tmulOE {S : SuperCommAlgebra} (M N P : S.Mod) (m : M.odd) (w : (N.tensor P).even) : (M.assocInv N P).oddMap (((M.tmulOE (N.tensor P)) m) w) = ((M.assocInvFoe N P) m) w

theorem RS.SuperCommAlgebra.Mod.assocHom_assocInv {S : SuperCommAlgebra} (M N P : S.Mod) : CategoryTheory.CategoryStruct.comp (M.assocHom N P) (M.assocInv N P) = CategoryTheory.CategoryStruct.id ((M.tensor N).tensor P)

Reassociating and then reassociating back is the identity.

theorem RS.SuperCommAlgebra.Mod.assocInv_assocHom {S : SuperCommAlgebra} (M N P : S.Mod) : CategoryTheory.CategoryStruct.comp (M.assocInv N P) (M.assocHom N P) = CategoryTheory.CategoryStruct.id (M.tensor (N.tensor P))

Reassociating back and then reassociating is the identity.

noncomputable def RS.SuperCommAlgebra.Mod.associator {S : SuperCommAlgebra} (M N P : S.Mod) : (M.tensor N).tensor P ≅ M.tensor (N.tensor P)

The associator: reassociation of a threefold tensor product, with no sign.

Equations

• M.associator N P = { hom := M.assocHom N P, inv := M.assocInv N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Naturality of the associator

theorem RS.SuperCommAlgebra.Mod.assocHom_naturality {S : SuperCommAlgebra} {M M' N N' P P' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') (h : P ⟶ P') : CategoryTheory.CategoryStruct.comp (tensorHom (tensorHom f g) h) (M'.assocHom N' P') = CategoryTheory.CategoryStruct.comp (M.assocHom N P) (tensorHom f (tensorHom g h))

The associator is natural in all three arguments.

The triangle identity

theorem RS.SuperCommAlgebra.Mod.triangle_identity {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.assocHom S.unitMod N) (tensorHom (CategoryTheory.CategoryStruct.id M) N.leftUnitorHom) = tensorHom M.rightUnitorHom (CategoryTheory.CategoryStruct.id N)

The triangle identity: the two ways of cancelling a unit in the middle of a threefold product agree.

The pentagon identity

theorem RS.SuperCommAlgebra.Mod.pentagon_identity {S : SuperCommAlgebra} (M N P Q : S.Mod) : CategoryTheory.CategoryStruct.comp (tensorHom (M.assocHom N P) (CategoryTheory.CategoryStruct.id Q)) (CategoryTheory.CategoryStruct.comp (M.assocHom (N.tensor P) Q) (tensorHom (CategoryTheory.CategoryStruct.id M) (N.assocHom P Q))) = CategoryTheory.CategoryStruct.comp ((M.tensor N).assocHom P Q) (M.assocHom N (P.tensor Q))

The pentagon identity: the two ways of reassociating a fourfold product agree.

The monoidal structure

@[instance_reducible]

noncomputable instance RS.SuperCommAlgebra.Mod.instMonoidalCategory {S : SuperCommAlgebra} : CategoryTheory.MonoidalCategory S.Mod

Super modules over a super-commutative ℂ-algebra form a monoidal category, with the balanced tensor product, the algebra itself as unit, and the associator and unitors built from the universal property.

Equations

• One or more equations did not get rendered due to their size.

The symmetry

theorem RS.SuperCommAlgebra.Mod.braidingHom_naturality_right {S : SuperCommAlgebra} (X : S.Mod) {Y Z : S.Mod} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id X) f) (X.braidingHom Z) = CategoryTheory.CategoryStruct.comp (X.braidingHom Y) (tensorHom f (CategoryTheory.CategoryStruct.id X))

The braiding is natural in its right-hand argument.

theorem RS.SuperCommAlgebra.Mod.braidingHom_naturality_left {S : SuperCommAlgebra} {X Y : S.Mod} (f : X ⟶ Y) (Z : S.Mod) : CategoryTheory.CategoryStruct.comp (tensorHom f (CategoryTheory.CategoryStruct.id Z)) (Y.braidingHom Z) = CategoryTheory.CategoryStruct.comp (X.braidingHom Z) (tensorHom (CategoryTheory.CategoryStruct.id Z) f)

The braiding is natural in its left-hand argument.

theorem RS.SuperCommAlgebra.Mod.hexagon_forward_identity {S : SuperCommAlgebra} (X Y Z : S.Mod) : CategoryTheory.CategoryStruct.comp (X.assocHom Y Z) (CategoryTheory.CategoryStruct.comp (X.braidingHom (Y.tensor Z)) (Y.assocHom Z X)) = CategoryTheory.CategoryStruct.comp (tensorHom (X.braidingHom Y) (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (Y.assocHom X Z) (tensorHom (CategoryTheory.CategoryStruct.id Y) (X.braidingHom Z)))

The first hexagon identity.

theorem RS.SuperCommAlgebra.Mod.hexagon_reverse_identity {S : SuperCommAlgebra} (X Y Z : S.Mod) : CategoryTheory.CategoryStruct.comp (X.assocInv Y Z) (CategoryTheory.CategoryStruct.comp ((X.tensor Y).braidingHom Z) (Z.assocInv X Y)) = CategoryTheory.CategoryStruct.comp (tensorHom (CategoryTheory.CategoryStruct.id X) (Y.braidingHom Z)) (CategoryTheory.CategoryStruct.comp (X.assocInv Z Y) (tensorHom (X.braidingHom Z) (CategoryTheory.CategoryStruct.id Y)))

The second hexagon identity.

@[instance_reducible]

noncomputable instance RS.SuperCommAlgebra.Mod.instSymmetricCategory {S : SuperCommAlgebra} : CategoryTheory.SymmetricCategory S.Mod

Super modules over a super-commutative ℂ-algebra form a symmetric monoidal category, the braiding being the Koszul swap.

Equations

• One or more equations did not get rendered due to their size.