Realization of a biproduct of module objects

Morphisms out of the two generators into a biproduct are pairs of morphisms, and the action on a biproduct is componentwise, so the realization of a biproduct is the biproduct of the realizations.

noncomputable def RS.gammaBiprodMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasBinaryBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M N : CategoryTheory.Mod D R) : gammaModule D L R (modBiprod R M N).X ⟶ (gammaModule D L R M.X).biprod (gammaModule D L R N.X)

The comparison of the realization of a biproduct with the biproduct of the realizations.

Equations

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

theorem RS.bijective_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (R : D) [CategoryTheory.MonObj R] (M N : CategoryTheory.Mod D R) (P : D) : Function.Bijective fun (f : P ⟶ M.X ⊞ N.X) => (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst, CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)

Morphisms into a binary biproduct are pairs, ℂ-linearly.

noncomputable def RS.gammaBiprodIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasBinaryBiproducts D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M N : CategoryTheory.Mod D R) : gammaModule D L R (modBiprod R M N).X ≅ (gammaModule D L R M.X).biprod (gammaModule D L R N.X)

The realization of a biproduct is the biproduct of the realizations.

Equations

• RS.gammaBiprodIso L R M N = RS.SuperCommAlgebra.Mod.isoOfComponents (RS.gammaBiprodMap L R M N) ⋯ ⋯