Stabilizers for the Krull topology are open

Mathlib/FieldTheory/KrullTopology.lean supplies the Krull topology on Gal(L/K) together with stabilizer_isOpen_of_isIntegral, the fact that a point of an integral extension L/K has an open stabilizer. This file draws the consequence for a unit of L, an automorphism fixing a unit being exactly one that fixes the underlying element.

Through Mathlib's continuousSMul_iff_stabilizer_isOpen this is what makes the units of an algebraic extension a discrete module over the Galois group, in the sense continuous cohomology asks for; TauCeti.unitsCoeff_continuousSMul is that consequence for a separable closure.

Main results

• TauCeti.stabilizer_isOpen_units: the stabilizer of a unit of L is an open subgroup of Gal(L/K).

theorem TauCeti.stabilizer_isOpen_units {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] (u : Lˣ) : IsOpen ↑(MulAction.stabilizer Gal(L/K) u)

The stabilizer of a unit of an integral extension is open: an automorphism fixes a unit exactly when it fixes the underlying element.