Homomorphisms of R-bialgebras

This file defines bundled homomorphisms of R-bialgebras. We simply mimic Mathlib/Algebra/Algebra/Hom.lean.

Main definitions

• BialgHom R A B: the type of R-bialgebra morphisms from A to B.
• Bialgebra.counitBialgHom R A : A →ₐc[R] R: the counit of a bialgebra as a bialgebra homomorphism.

Notations

• A →ₐc[R] B : R-bialgebra homomorphism from A to B.

structure BialgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] extends A →ₗc[R] B, A →* B : Type (max u_2 u_3)

Given R-algebras A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-bialgebra homomorphism A →ₐc[R] B is an R-algebra map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

• toFun : A → B
• map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : R) (x : A) : self.toFun (m • x) = (RingHom.id R) m • self.toFun x
• counit_comp : CoalgebraStruct.counit ∘ₗ self.toLinearMap = CoalgebraStruct.counit
• map_comp_comul : TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ self.toLinearMap
• map_one' : self.toFun 1 = 1
• map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y

def «term_→ₐc_» : Lean.TrailingParserDescr

Given R-algebras A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-bialgebra homomorphism A →ₐc[R] B is an R-algebra map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

def «term_→ₐc[_]_» : Lean.TrailingParserDescr

Given R-algebras A, B with comultiplication maps Δ_A, Δ_B and counit maps ε_A, ε_B, an R-bialgebra homomorphism A →ₐc[R] B is an R-algebra map f such that ε_B ∘ f = ε_A and (f ⊗ f) ∘ Δ_A = Δ_B ∘ f.

class BialgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] extends CoalgHomClass F R A B, MonoidHomClass F A B : Prop

BialgHomClass F R A B asserts F is a type of bundled bialgebra homomorphisms from A to B.

• map_add (f : F) (x y : A) : f (x + y) = f x + f y
• map_smulₛₗ (f : F) (c : R) (x : A) : f (c • x) = (RingHom.id R) c • f x
• counit_comp (f : F) : CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit
• map_comp_comul (f : F) : TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f
• map_mul (f : F) (x y : A) : f (x * y) = f x * f y
• map_one (f : F) : f 1 = 1

@[instance 100]

instance BialgHomClass.toAlgHomClass {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [BialgHomClass F R A B] : AlgHomClass F R A B

def BialgHomClass.toBialgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [BialgHomClass F R A B] (f : F) : A →ₐc[R] B

Turn an element of a type F satisfying BialgHomClass F R A B into an actual BialgHom. This is declared as the default coercion from F to A →ₐc[R] B.

instance BialgHomClass.instCoeToBialgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [BialgHomClass F R A B] : CoeHead F (A →ₐc[R] B)

@[simp]

theorem BialgHomClass.counitAlgHom_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] [FunLike F A B] [BialgHomClass F R A B] (f : F) : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A

@[simp]

theorem BialgHomClass.map_comp_comulAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] [FunLike F A B] [BialgHomClass F R A B] (f : F) : (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f

instance BialgHom.funLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : FunLike (A →ₐc[R] B) A B

instance BialgHom.bialgHomClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : BialgHomClass (A →ₐc[R] B) R A B

def BialgHom.Simps.apply {R : Type u_6} {α : Type u_7} {β : Type u_8} [CommSemiring R] [Semiring α] [Algebra R α] [Semiring β] [Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β] (f : α →ₐc[R] β) : α → β

See Note [custom simps projection]

def BialgHom.ofAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) : A →ₐc[R] B

Construct a bialgebra hom from an algebra hom respecting counit and comultiplication.

@[simp]

theorem BialgHom.ofAlgHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) (a✝ : A) : (ofAlgHom f counit_comp map_comp_comul) a✝ = (↑↑f.toRingHom).toFun a✝

@[simp]

theorem BialgHom.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {F : Type u_6} [FunLike F A B] [BialgHomClass F R A B] (f : F) : ⇑↑f = ⇑f

@[simp]

theorem BialgHom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (h : f.toFun 1 = 1) (h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y) : ⇑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = ⇑f

theorem BialgHom.coe_mks {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A → B} (h₀ : ∀ (x y : A), f (x + y) = f x + f y) (h₁ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₀ }.toFun x) (h₂ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ } = CoalgebraStruct.counit) (h₃ : TensorProduct.map { toFun := f, map_add' := h₀, map_smul' := h₁ } { toFun := f, map_add' := h₀, map_smul' := h₁ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ }) (h₄ : { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1) (h₅ : ∀ (x y : A), { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y) : ⇑{ toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f

@[simp]

theorem BialgHom.coe_coalgHom_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (h : f.toFun 1 = 1) (h₁ : ∀ (x y : A), f.toFun (x * y) = f.toFun x * f.toFun y) : ↑{ toCoalgHom := f, map_one' := h, map_mul' := h₁ } = f

@[simp]

theorem BialgHom.coe_toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) : ⇑↑f = ⇑f

theorem BialgHom.toCoalgHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (a : A) : f.toCoalgHom a = f a

@[simp]

theorem BialgHom.coe_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) : ⇑↑f = ⇑f

theorem BialgHom.coe_toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) : ⇑↑f = ⇑f

theorem BialgHom.toAlgHom_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) : ↑↑f = ↑f

theorem BialgHom.coe_fn_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective DFunLike.coe

theorem BialgHom.coe_fn_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₐc[R] B} : ⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂

theorem BialgHom.coe_coalgHom_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective CoalgHomClass.toCoalgHom

theorem BialgHom.coe_algHom_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective AlgHomClass.toAlgHom

theorem BialgHom.coe_linearMap_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] : Function.Injective fun (x : A →ₐc[R] B) => ↑x

theorem BialgHom.congr_fun {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₐc[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x

theorem BialgHom.congr_arg {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₐc[R] B) {x y : A} (h : x = y) : φ x = φ y

theorem BialgHom.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₐc[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) : φ₁ = φ₂

theorem BialgHom.ext_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {φ₁ φ₂ : A →ₐc[R] B} : φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x

theorem BialgHom.ext_of_ring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] {f g : R →ₐc[R] A} (h : f 1 = g 1) : f = g

theorem BialgHom.ext_of_ring_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] {f g : R →ₐc[R] A} : f = g ↔ f 1 = g 1

@[simp]

theorem BialgHom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₐc[R] B} (h₀ : ∀ (x y : A), f (x + y) = f x + f y) (h₁ : ∀ (m : R) (x : A), { toFun := ⇑f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₀ }.toFun x) (h₂ : CoalgebraStruct.counit ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } = CoalgebraStruct.counit) (h₃ : TensorProduct.map { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ }) (h₄ : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1) (h₅ : ∀ (x y : A), { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y) : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f

def BialgHom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐc[R] B) (f' : A → B) (h : f' = ⇑f) : A →ₐc[R] B

Copy of a BialgHom with a new toFun equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem BialgHom.coe_copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem BialgHom.copy_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f) : f.copy f' h = f

def BialgHom.id (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : A →ₐc[R] A

Identity map as a BialgHom.

@[simp]

theorem BialgHom.id_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (a : A) : (BialgHom.id R A) a = a

@[simp]

theorem BialgHom.coe_id {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : ⇑(BialgHom.id R A) = id

@[simp]

theorem BialgHom.id_toCoalgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : ↑(BialgHom.id R A) = CoalgHom.id R A

@[simp]

theorem BialgHom.id_toAlgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : ↑(BialgHom.id R A) = AlgHom.id R A

def BialgHom.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) : A →ₐc[R] C

Composition of bialgebra homomorphisms.

@[simp]

theorem BialgHom.comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) (a✝ : A) : (φ₁.comp φ₂) a✝ = φ₁ (φ₂ a✝)

@[simp]

theorem BialgHom.coe_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) : ⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂

@[simp]

theorem BialgHom.comp_toCoalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) : ↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂

@[simp]

theorem BialgHom.comp_toAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] (φ₁ : B →ₐc[R] C) (φ₂ : A →ₐc[R] B) : ↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂

@[simp]

theorem BialgHom.comp_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₐc[R] B) : φ.comp (BialgHom.id R A) = φ

@[simp]

theorem BialgHom.id_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₐc[R] B) : (BialgHom.id R B).comp φ = φ

theorem BialgHom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] [Semiring D] [Algebra R D] [CoalgebraStruct R A] [CoalgebraStruct R B] [CoalgebraStruct R C] [CoalgebraStruct R D] (φ₁ : C →ₐc[R] D) (φ₂ : B →ₐc[R] C) (φ₃ : A →ₐc[R] B) : (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)

theorem BialgHom.map_smul_of_tower {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (φ : A →ₐc[R] B) {R' : Type u_6} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) : φ (r • x) = r • φ x

instance BialgHom.End {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : Monoid (A →ₐc[R] A)

theorem BialgHom.End_toSemigroup_toMul_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (φ₁ φ₂ : A →ₐc[R] A) : φ₁ * φ₂ = φ₁.comp φ₂

theorem BialgHom.End_toOne_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] : 1 = BialgHom.id R A

@[simp]

theorem BialgHom.one_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (x : A) : 1 x = x

@[simp]

theorem BialgHom.mul_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [CoalgebraStruct R A] (φ ψ : A →ₐc[R] A) (x : A) : (φ * ψ) x = φ (ψ x)

noncomputable def Bialgebra.unitBialgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] : R →ₐc[R] A

The unit of a bialgebra as a BialgHom.

noncomputable def Bialgebra.counitBialgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] : A →ₐc[R] R

The counit of a bialgebra as a BialgHom.

@[simp]

theorem Bialgebra.counitBialgHom_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (x : A) : (counitBialgHom R A) x = CoalgebraStruct.counit x

@[simp]

theorem Bialgebra.counitBialgHom_toCoalgHom {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : ↑(counitBialgHom R A) = Coalgebra.counitCoalgHom R A

instance Bialgebra.subsingleton_to_ring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : Subsingleton (A →ₐc[R] R)

theorem Bialgebra.ext_to_ring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (f g : A →ₐc[R] R) : f = g

theorem Bialgebra.ext_to_ring_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f g : A →ₐc[R] R} : f = g ↔ True