Functoriality of geometric character groups

A morphism of commutative Hopf algebras sends group-like elements to group-like elements after extension to an algebraic closure. This gives a morphism between geometric character groups. The map is equivariant for the absolute-Galois actions because scalar extension applies the Hopf map only to the second tensor factor.

The resulting additive maps assemble the geometric character groups into a functor from commutative Hopf algebras to integral representations of the absolute Galois group. Restricting this functor to coordinate rings of tori is the character-lattice functor used in Galois descent.

Main declarations

• TauCeti.CommHopfAlgCat.geometricCharacterMap: the map on geometric characters induced by a Hopf-algebra morphism.
• TauCeti.CommHopfAlgCat.additiveCharacterMap: its integral-linear additive form.
• TauCeti.CommHopfAlgCat.geometricCharacterRepresentation: the absolute-Galois representation on geometric characters.
• TauCeti.CommHopfAlgCat.geometricCharacterFunctor: functoriality of that representation.

References

See J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.

noncomputable def TauCeti.CommHopfAlgCat.geometricCharacterMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : geometricCharacterGroup H →* geometricCharacterGroup K

A morphism of commutative Hopf algebras induces a homomorphism of their geometric character groups by scalar extension and restriction to group-like elements.

Equations

• TauCeti.CommHopfAlgCat.geometricCharacterMap f = TauCeti.GroupLike.map (CommHopfAlgCat.Hom.hom (TauCeti.CommHopfAlgCat.baseChangeMap f))

theorem TauCeti.CommHopfAlgCat.geometricCharacterMap_eq_groupLikeMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : geometricCharacterMap f = GroupLike.map (CommHopfAlgCat.Hom.hom (baseChangeMap f))

The geometric character map is the group-like map of the base-changed morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.val_geometricCharacterMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : geometricCharacterGroup H) : ↑((geometricCharacterMap f) x) = (CommHopfAlgCat.Hom.hom (baseChangeMap f)) ↑x

The value underlying the image of a geometric character is obtained by applying the base-changed Hopf-algebra morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterMap_smul {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (sigma : Field.absoluteGaloisGroup k) (x : geometricCharacterGroup H) : (geometricCharacterMap f) (sigma • x) = sigma • (geometricCharacterMap f) x

The map on geometric characters commutes with the absolute-Galois action.

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterMap_id {k : Type u} [Field k] (H : CommHopfAlgCat k) : geometricCharacterMap (CategoryTheory.CategoryStruct.id H) = MonoidHom.id (geometricCharacterGroup H)

Mapping geometric characters along an identity morphism is the identity.

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterMap_comp {k : Type u} [Field k] {H K L : CommHopfAlgCat k} (f : H ⟶ K) (g : K ⟶ L) : geometricCharacterMap (CategoryTheory.CategoryStruct.comp f g) = (geometricCharacterMap g).comp (geometricCharacterMap f)

Mapping geometric characters respects composition of Hopf-algebra morphisms.

noncomputable def TauCeti.CommHopfAlgCat.additiveCharacterMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : additiveCharacterGroup H →ₗ[ℤ] additiveCharacterGroup K

The integral-linear map on additive geometric character groups induced by a Hopf-algebra morphism.

Equations

• TauCeti.CommHopfAlgCat.additiveCharacterMap f = (MonoidHom.toAdditive (TauCeti.CommHopfAlgCat.geometricCharacterMap f)).toIntLinearMap

@[simp]

theorem TauCeti.CommHopfAlgCat.toMul_additiveCharacterMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : additiveCharacterGroup H) : Additive.toMul ((additiveCharacterMap f) x) = (geometricCharacterMap f) (Additive.toMul x)

Passing to the underlying multiplicative character identifies additiveCharacterMap with geometricCharacterMap.

@[simp]

theorem TauCeti.CommHopfAlgCat.additiveCharacterMap_smul {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (sigma : Field.absoluteGaloisGroup k) (x : additiveCharacterGroup H) : (additiveCharacterMap f) (sigma • x) = sigma • (additiveCharacterMap f) x

The additive character map is equivariant for the absolute-Galois action.

@[simp]

theorem TauCeti.CommHopfAlgCat.additiveCharacterMap_id {k : Type u} [Field k] (H : CommHopfAlgCat k) : additiveCharacterMap (CategoryTheory.CategoryStruct.id H) = LinearMap.id

The additive character map of an identity morphism is the identity linear map.

@[simp]

theorem TauCeti.CommHopfAlgCat.additiveCharacterMap_comp {k : Type u} [Field k] {H K L : CommHopfAlgCat k} (f : H ⟶ K) (g : K ⟶ L) : additiveCharacterMap (CategoryTheory.CategoryStruct.comp f g) = additiveCharacterMap g ∘ₗ additiveCharacterMap f

Additive character maps respect composition of Hopf-algebra morphisms.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.geometricCharacterRepresentation {k : Type u} [Field k] (H : CommHopfAlgCat k) : Rep ℤ (Field.absoluteGaloisGroup k)

The geometric character group as an integral representation of the absolute Galois group.

Equations

• TauCeti.CommHopfAlgCat.geometricCharacterRepresentation H = Rep.ofMulDistribMulAction (Field.absoluteGaloisGroup k) (TauCeti.CommHopfAlgCat.geometricCharacterGroup H)

theorem TauCeti.CommHopfAlgCat.geometricCharacterRepresentation_ρ_apply {k : Type u} [Field k] (H : CommHopfAlgCat k) (sigma : Field.absoluteGaloisGroup k) (x : additiveCharacterGroup H) : ((geometricCharacterRepresentation H).ρ sigma) x = sigma • x

The action map of the geometric-character representation is the scalar action on additive characters.

noncomputable def TauCeti.CommHopfAlgCat.geometricCharacterRepresentationMap {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : geometricCharacterRepresentation H ⟶ geometricCharacterRepresentation K

The equivariant morphism of geometric-character representations induced by a Hopf-algebra morphism.

Equations

• TauCeti.CommHopfAlgCat.geometricCharacterRepresentationMap f = Rep.ofHom (TauCeti.CommHopfAlgCat.additiveCharacterIntertwiningMap✝ f)

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterRepresentationMap_hom_apply {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : additiveCharacterGroup H) : (Rep.Hom.hom (geometricCharacterRepresentationMap f)) x = (additiveCharacterMap f) x

Evaluation of the representation morphism induced on geometric characters.

noncomputable def TauCeti.CommHopfAlgCat.geometricCharacterFunctor {k : Type u} [Field k] : CategoryTheory.Functor (CommHopfAlgCat k) (Rep ℤ (Field.absoluteGaloisGroup k))

Geometric character groups and their absolute-Galois actions are functorial in the coordinate Hopf algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterFunctor_obj {k : Type u} [Field k] (H : CommHopfAlgCat k) : geometricCharacterFunctor.obj H = geometricCharacterRepresentation H

The object part of geometricCharacterFunctor is the geometric-character representation.

@[simp]

theorem TauCeti.CommHopfAlgCat.geometricCharacterFunctor_map {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) : geometricCharacterFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (geometricCharacterRepresentationMap f) (CategoryTheory.eqToHom ⋯))

The morphism part of geometricCharacterFunctor is the induced equivariant character map.