Continuous Galois modules attached to a group of multiplicative type

The character and cocharacter groups of a group of multiplicative type carry mutually contragredient actions of the absolute Galois group. The character action is already known to be continuous for the Krull topology and the discrete topology on the group. This file proves the corresponding statement for cocharacters.

The key point is finite generation. Choose a finite generating family of the character group. The intersection of the open stabilizers of its generators fixes every character, hence fixes every functional on the character group under the contragredient action. This open subgroup therefore lies in the stabilizer of any prescribed cocharacter.

Main declarations

• TauCeti.MultiplicativeTypeCommHopfAlgCat.instDistribMulActionCocharacterLattice: the contragredient absolute-Galois action on cocharacters.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.stabilizer_cocharacterLattice_isOpen: every cocharacter has open stabilizer.
• TauCeti.MultiplicativeTypeCommHopfAlgCat.instContinuousSMulCocharacterLattice: the cocharacter group is a continuous discrete Galois module.

References

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

For a torus these groups are finite free lattices with a perfect pairing, so this completes the continuous character--cocharacter Galois-module interface in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap. The later absolute root datum will use these two continuous lattices together with their Galois-invariant perfect pairing.

@[instance_reducible]

noncomputable instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instDistribMulActionCocharacterLattice {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : DistribMulAction (Field.absoluteGaloisGroup k) T.cocharacterLattice

The absolute Galois group acts on the cocharacter group through the contragredient representation.

Equations

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

@[simp]

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.cocharacterLattice_smul_def {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (σ : Field.absoluteGaloisGroup k) (f : T.cocharacterLattice) : σ • f = (T.cocharacterGaloisRepresentation σ) f

Scalar multiplication on the cocharacter lattice is the existing contragredient Galois representation.

@[instance_reducible]

noncomputable instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instTopologicalSpaceCocharacterLattice {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : TopologicalSpace T.cocharacterLattice

The cocharacter lattice carries the discrete topology.

Equations

• T.instTopologicalSpaceCocharacterLattice = ⊥

instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instDiscreteTopologyCocharacterLattice {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : DiscreteTopology T.cocharacterLattice

The topology on the cocharacter lattice is discrete.

theorem TauCeti.MultiplicativeTypeCommHopfAlgCat.stabilizer_cocharacterLattice_isOpen {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) (f : T.cocharacterLattice) : IsOpen ↑(MulAction.stabilizer (Field.absoluteGaloisGroup k) f)

The stabilizer of every cocharacter of a group of multiplicative type is open in the absolute Galois group.

instance TauCeti.MultiplicativeTypeCommHopfAlgCat.instContinuousSMulCocharacterLattice {k : Type u} [Field k] (T : MultiplicativeTypeCommHopfAlgCat k) : ContinuousSMul (Field.absoluteGaloisGroup k) T.cocharacterLattice

The contragredient absolute-Galois action on the cocharacter lattice is continuous for the Krull topology and the discrete topology on the lattice.