Scalar extension of characters of a split bialgebra

Scalar extension sends a group-like element g to 1 ⊗ g. If a commutative bialgebra over a domain is torsion-free and spanned by its group-like elements, this map is an equivalence for every scalar extension with connected prime spectrum. In particular, extending the splitting field of a diagonalizable group does not create new characters. This allows characters computed over a splitting field to be compared with geometric characters.

Here ConnectedSpace (PrimeSpectrum K) includes nonemptiness of the spectrum and hence implies Nontrivial K; in particular, the zero ring is excluded.

The proof uses GroupLike.evaluationBialgEquiv to reconstruct the original bialgebra as the monoid algebra of its group-like elements, MonoidAlgebra.scalarTensorBialgEquiv for scalar extension, and MonoidAlgebra.groupLikeEquiv to classify the resulting characters. No finite-generation, smoothness, or characteristic hypothesis is needed.

Main declarations

• TauCeti.groupLikeBaseChange: the canonical scalar-extension map on characters.
• TauCeti.groupLikeBaseChange_bijective: preservation of characters under the stated spanning, torsion-free, and connected-spectrum hypotheses.
• TauCeti.groupLikeBaseChangeEquiv: the resulting multiplicative equivalence.

References

• J. S. Milne, Algebraic Groups (2017), Definition 12.7 and Theorems 12.8--12.9.

noncomputable def TauCeti.groupLikeBaseChange {R : Type u_1} {K : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring K] [Algebra R K] [Semiring A] [Bialgebra R A] : GroupLike R A →* GroupLike K (TensorProduct R K A)

Scalar extension of a group-like element, sending g to 1 ⊗ g.

Equations

• TauCeti.groupLikeBaseChange = { toFun := fun (g : GroupLike R A) => { val := 1 ⊗ₜ[R] ↑g, isGroupLikeElem_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.val_groupLikeBaseChange {R : Type u_1} {K : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring K] [Algebra R K] [Semiring A] [Bialgebra R A] (g : GroupLike R A) : ↑(groupLikeBaseChange g) = 1 ⊗ₜ[R] ↑g

The underlying value of an extended character.

@[simp]

theorem TauCeti.groupLikeBaseChange_map {R : Type u_1} {K : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring K] [Algebra R K] [Semiring A] [Bialgebra R A] {B : Type u_4} [Semiring B] [Bialgebra R B] (f : A →ₐc[R] B) (g : GroupLike R A) : groupLikeBaseChange ((GroupLike.map f) g) = (GroupLike.map (Bialgebra.TensorProduct.map (BialgHom.id K K) f)) (groupLikeBaseChange g)

Extending a character commutes with a bialgebra morphism.

theorem TauCeti.groupLikeBaseChange_bijective {R : Type u_4} {K : Type u_5} {A : Type u_6} [CommRing R] [IsDomain R] [CommRing K] [Algebra R K] [ConnectedSpace (PrimeSpectrum K)] [CommRing A] [Bialgebra R A] [Module.IsTorsionFree R A] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) : Function.Bijective ⇑groupLikeBaseChange

Scalar extension preserves the characters of a torsion-free commutative bialgebra spanned by group-like elements, provided the extended base has connected prime spectrum. The ConnectedSpace hypothesis includes nonemptiness, so the extended base is nontrivial.

noncomputable def TauCeti.groupLikeBaseChangeEquiv {R : Type u_4} {K : Type u_5} {A : Type u_6} [CommRing R] [IsDomain R] [CommRing K] [Algebra R K] [ConnectedSpace (PrimeSpectrum K)] [CommRing A] [Bialgebra R A] [Module.IsTorsionFree R A] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) : GroupLike R A ≃* GroupLike K (TensorProduct R K A)

The character equivalence induced by scalar extension of a split commutative bialgebra. Its forward map is the canonical scalar-extension map, independently of the spanning proof.

Equations

• TauCeti.groupLikeBaseChangeEquiv hspan = MulEquiv.ofBijective TauCeti.groupLikeBaseChange ⋯

@[simp]

theorem TauCeti.groupLikeBaseChangeEquiv_apply {R : Type u_4} {K : Type u_5} {A : Type u_6} [CommRing R] [IsDomain R] [CommRing K] [Algebra R K] [ConnectedSpace (PrimeSpectrum K)] [CommRing A] [Bialgebra R A] [Module.IsTorsionFree R A] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) (g : GroupLike R A) : (groupLikeBaseChangeEquiv hspan) g = groupLikeBaseChange g

The equivalence applies as the canonical scalar-extension map.

@[simp]

theorem TauCeti.one_tmul_val_groupLikeBaseChangeEquiv_symm {R : Type u_4} {K : Type u_5} {A : Type u_6} [CommRing R] [IsDomain R] [CommRing K] [Algebra R K] [ConnectedSpace (PrimeSpectrum K)] [CommRing A] [Bialgebra R A] [Module.IsTorsionFree R A] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) (g : GroupLike K (TensorProduct R K A)) : 1 ⊗ₜ[R] ↑((groupLikeBaseChangeEquiv hspan).symm g) = ↑g

Every extended character is the tensor with one of its unique original character.