Base change of the center of an affine group scheme

For a field extension k → K and a commutative Hopf k-algebra H, this file proves the coordinate identity

  baseChangeHopfIdeal (centerDefiningIdeal H) = centerDefiningIdeal (baseChange H).

Together with TauCeti.CommHopfAlgCat.quotientBaseChangeIso, this identifies the quotient coordinate Hopf algebras of the base change of the center and the center after base change. One containment follows because the base change of a central closed subgroup is central. For the other, the universal point of the center after base change restricts to a universally central point of H, so it kills every equation of the original center.

Main results

• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_centerDefiningIdeal: the defining ideal of the center commutes with extension of the ground field.
• TauCeti.CommHopfAlgCat.centerDefiningIdeal_baseChange_eq_augmentation_iff: a field extension preserves and reflects triviality of the center.
• TauCeti.CommHopfAlgCat.centerCoordinateBaseChangeIso: the coordinate isomorphism between the center after base change and the base change of the center.

References

• J. S. Milne, Algebraic Groups (2017), §1.k and §2.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapters 2 and 16.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_centerDefiningIdeal {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : baseChangeHopfIdeal (centerDefiningIdeal H) = centerDefiningIdeal (baseChange H)

Formation of the center commutes with extension of the ground field. The ideal of K ⊗[k] H generated by the center equations of H is exactly the ideal defining the center after base change.

@[simp]

theorem TauCeti.CommHopfAlgCat.centerDefiningIdeal_baseChange_eq_augmentation_iff {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : centerDefiningIdeal (baseChange H) = HopfIdeal.augmentation K ↑(baseChange H) ↔ centerDefiningIdeal H = HopfIdeal.augmentation k ↑H

A field extension preserves and reflects triviality of the scheme-theoretic center.

The statement uses the augmentation ideal, which cuts out the identity subgroup. Thus it detects the full center scheme, including infinitesimal structure invisible on field-valued points.

noncomputable def TauCeti.CommHopfAlgCat.centerCoordinateBaseChangeIso {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : centerCoordinateHopfAlgebra (baseChange H) ≅ baseChange (centerCoordinateHopfAlgebra H)

The center after a field extension has the base change of the original center as its coordinate Hopf algebra.

Equations

• TauCeti.CommHopfAlgCat.centerCoordinateBaseChangeIso H = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.CommHopfAlgCat.quotientBaseChangeIso (TauCeti.CommHopfAlgCat.centerDefiningIdeal H)

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_centerCoordinateBaseChangeIso_hom {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp (mkQuotient (baseChange H) (centerDefiningIdeal (baseChange H))) (centerCoordinateBaseChangeIso H).hom = baseChangeMap (mkQuotient H (centerDefiningIdeal H))

The center base-change comparison respects the quotient coordinate maps.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeMap_mkQuotient_comp_centerCoordinateBaseChangeIso_inv {k : Type u} {K : Type v} [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : CategoryTheory.CategoryStruct.comp (baseChangeMap (mkQuotient H (centerDefiningIdeal H))) (centerCoordinateBaseChangeIso H).inv = mkQuotient (baseChange H) (centerDefiningIdeal (baseChange H))

The inverse center base-change comparison respects the quotient coordinate maps.