Bialgebra structure on quotients

If I is a two-sided ideal of an R-bialgebra A whose underlying R-submodule is a coideal, then the quotient A ⧸ I inherits a bialgebra structure.

Main definitions

• Bialgebra.Quotient.counitAlgHom : the counit on A ⧸ I, as an R-algebra homomorphism.
• Bialgebra.Quotient.comulAlgHom : comultiplication on A ⧸ I as an R-algebra homomorphism.
• Bialgebra.Quotient.mkBialgHom : Ideal.Quotient.mkₐ as a bialgebra homomorphism.

Main results

• Bialgebra R (A ⧸ I) instance when [I.IsTwoSided] and [(I.restrictScalars R).IsCoideal].

def Bialgebra.Quotient.counitAlgHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : A ⧸ I →ₐ[R] R

The counit on A ⧸ I, as an R-algebra homomorphism.

Equations

• Bialgebra.Quotient.counitAlgHom I = Ideal.Quotient.liftₐ I (Bialgebra.counitAlgHom R A) ⋯

def Bialgebra.Quotient.comulAlgHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : A ⧸ I →ₐ[R] TensorProduct R (A ⧸ I) (A ⧸ I)

The comultiplication on A ⧸ I, as an R-algebra homomorphism.

Equations

• Bialgebra.Quotient.comulAlgHom I = Ideal.Quotient.liftₐ I ((Algebra.TensorProduct.map (Ideal.Quotient.mkₐ R I) (Ideal.Quotient.mkₐ R I)).comp (Bialgebra.comulAlgHom R A)) ⋯

theorem Bialgebra.Quotient.counit_comp_mkₐ {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : (counitAlgHom I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap = CoalgebraStruct.counit

theorem Bialgebra.Quotient.comul_comp_mkₐ {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : (comulAlgHom I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap = TensorProduct.map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ CoalgebraStruct.comul

@[instance_reducible]

instance Bialgebra.Quotient.instQuotientIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : Bialgebra R (A ⧸ I)

The bialgebra structure on A ⧸ I when I is a biideal.

Equations

• Bialgebra.Quotient.instQuotientIdeal I = Bialgebra.ofAlgHom (Bialgebra.Quotient.comulAlgHom I) (Bialgebra.Quotient.counitAlgHom I) ⋯ ⋯ ⋯

@[simp]

theorem Bialgebra.Quotient.counit_mk {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] (a : A) : CoalgebraStruct.counit ((Ideal.Quotient.mk I) a) = CoalgebraStruct.counit a

@[simp]

theorem Bialgebra.Quotient.comul_mk {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] (a : A) : CoalgebraStruct.comul ((Ideal.Quotient.mk I) a) = (TensorProduct.map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap) (CoalgebraStruct.comul a)

def Bialgebra.Quotient.mkBialgHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] : A →ₐc[R] A ⧸ I

Ideal.Quotient.mkₐ as a bialgebra homomorphism.

Equations

• Bialgebra.Quotient.mkBialgHom I = BialgHom.ofAlgHom (Ideal.Quotient.mkₐ R I) ⋯ ⋯

@[simp]

theorem Bialgebra.Quotient.mkBialgHom_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Bialgebra R A] (I : Ideal A) [I.IsTwoSided] [(Submodule.restrictScalars R I).IsCoideal] (a : A) : (mkBialgHom I) a = (Ideal.Quotient.mk I) a