Recovering morphisms from Galois-equivariant characters #

For a finite Galois extension L/k, descent of group algebras is fully faithful: Hopf algebra morphisms between the descended coordinate algebras correspond bijectively to equivariant homomorphisms of the exponent groups. The inverse takes the map on group-like elements after scalar extension and uses the canonical character comparisons.

This supplies the morphism part of the character-group classification of groups of multiplicative type split by L, including tori. The exponent groups need not be finitely generated or torsion-free.

Under the character comparison of Galois.Character, the descended morphisms of Galois.Map induce the original equivariant maps on exponent groups.

References #

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

source

noncomputable def BialgHom.groupAlgebraInvariantsCharacterMap {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (F : ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐc[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau)) :

rho.IntertwiningMap tau

The equivariant map of exponent groups recovered from a morphism of descended Hopf algebras. It is the map on characters after extending scalars to the splitting field.

Equations

F.groupAlgebraInvariantsCharacterMap = { toLinearMap := (BialgHom.invariantsCharacterAddHom✝ F).toIntLinearMap, isIntertwining' := ⋯ }

Instances For

source

@[simp]

theorem BialgHom.groupAlgebraInvariantsCharacterMap_apply {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (F : ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐc[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau)) (m : M) :

F.groupAlgebraInvariantsCharacterMap m = Multiplicative.toAdd ((TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv tau) ((TauCeti.GroupLike.map (Bialgebra.TensorProduct.map (BialgHom.id L L) F)) ((TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv rho).symm (Multiplicative.ofAdd m))))

Evaluation of the recovered map in terms of the canonical character comparisons.

source

@[simp]

theorem Representation.IntertwiningMap.groupAlgebraInvariantsCharacterEquiv_map {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (f : rho.IntertwiningMap tau) (x : GroupLike L (TensorProduct k L ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho))) :

(TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv tau) ((TauCeti.GroupLike.map (Bialgebra.TensorProduct.map (BialgHom.id L L) f.groupAlgebraInvariantsBialgHom)) x) = Multiplicative.ofAdd (f (Multiplicative.toAdd ((TauCeti.GaloisDescent.groupAlgebraInvariantsCharacterEquiv rho) x)))

The character comparison is natural for descended morphisms: their map on characters is the original equivariant map on exponents.

source

@[simp]

theorem Representation.IntertwiningMap.groupAlgebraInvariantsCharacterMap_groupAlgebraInvariantsBialgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (f : rho.IntertwiningMap tau) :

f.groupAlgebraInvariantsBialgHom.groupAlgebraInvariantsCharacterMap = f

Recovering the character map of a descended morphism returns the original map.

source

@[simp]

theorem BialgHom.groupAlgebraInvariantsBialgHom_groupAlgebraInvariantsCharacterMap {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (F : ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐc[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau)) :

F.groupAlgebraInvariantsCharacterMap.groupAlgebraInvariantsBialgHom = F

Descending the recovered character map returns the original Hopf algebra morphism. In particular, every morphism between the descended groups is induced by a character map.

source

noncomputable def Representation.groupAlgebraInvariantsBialgHomEquiv {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field k] [Field L] [Algebra k L] [FiniteDimensional k L] [IsGalois k L] [AddCommGroup M] [AddCommGroup N] (rho : Representation ℤ Gal(L/k) M) (tau : Representation ℤ Gal(L/k) N) :

rho.IntertwiningMap tau ≃ (↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐc[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau))

Full faithfulness of finite Galois descent for group algebras. Equivariant homomorphisms of exponent groups correspond bijectively to morphisms of their descended coordinate Hopf algebras. No finiteness or torsion-freeness assumption on the exponent groups is needed.

Equations