Realization of ind-super-objects as super algebras

The §4 descent works with commutative algebra in genuine ℤ/2-graded ℂ-modules. This file supplies the bridge in three layers.

• RS.SuperCommAlgebra — a super-commutative ℂ-algebra presented as a pair of ℂ-modules with the four graded multiplication blocks and the Koszul sign rule, mirroring the two-component design of RS.SuperVect. The key lemmas: the ideal generated by the odd part is nil (oddIdeal_le_nilradical, isNilpotent_of_mem_oddIdeal), hence proper on a nonzero algebra (oddIdeal_ne_top), so the quotient S.even ⧸ S.oddIdeal is a nonzero ordinary commutative ℂ-algebra (nontrivial_quotient_of_nontrivial) — step (i) of Deligne's §4.5 ending, feeding RS.exists_algHom_complex.

• RS.SuperMod — the category of ℤ/2-graded ℂ-modules of arbitrary dimension: pairs of ℂ-modules with grading-preserving linear maps, RS.SuperVect with the finiteness constraints removed, with its additive and ℂ-linear structure.

• RS.superRealize — the Γ-functor. The whole Ind-layer runs over a small category (RS.indOf, the Ind C instances), and RS.SuperVect is large, so the functor is stated at the tree's standard generality: a small preadditive C with finite colimits and a chosen generator pair g₀ g₁ : C (the unit and the odd line of a small model of SuperVect; SuperSmall.lean builds one). On an ind-object it takes Hom(indOf g₀, −) and Hom(indOf g₁, −) as the even and odd parts, with ℂ-module structures from the linear structure of Ind C. It is additive and ℂ-linear (superRealize_additive, superRealize_linear), and it reflects zero objects whenever the pair biproduct-generates C (isZero_of_isZero_superRealize), via the embedded-generator vanishing lemma indOf_hom_eq_zero and the recognition isZero_of_generator_hom_eq_zero of zero ind-objects by their values on C.

Super-commutative ℂ-algebras as graded pairs

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

A super-commutative ℂ-algebra, presented as a pair of ℂ-modules — the even and odd components — with the four graded multiplication blocks, associativity at every parity pattern, and commutativity with the Koszul sign: even elements are central and odd elements anticommute. This is the algebraic realization of a commutative monoid object of the ind-completion of super vector spaces.

• even : Type u

  The even component.

• odd : Type u'

  The odd component.

• evenAddCommGroup : AddCommGroup self.even
• evenModule : Module ℂ self.even
• oddAddCommGroup : AddCommGroup self.odd
• oddModule : Module ℂ self.odd
• one : self.even

  The multiplicative unit, an even element.

• mulEE : self.even →ₗ[ℂ] self.even →ₗ[ℂ] self.even

  Multiplication, even times even.

• mulEO : self.even →ₗ[ℂ] self.odd →ₗ[ℂ] self.odd

  Multiplication, even times odd.

• mulOE : self.odd →ₗ[ℂ] self.even →ₗ[ℂ] self.odd

  Multiplication, odd times even.

• mulOO : self.odd →ₗ[ℂ] self.odd →ₗ[ℂ] self.even

  Multiplication, odd times odd.

• one_mul_e (x : self.even) : (self.mulEE self.one) x = x

  The unit law on the even component.

• one_mul_o (u : self.odd) : (self.mulEO self.one) u = u

  The unit law on the odd component.

• assoc_eee (x y z : self.even) : (self.mulEE ((self.mulEE x) y)) z = (self.mulEE x) ((self.mulEE y) z)

  Associativity at parity pattern even-even-even.

• assoc_eeo (x y : self.even) (u : self.odd) : (self.mulEO ((self.mulEE x) y)) u = (self.mulEO x) ((self.mulEO y) u)

  Associativity at parity pattern even-even-odd.

• assoc_eoe (x : self.even) (u : self.odd) (y : self.even) : (self.mulOE ((self.mulEO x) u)) y = (self.mulEO x) ((self.mulOE u) y)

  Associativity at parity pattern even-odd-even.

• assoc_eoo (x : self.even) (u v : self.odd) : (self.mulOO ((self.mulEO x) u)) v = (self.mulEE x) ((self.mulOO u) v)

  Associativity at parity pattern even-odd-odd.

• assoc_oee (u : self.odd) (x y : self.even) : (self.mulOE ((self.mulOE u) x)) y = (self.mulOE u) ((self.mulEE x) y)

  Associativity at parity pattern odd-even-even.

• assoc_oeo (u : self.odd) (x : self.even) (v : self.odd) : (self.mulOO ((self.mulOE u) x)) v = (self.mulOO u) ((self.mulEO x) v)

  Associativity at parity pattern odd-even-odd.

• assoc_ooe (u v : self.odd) (y : self.even) : (self.mulEE ((self.mulOO u) v)) y = (self.mulOO u) ((self.mulOE v) y)

  Associativity at parity pattern odd-odd-even.

• assoc_ooo (u v w : self.odd) : (self.mulEO ((self.mulOO u) v)) w = (self.mulOE u) ((self.mulOO v) w)

  Associativity at parity pattern odd-odd-odd.

• comm_ee (x y : self.even) : (self.mulEE x) y = (self.mulEE y) x

  Even elements commute.

• comm_eo (x : self.even) (u : self.odd) : (self.mulEO x) u = (self.mulOE u) x

  Even and odd elements commute: the sign (−1)^{0·1} is 1.

• comm_oo (u v : self.odd) : (self.mulOO u) v = -(self.mulOO v) u

  Odd elements anticommute: the Koszul sign (−1)^{1·1} is −1.

theorem RS.SuperCommAlgebra.mulEO_mulOO_self (S : SuperCommAlgebra) (u v : S.odd) : (S.mulEO ((S.mulOO u) v)) u = 0

The recurring cancellation (uv)·u = 0 for odd u, v: moving u across v and across itself produces the two opposite signs at once.

theorem RS.SuperCommAlgebra.mulEE_mulOO_self (S : SuperCommAlgebra) (u v : S.odd) : (S.mulEE ((S.mulOO u) v)) ((S.mulOO u) v) = 0

Products of two odd elements are square-zero in the even component.

@[instance_reducible]

instance RS.SuperCommAlgebra.instCommRingEven (S : SuperCommAlgebra) : CommRing S.even

The even component is an ordinary commutative ring under the even-even multiplication block.

Equations

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

theorem RS.SuperCommAlgebra.mul_def (S : SuperCommAlgebra) (x y : S.even) : x * y = (S.mulEE x) y

Multiplication in the even ring is the even-even block.

theorem RS.SuperCommAlgebra.one_def (S : SuperCommAlgebra) : 1 = S.one

The unit of the even ring is the structural unit.

@[instance_reducible]

instance RS.SuperCommAlgebra.instAlgebraEven (S : SuperCommAlgebra) : Algebra ℂ S.even

The even component is a ℂ-algebra: the scalar action is the module structure, compatible with multiplication by bilinearity of the even-even block.

Equations

• S.instAlgebraEven = Algebra.ofModule ⋯ ⋯

def RS.SuperCommAlgebra.oddIdeal (S : SuperCommAlgebra) : Ideal S.even

The even part of the ideal generated by the odd component: the ideal of the even ring spanned by the products of two odd elements.

Equations

• S.oddIdeal = Ideal.span (Set.range fun (p : S.odd × S.odd) => (S.mulOO p.1) p.2)

theorem RS.SuperCommAlgebra.oddIdeal_le_nilradical (S : SuperCommAlgebra) : S.oddIdeal ≤ nilradical S.even

The odd-generated ideal is nil: it is spanned by square-zero elements of a commutative ring, so it lies inside the nilradical.

theorem RS.SuperCommAlgebra.isNilpotent_of_mem_oddIdeal (S : SuperCommAlgebra) {x : S.even} (hx : x ∈ S.oddIdeal) : IsNilpotent x

Every element of the odd-generated ideal is nilpotent.

theorem RS.SuperCommAlgebra.oddIdeal_ne_top (S : SuperCommAlgebra) [Nontrivial S.even] : S.oddIdeal ≠ ⊤

On a nonzero even ring the odd-generated ideal is proper: the unit is not nilpotent.

theorem RS.SuperCommAlgebra.nontrivial_quotient_oddIdeal (S : SuperCommAlgebra) [Nontrivial S.even] : Nontrivial (S.even ⧸ S.oddIdeal)

Killing the odd-generated ideal of a super-commutative ℂ-algebra with nonzero even part leaves a nonzero ordinary commutative ℂ-algebra.

theorem RS.SuperCommAlgebra.subsingleton_odd (S : SuperCommAlgebra) (h : Subsingleton S.even) : Subsingleton S.odd

A trivial even component trivializes the odd component: the unit acts as the identity on odd elements.

theorem RS.SuperCommAlgebra.nontrivial_even_of_nontrivial (S : SuperCommAlgebra) (h : Nontrivial S.even ∨ Nontrivial S.odd) : Nontrivial S.even

A nonzero super-commutative ℂ-algebra has nonzero even part.

theorem RS.SuperCommAlgebra.nontrivial_quotient_of_nontrivial (S : SuperCommAlgebra) (h : Nontrivial S.even ∨ Nontrivial S.odd) : Nontrivial (S.even ⧸ S.oddIdeal)

The odd-nil quotient (Deligne §4.5, step (i)): a nonzero super-commutative ℂ-algebra has a nonzero ordinary commutative ℂ-algebra quotient — the even part modulo the ideal generated by the odd part. The CommRing and Algebra ℂ structures on the quotient are the Ideal.Quotient instances over instCommRingEven and instAlgebraEven.

The category of ℤ/2-graded ℂ-modules

structure RS.SuperMod : Type (u + 1)

A super module over ℂ: a pair of complex modules of arbitrary dimension, the even and odd components — RS.SuperVect with the finiteness constraints removed.

• even : Type u

  The even-graded component.

• odd : Type u

  The odd-graded component.

• evenAddCommGroup : AddCommGroup self.even
• evenModule : Module ℂ self.even
• oddAddCommGroup : AddCommGroup self.odd
• oddModule : Module ℂ self.odd

structure RS.SuperMod.Hom (V W : SuperMod) : Type u

A morphism of super modules: a pair of ℂ-linear maps preserving the grading.

• evenMap : V.even →ₗ[ℂ] W.even

  The even component of the morphism.

• oddMap : V.odd →ₗ[ℂ] W.odd

  The odd component of the morphism.

theorem RS.SuperMod.Hom.ext_iff {V W : SuperMod} {x y : V.Hom W} : x = y ↔ x.evenMap = y.evenMap ∧ x.oddMap = y.oddMap

theorem RS.SuperMod.Hom.ext {V W : SuperMod} {x y : V.Hom W} (evenMap : x.evenMap = y.evenMap) (oddMap : x.oddMap = y.oddMap) : x = y

def RS.SuperMod.Hom.id (V : SuperMod) : V.Hom V

The identity morphism on a super module.

Equations

• RS.SuperMod.Hom.id V = { evenMap := LinearMap.id, oddMap := LinearMap.id }

def RS.SuperMod.Hom.comp {V W X : SuperMod} (g : W.Hom X) (f : V.Hom W) : V.Hom X

Composition of super-module morphisms.

Equations

• g.comp f = { evenMap := g.evenMap ∘ₗ f.evenMap, oddMap := g.oddMap ∘ₗ f.oddMap }

@[instance_reducible]

instance RS.SuperMod.instCategoryStruct : CategoryTheory.CategoryStruct.{u, u + 1} SuperMod

Super modules and grading-preserving maps form a category.

Equations

• RS.SuperMod.instCategoryStruct = { Hom := RS.SuperMod.Hom, id := RS.SuperMod.Hom.id, comp := fun {X Y Z : RS.SuperMod} (f : X.Hom Y) (g : Y.Hom Z) => g.comp f }

theorem RS.SuperMod.hom_ext {V W : SuperMod} {f g : V ⟶ W} (he : f.evenMap = g.evenMap) (ho : f.oddMap = g.oddMap) : f = g

Two morphisms agreeing in both components are equal.

theorem RS.SuperMod.hom_ext_iff {V W : SuperMod} {f g : V ⟶ W} : f = g ↔ f.evenMap = g.evenMap ∧ f.oddMap = g.oddMap

@[instance_reducible]

instance RS.SuperMod.instCategory : CategoryTheory.Category.{u, u + 1} SuperMod

SuperMod forms a category with grading-preserving linear maps.

Equations

• RS.SuperMod.instCategory = { toCategoryStruct := RS.SuperMod.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

Additive and linear structure, mirroring SuperVect

@[instance_reducible]

instance RS.SuperMod.instZeroHom {V W : SuperMod} : Zero (V ⟶ W)

The zero morphism: zero in both components.

Equations

• RS.SuperMod.instZeroHom = { zero := { evenMap := 0, oddMap := 0 } }

@[instance_reducible]

instance RS.SuperMod.instAddHom {V W : SuperMod} : Add (V ⟶ W)

Componentwise addition of morphisms.

Equations

• RS.SuperMod.instAddHom = { add := fun (f g : V ⟶ W) => { evenMap := f.evenMap + g.evenMap, oddMap := f.oddMap + g.oddMap } }

@[instance_reducible]

instance RS.SuperMod.instNegHom {V W : SuperMod} : Neg (V ⟶ W)

Componentwise negation.

Equations

• RS.SuperMod.instNegHom = { neg := fun (f : V ⟶ W) => { evenMap := -f.evenMap, oddMap := -f.oddMap } }

@[instance_reducible]

instance RS.SuperMod.instSubHom {V W : SuperMod} : Sub (V ⟶ W)

Componentwise subtraction.

Equations

• RS.SuperMod.instSubHom = { sub := fun (f g : V ⟶ W) => { evenMap := f.evenMap - g.evenMap, oddMap := f.oddMap - g.oddMap } }

@[instance_reducible]

instance RS.SuperMod.instSMulComplexHom {V W : SuperMod} : SMul ℂ (V ⟶ W)

Componentwise scaling by a complex number.

Equations

• RS.SuperMod.instSMulComplexHom = { smul := fun (c : ℂ) (f : V ⟶ W) => { evenMap := c • f.evenMap, oddMap := c • f.oddMap } }

@[instance_reducible]

instance RS.SuperMod.instSMulNatHom {V W : SuperMod} : SMul ℕ (V ⟶ W)

Componentwise natural scaling, definitional so that the AddCommGroup structure below has no transported nsmul field.

Equations

• RS.SuperMod.instSMulNatHom = { smul := fun (n : ℕ) (f : V ⟶ W) => { evenMap := n • f.evenMap, oddMap := n • f.oddMap } }

@[instance_reducible]

instance RS.SuperMod.instSMulIntHom {V W : SuperMod} : SMul ℤ (V ⟶ W)

Componentwise integer scaling, likewise definitional.

Equations

• RS.SuperMod.instSMulIntHom = { smul := fun (n : ℤ) (f : V ⟶ W) => { evenMap := n • f.evenMap, oddMap := n • f.oddMap } }

def RS.SuperMod.homComponents {V W : SuperMod} (f : V ⟶ W) : (V.even →ₗ[ℂ] W.even) × (V.odd →ₗ[ℂ] W.odd)

The components of a morphism determine it; the additive and module structures are pulled back componentwise.

Equations

• RS.SuperMod.homComponents f = (f.evenMap, f.oddMap)

theorem RS.SuperMod.homComponents_injective {V W : SuperMod} : Function.Injective homComponents

Componentwise equality of morphisms.

@[instance_reducible]

instance RS.SuperMod.instAddCommGroupHom {V W : SuperMod} : AddCommGroup (V ⟶ W)

Morphisms form an abelian group, pulled back along the injection into the pair of component maps.

Equations

• RS.SuperMod.instAddCommGroupHom = Function.Injective.addCommGroup RS.SuperMod.homComponents ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance RS.SuperMod.instModuleComplexHom {V W : SuperMod} : Module ℂ (V ⟶ W)

Morphisms form a ℂ-module, pulled back the same way.

Equations

• RS.SuperMod.instModuleComplexHom = Function.Injective.module ℂ { toFun := RS.SuperMod.homComponents, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem RS.SuperMod.add_evenMap {V W : SuperMod} (f g : V ⟶ W) : (f + g).evenMap = f.evenMap + g.evenMap

Addition of morphisms is componentwise on the even part.

@[simp]

theorem RS.SuperMod.add_oddMap {V W : SuperMod} (f g : V ⟶ W) : (f + g).oddMap = f.oddMap + g.oddMap

Addition of morphisms is componentwise on the odd part.

@[simp]

theorem RS.SuperMod.zero_evenMap {V W : SuperMod} : Hom.evenMap 0 = 0

The zero morphism's even component is zero.

@[simp]

theorem RS.SuperMod.zero_oddMap {V W : SuperMod} : Hom.oddMap 0 = 0

The zero morphism's odd component is zero.

@[simp]

theorem RS.SuperMod.smul_evenMap {V W : SuperMod} (c : ℂ) (f : V ⟶ W) : (c • f).evenMap = c • f.evenMap

Scalar multiplication is componentwise on the even part.

@[simp]

theorem RS.SuperMod.smul_oddMap {V W : SuperMod} (c : ℂ) (f : V ⟶ W) : (c • f).oddMap = c • f.oddMap

Scalar multiplication is componentwise on the odd part.

@[instance_reducible]

instance RS.SuperMod.instPreadditive : CategoryTheory.Preadditive SuperMod

SuperMod is preadditive: composition is bilinear componentwise.

Equations

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

@[instance_reducible]

instance RS.SuperMod.instLinear : CategoryTheory.Linear ℂ SuperMod

SuperMod is ℂ-linear: composition is ℂ-bilinear componentwise.

Equations

• RS.SuperMod.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

theorem RS.SuperMod.even_eq_zero_of_isZero {V : SuperMod} (h : CategoryTheory.Limits.IsZero V) (x : V.even) : x = 0

Even elements of a zero super module vanish: the identity morphism is the zero morphism.

theorem RS.SuperMod.odd_eq_zero_of_isZero {V : SuperMod} (h : CategoryTheory.Limits.IsZero V) (x : V.odd) : x = 0

Odd elements of a zero super module vanish.

The Γ-functor on the ind-completion

noncomputable def RS.superRealize {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (g₀ g₁ : C) [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] : CategoryTheory.Functor (CategoryTheory.Ind C) SuperMod

The realization functor relative to a generator pair g₀ g₁ : C — the unit and the odd line of the small model of SuperVect in the intended instantiation. An ind-object realizes as the ℤ/2-graded ℂ-module of morphisms out of the embedded generators: Hom(indOf g₀, −) in even degree and Hom(indOf g₁, −) in odd degree, with the ℂ-module structures given by the linear structure of Ind C.

Equations

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

instance RS.superRealize_additive {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (g₀ g₁ : C) [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] : (superRealize g₀ g₁).Additive

The realization functor is additive: postcomposition distributes over sums of morphisms of ind-objects.

instance RS.superRealize_linear {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (g₀ g₁ : C) [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] : CategoryTheory.Functor.Linear ℂ (superRealize g₀ g₁)

The realization functor is ℂ-linear.

Zero reflection

def RS.BiproductGenerates {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {ι : Type u_1} (g : ι → C) : Prop

A family of objects biproduct-generates a category if every object is isomorphic to a finite biproduct of members of the family. For the small model of SuperVect the two-member family of the unit and the odd line generates in this sense.

Equations

• RS.BiproductGenerates g = ∀ (X : C), ∃ (n : ℕ) (w : Fin n → ι), Nonempty (X ≅ ⨁ g ∘ w)

theorem RS.indOf_hom_eq_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {ι : Type u_1} {g : ι → C} {F : CategoryTheory.Ind C} (hvan : ∀ (i : ι) (f : indOf.obj (g i) ⟶ F), f = 0) {n : ℕ} {w : Fin n → ι} {X : C} (φ : X ≅ ⨁ g ∘ w) (f : indOf.obj X ⟶ F) : f = 0

Morphisms from an embedded object into an ind-object vanish once they vanish from the embedded generators, along a biproduct decomposition of the object: the embedding is additive, so the biproduct decomposition of the identity transports.

theorem RS.isZero_ind_of_hom_eq_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {F : CategoryTheory.Ind C} (h : ∀ (X : C) (f : indOf.obj X ⟶ F), f = 0) : CategoryTheory.Limits.IsZero F

Zero recognition on values: an ind-object with no nonzero morphism from any embedded object is zero. The underlying presheaf has singleton values, so it is isomorphic to the presheaf of the embedded zero object, and full faithfulness of the inclusion pulls the isomorphism back.

theorem RS.isZero_of_generator_hom_eq_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] {ι : Type u_1} {g : ι → C} (hgen : BiproductGenerates g) {F : CategoryTheory.Ind C} (hvan : ∀ (i : ι) (f : indOf.obj (g i) ⟶ F), f = 0) : CategoryTheory.Limits.IsZero F

Zero recognition by generators: an ind-object with no nonzero morphism from the embedded members of a biproduct-generating family is zero.

def RS.generatorPair {C : Type v} (g₀ g₁ : C) : Bool → C

The generator pair of the realization functor as a Bool-indexed family: false is the even generator, true the odd one.

Equations

• RS.generatorPair g₀ g₁ b = bif b then g₁ else g₀

theorem RS.isZero_of_isZero_superRealize {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (g₀ g₁ : C) [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] (hgen : BiproductGenerates (generatorPair g₀ g₁)) {F : CategoryTheory.Ind C} (hF : CategoryTheory.Limits.IsZero ((superRealize g₀ g₁).obj F)) : CategoryTheory.Limits.IsZero F

The realization functor reflects zero objects: over a biproduct-generating pair, an ind-object whose even and odd realizations vanish is zero.

The convolution algebra of a commutative monoid object

The even half of the monoid transport: for a commutative monoid object R of a braided ℂ-linear monoidal category — Ind C with its transported structure in the intended instantiation — the morphisms 𝟙 ⟶ R carry an ordinary commutative ℂ-algebra structure under the convolution product a · b = λ⁻¹ ≫ (a ⊗ b) ≫ μ. Together with the unit identification indOfUnitIso this equips the even part of superRealize on a commutative monoid object with its ring structure.

noncomputable def RS.unitHomMul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R

The convolution product of morphisms from the unit into a monoid object.

Equations

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

theorem RS.one_unitHomMul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R CategoryTheory.MonObj.one a = a

The monoid unit is a left unit for convolution.

theorem RS.unitHomMul_one {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R a CategoryTheory.MonObj.one = a

The monoid unit is a right unit for convolution.

theorem RS.unitHomMul_assoc {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] (a b c : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R (unitHomMul R a b) c = unitHomMul R a (unitHomMul R b c)

Convolution is associative.

theorem RS.unitHomMul_comm {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R a b = unitHomMul R b a

Convolution against a commutative monoid object is commutative.

theorem RS.add_unitHomMul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (a a' b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R (a + a') b = unitHomMul R a b + unitHomMul R a' b

Convolution is additive on the left.

theorem RS.unitHomMul_add {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (a b b' : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R a (b + b') = unitHomMul R a b + unitHomMul R a b'

Convolution is additive on the right.

theorem RS.zero_unitHomMul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R 0 b = 0

Convolution kills zero on the left.

theorem RS.unitHomMul_zero {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R a 0 = 0

Convolution kills zero on the right.

theorem RS.smul_unitHomMul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (r : ℂ) (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R (r • a) b = r • unitHomMul R a b

Convolution is ℂ-homogeneous on the left.

theorem RS.unitHomMul_smul {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (r : ℂ) (a b : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : unitHomMul R a (r • b) = r • unitHomMul R a b

Convolution is ℂ-homogeneous on the right.

@[reducible]

noncomputable def RS.unitHomCommRing {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] : CommRing (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)

The convolution ring: for a commutative monoid object of a braided preadditive monoidal category the morphisms from the unit form a commutative ring under convolution. Deliberately a definition rather than an instance: at R = 𝟙 the type coincides with End (𝟙_ D), whose composition monoid is a distinct (if Eckmann–Hilton-equal) multiplication.

Equations

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

@[reducible]

noncomputable def RS.unitHomAlgebra {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.IsCommMonObj R] : Algebra ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R)

The convolution ℂ-algebra: with ℂ-linear structure the convolution ring of a commutative monoid object is a commutative ℂ-algebra — the even Γ-algebra of the monoid transport once the unit of Ind C is identified with the embedded even generator (indOfUnitIso).

Equations

• RS.unitHomAlgebra R = Algebra.ofModule ⋯ ⋯