Descent of Hopf ideals

A closed subgroup of an affine group over a field k is cut out by a Hopf ideal of the coordinate Hopf algebra H. This file identifies the Hopf ideals of a scalar extension L ⊗[k] H that come from Hopf ideals of H, that is, the closed subgroups of the base-changed group that are defined over k.

When the ground-field map is surjective, every Hopf ideal after scalar extension comes from a Hopf ideal over the original field. The coefficient Hopf ideal for the one-element basis supplies the descent. This applies to an algebraic extension of an algebraically closed field and allows geometric subgroup conditions to be checked over that field itself.

Along a Galois extension L / k, possibly infinite, a Hopf ideal of L ⊗[k] H descends exactly when it is stable under the action of Gal(L / k) on the scalar factor. The descended Hopf ideal is unique, consists of the elements h with 1 ⊗ h in the given ideal, and is the coefficient Hopf ideal in any basis of L. Galois descent of subspaces supplies the underlying ideal, and the coefficient Hopf ideal supplies the Hopf structure without rechecking it. This is the descent step for closed subgroups characterized geometrically, such as the unipotent radical, over a perfect field, whose algebraic closure is Galois.

Main declarations

• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_surjective: every Hopf ideal descends along a surjective map of ground fields.
• Module.Basis.baseChangeHopfIdeal_coefficientHopfIdeal_of_forall_map_mem: a Galois-stable Hopf ideal is the base change of its coefficient Hopf ideal.
• Module.Basis.mem_coefficientHopfIdeal_iff_of_forall_map_mem: that coefficient Hopf ideal consists of the elements h with 1 ⊗ h in the Galois-stable Hopf ideal.
• TauCeti.CommHopfAlgCat.existsUnique_baseChangeHopfIdeal_eq_iff: along a Galois extension, the base-changed Hopf ideals are exactly the Galois-stable ones, each descending uniquely.

References

• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §AG.14.
• J. S. Milne, Algebraic Groups (2017), Appendix A.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_surjective {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} (h : Function.Surjective ⇑(algebraMap k K)) : Function.Surjective baseChangeHopfIdeal

Every Hopf ideal descends along a surjective map of ground fields.

theorem Module.Basis.baseChangeHopfIdeal_coefficientHopfIdeal_of_forall_map_mem {k : Type u} {L : Type w} [Field k] [Field L] [Algebra k L] [IsGalois k L] {H : CommHopfAlgCat k} {κ : Type u_1} [DecidableEq κ] (b : Basis κ k L) (I : TauCeti.HopfIdeal L ↑(TauCeti.CommHopfAlgCat.baseChange H)) (hI : ∀ (σ : Gal(L/k)), ∀ x ∈ I, (TensorProduct.map σ.toLinearMap LinearMap.id) x ∈ I) : TauCeti.CommHopfAlgCat.baseChangeHopfIdeal (b.coefficientHopfIdeal I) = I

Galois descent of Hopf ideals. Along a Galois extension L / k, a Hopf ideal of L ⊗[k] H stable under the scalar-factor Galois action is the base change of its coefficient Hopf ideal in any basis of L.

theorem Module.Basis.mem_coefficientHopfIdeal_iff_of_forall_map_mem {k : Type u} {L : Type w} [Field k] [Field L] [Algebra k L] [IsGalois k L] {H : CommHopfAlgCat k} {κ : Type u_1} [DecidableEq κ] (b : Basis κ k L) (I : TauCeti.HopfIdeal L ↑(TauCeti.CommHopfAlgCat.baseChange H)) (hI : ∀ (σ : Gal(L/k)), ∀ x ∈ I, (TensorProduct.map σ.toLinearMap LinearMap.id) x ∈ I) (h : ↑H) : h ∈ b.coefficientHopfIdeal I ↔ 1 ⊗ₜ[k] h ∈ I

The Hopf ideal descended from a Galois-stable Hopf ideal I of L ⊗[k] H consists of the elements h of H with 1 ⊗ h ∈ I.

theorem TauCeti.CommHopfAlgCat.existsUnique_baseChangeHopfIdeal_eq_iff {k : Type u} {L : Type w} [Field k] [Field L] [Algebra k L] [IsGalois k L] {H : CommHopfAlgCat k} (I : HopfIdeal L ↑(baseChange H)) : (∃! J : HopfIdeal k ↑H, baseChangeHopfIdeal J = I) ↔ ∀ (σ : Gal(L/k)), ∀ x ∈ I, (TensorProduct.map σ.toLinearMap LinearMap.id) x ∈ I

Along a Galois extension L / k, a Hopf ideal of L ⊗[k] H is the base change of a Hopf ideal of H exactly when it is stable under the scalar-factor Galois action, and that Hopf ideal of H is then unique. Geometrically, a closed subgroup of the base-changed group is defined over k exactly when it is stable under Gal(L / k).