Morphisms of super modules

A morphism of super modules over a super-commutative algebra is a pair of ℂ-linear maps, one in each degree, commuting with the four action blocks. Postcomposition with a morphism of module objects realizes one.

structure RS.SuperCommAlgebra.Mod.Hom {S : SuperCommAlgebra} (M : S.Mod) (N : S.Mod) : Type (max (max (max u_3 u_4) u_5) u_6)

A morphism of super modules: a degreewise ℂ-linear map commuting with all four actions.

• evenMap : M.even →ₗ[ℂ] N.even

  The even component.

• oddMap : M.odd →ₗ[ℂ] N.odd

  The odd component.

• map_actEE (x : S.even) (m : M.even) : self.evenMap ((M.actEE x) m) = (N.actEE x) (self.evenMap m)

  Compatibility with the even-on-even action.

• map_actEO (x : S.even) (m : M.odd) : self.oddMap ((M.actEO x) m) = (N.actEO x) (self.oddMap m)

  Compatibility with the even-on-odd action.

• map_actOE (u : S.odd) (m : M.even) : self.oddMap ((M.actOE u) m) = (N.actOE u) (self.evenMap m)

  Compatibility with the odd-on-even action.

• map_actOO (u : S.odd) (m : M.odd) : self.evenMap ((M.actOO u) m) = (N.actOO u) (self.oddMap m)

  Compatibility with the odd-on-odd action.

theorem RS.SuperCommAlgebra.Mod.Hom.ext_iff {S : SuperCommAlgebra} {M : S.Mod} {N : S.Mod} {x y : M.Hom N} : x = y ↔ x.evenMap = y.evenMap ∧ x.oddMap = y.oddMap

theorem RS.SuperCommAlgebra.Mod.Hom.ext {S : SuperCommAlgebra} {M : S.Mod} {N : S.Mod} {x y : M.Hom N} (evenMap : x.evenMap = y.evenMap) (oddMap : x.oddMap = y.oddMap) : x = y

def RS.SuperCommAlgebra.Mod.Hom.id {S : SuperCommAlgebra} (M : S.Mod) : M.Hom M

The identity morphism of super modules.

Equations

• RS.SuperCommAlgebra.Mod.Hom.id M = { evenMap := LinearMap.id, oddMap := LinearMap.id, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

def RS.SuperCommAlgebra.Mod.Hom.comp {S : SuperCommAlgebra} {M : S.Mod} {N : S.Mod} {P : S.Mod} (f : M.Hom N) (g : N.Hom P) : M.Hom P

Composition of morphisms of super modules.

Equations

• f.comp g = { evenMap := g.evenMap ∘ₗ f.evenMap, oddMap := g.oddMap ∘ₗ f.oddMap, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.instCategory {S : SuperCommAlgebra} : CategoryTheory.Category.{max u_3 u_4, max (max (max (u_3 + 1) (u_4 + 1)) u_2) u_1} S.Mod

Super modules over a fixed algebra form a category.

Equations

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

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homZero {S : SuperCommAlgebra} (M N : S.Mod) : Zero (M ⟶ N)

The zero morphism of super modules.

Equations

• M.homZero N = { zero := { evenMap := 0, oddMap := 0, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ } }

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homAdd {S : SuperCommAlgebra} (M N : S.Mod) : Add (M ⟶ N)

Addition of morphisms of super modules.

Equations

• M.homAdd N = { add := fun (f g : M ⟶ N) => { evenMap := f.evenMap + g.evenMap, oddMap := f.oddMap + g.oddMap, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ } }

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homNeg {S : SuperCommAlgebra} (M N : S.Mod) : Neg (M ⟶ N)

Negation of morphisms of super modules.

Equations

• M.homNeg N = { neg := fun (f : M ⟶ N) => { evenMap := -f.evenMap, oddMap := -f.oddMap, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ } }

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homSMul {S : SuperCommAlgebra} (M N : S.Mod) : SMul ℂ (M ⟶ N)

Scaling of morphisms of super modules.

Equations

• M.homSMul N = { smul := fun (c : ℂ) (f : M ⟶ N) => { evenMap := c • f.evenMap, oddMap := c • f.oddMap, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ } }

@[simp]

theorem RS.SuperCommAlgebra.Mod.add_evenMap {S : SuperCommAlgebra} {M N : S.Mod} (f g : M ⟶ N) : (f + g).evenMap = f.evenMap + g.evenMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.add_oddMap {S : SuperCommAlgebra} {M N : S.Mod} (f g : M ⟶ N) : (f + g).oddMap = f.oddMap + g.oddMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.zero_evenMap {S : SuperCommAlgebra} {M N : S.Mod} : Hom.evenMap 0 = 0

@[simp]

theorem RS.SuperCommAlgebra.Mod.zero_oddMap {S : SuperCommAlgebra} {M N : S.Mod} : Hom.oddMap 0 = 0

@[simp]

theorem RS.SuperCommAlgebra.Mod.neg_evenMap {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) : (-f).evenMap = -f.evenMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.neg_oddMap {S : SuperCommAlgebra} {M N : S.Mod} (f : M ⟶ N) : (-f).oddMap = -f.oddMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.smul_evenMap {S : SuperCommAlgebra} {M N : S.Mod} (c : ℂ) (f : M ⟶ N) : (c • f).evenMap = c • f.evenMap

@[simp]

theorem RS.SuperCommAlgebra.Mod.smul_oddMap {S : SuperCommAlgebra} {M N : S.Mod} (c : ℂ) (f : M ⟶ N) : (c • f).oddMap = c • f.oddMap

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.homAddCommGroup {S : SuperCommAlgebra} (M N : S.Mod) : AddCommGroup (M ⟶ N)

Morphisms of super modules form an additive group.

Equations

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

@[instance_reducible]

instance RS.SuperCommAlgebra.Mod.instPreadditive {S : SuperCommAlgebra} : CategoryTheory.Preadditive S.Mod

Super modules form a preadditive category.

Equations

• RS.SuperCommAlgebra.Mod.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

theorem RS.gact_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {M N : D} [CategoryTheory.ModObj R M] [CategoryTheory.ModObj R N] (f : M ⟶ N) [CategoryTheory.IsModHom R f] {X Y : D} (a : X ⟶ R) (m : Y ⟶ M) : CategoryTheory.CategoryStruct.comp (gact a m) f = gact a (CategoryTheory.CategoryStruct.comp m f)

The convolution action is natural in the module object.

noncomputable def RS.gammaModuleMap {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] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {M N : D} [CategoryTheory.ModObj R M] [CategoryTheory.ModObj R N] (f : M ⟶ N) [CategoryTheory.IsModHom R f] : gammaModule D L R M ⟶ gammaModule D L R N

Postcomposition realizes a morphism of super modules.

Equations

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