Bialgebras

In this file we define Bialgebras.

Main definitions

• Bialgebra R A: the structure of a bialgebra on the R-algebra A;
• CommSemiring.toBialgebra: a commutative semiring is a bialgebra over itself.

Implementation notes

Rather than the "obvious" axiom ∀ a b, counit (a * b) = counit a * counit b, the far more convoluted mul_compr₂_counit is used as a structure field; this says that the corresponding two maps A →ₗ[R] A →ₗ[R] R are equal; a similar trick is used for comultiplication as well. An alternative constructor Bialgebra.mk' is provided with the more easily-readable axioms. The argument for using the more convoluted axioms is that in practice there is evidence that they will be easier to prove (especially when dealing with things like tensor products of bialgebras). This does make the definition more surprising to mathematicians, however mathlib is no stranger to definitions which are surprising to mathematicians -- see for example its definition of a group. Note that this design decision is also compatible with that of Coalgebra. The lengthy docstring for these convoluted fields attempts to explain what is going on.

The constructor Bialgebra.ofAlgHom is dual to the default constructor: For R is a commutative semiring and A a R-algebra, it consumes the counit and comultiplication as algebra homomorphisms that satisfy the coalgebra axioms to define a bialgebra structure on A.

References

• https://en.wikipedia.org/wiki/Bialgebra

Tags

bialgebra

class Bialgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends Algebra R A, Coalgebra R A : Type (max u v)

A bialgebra over a commutative (semi)ring R is both an algebra and a coalgebra over R, such that the counit and comultiplication are algebra morphisms.

• smul : R → A → A
• algebraMap : R →+* A
• commutes' (r : R) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : R) (x : A) : r • x = Algebra.algebraMap r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul = LinearMap.lTensor A comul ∘ₗ comul
• rTensor_counit_comp_comul : LinearMap.rTensor A counit ∘ₗ comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A counit ∘ₗ comul = (TensorProduct.mk R A R).flip 1
• counit_one : CoalgebraStruct.counit 1 = 1

  The counit on a bialgebra preserves 1.

• mul_compr₂_counit : (LinearMap.mul R A).compr₂ CoalgebraStruct.counit = (LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit

  The counit on a bialgebra preserves multiplication. Note that this is written in a rather obscure way: it says that two bilinear maps A →ₗ[R] A →ₗ[R] are equal. The two corresponding equal linear maps A ⊗[R] A →ₗ[R] are the following: the first factors through A and is multiplication on A followed by counit. The second factors through R ⊗[R] R, and is counit ⊗ counit followed by multiplication on R.

  See Bialgebra.mk' for a constructor for bialgebras which uses the more familiar but mathematically equivalent counit (a * b) = counit a * counit b.

• comul_one : CoalgebraStruct.comul 1 = 1

  The comultiplication on a bialgebra preserves 1.

• mul_compr₂_comul : (LinearMap.mul R A).compr₂ CoalgebraStruct.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul

  The comultiplication on a bialgebra preserves multiplication. This is written in a rather obscure way: it says that two bilinear maps A →ₗ[R] A →ₗ[R] (A ⊗[R] A) are equal. The corresponding equal linear maps A ⊗[R] A →ₗ[R] A ⊗[R] A are firstly multiplication followed by comul, and secondly comul ⊗ comul followed by multiplication on A ⊗[R] A.

  See Bialgebra.mk' for a constructor for bialgebras which uses the more familiar but mathematically equivalent comul (a * b) = comul a * comul b.

@[simp]

theorem Bialgebra.counit_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a b : A) : CoalgebraStruct.counit (a * b) = CoalgebraStruct.counit a * CoalgebraStruct.counit b

@[simp]

theorem Bialgebra.comul_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a b : A) : CoalgebraStruct.comul (a * b) = CoalgebraStruct.comul a * CoalgebraStruct.comul b

noncomputable def Bialgebra.mk' (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] [C : Coalgebra R A] (counit_one : CoalgebraStruct.counit 1 = 1) (counit_mul : ∀ {a b : A}, CoalgebraStruct.counit (a * b) = CoalgebraStruct.counit a * CoalgebraStruct.counit b) (comul_one : CoalgebraStruct.comul 1 = 1) (comul_mul : ∀ {a b : A}, CoalgebraStruct.comul (a * b) = CoalgebraStruct.comul a * CoalgebraStruct.comul b) : Bialgebra R A

If R is a field (or even a commutative semiring) and A is an R-algebra with a coalgebra structure, then Bialgebra.mk' consumes proofs that the counit and comultiplication preserve the identity and multiplication, and produces a bialgebra structure on A.

Equations

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

noncomputable def Bialgebra.counitAlgHom (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] : A →ₐ[R] R

counitAlgHom R A is the counit of the R-bialgebra A, as an R-algebra map.

Equations

• Bialgebra.counitAlgHom R A = AlgHom.ofLinearMap CoalgebraStruct.counit ⋯ ⋯

@[simp]

theorem Bialgebra.counitAlgHom_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) : (counitAlgHom R A) a = CoalgebraStruct.counit a

noncomputable def Bialgebra.comulAlgHom (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] : A →ₐ[R] TensorProduct R A A

comulAlgHom R A is the comultiplication of the R-bialgebra A, as an R-algebra map.

Equations

• Bialgebra.comulAlgHom R A = AlgHom.ofLinearMap CoalgebraStruct.comul ⋯ ⋯

@[simp]

theorem Bialgebra.comulAlgHom_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) : (comulAlgHom R A) a = CoalgebraStruct.comul a

@[simp]

theorem Bialgebra.counit_algebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (r : R) : CoalgebraStruct.counit ((algebraMap R A) r) = r

@[simp]

theorem Bialgebra.comul_algebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (r : R) : CoalgebraStruct.comul ((algebraMap R A) r) = (algebraMap R (TensorProduct R A A)) r

@[simp]

theorem Bialgebra.counit_natCast {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (n : ℕ) : CoalgebraStruct.counit ↑n = ↑n

@[simp]

theorem Bialgebra.comul_natCast {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (n : ℕ) : CoalgebraStruct.comul ↑n = ↑n

@[simp]

theorem Bialgebra.counit_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) (n : ℕ) : CoalgebraStruct.counit (a ^ n) = CoalgebraStruct.counit a ^ n

@[simp]

theorem Bialgebra.comul_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) (n : ℕ) : CoalgebraStruct.comul (a ^ n) = CoalgebraStruct.comul a ^ n

noncomputable instance CommSemiring.toBialgebra (R : Type u) [CommSemiring R] : Bialgebra R R

Every commutative (semi)ring is a bialgebra over itself

Equations

• CommSemiring.toBialgebra R = { toAlgebra := Algebra.id R, toCoalgebra := CommSemiring.toCoalgebra R, counit_one := ⋯, mul_compr₂_counit := ⋯, comul_one := ⋯, mul_compr₂_comul := ⋯ }

@[reducible, inline]

noncomputable abbrev Bialgebra.ofAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (comul : A →ₐ[R] TensorProduct R A A) (counit : A →ₐ[R] R) (h_coassoc : (↑(Algebra.TensorProduct.assoc R A A A)).comp ((Algebra.TensorProduct.map comul (AlgHom.id R A)).comp comul) = (Algebra.TensorProduct.map (AlgHom.id R A) comul).comp comul) (h_rTensor : (Algebra.TensorProduct.map counit (AlgHom.id R A)).comp comul = ↑(Algebra.TensorProduct.lid R A).symm) (h_lTensor : (Algebra.TensorProduct.map (AlgHom.id R A) counit).comp comul = ↑(Algebra.TensorProduct.rid R R A).symm) : Bialgebra R A

If R is a commutative semiring and A is an R-algebra, then Bialgebra.ofAlgHom consumes the counit and comultiplication as algebra homomorphisms that satisfy the coalgebra axioms to define a bialgebra structure on A.

Equations

• Bialgebra.ofAlgHom comul counit h_coassoc h_rTensor h_lTensor = Bialgebra.mk' R A ⋯ ⋯ ⋯ ⋯