Smoothness of closed subgroups under faithfully flat base change

A closed subgroup cut out by a Hopf ideal J is smooth exactly when the closed subgroup cut out by its base change J_K along a faithfully flat extension k → K is smooth. The coordinate quotient of J_K is identified with the base change of the coordinate quotient of J by CommHopfAlgCat.quotientBaseChangeIso. Smoothness is preserved by base change, and descends along the faithfully flat extension by Mathlib's Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat.

Main declarations

• TauCeti.smoothCommHopfAlgProperty_quotient_baseChange_iff: smoothness of a closed subgroup is equivalent to smoothness of its faithfully flat base change.

theorem TauCeti.smoothCommHopfAlgProperty_quotient_baseChange_iff {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} [Module.FaithfullyFlat k K] (J : HopfIdeal k ↑H) : smoothCommHopfAlgProperty K ((CommHopfAlgCat.baseChange H).quotient (CommHopfAlgCat.baseChangeHopfIdeal J)) ↔ smoothCommHopfAlgProperty k (H.quotient J)

Along a faithfully flat extension k → K, the closed subgroup cut out by a Hopf ideal J is smooth exactly when the closed subgroup cut out by its base change J_K is smooth.