Biproducts of super modules

Super modules over a fixed super-commutative ℂ-algebra carry a zero object and binary biproducts, and both are computed componentwise: the zero module is trivial in each degree, and the biproduct of two super modules is the product of the even components together with the product of the odd components, acted on blockwise.

Nothing here needs the graded axioms in any essential way. Each of the ten axioms of RS.SuperCommAlgebra.Mod is a pointwise identity, so it holds in a product as soon as it holds in each factor, and the four structure morphisms are the four ℂ-linear structure maps of a product of modules taken in each degree at once.

Since the category is preadditive, the bicone assembled from those four morphisms is a bilimit as soon as it satisfies the total identity fst ≫ inl + snd ≫ inr = 𝟙, which in each degree is the componentwise statement (p.1, 0) + (0, p.2) = p. Finite biproducts then follow formally from the zero object and the binary ones.

Componentwise action blocks

def RS.SuperCommAlgebra.Mod.prodAct {A : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup E₁] [Module ℂ E₁] [AddCommGroup E₂] [Module ℂ E₂] [AddCommGroup F₁] [Module ℂ F₁] [AddCommGroup F₂] [Module ℂ F₂] (f : A →ₗ[ℂ] E₁ →ₗ[ℂ] F₁) (g : A →ₗ[ℂ] E₂ →ₗ[ℂ] F₂) : A →ₗ[ℂ] E₁ × E₂ →ₗ[ℂ] F₁ × F₂

The componentwise action block: a pair of bilinear action blocks acting on the two factors of a product separately. The four action blocks of a biproduct of super modules are the four instances of this construction.

Equations

• RS.SuperCommAlgebra.Mod.prodAct f g = LinearMap.mk₂ ℂ (fun (a : A) (p : E₁ × E₂) => ((f a) p.1, (g a) p.2)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.SuperCommAlgebra.Mod.prodAct_apply {A : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {F₁ : Type u_4} {F₂ : Type u_5} [AddCommGroup A] [Module ℂ A] [AddCommGroup E₁] [Module ℂ E₁] [AddCommGroup E₂] [Module ℂ E₂] [AddCommGroup F₁] [Module ℂ F₁] [AddCommGroup F₂] [Module ℂ F₂] (f : A →ₗ[ℂ] E₁ →ₗ[ℂ] F₁) (g : A →ₗ[ℂ] E₂ →ₗ[ℂ] F₂) (a : A) (p : E₁ × E₂) : ((prodAct f g) a) p = ((f a) p.1, (g a) p.2)

theorem RS.SuperCommAlgebra.Mod.inl_fst_add_inr_snd {E₁ : Type u_2} {E₂ : Type u_3} [AddCommGroup E₁] [Module ℂ E₁] [AddCommGroup E₂] [Module ℂ E₂] (p : E₁ × E₂) : (LinearMap.inl ℂ E₁ E₂) ((LinearMap.fst ℂ E₁ E₂) p) + (LinearMap.inr ℂ E₁ E₂) ((LinearMap.snd ℂ E₁ E₂) p) = p

The total identity for a product of ℂ-modules, in the form in which each degree of the biproduct of super modules needs it.

The zero module

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

The zero super module: both components trivial, all four actions zero.

Equations

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

theorem RS.SuperCommAlgebra.Mod.isZero_zeroMod (S : SuperCommAlgebra) : CategoryTheory.Limits.IsZero (zeroMod S)

The zero super module is a zero object.

instance RS.SuperCommAlgebra.Mod.hasZeroObject {S : SuperCommAlgebra} : CategoryTheory.Limits.HasZeroObject S.Mod

Super modules have a zero object.

The binary biproduct

def RS.SuperCommAlgebra.Mod.biprod {S : SuperCommAlgebra} (M N : S.Mod) : S.Mod

The biproduct of two super modules: the product of the even components, the product of the odd components, and the four action blocks taken componentwise.

Equations

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

The four structure morphisms

def RS.SuperCommAlgebra.Mod.biprodInl {S : SuperCommAlgebra} (M N : S.Mod) : M ⟶ M.biprod N

The injection of the first summand into the biproduct.

Equations

• M.biprodInl N = { evenMap := LinearMap.inl ℂ M.even N.even, oddMap := LinearMap.inl ℂ M.odd N.odd, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

def RS.SuperCommAlgebra.Mod.biprodInr {S : SuperCommAlgebra} (M N : S.Mod) : N ⟶ M.biprod N

The injection of the second summand into the biproduct.

Equations

• M.biprodInr N = { evenMap := LinearMap.inr ℂ M.even N.even, oddMap := LinearMap.inr ℂ M.odd N.odd, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

def RS.SuperCommAlgebra.Mod.biprodFst {S : SuperCommAlgebra} (M N : S.Mod) : M.biprod N ⟶ M

The projection of the biproduct onto the first summand.

Equations

• M.biprodFst N = { evenMap := LinearMap.fst ℂ M.even N.even, oddMap := LinearMap.fst ℂ M.odd N.odd, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

def RS.SuperCommAlgebra.Mod.biprodSnd {S : SuperCommAlgebra} (M N : S.Mod) : M.biprod N ⟶ N

The projection of the biproduct onto the second summand.

Equations

• M.biprodSnd N = { evenMap := LinearMap.snd ℂ M.even N.even, oddMap := LinearMap.snd ℂ M.odd N.odd, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

@[simp]

theorem RS.SuperCommAlgebra.Mod.comp_evenMap {S : SuperCommAlgebra} {M N P : S.Mod} (f : M ⟶ N) (g : N ⟶ P) : (CategoryTheory.CategoryStruct.comp f g).evenMap = g.evenMap ∘ₗ f.evenMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.comp_oddMap {S : SuperCommAlgebra} {M N P : S.Mod} (f : M ⟶ N) (g : N ⟶ P) : (CategoryTheory.CategoryStruct.comp f g).oddMap = g.oddMap ∘ₗ f.oddMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.id_evenMap {S : SuperCommAlgebra} (M : S.Mod) : (CategoryTheory.CategoryStruct.id M).evenMap = LinearMap.id

@[simp]

theorem RS.SuperCommAlgebra.Mod.id_oddMap {S : SuperCommAlgebra} (M : S.Mod) : (CategoryTheory.CategoryStruct.id M).oddMap = LinearMap.id

The bicone identities

@[simp]

theorem RS.SuperCommAlgebra.Mod.biprodInl_fst {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.biprodInl N) (M.biprodFst N) = CategoryTheory.CategoryStruct.id M

@[simp]

theorem RS.SuperCommAlgebra.Mod.biprodInl_snd {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.biprodInl N) (M.biprodSnd N) = 0

@[simp]

theorem RS.SuperCommAlgebra.Mod.biprodInr_fst {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.biprodInr N) (M.biprodFst N) = 0

@[simp]

theorem RS.SuperCommAlgebra.Mod.biprodInr_snd {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.biprodInr N) (M.biprodSnd N) = CategoryTheory.CategoryStruct.id N

theorem RS.SuperCommAlgebra.Mod.biprodTotal {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.CategoryStruct.comp (M.biprodFst N) (M.biprodInl N) + CategoryTheory.CategoryStruct.comp (M.biprodSnd N) (M.biprodInr N) = CategoryTheory.CategoryStruct.id (M.biprod N)

The total identity: the two projections followed by the two injections recover the identity of the biproduct.

Binary and finite biproducts

def RS.SuperCommAlgebra.Mod.biprodBicone {S : SuperCommAlgebra} (M N : S.Mod) : CategoryTheory.Limits.BinaryBicone M N

The binary bicone of two super modules, with vertex their biproduct.

Equations

• M.biprodBicone N = { pt := M.biprod N, fst := M.biprodFst N, snd := M.biprodSnd N, inl := M.biprodInl N, inr := M.biprodInr N, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }

def RS.SuperCommAlgebra.Mod.biprodBiconeIsBilimit {S : SuperCommAlgebra} (M N : S.Mod) : (M.biprodBicone N).IsBilimit

The biproduct bicone is a bilimit: it is simultaneously a product cone and a coproduct cocone.

Equations

• M.biprodBiconeIsBilimit N = CategoryTheory.Limits.isBinaryBilimitOfTotal (M.biprodBicone N) ⋯

instance RS.SuperCommAlgebra.Mod.hasBinaryBiproducts {S : SuperCommAlgebra} : CategoryTheory.Limits.HasBinaryBiproducts S.Mod

Super modules have binary biproducts.

instance RS.SuperCommAlgebra.Mod.hasFiniteBiproducts {S : SuperCommAlgebra} : CategoryTheory.Limits.HasFiniteBiproducts S.Mod

Super modules have finite biproducts.