The four-block Γ-algebra of a commutative monoid at an odd line

RS.SuperRealize supplies the even half of the §4 monoid transport: the convolution product unitHomMul making 𝟙_ D ⟶ R a commutative ℂ-algebra for a commutative monoid object R. This file supplies the full super-commutative algebra. Fix an odd line o : D: an object with a chosen trivialization ho : o ⊗ o ≅ 𝟙_ D on which the braiding acts by -1. The four graded blocks of R-valued points are

• even = 𝟙_ D ⟶ R and odd = o ⟶ R — the o ⟶ R form is chosen over 𝟙_ D ⟶ o ⊗ R because the odd-odd product then pairs the two source copies of o directly through ho;
• EE = convolution through (λ_ (𝟙_ D)).inv (definitionally the existing unitHomMul);
• EO = convolution through (λ_ o).inv;
• OE = convolution through (ρ_ o).inv;
• OO = convolution through ho.inv.

All four are instances of a single construction, convolution along a prefix: convAlong R p f g = p ≫ (f ⊗ₘ g) ≫ μ for a chosen p : A ⟶ X ⊗ Y. Associativity holds once and for all (convAlong_assoc) given a single coherence identity relating the four prefixes involved; the eight parity associativities are the eight instantiations. Seven of the eight coherence residues are consequences of monoidal coherence and the naturality of the unitors; the eighth — the odd-odd-odd pattern — genuinely compares the two ways of trivializing one factor of o ⊗ o ⊗ o through ho and is not a formal consequence of the data (ho, hβ). It is stated as the hypothesis hα of superGammaAlgebra; it holds in super vector spaces (both sides are x ↦ e ⊗ e ⊗ x-type maps for a basis vector e of the odd line) and more generally whenever ho is a coherent self-duality.

Commutativity likewise holds once (convAlong_braid, from the commutativity of μ and the naturality of the braiding); the even-even and even-odd patterns follow from the unit braiding identities, and the odd-odd pattern picks up the Koszul sign from hβ. The package superGammaAlgebra assembles the blocks into an RS.SuperCommAlgebra, feeding the odd-nil quotient theory of RS.SuperRealize.

Convolution along a prefix

def RS.convAlong {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f : X ⟶ R) (g : Y ⟶ R) : A ⟶ R

Convolution along a prefix: for a monoid object R and a chosen morphism p : A ⟶ X ⊗ Y, the pairing sending f : X ⟶ R and g : Y ⟶ R to p ≫ (f ⊗ₘ g) ≫ μ : A ⟶ R. All four graded multiplication blocks of the Γ-algebra at an odd line are instances, at the prefixes (λ_ (𝟙_ D)).inv, (λ_ o).inv, (ρ_ o).inv and ho.inv.

Equations

• RS.convAlong R p f g = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) CategoryTheory.MonObj.mul)

theorem RS.convAlong_one_left {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {Z : D} (x : Z ⟶ R) : convAlong R (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv CategoryTheory.MonObj.one x = x

The monoid unit is a left unit for convolution along a left unitor prefix.

theorem RS.convAlong_assoc {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] {B A A' X Y Z : D} (q : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A Z) (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (q' : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X A') (p' : A' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) (hpq : CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight p Z) (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) = CategoryTheory.CategoryStruct.comp q' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X p')) (f : X ⟶ R) (g : Y ⟶ R) (h : Z ⟶ R) : convAlong R q (convAlong R p f g) h = convAlong R q' f (convAlong R p' g h)

Generic associativity of prefixed convolution. Given inner and outer prefixes on each side whose two composites into X ⊗ Y ⊗ Z agree (hpq), the two iterated convolutions agree. The eight parity associativities of the Γ-algebra are the eight instantiations, with hpq a coherence residue in each case.

theorem RS.convAlong_braid {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f : X ⟶ R) (g : Y ⟶ R) : convAlong R p f g = convAlong R (CategoryTheory.CategoryStruct.comp p (β_ X Y).hom) g f

Generic commutativity of prefixed convolution against a commutative monoid object: exchanging the two arguments costs composing the prefix with the braiding. The Koszul signs of the Γ-algebra arise from evaluating the braiding on the prefixes.

theorem RS.convAlong_ee_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) : convAlong R (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv a b = convAlong R (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv b a

Even-even commutativity: at the unit prefix the braiding correction collapses through the unit braiding identities.

theorem RS.convAlong_eo_comm {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] {o : D} (a : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) (x : o ⟶ R) : convAlong R (CategoryTheory.MonoidalCategoryStruct.leftUnitor o).inv a x = convAlong R (CategoryTheory.MonoidalCategoryStruct.rightUnitor o).inv x a

Even-odd commutativity: the braiding against the unit turns the left unitor prefix into the right unitor prefix, with no sign.

Bilinearity

theorem RS.convAlong_add_left {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f f' : X ⟶ R) (g : Y ⟶ R) : convAlong R p (f + f') g = convAlong R p f g + convAlong R p f' g

Prefixed convolution is additive in the left argument.

theorem RS.convAlong_add_right {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f : X ⟶ R) (g g' : Y ⟶ R) : convAlong R p f (g + g') = convAlong R p f g + convAlong R p f g'

Prefixed convolution is additive in the right argument.

theorem RS.convAlong_oo_comm {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] {o : D} (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (hβ : (β_ o o).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)) (x y : o ⟶ R) : convAlong R ho.inv x y = -convAlong R ho.inv y x

Odd-odd anticommutativity. At a trivialization prefix ho.inv on whose source the braiding acts by -1, exchanging the arguments of prefixed convolution costs the Koszul sign.

theorem RS.convAlong_smul_left {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (r : ℂ) (f : X ⟶ R) (g : Y ⟶ R) : convAlong R p (r • f) g = r • convAlong R p f g

Prefixed convolution is ℂ-homogeneous in the left argument.

theorem RS.convAlong_smul_right {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (r : ℂ) (f : X ⟶ R) (g : Y ⟶ R) : convAlong R p f (r • g) = r • convAlong R p f g

Prefixed convolution is ℂ-homogeneous in the right argument.

def RS.convAlongHom {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) : (X ⟶ R) →ₗ[ℂ] (Y ⟶ R) →ₗ[ℂ] A ⟶ R

Prefixed convolution packaged as a ℂ-bilinear map on hom ℂ-modules.

Equations

• RS.convAlongHom R p = LinearMap.mk₂ ℂ (RS.convAlong R p) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.convAlongHom_apply {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {A X Y : D} (p : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (f : X ⟶ R) (g : Y ⟶ R) : ((convAlongHom R p) f) g = convAlong R p f g

Application of the packaged bilinear map is prefixed convolution.

The Γ-algebra at an odd line

def RS.superGammaAlgebra {D : Type u} [CategoryTheory.Category.{u', u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (o : D) (ho : CategoryTheory.MonoidalCategoryStruct.tensorObj o o ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (hβ : (β_ o o).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj o o)) (hα : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor o).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ho.inv o) (CategoryTheory.MonoidalCategoryStruct.associator o o o).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor o).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft o ho.inv)) : SuperCommAlgebra

The four-block Γ-algebra of a commutative monoid object at an odd line. For a commutative monoid object R of a braided ℂ-linear monoidal category and an odd line o — an object with a trivialization ho : o ⊗ o ≅ 𝟙_ D on which the braiding acts by -1 (hβ) and which is associativity-coherent (hα: the two insertions of ho.inv into o agree through the associator) — the morphisms 𝟙_ D ⟶ R and o ⟶ R form a super-commutative ℂ-algebra under prefixed convolution. The even block is the convolution algebra of RS.SuperRealize; the odd-odd block pairs the sources through ho and anticommutes by hβ.

The hypothesis hα is not a formal consequence of (ho, hβ): it pins down the compatibility of the chosen trivialization with the associator, and holds for the standard odd line of super vector spaces (hence in Ind SmallSuperVect).

Equations

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

Instantiation notes: D := Ind SmallSuperVect

Applying superGammaAlgebra over the intended ind-completion requires the following instance stack on Ind SmallSuperVect (not assembled here; recorded for the instantiation lane):

• Preadditive (Ind SmallSuperVect) and the ℂ-linear structure — the tree's route is through RS.ScalarLinear (linearity of a preadditive category over the scalars of its unit endomorphisms) rather than a direct Day-convolution transport;
• the monoidal structure and its braiding on the ind-completion — RS.IndMonoidal / RS.ScalarBraiding layer, with MonoidalPreadditive and MonoidalLinear ℂ verified against the transported tensor;
• the odd line: o := indOf sOdd, with ho induced by the isomorphism sOdd ⊗ sOdd ≅ sEven ≅ 𝟙 of RS.SuperSmall (sEvenIso after the embedding), hβ from the sign of the super braiding on the odd generator, and hα by evaluating both sides on the one-dimensional odd line;
• the monoid object R supplied by the §4 descent, with IsCommMonObj R from commutativity of the transported multiplication.