The Γ-algebra of a commutative monoid object

A commutative monoid object R of a symmetric ℂ-linear monoidal category D equipped with an odd line L realizes as a super-commutative ℂ-algebra (RS.SuperCommAlgebra): the even part is 𝟙_ D ⟶ R, the odd part is L.obj ⟶ R, and the four graded multiplication blocks are the convolution product of the monoid sandwiched between the coherence isomorphisms that identify the sources.

Everything rests on one ungraded operation, RS.gmul: the convolution (a ⊗ₘ b) ≫ μ of two morphisms into R at arbitrary sources. Its three structural laws — associativity up to the associator (RS.gmul_assoc), the two unit laws (RS.gmul_one_left, RS.gmul_one_right) and commutativity up to the braiding (RS.gmul_comm) — hold once and for all, and each of the thirteen axioms of RS.SuperCommAlgebra is one of them conjugated by coherence isomorphisms. The Koszul sign is the sole place where the odd line enters: RS.gmul_comm produces the self-braiding of L.obj, which RS.OddLine.braid_neg identifies with -𝟙.

The odd-odd-odd associativity is the one axiom not implied by coherence alone: it is the first triangle identity of the self-duality of the odd line, RS.OddLine.evaluation_coevaluation.

Ungraded convolution

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

The convolution product of two morphisms into a monoid object, taken at arbitrary sources: tensor the two morphisms and multiply.

Equations

• RS.gmul a b = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) CategoryTheory.MonObj.mul

theorem RS.gmul_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {X Y : D} (a : X ⟶ R) (b : Y ⟶ R) : gmul a b = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) CategoryTheory.MonObj.mul

Convolution unfolded.

theorem RS.comp_gmul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {W X Y : D} (f : W ⟶ X) (a : X ⟶ R) (b : Y ⟶ R) : gmul (CategoryTheory.CategoryStruct.comp f a) b = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) (gmul a b)

Reindexing the left source of a convolution.

theorem RS.gmul_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {X Y Z : D} (a : X ⟶ R) (g : Z ⟶ Y) (b : Y ⟶ R) : gmul a (CategoryTheory.CategoryStruct.comp g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) (gmul a b)

Reindexing the right source of a convolution.

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

Convolution is associative, up to the associator of the three sources.

theorem RS.gmul_one_left {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {Y : D} (b : Y ⟶ R) : gmul CategoryTheory.MonObj.one b = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom b

The monoid unit is a left unit for convolution.

theorem RS.gmul_one_right {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] {X : D} (a : X ⟶ R) : gmul a CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom a

The monoid unit is a right unit for convolution.

theorem RS.gmul_comm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj R] {X Y : D} (a : X ⟶ R) (b : Y ⟶ R) : gmul a b = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (gmul b a)

Convolution against a commutative monoid object is commutative, up to the braiding of the two sources.

theorem RS.add_gmul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {X Y : D} (a a' : X ⟶ R) (b : Y ⟶ R) : gmul (a + a') b = gmul a b + gmul a' b

Convolution is additive in its left argument.

theorem RS.gmul_add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {X Y : D} (a : X ⟶ R) (b b' : Y ⟶ R) : gmul a (b + b') = gmul a b + gmul a b'

Convolution is additive in its right argument.

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

Convolution is ℂ-homogeneous in its left argument.

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

Convolution is ℂ-homogeneous in its right argument.

The bundled bilinear convolution

noncomputable def RS.gmulLin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [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 ⟶ R) →ₗ[ℂ] W ⟶ R

The convolution product 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 multiplication blocks of RS.gammaAlgebra are the four instances of this construction.

Equations

• RS.gmulLin s = LinearMap.mk₂ ℂ (fun (a : X ⟶ R) (b : Y ⟶ R) => CategoryTheory.CategoryStruct.comp s (RS.gmul a b)) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RS.gmulLin_apply {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [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) (b : Y ⟶ R) : ((gmulLin s) a) b = CategoryTheory.CategoryStruct.comp s (gmul a b)

theorem RS.gmulLin_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {R : D} [CategoryTheory.MonObj R] [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) (c : Z ⟶ R) : ((gmulLin s₁) (((gmulLin s₂) a) b)) c = ((gmulLin s₃) a) (((gmulLin s₄) b) c)

The transported associativity law: given a coherence identity between the two ways of reassociating the chosen sources, the two bracketings of a triple convolution agree.

The super-commutative algebra of a commutative monoid

noncomputable def RS.gammaAlgebra (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] : SuperCommAlgebra

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

The four blocks are the convolution product conjugated by the coherence isomorphisms that identify each source with a tensor product of the two sources involved: 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. The Koszul sign of comm_oo is exactly RS.OddLine.braid_neg.

Equations

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