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, and the pointwise form for a single element integral over K, with no hypothesis on the extension L/K: the orbit map σ ↦ σ x is locally constant.

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).
• IsIntegral.isLocallyConstant_apply: for x integral over K, the orbit map σ ↦ σ x on Gal(L/K) is locally constant.
• IntermediateField.isOpen_ker_comp_restrictNormalHom: a character of Gal(E/K) for a finite normal intermediate field E, read on Gal(L/K) through restriction, has open kernel.

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.

theorem IsIntegral.isLocallyConstant_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : IsLocallyConstant fun (σ : Gal(L/K)) => σ x

The orbit map of an integral element is locally constant for the Krull topology: near σ₀ lie the automorphisms σ₀ * τ with τ fixing the finite extension K⟮x⟯, and these all send x to σ₀ x. Unlike stabilizer_isOpen_of_isIntegral, nothing is asked of L / K, so L may be transcendental over K.

theorem IntermediateField.isOpen_ker_comp_restrictNormalHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {A : Type u_3} [AddGroup A] (E : IntermediateField K L) [FiniteDimensional K ↥E] [Normal K ↥E] (χ : Additive Gal(↥E/K) →+ A) : IsOpen ↑(χ.comp (MonoidHom.toAdditive (AlgEquiv.restrictNormalHom ↥E))).ker

A character of a finite normal layer has open kernel: a character of Gal(E/K) for a finite normal intermediate field E, read on Gal(L/K) through restriction to E, vanishes on the open subgroup fixing E.