Module

AlgebraicInertiaCentrality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AlgebraicInertiaCentrality

2 declarations indexed from sourceView source ↗

Module documentation

Central Galois elements from finite inertia

Over a Henselian base of residue characteristic zero containing all p-power roots, finite p-group inertia yields central restrictions at larger finite layers and a nonidentity central element of the absolute Galois group.

Imports6

Imported by2

theorem

exists_inertia_with_finite_central_restriction

L29 ↗

RamificationTheory.HilbertRamification.ValuationSubring.exists_inertia_with_finite_central_restriction

Documentation

A p-power-order finite inertia lift gives a central Galois automorphism at any larger finite layer, with the prescribed restriction downstairs.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsGalois K L]

Lean source · statement

theorem exists_inertia_with_finite_central_restriction
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    [CharZero (IsLocalRing.ResidueField A)]
    (p : ℕ) [Fact p.Prime]
    (hroots : ∀ n : ℕ, ∃ ζ : K, IsPrimitiveRoot ζ (p ^ n))
    (E F : FiniteGaloisIntermediateField K L) (hEF : E ≤ F)
    (hE : IsPGroup p (inertiaGroup K (A.comap E.toIntermediateField.val.toRingHom)))
    (τ : inertiaGroup K (A.comap E.toIntermediateField.val.toRingHom)) :
    ∃ σ : inertiaGroup K A, finiteInertiaRestriction A E σ = τ ∧
      ∀ g : Gal(F/K), Commute g
        ((inertiaGroupToAut (K := K) A σ).restrictNormal F)

theorem

exists_ne_one_mem_center_of_finite_inertia_pGroup

L83 ↗

RamificationTheory.HilbertRamification.ValuationSubring.exists_ne_one_mem_center_of_finite_inertia_pGroup