The quotient of an affine group by a normal subgroup

Let H be a commutative Hopf algebra over R, representing the affine group G = Spec H, and let I be a normal Hopf ideal, cutting out a normal closed subgroup N. The coinvariants H^{co H/I} of I are the functions on G invariant under right translation by N. When H, the coinvariants, and H ⧸ H^{co H/I} are flat (for instance over a field), the coinvariants form a Hopf subalgebra of H. This file packages them as a commutative Hopf algebra, the coordinate ring of the quotient G ⧸ N, together with the coordinate map of the projection G → G ⧸ N.

The projection is the quotient of G by N in the category of affine groups: N lies in its kernel, and every homomorphism out of G whose kernel contains N factors uniquely through it. In coordinates, a morphism f : K ⟶ H of commutative Hopf algebras has image in the coinvariants exactly when its kernel Hopf ideal is contained in I; this criterion needs neither flatness nor normality.

Over a field, the projection is moreover faithfully flat with kernel exactly N, so that G ⧸ N represents the fppf quotient sheaf TauCeti.CommHopfAlgCat.fppfQuotientSheaf (Takeuchi's theorem). Those two facts are not proved here: only the inclusion of N in the kernel is.

Main declarations

• TauCeti.HopfIdeal.forall_hom_mem_coinvariants_iff: a morphism lands in the coinvariants of I exactly when its kernel Hopf ideal is contained in I.
• TauCeti.HopfIdeal.IsNormal.isHopfSubalgebra_coinvariants: the coinvariants of a normal Hopf ideal form a Hopf subalgebra.
• TauCeti.CommHopfAlgCat.coinvariants: the coordinate Hopf algebra of G ⧸ N.
• TauCeti.CommHopfAlgCat.coinvariantsι: the coordinate map of the projection G → G ⧸ N.
• TauCeti.CommHopfAlgCat.kernelHopfIdeal_coinvariantsι_le: N lies in the kernel of the projection.
• TauCeti.CommHopfAlgCat.liftCoinvariants and TauCeti.CommHopfAlgCat.exists_comp_coinvariantsι_iff: the universal property of the projection.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§15.1 and 16.3.
• M. Takeuchi, A correspondence between Hopf ideals and sub-Hopf algebras, Manuscripta Math. 7 (1972), 251–270.
• J. S. Milne, Algebraic Groups (2017), §5.c.

theorem TauCeti.HopfIdeal.forall_hom_mem_coinvariants_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} (f : K ⟶ H) : (∀ (x : ↑K), (CommHopfAlgCat.Hom.hom f) x ∈ I.coinvariants) ↔ CommHopfAlgCat.kernelHopfIdeal f ≤ I

Coinvariants and kernels. A morphism f : K ⟶ H of commutative Hopf algebras takes values in the coinvariants of I exactly when its kernel Hopf ideal is contained in I. Geometrically, the pullbacks of functions along a homomorphism φ out of G are right invariant under the subgroup N cut out by I exactly when N lies in the kernel of φ.

theorem TauCeti.HopfIdeal.IsNormal.isHopfSubalgebra_coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : I.coinvariants.IsHopfSubalgebra

The coinvariants of a normal Hopf ideal form a Hopf subalgebra, when H and H ⧸ H^{co H/I} are flat, for instance over a field.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : CommHopfAlgCat R

The coordinate Hopf algebra of the quotient G ⧸ N of the affine group G = Spec H by the normal closed subgroup N cut out by the normal Hopf ideal I: the coinvariants H^{co H/I}, the functions on G invariant under right translation by N.

Equations

• TauCeti.CommHopfAlgCat.coinvariants hI = TauCeti.CommHopfAlgCat.ofHopfSubalgebra ⋯

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.coinvariantsι {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : coinvariants hI ⟶ H

The coordinate map of the projection G → G ⧸ N: the inclusion of the coinvariants.

Equations

• TauCeti.CommHopfAlgCat.coinvariantsι hI = TauCeti.CommHopfAlgCat.hopfSubalgebraι ⋯

theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_coinvariantsι_le {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : kernelHopfIdeal (coinvariantsι hI) ≤ I

The normal subgroup N lies in the kernel of the projection G → G ⧸ N.

noncomputable def TauCeti.CommHopfAlgCat.liftCoinvariants {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) (hf : kernelHopfIdeal f ≤ I) : K ⟶ coinvariants hI

A homomorphism out of G whose kernel contains N factors through G → G ⧸ N: in coordinates, a morphism f : K ⟶ H whose kernel Hopf ideal is contained in I factors through the coinvariants.

Equations

• TauCeti.CommHopfAlgCat.liftCoinvariants hI f hf = TauCeti.CommHopfAlgCat.liftHopfSubalgebra ⋯ f ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.coe_liftCoinvariants_apply {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) (hf : kernelHopfIdeal f ≤ I) (x : ↑K) : ↑((CommHopfAlgCat.Hom.hom (liftCoinvariants hI f hf)) x) = (CommHopfAlgCat.Hom.hom f) x

The factorization through the coinvariants preserves the values of the original morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.liftCoinvariants_comp_coinvariantsι {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) (hf : kernelHopfIdeal f ≤ I) : CategoryTheory.CategoryStruct.comp (liftCoinvariants hI f hf) (coinvariantsι hI) = f

The factorization through G → G ⧸ N recovers the original morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.liftCoinvariants_comp_coinvariantsι_assoc {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) (hf : kernelHopfIdeal f ≤ I) {Z : CommHopfAlgCat R} (h : H ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftCoinvariants hI f hf) (CategoryTheory.CategoryStruct.comp (coinvariantsι hI) h) = CategoryTheory.CategoryStruct.comp f h

The factorization through G → G ⧸ N recovers the original morphism.

theorem TauCeti.CommHopfAlgCat.liftCoinvariants_unique {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) (hf : kernelHopfIdeal f ≤ I) (g : K ⟶ coinvariants hI) (hg : CategoryTheory.CategoryStruct.comp g (coinvariantsι hI) = f) : g = liftCoinvariants hI f hf

The factorization through G → G ⧸ N is unique.

theorem TauCeti.CommHopfAlgCat.exists_comp_coinvariantsι_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R ↥I.coinvariants] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) (f : K ⟶ H) : (∃ (g : K ⟶ coinvariants hI), CategoryTheory.CategoryStruct.comp g (coinvariantsι hI) = f) ↔ kernelHopfIdeal f ≤ I

Universal property of G ⧸ N. A homomorphism out of G factors through the projection G → G ⧸ N exactly when its kernel contains N: in coordinates, a morphism f : K ⟶ H factors through the coinvariants exactly when its kernel Hopf ideal is contained in I.