NYLL
Module

HenselianResidueAction.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianResidueAction
12 declarations indexed from sourceView source ↗

Module documentation

Full residue Galois action over a Henselian valued field

Reduction acts on the actual residue-field algebra. Fixed integers descend to the base field, identifying the scalars needed for residue surjectivity. Finite residue bases lift to finitely many algebraic field elements, proving Krull continuity. Reduction is an open quotient with the actual inertia kernel.

Imports7
Imported by6

Declarations

theorem

canonical_hasExtension

L38 ↗
RamificationTheory.HilbertRamification.ValuationSubring.canonical_hasExtension
Source context 5 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
omit [IsGalois K L] [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)] in
Lean source · statement
theorem canonical_hasExtension :
    v.valuationSubring.valuation.HasExtension w.valuationSubring.valuation
def

henselianGalToDecomposition

L49 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianGalToDecomposition
Documentation

Over a Henselian base the full Galois group acts on the chosen valuation.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · full declaration
def henselianGalToDecomposition : Gal(L/K) →* decompositionGroup K w.valuationSubring where
  toFun σ := ⟨σ, by
    have := canonical_hasExtension v w
    rw [decompositionGroup_eq_top_of_henselianRing v.valuationSubring w.valuationSubring]
    exact Subgroup.mem_top σ⟩
  map_one' := rfl
  map_mul' _ _ := rfl
def

henselianResidueAction

L58 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction
Documentation

The actual full residue action over the canonical residue-field algebra.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · full declaration
def henselianResidueAction : Gal(L/K) →*
    Gal(ResidueField w.valuationSubring / ResidueField v.valuationSubring) where
  toFun σ :=
    { residueAction K w.valuationSubring (henselianGalToDecomposition v w σ) with
      commutes' := by
        intro z
        obtain ⟨a, rfl⟩ := residue_surjective z
        rw [_root_.Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap]
        change residue w.valuationSubring
          ((henselianGalToDecomposition v w σ) •
            algebraMap v.valuationSubring w.valuationSubring a) =
          residue w.valuationSubring (algebraMap v.valuationSubring w.valuationSubring a)
        apply congrArg (residue w.valuationSubring)
        apply Subtype.ext
        exact σ.commutes (a : K) }
  map_one' := by
    apply AlgEquiv.ext
    intro z
    exact congrArg
      (fun f : ResidueField w.valuationSubring ≃+* ResidueField w.valuationSubring => f z)
      ((residueAction K w.valuationSubring).map_one)
  map_mul' σ τ := by
    apply AlgEquiv.ext
    intro z
    exact congrArg
      (fun f : ResidueField w.valuationSubring ≃+* ResidueField w.valuationSubring => f z)
      ((residueAction K w.valuationSubring).map_mul
        (henselianGalToDecomposition v w σ) (henselianGalToDecomposition v w τ))
theorem

henselianResidueAction_residue

L87 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_residue
Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueAction_residue (σ : Gal(L/K)) (x : w.valuationSubring) :
    henselianResidueAction v w σ (residue w.valuationSubring x) =
      residue w.valuationSubring ((henselianGalToDecomposition v w σ) • x)
theorem

decompositionResidue_scalar_range_subset_base

L91 ↗
RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidue_scalar_range_subset_base
Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem decompositionResidue_scalar_range_subset_base :
    Set.range (algebraMap (decompositionResidueField K w.valuationSubring)
      (ResidueField w.valuationSubring)) ⊆
      Set.range
        (algebraMap (ResidueField v.valuationSubring) (ResidueField w.valuationSubring))
theorem

henselianResidueAction_surjective

L118 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_surjective
Documentation

Every automorphism of the actual residue extension lifts to a field Galois automorphism over a Henselian base.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueAction_surjective : Function.Surjective (henselianResidueAction v w)
theorem

henselianResidueExtension_isIntegral

L137 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueExtension_isIntegral
Documentation

The actual residue extension of an algebraic Galois extension of a Henselian valued field is algebraic.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueExtension_isIntegral :
    Algebra.IsIntegral (ResidueField v.valuationSubring) (ResidueField w.valuationSubring)
theorem

henselianResidueExtension_isAlgClosure

L165 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueExtension_isAlgClosure
Documentation

The chosen residue of an algebraic closure is an algebraic closure of the actual base residue field.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueExtension_isAlgClosure [IsAlgClosed L] :
    IsAlgClosure (ResidueField v.valuationSubring) (ResidueField w.valuationSubring)
theorem

henselianResidueAction_continuous

L171 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_continuous
Documentation

The actual residue action is continuous for the Krull topologies.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueAction_continuous : Continuous (henselianResidueAction v w)
def

henselianResidueContinuousHom

L207 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueContinuousHom
Documentation

Full reduction, bundled as a continuous homomorphism.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
def henselianResidueContinuousHom : Gal(L/K) →ₜ*
    Gal(ResidueField w.valuationSubring / ResidueField v.valuationSubring)
theorem

henselianResidueAction_ker

L212 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_ker
Documentation

The kernel of full reduction consists exactly of the actual inertia elements.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueAction_ker :
    (henselianResidueAction v w).ker =
      (inertiaGroup K w.valuationSubring).comap (henselianGalToDecomposition v w)
theorem

henselianResidueAction_isOpenQuotientMap

L228 ↗
RamificationTheory.HilbertRamification.ValuationSubring.henselianResidueAction_isOpenQuotientMap
Documentation

The full residue action is an open quotient map.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.ValuationSubring
open IsLocalRing
variable {K L Γ Δ : Type*} [Field K] [Field L] [Algebra K L]
  [LinearOrderedCommGroupWithZero Γ] [LinearOrderedCommGroupWithZero Δ]
  (v : _root_.Valuation K Γ) (w : _root_.Valuation L Δ) [v.HasExtension w]
  [IsGalois K L]
  [HenselianRing v.valuationSubring (maximalIdeal v.valuationSubring)]
Lean source · statement
theorem henselianResidueAction_isOpenQuotientMap :
    IsOpenQuotientMap (henselianResidueAction v w)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.