Basic facts about bialgebra morphisms #
BialgHom.id_toRingHom identifies the direct ring-homomorphism coercion of the identity.
It complements Mathlib's BialgHom.id_toAlgHom, which concerns the algebra-homomorphism
coercion.
The ordinary kernel of a bialgebra morphism is killed by the counit, and its comultiplication lies in the kernel of the tensor-square map. These facts require only the algebra and coalgebra structures used to define a bialgebra morphism, without an antipode.
@[simp]
theorem
BialgHom.id_toRingHom
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
[CoalgebraStruct R A]
:
The ring homomorphism underlying the identity bialgebra morphism is the identity.
theorem
BialgHom.comul_mem_ker_tensorProduct_map
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[CoalgebraStruct R A]
{B : Type u_3}
[Semiring B]
[Algebra R B]
[CoalgebraStruct R B]
(f : A →ₐc[R] B)
{x : A}
(hx : x ∈ RingHom.ker ↑f)
:
The tensor-square map sends the comultiplication of an element in the kernel of a bialgebra morphism to zero.
theorem
BialgHom.counit_eq_zero_of_mem_ker
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[CoalgebraStruct R A]
{B : Type u_3}
[Semiring B]
[Algebra R B]
[CoalgebraStruct R B]
(f : A →ₐc[R] B)
{x : A}
(hx : x ∈ RingHom.ker ↑f)
:
The counit vanishes on the ordinary kernel of a bialgebra morphism.