English
Let R be a commutative semiring and A an R-algebra. If we are given R-algebra homomorphisms Δ: A → A ⊗R A and ε: A → R satisfying the coalgebra axioms (coassociativity) and the compatibility conditions with the tensor product, then A can be endowed with a Bialgebra structure over R whose comultiplication is Δ and counit is ε.
Русский
Пусть R — коммутативная полускольная кольцо и A — R-алгебра. Если заданы алгебраические во множество A гомоморфизмы Δ: A → A ⊗R A и ε: A → R, удовлетворяющие коалгебраическим аксиомам (коассоциация) и совместимости с тензорным произведением, тогда A можно наделить структурой биалгебры над R, где копьютирование равно Δ, а counit равен ε.
LaTeX
$$$\\exists \\Delta : A \\to_R A \\otimes_R A\\ ,\\ \\varepsilon : A \\to_R R\\ ,\\ (\\Delta, \\varepsilon)\\text{ satisfy coassociativity and counit compatibility with tensor product, giving a } Bialgebra(R,A).$$$
Lean4
/-- 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`. -/
abbrev ofAlgHom (comul : A →ₐ[R] (A ⊗[R] A)) (counit : A →ₐ[R] R)
(h_coassoc :
(Algebra.TensorProduct.assoc R R A A A).toAlgHom.comp ((Algebra.TensorProduct.map comul (.id R A)).comp comul) =
(Algebra.TensorProduct.map (.id R A) comul).comp comul)
(h_rTensor : (Algebra.TensorProduct.map counit (.id R A)).comp comul = (Algebra.TensorProduct.lid R A).symm)
(h_lTensor : (Algebra.TensorProduct.map (.id R A) counit).comp comul = (Algebra.TensorProduct.rid R R A).symm) :
Bialgebra R A :=
letI : Coalgebra R A :=
{ comul := comul
counit := counit
coassoc := congr(($h_coassoc).toLinearMap)
rTensor_counit_comp_comul := congr(($h_rTensor).toLinearMap)
lTensor_counit_comp_comul := congr(($h_lTensor).toLinearMap) }
.mk' _ _ (map_one counit) (map_mul counit _ _) (map_one comul) (map_mul comul _ _)
