Descent of normal closed subgroups

Normality of a closed subgroup can be checked after extending the ground field. The pointwise criterion for normality is reflected by the injective map from any value algebra into its scalar extension. This permits descent of the normality condition in the construction of solvable radicals.

theorem TauCeti.CommHopfAlgCat.isNormal_of_baseChangeHopfIdeal {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : (baseChangeHopfIdeal I).IsNormal) : I.IsNormal

Normality of a closed subgroup is reflected by extension of the ground field.

@[simp]

theorem TauCeti.CommHopfAlgCat.isNormal_baseChangeHopfIdeal_iff {k : Type u} {K : Type w} [Field k] [Field K] [Algebra k K] {H : CommHopfAlgCat k} (I : HopfIdeal k ↑H) : (baseChangeHopfIdeal I).IsNormal ↔ I.IsNormal

A closed subgroup is normal exactly when its base change to a field extension is normal.