The Γ-module of a module object

A module object M over a commutative monoid object R of a symmetric ℂ-linear monoidal category with an odd line L realizes as a module over the super-commutative ℂ-algebra RS.gammaAlgebra D L R: the even part is 𝟙_ D ⟶ M, the odd part is L.obj ⟶ M, and the four graded action blocks are the convolution of the internal action sandwiched between the same coherence isomorphisms that identify the sources in RS.gammaAlgebra.

The pattern of RS.GammaAlgebra repeats one level down. Everything rests on a single ungraded operation, RS.gact: the convolution (a ⊗ₘ m) ≫ γ of a morphism into R against a morphism into M, at arbitrary sources. Its two structural laws — associativity against RS.gmul up to the associator (RS.gact_assoc) and the unit law (RS.gact_one) — hold once and for all, and each of the ten axioms of RS.SuperCommAlgebra.Mod is one of them conjugated by coherence isomorphisms.

There is no commutativity axiom for a module, so the odd line enters only through the source identification L.sq of the odd-odd block; as in the algebra, the odd-odd-odd associativity is the one axiom not implied by coherence alone, and it is again the first triangle identity of the self-duality of the odd line, RS.OddLine.evaluation_coevaluation.

Modules over a super-commutative ℂ-algebra

structure RS.SuperCommAlgebra.Mod (S : SuperCommAlgebra) : Type (max (max (max u u') (w + 1)) (w' + 1))

A module over a super-commutative ℂ-algebra, presented as a pair of ℂ-modules — the even and odd components — with the four graded action blocks, the two unit laws and associativity at every parity pattern of a scalar pair acting on a module element.

The blocks are indexed by the parities of the two algebra arguments and of the module argument, and the parity of the value is their sum: assoc_xyz says that acting by the product of an x-parity and a y-parity scalar is acting by the second and then by the first.

• even : Type w

  The even component.

• odd : Type w'

  The odd component.

• evenAddCommGroup : AddCommGroup self.even
• evenModule : Module ℂ self.even
• oddAddCommGroup : AddCommGroup self.odd
• oddModule : Module ℂ self.odd
• actEE : S.even →ₗ[ℂ] self.even →ₗ[ℂ] self.even

  The action of an even scalar on an even element.

• actEO : S.even →ₗ[ℂ] self.odd →ₗ[ℂ] self.odd

  The action of an even scalar on an odd element.

• actOE : S.odd →ₗ[ℂ] self.even →ₗ[ℂ] self.odd

  The action of an odd scalar on an even element.

• actOO : S.odd →ₗ[ℂ] self.odd →ₗ[ℂ] self.even

  The action of an odd scalar on an odd element.

• one_act_e (m : self.even) : (self.actEE S.one) m = m

  The unit acts as the identity on the even component.

• one_act_o (m : self.odd) : (self.actEO S.one) m = m

  The unit acts as the identity on the odd component.

• assoc_eee (x y : S.even) (m : self.even) : (self.actEE ((S.mulEE x) y)) m = (self.actEE x) ((self.actEE y) m)

  Associativity at parity pattern even-even-even.

• assoc_eeo (x y : S.even) (m : self.odd) : (self.actEO ((S.mulEE x) y)) m = (self.actEO x) ((self.actEO y) m)

  Associativity at parity pattern even-even-odd.

• assoc_eoe (x : S.even) (u : S.odd) (m : self.even) : (self.actOE ((S.mulEO x) u)) m = (self.actEO x) ((self.actOE u) m)

  Associativity at parity pattern even-odd-even.

• assoc_eoo (x : S.even) (u : S.odd) (m : self.odd) : (self.actOO ((S.mulEO x) u)) m = (self.actEE x) ((self.actOO u) m)

  Associativity at parity pattern even-odd-odd.

• assoc_oee (u : S.odd) (x : S.even) (m : self.even) : (self.actOE ((S.mulOE u) x)) m = (self.actOE u) ((self.actEE x) m)

  Associativity at parity pattern odd-even-even.

• assoc_oeo (u : S.odd) (x : S.even) (m : self.odd) : (self.actOO ((S.mulOE u) x)) m = (self.actOO u) ((self.actEO x) m)

  Associativity at parity pattern odd-even-odd.

• assoc_ooe (u v : S.odd) (m : self.even) : (self.actEE ((S.mulOO u) v)) m = (self.actOO u) ((self.actOE v) m)

  Associativity at parity pattern odd-odd-even.

• assoc_ooo (u v : S.odd) (m : self.odd) : (self.actEO ((S.mulOO u) v)) m = (self.actOE u) ((self.actOO v) m)

  Associativity at parity pattern odd-odd-odd.

Ungraded convolution against a module object

noncomputable def RS.gact {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] {X Y : D} (a : X ⟶ R) (m : Y ⟶ M) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ M

The convolution action of a morphism into a monoid object on a morphism into a module object, taken at arbitrary sources: tensor the two morphisms and act.

Equations

• RS.gact a m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) (RS.actLeft R M)

theorem RS.gact_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] {X Y : D} (a : X ⟶ R) (m : Y ⟶ M) : gact a m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) (actLeft R M)

The convolution action unfolded.

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

Reindexing the scalar source of a convolution action.

theorem RS.gact_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] {X Y Z : D} (a : X ⟶ R) (g : Z ⟶ Y) (m : Y ⟶ M) : gact a (CategoryTheory.CategoryStruct.comp g m) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) (gact a m)

Reindexing the module source of a convolution action.

theorem RS.gact_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] {X Y Z : D} (a : X ⟶ R) (b : Y ⟶ R) (m : Z ⟶ M) : gact (gmul a b) m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (gact a (gact b m))

The convolution action is associative against the convolution product, up to the associator of the three sources.

theorem RS.gact_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] {Y : D} (m : Y ⟶ M) : gact CategoryTheory.MonObj.one m = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom m

The monoid unit acts as the identity.

theorem RS.add_gact {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {X Y : D} (a a' : X ⟶ R) (m : Y ⟶ M) : gact (a + a') m = gact a m + gact a' m

The convolution action is additive in its scalar argument.

theorem RS.gact_add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {X Y : D} (a : X ⟶ R) (m m' : Y ⟶ M) : gact a (m + m') = gact a m + gact a m'

The convolution action is additive in its module argument.

theorem RS.smul_gact {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (r : ℂ) {X Y : D} (a : X ⟶ R) (m : Y ⟶ M) : gact (r • a) m = r • gact a m

The convolution action is ℂ-homogeneous in its scalar argument.

theorem RS.gact_smul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (r : ℂ) {X Y : D} (a : X ⟶ R) (m : Y ⟶ M) : gact a (r • m) = r • gact a m

The convolution action is ℂ-homogeneous in its module argument.

The bundled bilinear convolution action

noncomputable def RS.gactLin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {W X Y : D} (s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) : (X ⟶ R) →ₗ[ℂ] (Y ⟶ M) →ₗ[ℂ] W ⟶ M

The convolution action as a ℂ-bilinear map of hom-modules, transported along a chosen morphism s from the intended source into the tensor product of the two given sources. The four graded action blocks of RS.gammaModule are the four instances of this construction.

Equations

• RS.gactLin s = LinearMap.mk₂ ℂ (fun (a : X ⟶ R) (m : Y ⟶ M) => CategoryTheory.CategoryStruct.comp s (RS.gact a m)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.gactLin_apply {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {W X Y : D} (s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (a : X ⟶ R) (m : Y ⟶ M) : ((gactLin s) a) m = CategoryTheory.CategoryStruct.comp s (gact a m)

theorem RS.gactLin_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {M : D} [CategoryTheory.ModObj R M] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {W W' V X Y Z : D} (s₁ : W' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W Z) (s₂ : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (s₃ : W' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X V) (s₄ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) (h : CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight s₂ Z) (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X s₄)) (a : X ⟶ R) (b : Y ⟶ R) (m : Z ⟶ M) : ((gactLin s₁) (((gmulLin s₂) a) b)) m = ((gactLin s₃) a) (((gactLin s₄) b) m)

The transported associativity law: given a coherence identity between the two ways of reassociating the chosen sources, acting by a convolution product agrees with acting twice.

The Γ-module of a module object

noncomputable def RS.gammaModule (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 : D) [CategoryTheory.ModObj R M] : (gammaAlgebra D L R).Mod

The Γ-module of a module object: for a module object M over a commutative monoid object R of a symmetric ℂ-linear monoidal category carrying an odd line L, the morphisms 𝟙_ D ⟶ M and L.obj ⟶ M form a module over the super-commutative ℂ-algebra RS.gammaAlgebra D L R under the convolution action.

The four blocks are the convolution action conjugated by the same coherence isomorphisms that identify the sources in RS.gammaAlgebra: the left unitor for even-even and even-odd, the right unitor for odd-even, and the square trivialisation L.sq of the odd line for odd-odd.

Equations

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