Characters over an extension of a splitting ring

For a tower k → L → K, the scalar-tower homomorphism extends characters without any splitting assumption. A commutative k-bialgebra split over L has the same characters over L and K, provided L is a domain, L ⊗[k] A is torsion-free over L, and Spec K is connected. The comparison extends the coefficients of a character, and intertwines compatible scalar automorphisms of L and K. This identifies splitting-field characters with geometric characters while retaining the Galois action.

The construction uses groupLikeBaseChangeEquiv and baseChangeTowerBialgEquiv.

noncomputable def TauCeti.groupLikeScalarTowerHom {k : Type u_1} {L : Type u_2} {K : Type u_3} {A : Type u_4} [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring A] [Bialgebra k A] : GroupLike L (TensorProduct k L A) →* GroupLike K (TensorProduct k K A)

Extension of the coefficients of a character through a tower of scalar rings.

Equations

• TauCeti.groupLikeScalarTowerHom = (TauCeti.GroupLike.mapEquiv (TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv k L A K)).toMonoidHom.comp TauCeti.groupLikeBaseChange

@[simp]

theorem TauCeti.val_groupLikeScalarTowerHom {k : Type u_1} {L : Type u_2} {K : Type u_3} {A : Type u_4} [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring A] [Bialgebra k A] (x : GroupLike L (TensorProduct k L A)) : ↑(groupLikeScalarTowerHom x) = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k L K) (AlgHom.id k A)) ↑x

The scalar-tower map extends the scalar coefficients of a character.

noncomputable def TauCeti.groupLikeScalarTowerEquiv {k : Type u_1} {L : Type u_2} {K : Type u_3} {A : Type u_4} [CommRing k] [CommRing L] [Algebra k L] [CommRing K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [CommRing A] [Bialgebra k A] [IsDomain L] [ConnectedSpace (PrimeSpectrum K)] [Module.IsTorsionFree L (TensorProduct k L A)] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) : GroupLike L (TensorProduct k L A) ≃* GroupLike K (TensorProduct k K A)

Extension of the coefficients of a character through a tower, when the intermediate scalar extension is spanned by its group-like elements.

Equations

• TauCeti.groupLikeScalarTowerEquiv hspan = (TauCeti.groupLikeBaseChangeEquiv hspan).trans (TauCeti.GroupLike.mapEquiv (TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv k L A K))

@[simp]

theorem TauCeti.val_groupLikeScalarTowerEquiv {k : Type u_1} {L : Type u_2} {K : Type u_3} {A : Type u_4} [CommRing k] [CommRing L] [Algebra k L] [CommRing K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [CommRing A] [Bialgebra k A] [IsDomain L] [ConnectedSpace (PrimeSpectrum K)] [Module.IsTorsionFree L (TensorProduct k L A)] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) (x : GroupLike L (TensorProduct k L A)) : ↑((groupLikeScalarTowerEquiv hspan) x) = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k L K) (AlgHom.id k A)) ↑x

The character comparison extends coefficients and leaves the original bialgebra fixed.

theorem TauCeti.groupLikeScalarTowerEquiv_smul {k : Type u_1} {L : Type u_2} {K : Type u_3} {A : Type u_4} [CommRing k] [CommRing L] [Algebra k L] [CommRing K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [CommRing A] [Bialgebra k A] [IsDomain L] [ConnectedSpace (PrimeSpectrum K)] [Module.IsTorsionFree L (TensorProduct k L A)] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) (σ : K ≃ₐ[k] K) (τ : L ≃ₐ[k] L) (hστ : ∀ (a : L), σ ((algebraMap L K) a) = (algebraMap L K) (τ a)) (x : GroupLike L (TensorProduct k L A)) : (groupLikeScalarTowerEquiv hspan) (τ • x) = σ • (groupLikeScalarTowerEquiv hspan) x

Compatible scalar automorphisms commute with extending a character through a tower.

This is an explicit rewrite rule: simp cannot infer σ from the left-hand side. Use it with the chosen compatible automorphisms and their compatibility proof.