Base change of diagonalizable-group points

For a commutative group G, the diagonalizable group D(G) over k is represented by the Hopf algebra k[G]. The imported TauCeti.MonoidAlgebra.scalarTensorBialgEquiv identifies its base change K ⊗[k] k[G] with K[G] as a bialgebra. This file records the corresponding calculation on functors of points: if A is a commutative K-algebra, then the A-valued points of the base-changed Hopf algebra are still the character group G →* Aˣ.

The construction is the composition of two existing Tau Ceti equivalences: AlgHom.baseChangePointsMulEquiv, which identifies points of K ⊗[k] k[G] with k-algebra maps out of k[G], and DiagonalizableGroup.pointsMulEquiv, which identifies those maps with characters. The lemmas here spell out the values on the group-like generators 1 ⊗ single g 1, the inverse map, and compatibility with the contravariant functoriality in G.

This advances the ReductiveGroups roadmap, Layer 0 ("Base change. K ⊗[k] A as a Hopf algebra over K") and Layer 4 ("Diagonalizable groups and groups of multiplicative type: M ↦ D(M) = Spec k[M]").

Main declarations

• TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv: the multiplicative equivalence from base-changed points of D(G) to the character group G →* Aˣ.
• TauCeti.DiagonalizableGroup.baseChangeCoordinateRingIso: base change of the finite-type coordinate Hopf algebra of D(G) is the corresponding coordinate Hopf algebra over the new base.
• TauCeti.DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso: the same isomorphism read in CommHopfAlgCat.
• TauCeti.DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso_hom_apply: its forward map is the scalar-tensor bialgebra equivalence.
• TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_apply_coe: the equivalence reads a point by evaluating it on 1 ⊗ single g 1.
• TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_mapDomain_scalarTensorBialgEquiv: the coordinate-ring and points-level base-change equivalences agree.
• TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_mapDomain: under a homomorphism G →* G', the base-changed points map is precomposition of characters.

References

The group-algebra Hopf structure and MonoidAlgebra.mapDomainBialgHom are Mathlib's Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra and Mathlib.RingTheory.Bialgebra.MonoidAlgebra. The base-change equivalence and the diagonalizable-group points calculation are Tau Ceti's TauCeti.AlgHom.baseChangePointsMulEquiv and TauCeti.DiagonalizableGroup.pointsMulEquiv.

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.baseChangeCoordinateRingIso (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (G : FGCommGrpCat) : (coordinateRing k G).baseChange ≅ coordinateRing K G

The coordinate Hopf algebra of a finite-type diagonalizable group commutes with base change. This is the bundled form of MonoidAlgebra.scalarTensorBialgEquiv for a finitely generated commutative group G:

K ⊗[k] k[G] ≅ K[G].

It is an abbreviation so that MonoidAlgebra.scalarTensorBialgEquiv_tmul and MonoidAlgebra.scalarTensorBialgEquiv_symm_single apply directly to its forward and inverse maps, without duplicating their statements at this bundling layer.

Equations

• TauCeti.DiagonalizableGroup.baseChangeCoordinateRingIso k K G = (TauCeti.finiteTypeCommHopfAlgProperty K).isoMk (CommHopfAlgCat.isoMk (TauCeti.MonoidAlgebra.scalarTensorBialgEquiv k K))

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (G : FGCommGrpCat) : CommHopfAlgCat.baseChange (coordinateRing k G).obj ≅ (coordinateRing K G).obj

The CommHopfAlgCat-level form of baseChangeCoordinateRingIso, obtained by forgetting the finite-type property. It is the isomorphism K ⊗[k] k[G] ≅ K[G] of commutative Hopf algebras.

Equations

• TauCeti.DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso k K G = (TauCeti.finiteTypeCommHopfAlgProperty K).ι.mapIso (TauCeti.DiagonalizableGroup.baseChangeCoordinateRingIso k K G)

theorem TauCeti.DiagonalizableGroup.baseChangeCoordinateHopfAlgebraIso_hom_apply (k : Type u) (K : Type v) [CommRing k] [CommRing K] [Algebra k K] (G : FGCommGrpCat) (x : TensorProduct k K (MonoidAlgebra k ↑G)) : (CommHopfAlgCat.Hom.hom (baseChangeCoordinateHopfAlgebraIso k K G).hom) x = (MonoidAlgebra.scalarTensorBialgEquiv k K) x

The forward map of the categorical coordinate-ring base-change isomorphism is the scalar-tensor bialgebra equivalence.

This is the interface lemma for crossing the two bundling layers: forgetting the finite-type property leaves the underlying morphism untouched, so the underlying bialgebra map of baseChangeCoordinateHopfAlgebraIso is the one packaged by CommHopfAlgCat.isoMk.

noncomputable def TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] : WithConv (TensorProduct k K (MonoidAlgebra k G) →ₐ[K] A) ≃* (G →* Aˣ)

The A-points of the base change K ⊗[k] k[G] of the diagonalizable group D(G) are the character group G →* Aˣ.

The source is the convolution group of K-algebra maps out of the base-changed Hopf algebra. The target is the ordinary pointwise-multiplication group of characters.

Equations

• TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv = TauCeti.AlgHom.baseChangePointsMulEquiv.symm.trans TauCeti.DiagonalizableGroup.pointsMulEquiv

@[simp]

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_apply {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] (f : WithConv (TensorProduct k K (MonoidAlgebra k G) →ₐ[K] A)) : baseChangePointsMulEquiv f = charOfPoint (AlgHom.baseChangePointsMulEquiv.symm f).ofConv

Applying baseChangePointsMulEquiv first restricts a base-changed point along g ↦ 1 ⊗ single g 1, then reads off its character.

@[simp]

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_apply_coe {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] (f : WithConv (TensorProduct k K (MonoidAlgebra k G) →ₐ[K] A)) (g : G) : ↑((baseChangePointsMulEquiv f) g) = f.ofConv (1 ⊗ₜ[k] MonoidAlgebra.single g 1)

The base-changed diagonalizable-points equivalence reads a point by evaluating it on the base-changed group-like element 1 ⊗ single g 1.

@[simp]

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_symm_apply_tmul_single {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] (χ : G →* Aˣ) (s : K) (g : G) (r : k) : (baseChangePointsMulEquiv.symm χ).ofConv (s ⊗ₜ[k] MonoidAlgebra.single g r) = s • r • ↑(χ g)

The inverse base-changed diagonalizable-points equivalence extends a character after base change. On a pure tensor it sends s ⊗ single g r to s • (r • χ g).

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_symm_apply_single_one {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] (χ : G →* Aˣ) (g : G) : (baseChangePointsMulEquiv.symm χ).ofConv (1 ⊗ₜ[k] MonoidAlgebra.single g 1) = ↑(χ g)

The inverse base-changed diagonalizable-points equivalence takes 1 ⊗ single g 1 to the value of the character at g.

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_mapDomain_scalarTensorBialgEquiv {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] (f : WithConv (MonoidAlgebra K G →ₐ[K] A)) : baseChangePointsMulEquiv ((AlgHom.mapDomain ↑(MonoidAlgebra.scalarTensorBialgEquiv k K)) f) = pointsMulEquiv f

The coordinate-ring and functor-of-points base-change identifications agree. A point of K[G], restricted along K ⊗[k] k[G] ≃ₐc[K] K[G], gives the same character under baseChangePointsMulEquiv as it does under the ordinary pointsMulEquiv over K.

theorem TauCeti.DiagonalizableGroup.baseChangePointsMulEquiv_mapDomain {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] {G' : Type u_1} [CommGroup G'] (φ : G →* G') (f : WithConv (TensorProduct k K (MonoidAlgebra k G') →ₐ[K] A)) : baseChangePointsMulEquiv ((AlgHom.mapDomain (Bialgebra.TensorProduct.map (BialgHom.id K K) (MonoidAlgebra.mapDomainBialgHom k φ))) f) = (baseChangePointsMulEquiv f).comp φ

Under base change, the points map induced contravariantly by φ : G →* G' is precomposition of characters by φ.

theorem TauCeti.DiagonalizableGroup.mapDomain_baseChangePointsMulEquiv_symm_apply {k : Type u} {K : Type v} {A : Type w} {G : Type w'} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] [CommGroup G] {G' : Type u_1} [CommGroup G'] (φ : G →* G') (χ : G' →* Aˣ) : (AlgHom.mapDomain (Bialgebra.TensorProduct.map (BialgHom.id K K) (MonoidAlgebra.mapDomainBialgHom k φ))) (baseChangePointsMulEquiv.symm χ) = baseChangePointsMulEquiv.symm (χ.comp φ)

Mapping the base-changed point attached to a character is precomposition of that character by the homomorphism of character groups.