Hopf algebra structure on quotients by Hopf ideals

A Hopf ideal of an R-Hopf algebra A is a biideal stable under the antipode. The quotient by a Hopf ideal inherits a Hopf algebra structure.

Main definitions

• Ideal.IsHopfIdeal R I : I is a coideal (as an R-submodule) stable under the antipode.

Main results

• HopfAlgebra R (A ⧸ I) instance when [I.IsTwoSided] and [I.IsHopfIdeal R].

class Ideal.IsHopfIdeal (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebraStruct R A] (I : Ideal A) extends (Submodule.restrictScalars R I).IsCoideal : Prop

An ideal whose underlying R-submodule is a coideal and which is stable under the antipode (S(I) ⊆ I). Together with I.IsTwoSided, this makes I a Hopf ideal.

• counit_eq_zero ⦃x : A⦄ : x ∈ restrictScalars R I → CoalgebraStruct.counit x = 0
• map_mkQ_comul_eq_zero ⦃x : A⦄ : x ∈ restrictScalars R I → (TensorProduct.map (restrictScalars R I).mkQ (restrictScalars R I).mkQ) (CoalgebraStruct.comul x) = 0
• antipode_mem ⦃x : A⦄ : x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I

theorem Ideal.isHopfIdeal_iff (R : Type u_1) {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebraStruct R A] (I : Ideal A) : IsHopfIdeal R I ↔ (Submodule.restrictScalars R I).IsCoideal ∧ ∀ ⦃x : A⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I

@[instance_reducible]

instance HopfAlgebra.Quotient.instHopfAlgebraStructQuotientIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebraStruct R A] (I : Ideal A) [I.IsTwoSided] [Ideal.IsHopfIdeal R I] : HopfAlgebraStruct R (A ⧸ I)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HopfAlgebra.Quotient.antipode_mk {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebraStruct R A] (I : Ideal A) [I.IsTwoSided] [Ideal.IsHopfIdeal R I] (a : A) : (antipode R) ((Ideal.Quotient.mk I) a) = (Ideal.Quotient.mk I) ((antipode R) a)

@[deprecated HopfAlgebra.Quotient.antipode_mk (since := "2026-09-19")]

theorem HopfAlgebra.Quotient.antipode_comp_mkₐ {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebraStruct R A] (I : Ideal A) [I.IsTwoSided] [Ideal.IsHopfIdeal R I] : antipode R ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap = (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ antipode R

@[instance_reducible]

noncomputable instance HopfAlgebra.Quotient.instQuotientIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [HopfAlgebra R A] (I : Ideal A) [I.IsTwoSided] [Ideal.IsHopfIdeal R I] : HopfAlgebra R (A ⧸ I)

Equations

• HopfAlgebra.Quotient.instQuotientIdeal I = HopfAlgebra.ofSurjective (Bialgebra.Quotient.mkBialgHom I) ⋯ ⋯