Functoriality of the biproduct of super modules

A pair of morphisms of super modules induces one on the biproducts, componentwise; a pair of isomorphisms induces an isomorphism.

def RS.SuperCommAlgebra.Mod.biprodMap {S : SuperCommAlgebra} {M M' N N' : S.Mod} (f : M ⟶ M') (g : N ⟶ N') : M.biprod N ⟶ M'.biprod N'

The biproduct of two morphisms of super modules.

Equations

• RS.SuperCommAlgebra.Mod.biprodMap f g = { evenMap := f.evenMap.prodMap g.evenMap, oddMap := f.oddMap.prodMap g.oddMap, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

theorem RS.SuperCommAlgebra.Mod.bijective_evenMap {S : SuperCommAlgebra} {M N : S.Mod} (e : M ≅ N) : Function.Bijective ⇑e.hom.evenMap

The even component of an isomorphism is bijective.

theorem RS.SuperCommAlgebra.Mod.bijective_oddMap {S : SuperCommAlgebra} {M N : S.Mod} (e : M ≅ N) : Function.Bijective ⇑e.hom.oddMap

The odd component of an isomorphism is bijective.