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.

References

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

Tags

bialgebra

class Bialgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends Algebra , Coalgebra : 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
• toFun : R → A
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : R), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : R) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : R) (x : A), r • x = Algebra.toRingHom r * x
• comul : A →ₗ[R] TensorProduct R A A
• counit : A →ₗ[R] R
• coassoc : ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul
• rTensor_counit_comp_comul : LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R R A) 1
• lTensor_counit_comp_comul : LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R A R).flip 1
• counit_one : Coalgebra.counit 1 = 1

  The counit on a bialgebra preserves 1.

• mul_compr₂_counit : (LinearMap.mul R A).compr₂ Coalgebra.counit = (LinearMap.mul R R).compl₁₂ Coalgebra.counit Coalgebra.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 : Coalgebra.comul 1 = 1

  The comultiplication on a bialgebra preserves 1.

• mul_compr₂_comul : (LinearMap.mul R A).compr₂ Coalgebra.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ Coalgebra.comul Coalgebra.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 multiplcation 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_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : Bialgebra R A] : Coalgebra.counit 1 = 1

The counit on a bialgebra preserves 1.

theorem Bialgebra.mul_compr₂_counit {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : Bialgebra R A] : (LinearMap.mul R A).compr₂ Coalgebra.counit = (LinearMap.mul R R).compl₁₂ Coalgebra.counit Coalgebra.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.

@[simp]

theorem Bialgebra.comul_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : Bialgebra R A] : Coalgebra.comul 1 = 1

The comultiplication on a bialgebra preserves 1.

theorem Bialgebra.mul_compr₂_comul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [self : Bialgebra R A] : (LinearMap.mul R A).compr₂ Coalgebra.comul = (LinearMap.mul R (TensorProduct R A A)).compl₁₂ Coalgebra.comul Coalgebra.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 multiplcation 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 : A) (b : A) : Coalgebra.counit (a * b) = Coalgebra.counit a * Coalgebra.counit b

@[simp]

theorem Bialgebra.comul_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) (b : A) : Coalgebra.comul (a * b) = Coalgebra.comul a * Coalgebra.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 : Coalgebra.counit 1 = 1) (counit_mul : ∀ {a b : A}, Coalgebra.counit (a * b) = Coalgebra.counit a * Coalgebra.counit b) (comul_one : Coalgebra.comul 1 = 1) (comul_mul : ∀ {a b : A}, Coalgebra.comul (a * b) = Coalgebra.comul a * Coalgebra.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

• Bialgebra.mk' R A counit_one counit_mul comul_one comul_mul = Bialgebra.mk counit_one ⋯ comul_one ⋯

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 Coalgebra.counit ⋯ ⋯

@[simp]

theorem Bialgebra.counitAlgHom_apply (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) : (Bialgebra.counitAlgHom R A) a = Coalgebra.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 Coalgebra.comul ⋯ ⋯

@[simp]

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

@[simp]

theorem Bialgebra.counit_algebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (r : R) : Coalgebra.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) : Coalgebra.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 : ℕ) : Coalgebra.counit ↑n = ↑n

@[simp]

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

@[simp]

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

@[simp]

theorem Bialgebra.comul_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) (n : ℕ) : Coalgebra.comul (a ^ n) = Coalgebra.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 = Bialgebra.mk ⋯ ⋯ ⋯ ⋯