The coalgebra carried by a commutative Frobenius algebra

For a finite-free commutative Frobenius algebra, the inverse metric tensor C = F.casimir defines a comultiplication by

Δ(a) = (a ⊗ 1) C.

This file proves that multiplication and comultiplication satisfy the Frobenius relation and that Δ, together with the original Frobenius functional, gives a cocommutative coalgebra. The construction is explicit in the Frobenius object F; it is deliberately not installed as a global typeclass instance, because the same algebra may carry several Frobenius functionals.

Reading the Lean notation

• Multiplication on A ⊗[R] A is componentwise: (a ⊗ b) * (c ⊗ d) = ac ⊗ bd.
• LinearMap.mulRight R C is the linear map t ↦ t * C.
• f.comp g means first apply g, then apply f.
• The tensor associator appears explicitly in mathlib's coassociativity law.

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorEndEquiv_includeLeft_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) (t : TensorProduct R A A) (x : A) : (F.pairing.tensorEndEquiv (a ⊗ₜ[R] 1 * t)) x = (F.pairing.tensorEndEquiv t) (a * x)

Multiplying the first tensor leg by a moves the input of the associated endomorphism from x to a * x.

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorEndEquiv_includeRight_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) (t : TensorProduct R A A) (x : A) : (F.pairing.tensorEndEquiv (1 ⊗ₜ[R] a * t)) x = a * (F.pairing.tensorEndEquiv t) x

Multiplying the second tensor leg by a multiplies the output of the associated endomorphism by a.

theorem AxiomaticGW.CommFrobeniusAlgebra.includeLeft_mul_casimir_eq_includeRight_mul_casimir {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : a ⊗ₜ[R] 1 * F.casimir = 1 ⊗ₜ[R] a * F.casimir

The Casimir tensor is balanced over the algebra: (a ⊗ 1) * C = (1 ⊗ a) * C.

This tensor identity is the main computational form of invariance of the Frobenius pairing.

noncomputable def AxiomaticGW.CommFrobeniusAlgebra.comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : A →ₗ[R] TensorProduct R A A

The canonical Frobenius comultiplication Δ(a) = (a ⊗ 1) * C.

Equations

• F.comul = LinearMap.mulRight R F.casimir ∘ₗ Algebra.TensorProduct.includeLeft.toLinearMap

theorem AxiomaticGW.CommFrobeniusAlgebra.comul_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : F.comul a = a ⊗ₜ[R] 1 * F.casimir

Evaluation formula using the first leg of the Casimir tensor.

theorem AxiomaticGW.CommFrobeniusAlgebra.comul_apply_right {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : F.comul a = 1 ⊗ₜ[R] a * F.casimir

Equivalent evaluation formula using the second leg.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.comul_one {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : F.comul 1 = F.casimir

The Casimir tensor is the comultiplication of the algebra unit.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorEndEquiv_comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a x : A) : (F.pairing.tensorEndEquiv (F.comul a)) x = a * x

Contracting Δ(a) with the metric gives multiplication by a.

theorem AxiomaticGW.CommFrobeniusAlgebra.comul_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a b : A) : F.comul (a * b) = a ⊗ₜ[R] 1 * F.comul b

Left-linearity of comultiplication, one half of the Frobenius relation.

theorem AxiomaticGW.CommFrobeniusAlgebra.comul_mul_right {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a b : A) : F.comul (a * b) = 1 ⊗ₜ[R] b * F.comul a

Right-linearity of comultiplication, the other half of the Frobenius relation.

theorem AxiomaticGW.CommFrobeniusAlgebra.comm_mul_tmul_left {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (a : A) (t : TensorProduct R A A) : (TensorProduct.comm R A A) (a ⊗ₜ[R] 1 * t) = 1 ⊗ₜ[R] a * (TensorProduct.comm R A A) t

Swapping the tensor factors in a product swaps each factor.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.comm_comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : (TensorProduct.comm R A A) (F.comul a) = F.comul a

The canonical Frobenius comultiplication is cocommutative.

theorem AxiomaticGW.CommFrobeniusAlgebra.lid_counit_rTensor {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (t : TensorProduct R A A) : (TensorProduct.lid R A) ((LinearMap.rTensor A F.counit) t) = (F.pairing.tensorEndEquiv t) 1

Applying the left tensor unitor after contracting the first leg with the counit is the same as contracting the tensor against 1 via the metric.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.rTensor_counit_comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : (LinearMap.rTensor A F.counit) (F.comul a) = 1 ⊗ₜ[R] a

The first counit law, written in mathlib's explicit-unitor convention.

theorem AxiomaticGW.CommFrobeniusAlgebra.rid_counit_lTensor {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (t : TensorProduct R A A) : (TensorProduct.rid R A) ((LinearMap.lTensor A F.counit) t) = (F.pairing.tensorEndEquiv ((TensorProduct.comm R A A) t)) 1

Applying the right tensor unitor after contracting the second leg with the counit can be computed by first swapping the tensor.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.lTensor_counit_comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : (LinearMap.lTensor A F.counit) (F.comul a) = a ⊗ₜ[R] 1

The second counit law.

theorem AxiomaticGW.CommFrobeniusAlgebra.mul'_includeLeft_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (a : A) (t : TensorProduct R A A) : (LinearMap.mul' R A) (a ⊗ₜ[R] 1 * t) = a * (LinearMap.mul' R A) t

Multiplying a fixed element into the first tensor leg commutes with multiplying the two tensor legs together.

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.mul'_comul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : (LinearMap.mul' R A) (F.comul a) = a * F.handleElement

Multiplication after comultiplication is multiplication by the handle element: μ(Δ(a)) = a * E.

Coassociativity

To compare tensors with three factors, we use the same perfect pairing to turn the first tensor factor into the input of a linear map. This avoids a basis calculation: the resulting map is an equivalence, so equality after contraction proves equality of the original tensors.

noncomputable def AxiomaticGW.CommFrobeniusAlgebra.tensorModuleHomEquiv {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (W : Type u_3) [AddCommGroup W] [Module R W] : TensorProduct R A W ≃ₗ[R] A →ₗ[R] W

Contract the first factor of A ⊗ W, for an arbitrary target module W. The earlier tensorEndEquiv is the special case W = A.

Equations

• F.tensorModuleHomEquiv W = (TensorProduct.congr F.pairing.toDual (LinearEquiv.refl R W)).trans (dualTensorHomEquiv R A W)

@[simp]

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorModuleHomEquiv_tmul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) {W : Type u_3} [AddCommGroup W] [Module R W] (a x : A) (w : W) : ((F.tensorModuleHomEquiv W) (a ⊗ₜ[R] w)) x = (F.pairing.form a) x • w

Evaluation of tensorModuleHomEquiv on a pure tensor.

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorModuleHomEquiv_assoc_tmul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (s : TensorProduct R A A) (q x : A) : ((F.tensorModuleHomEquiv (TensorProduct R A A)) ((TensorProduct.assoc R A A A) (s ⊗ₜ[R] q))) x = (F.pairing.tensorEndEquiv s) x ⊗ₜ[R] q

Contracting the first leg after reassociating (A ⊗ A) ⊗ A contracts the first leg of the inner two-tensor.

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorModuleHomEquiv_assoc_comul_rTensor {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (t : TensorProduct R A A) (x : A) : ((F.tensorModuleHomEquiv (TensorProduct R A A)) ((TensorProduct.assoc R A A A) ((LinearMap.rTensor A F.comul) t))) x = x ⊗ₜ[R] 1 * t

After applying Δ to the first tensor factor, contraction turns it into multiplication by the contracted vector.

theorem AxiomaticGW.CommFrobeniusAlgebra.tensorModuleHomEquiv_comul_lTensor {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (t : TensorProduct R A A) (x : A) : ((F.tensorModuleHomEquiv (TensorProduct R A A)) ((LinearMap.lTensor A F.comul) t)) x = F.comul ((F.pairing.tensorEndEquiv t) x)

After applying Δ to the second tensor factor, contraction may be moved through Δ by linearity.

theorem AxiomaticGW.CommFrobeniusAlgebra.coassoc_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) (a : A) : (TensorProduct.assoc R A A A) ((LinearMap.rTensor A F.comul) (F.comul a)) = (LinearMap.lTensor A F.comul) (F.comul a)

Pointwise coassociativity of the canonical comultiplication.

theorem AxiomaticGW.CommFrobeniusAlgebra.coassoc {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A F.comul ∘ₗ F.comul = LinearMap.lTensor A F.comul ∘ₗ F.comul

Coassociativity as an equality of linear maps, in exactly the form required by mathlib's Coalgebra structure.

Interoperability with mathlib's coalgebra API

@[reducible]

noncomputable def AxiomaticGW.CommFrobeniusAlgebra.toCoalgebraStruct {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : CoalgebraStruct R A

The comultiplication and original Frobenius functional, bundled as mathlib's preliminary CoalgebraStruct.

Equations

• F.toCoalgebraStruct = { comul := F.comul, counit := F.counit }

@[reducible]

noncomputable def AxiomaticGW.CommFrobeniusAlgebra.toCoalgebra {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : Coalgebra R A

A finite-free commutative Frobenius algebra canonically determines a coalgebra.

This is an explicit definition rather than a global instance. To use mathlib's coalgebra notation and lemmas locally, write

letI : Coalgebra R A := F.toCoalgebra

Equations

• F.toCoalgebra = { comul := F.comul, counit := F.counit, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

theorem AxiomaticGW.CommFrobeniusAlgebra.toIsCocomm {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Free R A] [Module.Finite R A] (F : CommFrobeniusAlgebra R A) : Coalgebra.IsCocomm R A

The coalgebra obtained from a commutative Frobenius algebra is cocommutative.

This declaration is designed for local use immediately after installing F.toCoalgebra.