Central points under base change

Let H be a bialgebra over k, let K be a commutative k-algebra, and let A be a commutative K-algebra. The standard equivalence

  (K ⊗[k] H →ₐ[K] A) ≃ (H →ₐ[k] A)

identifies universally central points on the two sides. The reverse implication uses the full universal definition of centrality: a k-algebra map out of A gives its codomain the induced K-algebra structure, so every test point before base change is also a test point after base change.

Main results

• TauCeti.HopfAlgebra.isCentralPoint_baseChangePointsMulEquiv_symm_iff: the unbundled base-change equivalence preserves and reflects universal centrality.
• TauCeti.CommHopfAlgCat.isCentralPoint_baseChangePointsMulEquiv_iff: the corresponding statement for bundled commutative Hopf algebras and their functors of points.

References

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

@[simp]

theorem TauCeti.HopfAlgebra.isCentralPoint_baseChangePointsMulEquiv_symm_iff {k : Type u} {K H A : Type v} [CommRing k] [CommRing K] [Ring H] [CommRing A] [Algebra k K] [Bialgebra k H] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (g : WithConv (TensorProduct k K H →ₐ[K] A)) : IsCentralPoint (AlgHom.baseChangePointsMulEquiv.symm g) ↔ IsCentralPoint g

Universal centrality is preserved and reflected by the base-change equivalence on points.

The equivalence is written in the restriction direction, from a point of K ⊗[k] H to a point of H.

@[simp]

theorem TauCeti.CommHopfAlgCat.isCentralPoint_baseChangePointsMulEquiv_iff {k : Type u} {K : Type v} [CommRing k] [CommRing K] [Algebra k K] (H : CommHopfAlgCat k) (A : CommAlgCat K) (g : ↑(HopfAlgebra.points A)) : HopfAlgebra.IsCentralPoint ((baseChangePointsMulEquiv A H) g) ↔ HopfAlgebra.IsCentralPoint g

The bundled base-change equivalence on points preserves and reflects universal centrality.