Module

ResidueZeroInertiaDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.ResidueZeroInertiaDetection

2 declarations indexed from sourceView source ↗

Module documentation

Kummer detection of inertia in residue characteristic zero

A nonidentity inertia element in a prime-degree Galois extension supplies a primitive root. Every primary root descends to the base, and finite residual primary roots make the existing roots-downstairs Kummer detection applicable.

Imports5

Imported by2

theorem

residueZero_inertia_exists_moved_h1

L34 ↗

Yamaguchi26AbfaithfulGalois.residueZero_inertia_exists_moved_h1

Documentation

In a prime-degree Galois extension with residue characteristic zero, every nonidentity inertia element moves a continuous degree-one Kummer class when the residual primary roots are finite.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v w
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem residueZero_inertia_exists_moved_h1
    [CharZero K] [FiniteDimensional K L] [IsGalois K L]
    (F : HenselianDVF.{v, w} L) [CharZero F.residueField]
    {p : ℕ} (hp : p.Prime) (hdeg : Module.finrank K L = p)
    [Finite (CommGroup.primaryComponent F.residueFieldˣ p)]
    (τ : inertiaGroup K F.valuation.valuationSubring) (hτ : τ ≠ 1) :
    ∃ s : ℕ, 1 ≤ s ∧ (primitiveRoots (p ^ s) L).Nonempty ∧
      (∀ m : ℕ, (primitiveRoots (p ^ m) L).Nonempty → m ≤ s) ∧
      ∃ c : ClassFieldTower.ProP.ContinuousH1ZMod
          (p := p ^ s) (G := Field.absoluteGaloisGroup L),
        ∃ σ : Gal(AlgebraicClosure L/L),
          c (Additive.ofMul
              (absoluteGaloisConjugate
                ((τ : decompositionGroup K F.valuation.valuationSubring) :
                  Gal(L/K)).toRingEquiv σ : Field.absoluteGaloisGroup L)) ≠
            c (Additive.ofMul (σ : Field.absoluteGaloisGroup L))

theorem

residueZero_inertia_abelianization_action_ne_one

L100 ↗

Yamaguchi26AbfaithfulGalois.residueZero_inertia_abelianization_action_ne_one