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.ofSurjective : the Hopf algebra axioms transfer along a surjective bialgebra homomorphism intertwining the antipodes.
• HopfAlgebra R (A ⧸ I) instance when [I.IsTwoSided] and [I.IsHopfIdeal R].

theorem LinearMap.algHom_comp_convOne {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebraStruct R B] (g : A →ₐ[R] B) : g.toLinearMap ∘ₗ WithConv.ofConv 1 = WithConv.ofConv 1

Post-composition by an algebra homomorphism preserves the convolution unit.

theorem LinearMap.convOne_comp_coalgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebraStruct R B] (g : A →ₗc[R] B) : WithConv.ofConv 1 ∘ₗ g.toLinearMap = WithConv.ofConv 1

Pre-composition by a coalgebra homomorphism preserves the convolution unit.

@[reducible, inline]

noncomputable abbrev HopfAlgebra.ofSurjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [HopfAlgebra R A] [HopfAlgebraStruct R B] (f : A →ₐc[R] B) (hf : Function.Surjective ⇑f) (hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R) : HopfAlgebra R B

Transfer the Hopf algebra axioms along a surjective bialgebra homomorphism intertwining the antipodes.

Equations

• HopfAlgebra.ofSurjective f hf hS = HopfAlgebra.ofConvInverse (HopfAlgebraStruct.antipode 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

@[implicit_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)

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

@[implicit_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) ⋯ ⋯