Module

AlgebraicGaloisOrbits.lean

Nyll.GaloisCohomology.Topology.AlgebraicGaloisOrbits

2 declarations indexed from sourceView source ↗

Module documentation

Locally constant orbit maps in algebraic Galois groups

A single algebraic element is fixed by an open subgroup. Its orbit map, and the induced orbit map on units, are locally constant in the Krull topology.

Imports2

Mathlib.FieldTheory.KrullTopology
Mathlib.Topology.LocallyConstant.Basic

Imported by3

theorem

isLocallyConstant_galois_apply

L25 ↗

GaloisCohomology.isLocallyConstant_galois_apply

Documentation

Evaluation at an algebraic element is locally constant.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Pointwise
namespace GaloisCohomology
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
  [Algebra.IsIntegral K Ω]

Lean source · full declaration

theorem isLocallyConstant_galois_apply (x : Ω) :
    IsLocallyConstant (fun σ : Gal(Ω/K) => σ x) := by
  apply (IsLocallyConstant.iff_exists_open _).mpr
  intro σ
  let E : IntermediateField K Ω := IntermediateField.adjoin K {x}
  have : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
  refine ⟨σ • (E.fixingSubgroup : Set Gal(Ω/K)),
    E.fixingSubgroup_isOpen.leftCoset σ, ?_, ?_⟩
  · exact ⟨1, E.fixingSubgroup.one_mem, mul_one σ⟩
  · rintro τ ⟨ρ, hρ, rfl⟩
    have hfix : ρ x = x :=
      (IntermediateField.mem_fixingSubgroup_iff E ρ).mp hρ x
        (IntermediateField.mem_adjoin_simple_self K x)
    change σ (ρ x) = σ x
    exact congrArg σ hfix

theorem

isLocallyConstant_galois_units

L43 ↗

GaloisCohomology.isLocallyConstant_galois_units