Central points of an affine group scheme

Let H be a commutative bialgebra over R, so that A ↦ (H →ₐ[R] A) is the functor of points of the affine monoid scheme Spec H, a group functor when H is a Hopf algebra. A point g : H →ₐ[R] A is central when its image in G(B) commutes with every B-point of G, for every A-algebra B, and not merely with the points over A itself.

Quantifying over all value algebras is what makes the notion correct: an element of the abstract group G(A) may commute with everything in G(A) without commuting with the points of G over larger algebras, so the naive condition does not describe a subgroup scheme. The same functorial formulation is used for the kernel of a central isogeny in TauCeti.GroupScheme.HasCentralKernel.

The main result is that a single test algebra decides the question: TauCeti.HopfAlgebra.isCentralPoint_iff_commute_includeRight says that g is central exactly when its image in G(A ⊗[R] H) commutes with the tautological point h ↦ 1 ⊗ₜ h. Every other value algebra is a specialization of that universal one, because an algebra map out of A ⊗[R] H is exactly a pair consisting of an A-algebra and a point.

Specialized to the tautological point of G over H itself, the criterion says that G is a commutative group functor exactly when H is cocommutative (TauCeti.HopfAlgebra.isCentralPoint_id_iff_isCocomm).

Main declarations

• TauCeti.HopfAlgebra.IsCentralPoint: centrality of a point of the functor of points.
• TauCeti.HopfAlgebra.center: the central points as a subgroup of the group of points.
• TauCeti.HopfAlgebra.instIsMulCommutativeCenter: the central points form a commutative group.

Main results

• TauCeti.HopfAlgebra.isCentralPoint_iff_commute_includeRight: one test algebra suffices.
• TauCeti.HopfAlgebra.commute_includeLeft_includeRight_iff_isCocomm: the two tensor-factor points of H commute exactly when H is cocommutative.
• TauCeti.HopfAlgebra.convMul_includeRight_includeLeft: the convolution product of the two tensor-factor points in the reversed order is the flipped comultiplication.
• TauCeti.HopfAlgebra.isCentralPoint_id_iff_isCocomm: the tautological point is central exactly when H is cocommutative.
• TauCeti.HopfAlgebra.IsCentralPoint.mapDomain_bialgEquiv and TauCeti.HopfAlgebra.isCentralPoint_mapDomain_bialgEquiv_iff: centrality is invariant under a change of coordinate bialgebra by an equivalence.

References

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

This is a prerequisite for the center Z(G) in Layer 6, "Reductive and semisimple groups", of TauCetiRoadmap/ReductiveGroups/README.md.

def TauCeti.HopfAlgebra.IsCentralPoint {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : Prop

A point g of Spec H with values in A is central when, for every R-algebra map φ : A →ₐ[R] B into a commutative R-algebra, the point φ ∘ g commutes with every B-point of Spec H.

Commuting with the points over A alone is a strictly weaker condition and does not describe a subgroup scheme; this is why the value algebra is quantified over. The quantified value algebras live in Type (max v w), which contains the universal test algebra A ⊗[R] H. TauCeti.HopfAlgebra.isCentralPoint_iff_commute_includeRight shows, when the coordinate and value algebras are in the same universe, that this single value algebra already decides centrality.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.HopfAlgebra.isCentralPoint_def {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : IsCentralPoint g ↔ ∀ ⦃B : Type (max v w)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (φ : A →ₐ[R] B) (h : WithConv (H →ₐ[R] B)), Commute ((AlgHom.mapValue φ) g) h

Centrality, restated as the defining condition.

theorem TauCeti.HopfAlgebra.IsCentralPoint.commute {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] {g : WithConv (H →ₐ[R] A)} (hg : IsCentralPoint g) (h : WithConv (H →ₐ[R] A)) : Commute g h

A central point commutes with every point over its own value algebra.

theorem TauCeti.HopfAlgebra.IsCentralPoint.mapValue {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] {g : WithConv (H →ₐ[R] A)} (hg : IsCentralPoint g) {B : Type (max v w)} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) : IsCentralPoint ((AlgHom.mapValue φ) g)

Centrality is preserved by change of value algebra.

theorem TauCeti.HopfAlgebra.IsCentralPoint.mapDomain_bialgEquiv {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] {K : Type v} [Ring K] [Bialgebra R K] {g : WithConv (K →ₐ[R] A)} (hg : IsCentralPoint g) (e : H ≃ₐc[R] K) : IsCentralPoint ((AlgHom.mapDomain e.toBialgHom) g)

Precomposition by a bialgebra equivalence preserves universal centrality of points.

theorem TauCeti.HopfAlgebra.isCentralPoint_mapDomain_bialgEquiv_iff {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] {K : Type v} [Ring K] [Bialgebra R K] (e : H ≃ₐc[R] K) (g : WithConv (K →ₐ[R] A)) : IsCentralPoint ((AlgHom.mapDomain e.toBialgHom) g) ↔ IsCentralPoint g

Precomposition by a bialgebra equivalence preserves and reflects universal centrality of points. This is invariance of the center of the functor of points under a change of coordinate Hopf algebra.

theorem TauCeti.HopfAlgebra.isCentralPoint_one {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] : IsCentralPoint 1

The identity point is central.

theorem TauCeti.HopfAlgebra.IsCentralPoint.mul {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] {g g' : WithConv (H →ₐ[R] A)} (hg : IsCentralPoint g) (hg' : IsCentralPoint g') : IsCentralPoint (g * g')

A product of central points is central.

theorem TauCeti.HopfAlgebra.isCentralPoint_of_isCocomm {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [Bialgebra R H] [CommRing A] [Algebra R A] [Coalgebra.IsCocomm R H] (g : WithConv (H →ₐ[R] A)) : IsCentralPoint g

Over a cocommutative bialgebra every point is central, the group functor being commutative.

theorem TauCeti.HopfAlgebra.IsCentralPoint.inv {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] {g : WithConv (H →ₐ[R] A)} (hg : IsCentralPoint g) : IsCentralPoint g⁻¹

The inverse of a central point is central.

noncomputable def TauCeti.HopfAlgebra.center (R : Type u) (H : Type v) (A : Type w) [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] : Subgroup (WithConv (H →ₐ[R] A))

The center of the functor of points, as a subgroup of the group of A-points.

Its elements are the points that stay central after every change of value algebra, so the construction is natural in A (TauCeti.HopfAlgebra.mapValue_mem_center). It is contained in, and in general strictly smaller than, the abstract center of the group G(A).

Equations

• TauCeti.HopfAlgebra.center R H A = { carrier := {g : WithConv (H →ₐ[R] A) | TauCeti.HopfAlgebra.IsCentralPoint g}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.HopfAlgebra.mem_center {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] {g : WithConv (H →ₐ[R] A)} : g ∈ center R H A ↔ IsCentralPoint g

theorem TauCeti.HopfAlgebra.center_le_center {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] : center R H A ≤ Subgroup.center (WithConv (H →ₐ[R] A))

The center of the functor of points is contained in the abstract center of the group of A-points. The inclusion is generally strict: an abstractly central point need not stay central over larger value algebras.

instance TauCeti.HopfAlgebra.instIsMulCommutativeCenter {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] : IsMulCommutative ↥(center R H A)

The universally central points form a commutative group.

theorem TauCeti.HopfAlgebra.mapValue_mem_center {R : Type u} {H : Type v} {A : Type w} [CommRing R] [Ring H] [HopfAlgebra R H] [CommRing A] [Algebra R A] {B : Type (max v w)} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) {g : WithConv (H →ₐ[R] A)} (hg : g ∈ center R H A) : (AlgHom.mapValue φ) g ∈ center R H B

The center is natural in the value algebra.

theorem TauCeti.HopfAlgebra.isCentralPoint_iff_commute_includeRight {R : Type u} {H A : Type v} [CommRing R] [CommRing H] [Bialgebra R H] [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : IsCentralPoint g ↔ Commute ((AlgHom.mapValue Algebra.TensorProduct.includeLeft) g) (WithConv.toConv Algebra.TensorProduct.includeRight)

A single value algebra decides centrality. A point g of Spec H over A is central exactly when its image over A ⊗[R] H commutes with the tautological point h ↦ 1 ⊗ₜ h.

Every pair consisting of an A-algebra B and a B-point of Spec H is the same thing as an algebra map A ⊗[R] H →ₐ[R] B, and the convolution product is functorial in the value algebra, so the universal case implies all the others.

theorem TauCeti.HopfAlgebra.convMul_includeRight_includeLeft {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] : WithConv.toConv Algebra.TensorProduct.includeRight * WithConv.toConv Algebra.TensorProduct.includeLeft = WithConv.toConv ((↑(Algebra.TensorProduct.comm R H H)).comp (Bialgebra.comulAlgHom R H))

The convolution product of the two tensor-factor points, taken in the other order, is the comultiplication followed by the flip of the tensor factors.

theorem TauCeti.HopfAlgebra.commute_includeLeft_includeRight_iff_isCocomm (R : Type u) (H : Type v) [CommRing R] [CommRing H] [Bialgebra R H] : Commute (WithConv.toConv Algebra.TensorProduct.includeLeft) (WithConv.toConv Algebra.TensorProduct.includeRight) ↔ Coalgebra.IsCocomm R H

The two tensor-factor points of H commute exactly when H is cocommutative. The two convolution products are the comultiplication and its flip, so their equality is precisely cocommutativity.

theorem TauCeti.HopfAlgebra.isCentralPoint_id_iff_isCocomm (R : Type u) (H : Type v) [CommRing R] [CommRing H] [Bialgebra R H] : IsCentralPoint (WithConv.toConv (AlgHom.id R H)) ↔ Coalgebra.IsCocomm R H

The tautological point is central exactly when H is cocommutative, that is, exactly when the group functor of Spec H is commutative.