Geometric characters of a descended group algebra

The characters of a group algebra descended along a finite Galois extension L/k recover its exponent group over every L-algebra K with connected prime spectrum. Compatible scalar automorphisms of K and L act on those characters by the prescribed action on exponents. In particular, taking K to be an algebraic closure recovers the absolute-Galois module of geometric characters, not just the characters over L.

No finite generation or torsion-freeness assumption on the exponent group is needed. The comparison uses groupAlgebraInvariantsCharacterEquiv over L and the scalar-tower equivalence for characters.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Appendix A.64.

noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsGeometricCharacterEquiv {k : Type u_1} {L : Type u_2} {K : Type u_3} {M : Type u_4} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [CommRing K] [ConnectedSpace (PrimeSpectrum K)] [Algebra k K] [Algebra L K] [IsScalarTower k L K] (ρ : Representation ℤ Gal(L/k) M) : GroupLike K (TensorProduct k K ↥(groupAlgebraInvariants ρ)) ≃* Multiplicative M

Characters of a descended group algebra over any algebra over the splitting field with connected prime spectrum are its original exponent group.

Equations

• TauCeti.GaloisDescent.groupAlgebraInvariantsGeometricCharacterEquiv ρ = (TauCeti.groupLikeScalarTowerEquiv ⋯).symm.trans (TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv ρ)

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsGeometricCharacterEquiv_symm_apply_val {k : Type u_1} {L : Type u_2} {K : Type u_3} {M : Type u_4} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [CommRing K] [ConnectedSpace (PrimeSpectrum K)] [Algebra k K] [Algebra L K] [IsScalarTower k L K] (ρ : Representation ℤ Gal(L/k) M) (m : Multiplicative M) : ↑((groupAlgebraInvariantsGeometricCharacterEquiv ρ).symm m) = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k L K) (AlgHom.id k ↥(groupAlgebraInvariants ρ))) ((groupAlgebraInvariantsBaseChangeBialgEquiv ρ).symm (MonoidAlgebra.single m 1))

The inverse character comparison is the coefficient extension of the character with the same exponent over the splitting field.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsGeometricCharacterEquiv_apply_eq_iff {k : Type u_1} {L : Type u_2} {K : Type u_3} {M : Type u_4} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [CommRing K] [ConnectedSpace (PrimeSpectrum K)] [Algebra k K] [Algebra L K] [IsScalarTower k L K] (ρ : Representation ℤ Gal(L/k) M) (x : GroupLike K (TensorProduct k K ↥(groupAlgebraInvariants ρ))) (m : Multiplicative M) : (groupAlgebraInvariantsGeometricCharacterEquiv ρ) x = m ↔ ↑x = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k L K) (AlgHom.id k ↥(groupAlgebraInvariants ρ))) ((groupAlgebraInvariantsBaseChangeBialgEquiv ρ).symm (MonoidAlgebra.single m 1))

A geometric character has exponent m exactly when it is the extension of the splitting-field character indexed by m.

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsGeometricCharacterEquiv_smul {k : Type u_1} {L : Type u_2} {K : Type u_3} {M : Type u_4} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] [CommRing K] [ConnectedSpace (PrimeSpectrum K)] [Algebra k K] [Algebra L K] [IsScalarTower k L K] (ρ : Representation ℤ Gal(L/k) M) (σ : K ≃ₐ[k] K) (τ : Gal(L/k)) (hστ : ∀ (a : L), σ ((algebraMap L K) a) = (algebraMap L K) (τ a)) (x : GroupLike K (TensorProduct k K ↥(groupAlgebraInvariants ρ))) : (groupAlgebraInvariantsGeometricCharacterEquiv ρ) (σ • x) = Multiplicative.ofAdd ((ρ τ) (Multiplicative.toAdd ((groupAlgebraInvariantsGeometricCharacterEquiv ρ) x)))

The character comparison intertwines compatible scalar automorphisms with the given action on exponents.