Continuity of the absolute-Galois action on geometric characters

For a commutative Hopf algebra H over a field k, the geometric character group X*(H) carries the discrete topology. Its absolute-Galois action is continuous for the Krull topology. Indeed, every element of the scalar extension k̄ ⊗[k] H is a finite sum of pure tensors. The finitely many scalar coefficients lie in finite extensions of k, so their common fixing subgroup is open and fixes the tensor. The same is therefore true for each group-like element.

For tori, this makes the finite free character lattice constructed in TauCeti.Algebra.AlgebraicGroup.Torus.CharacterLattice.Basic a continuous discrete Galois module.

Main declarations

• TauCeti.CommHopfAlgCat.instTopologicalSpaceGeometricCharacterGroup: the discrete topology on geometric characters.
• TauCeti.CommHopfAlgCat.stabilizer_groupLike_isOpen: every scalar-extended group-like stabilizer is open.
• TauCeti.CommHopfAlgCat.instContinuousSMulGeometricCharacterGroup: continuity of the absolute-Galois action.
• TauCeti.CommHopfAlgCat.stabilizer_additiveGroupLike_isOpen: every additive group-like stabilizer is open.
• TauCeti.CommHopfAlgCat.instContinuousSMulAdditiveCharacterGroup: continuity of the additive character-lattice action.

References

See J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17, for the character lattice of a torus as a continuous Galois module.

@[instance_reducible]

noncomputable instance TauCeti.CommHopfAlgCat.instTopologicalSpaceGeometricCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) : TopologicalSpace (geometricCharacterGroup H)

The geometric character group carries its natural discrete topology.

Equations

• TauCeti.CommHopfAlgCat.instTopologicalSpaceGeometricCharacterGroup H = ⊥

instance TauCeti.CommHopfAlgCat.instDiscreteTopologyGeometricCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) : DiscreteTopology (geometricCharacterGroup H)

The topology on the geometric character group is discrete.

theorem TauCeti.CommHopfAlgCat.stabilizer_groupLike_isOpen {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] (x : GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)) : IsOpen ↑(MulAction.stabilizer (Field.absoluteGaloisGroup k) x)

The stabilizer of every group-like element after scalar extension is open.

theorem TauCeti.CommHopfAlgCat.continuousSMul_groupLike {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] [TopologicalSpace (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))] [DiscreteTopology (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))] : ContinuousSMul (Field.absoluteGaloisGroup k) (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))

The absolute-Galois action on scalar-extended group-like elements is continuous whenever they carry the discrete topology.

instance TauCeti.CommHopfAlgCat.instContinuousSMulGeometricCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) : ContinuousSMul (Field.absoluteGaloisGroup k) (geometricCharacterGroup H)

The absolute-Galois action on geometric characters is continuous for the Krull topology and the discrete topology on the character group.

theorem TauCeti.CommHopfAlgCat.stabilizer_additiveGroupLike_isOpen {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] (x : Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A))) : IsOpen ↑(MulAction.stabilizer (Field.absoluteGaloisGroup k) x)

The stabilizer of every additive group-like element after scalar extension is open.

theorem TauCeti.CommHopfAlgCat.continuousSMul_additiveGroupLike {k : Type u} [Field k] {A : Type v} [Semiring A] [Bialgebra k A] [TopologicalSpace (Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)))] [DiscreteTopology (Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)))] : ContinuousSMul (Field.absoluteGaloisGroup k) (Additive (GroupLike (AlgebraicClosure k) (TensorProduct k (AlgebraicClosure k) A)))

The absolute-Galois action on additive scalar-extended group-like elements is continuous whenever they carry the discrete topology.

instance TauCeti.CommHopfAlgCat.instContinuousSMulAdditiveCharacterGroup {k : Type u} [Field k] (H : CommHopfAlgCat k) : ContinuousSMul (Field.absoluteGaloisGroup k) (additiveCharacterGroup H)

The additive character group carries the continuous action transported from geometric characters.