Module

ResidueExtension.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ResidueExtension

37 declarations indexed from sourceView source ↗

Module documentation

Residue extensions

Constructs the maps induced on valuation rings, residue fields, and residue units by a valued extension, with degree, trace, norm, and Frobenius results.

Imports12

Mathlib.SetTheory.Cardinal.Finite
Mathlib.FieldTheory.Finite.GaloisField
Mathlib.LinearAlgebra.Dimension.DivisionRing
Mathlib.NumberTheory.RamificationInertia.Inertia
Mathlib.NumberTheory.RamificationInertia.Ramification
Mathlib.RingTheory.Ideal.Norm.AbsNorm
Mathlib.RingTheory.RamificationInertia.Basic
Mathlib.RingTheory.SimpleModule.Basic
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.Trace.Basic
Mathlib.RingTheory.Valuation.Extension
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.ResidueUnits

Imported by8

def

integerRingMapOfValuationExtension

L36 ↗

LocalFieldTheory.integerRingMapOfValuationExtension

Documentation

The local-ring homomorphism on valuation integer rings induced by an extension of valuations.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerRingMapOfValuationExtension (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    𝒪[K] →+* 𝒪[L]

instance

integerRingMapOfValuationExtension_isLocalHom

L43 ↗

LocalFieldTheory.integerRingMapOfValuationExtension_isLocalHom

Documentation

The map of valuation rings induced by a valued-field extension is a local ring homomorphism.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

instance integerRingMapOfValuationExtension_isLocalHom (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    IsLocalHom (integerRingMapOfValuationExtension K L)

theorem

integerRingMapOfValuationExtension_apply

L52 ↗

LocalFieldTheory.integerRingMapOfValuationExtension_apply

Documentation

The valuation-ring map of an extension is the ambient algebra map on underlying elements.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRingMapOfValuationExtension_apply (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : 𝒪[K]) :
    integerRingMapOfValuationExtension K L x = algebraMap 𝒪[K] 𝒪[L] x

def

residueFieldMapOfValuationExtension

L63 ↗

LocalFieldTheory.residueFieldMapOfValuationExtension

Documentation

The residue-field map induced by a valuation extension. This is the canonical algebraMap 𝓀[K] 𝓀[L], named so later local class field theory files can use it without unfolding mathlib's valuation-extension instances.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def residueFieldMapOfValuationExtension (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    𝓀[K] →+* 𝓀[L]

theorem

residueFieldMapOfValuationExtension_eq_algebraMap

L71 ↗

LocalFieldTheory.residueFieldMapOfValuationExtension_eq_algebraMap

Documentation

The map between residue fields induced by a valued extension agrees with the residue-field algebra map.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueFieldMapOfValuationExtension_eq_algebraMap (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    residueFieldMapOfValuationExtension K L = algebraMap 𝓀[K] 𝓀[L]

theorem

residueFieldMapOfValuationExtension_residue

L80 ↗

LocalFieldTheory.residueFieldMapOfValuationExtension_residue

Documentation

The residue-field map sends the residue of a base integer to the residue of its image in the extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueFieldMapOfValuationExtension_residue (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : 𝒪[K]) :
    residueFieldMapOfValuationExtension K L (IsLocalRing.residue 𝒪[K] x) =
      IsLocalRing.residue 𝒪[L] (integerRingMapOfValuationExtension K L x)

theorem

residueField_algebraMap_residue

L90 ↗

LocalFieldTheory.residueField_algebraMap_residue

Documentation

The residue-field algebra map commutes with reduction of valuation-ring elements.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueField_algebraMap_residue (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : 𝒪[K]) :
    algebraMap 𝓀[K] 𝓀[L] (IsLocalRing.residue 𝒪[K] x) =
      IsLocalRing.residue 𝒪[L] (algebraMap 𝒪[K] 𝒪[L] x)

def

residueUnitsMapOfValuationExtension

L99 ↗

LocalFieldTheory.residueUnitsMapOfValuationExtension

Documentation

The induced map on residue-field unit groups.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def residueUnitsMapOfValuationExtension (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    𝓀[K]ˣ →* 𝓀[L]ˣ

theorem

residueUnitsMapOfValuationExtension_apply

L108 ↗

LocalFieldTheory.residueUnitsMapOfValuationExtension_apply

Documentation

The induced map on residue-field units applies the residue-field extension map to the underlying residue.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueUnitsMapOfValuationExtension_apply (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝓀[K]ˣ) :
    ((residueUnitsMapOfValuationExtension K L u : 𝓀[L]ˣ) : 𝓀[L]) =
      algebraMap 𝓀[K] 𝓀[L] (u : 𝓀[K])

theorem

residueUnitsMapOfValuationExtension_injective

L117 ↗

LocalFieldTheory.residueUnitsMapOfValuationExtension_injective

Documentation

The induced map on residue-field unit groups is injective.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueUnitsMapOfValuationExtension_injective (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Function.Injective (residueUnitsMapOfValuationExtension K L)

def

integerUnitsMapOfValuationExtension

L124 ↗

LocalFieldTheory.integerUnitsMapOfValuationExtension

Documentation

Base integer units embedded into extension integer units.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsMapOfValuationExtension (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    𝒪[K]ˣ →* 𝒪[L]ˣ

theorem

integerUnitsMapOfValuationExtension_apply

L133 ↗

LocalFieldTheory.integerUnitsMapOfValuationExtension_apply

Documentation

The induced map on valuation-ring units applies the extension's integer-ring map to the underlying unit.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsMapOfValuationExtension_apply (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝒪[K]ˣ) :
    ((integerUnitsMapOfValuationExtension K L u : 𝒪[L]ˣ) : 𝒪[L]) =
      integerRingMapOfValuationExtension K L (u : 𝒪[K])

theorem

residueUnitsMap_integerUnitsToResidueUnits

L144 ↗

LocalFieldTheory.residueUnitsMap_integerUnitsToResidueUnits

Documentation

Mapping an integer unit to the extension and then reducing agrees with reducing first and mapping residue units.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueUnitsMap_integerUnitsToResidueUnits (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝒪[K]ˣ) :
    residueUnitsMapOfValuationExtension K L (integerUnitsToResidueUnits K u) =
      integerUnitsToResidueUnits L (integerUnitsMapOfValuationExtension K L u)

theorem

integerUnitsMapOfValuationExtension_mem_principalUnits_one

L154 ↗

LocalFieldTheory.integerUnitsMapOfValuationExtension_mem_principalUnits_one

Documentation

A first principal unit remains a first principal unit after extension of valued fields.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsMapOfValuationExtension_mem_principalUnits_one (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝒪[K]ˣ) (hu : u ∈ principalUnits K 1) :
    integerUnitsMapOfValuationExtension K L u ∈ principalUnits L 1

def

integerUnitsModPrincipalUnitsMapOfValuationExtension

L165 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsMapOfValuationExtension

Documentation

The map on integer-unit residue quotients induced by a valuation extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsModPrincipalUnitsMapOfValuationExtension (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    IntegerUnitsModPrincipalUnits K →* IntegerUnitsModPrincipalUnits L

theorem

integerUnitsModPrincipalUnitsMapOfValuationExtension_mk

L180 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsMapOfValuationExtension_mk

Documentation

The map modulo first principal units sends a class to the class of the extended integer unit.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsMapOfValuationExtension_mk (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsMapOfValuationExtension K L
        (integerUnitsModPrincipalUnitsMk K u) =
      integerUnitsModPrincipalUnitsMk L
        (integerUnitsMapOfValuationExtension K L u)

theorem

integerUnitsModPrincipalUnitsMap_residue_comm

L192 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsMap_residue_comm

Documentation

The quotient map modulo first principal units commutes with the residue-unit comparison equivalence.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsMap_residue_comm (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : IntegerUnitsModPrincipalUnits K) :
    integerUnitsModPrincipalUnitsEquivResidueUnits L
        (integerUnitsModPrincipalUnitsMapOfValuationExtension K L x) =
      residueUnitsMapOfValuationExtension K L
        (integerUnitsModPrincipalUnitsEquivResidueUnits K x)

theorem

principalUnits_one_of_integerUnitsMap_mem_principalUnits_one

L215 ↗

LocalFieldTheory.principalUnits_one_of_integerUnitsMap_mem_principalUnits_one

Documentation

If the extension of an integer unit is a first principal unit, its class modulo first principal units is trivial.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem principalUnits_one_of_integerUnitsMap_mem_principalUnits_one (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    {a : 𝒪[K]ˣ}
    (haL : integerUnitsMapOfValuationExtension K L a ∈ principalUnits L 1) :
    a ∈ principalUnits K 1

def

integerUnitsModPrincipalUnitsResidueNormOfValuationExtension

L233 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsResidueNormOfValuationExtension

Documentation

The residue-field norm transported to the integer-unit quotients 𝒪[L]ˣ/U_L¹ → 𝒪[K]ˣ/U_K¹.

This is not the local field norm on integer units; it is the quotient-level residue norm model used before proving compatibility with normIntegerUnits.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

def integerUnitsModPrincipalUnitsResidueNormOfValuationExtension (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    IntegerUnitsModPrincipalUnits L →* IntegerUnitsModPrincipalUnits K

theorem

integerUnitsModPrincipalUnitsResidueNorm_residue

L243 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsResidueNorm_residue

Documentation

The residue norm on classes modulo first principal units agrees with the finite residue-field norm.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsResidueNorm_residue (K L : Type u)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : IntegerUnitsModPrincipalUnits L) :
    integerUnitsModPrincipalUnitsEquivResidueUnits K
        (integerUnitsModPrincipalUnitsResidueNormOfValuationExtension K L x) =
      Units.map (Algebra.norm 𝓀[K] (S := 𝓀[L]))
        (integerUnitsModPrincipalUnitsEquivResidueUnits L x)

theorem

residueUnitsMap_residueField_norm_eq_prod_algEquiv

L262 ↗

LocalFieldTheory.residueUnitsMap_residueField_norm_eq_prod_algEquiv

Documentation

The finite-field residue norm, after base extension to 𝓀[L], is the product over all residue-field automorphisms.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem residueUnitsMap_residueField_norm_eq_prod_algEquiv (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝓀[L]ˣ) :
    residueUnitsMapOfValuationExtension K L
        (Units.map (Algebra.norm 𝓀[K] (S := 𝓀[L])) u) =
      Finset.univ.prod (fun τ : 𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L] =>
        Units.mapEquiv τ.toMulEquiv u) := by
  ext
  change algebraMap 𝓀[K] 𝓀[L] (Algebra.norm 𝓀[K] (u : 𝓀[L])) =
    ↑(Finset.univ.prod (fun τ : 𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L] =>
      Units.mapEquiv τ.toMulEquiv u))
  rw [Algebra.norm_eq_prod_automorphisms]
  simp

theorem

integerUnitsModPrincipalUnitsResidueNorm_base_extend_eq_prod_algEquiv

L281 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsResidueNorm_base_extend_eq_prod_algEquiv

Documentation

Quotient-level form of residueUnitsMap_residueField_norm_eq_prod_algEquiv.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · full declaration

theorem integerUnitsModPrincipalUnitsResidueNorm_base_extend_eq_prod_algEquiv
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (x : IntegerUnitsModPrincipalUnits L) :
    residueUnitsMapOfValuationExtension K L
        (integerUnitsModPrincipalUnitsEquivResidueUnits K
          (integerUnitsModPrincipalUnitsResidueNormOfValuationExtension K L x)) =
      Finset.univ.prod (fun τ : 𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L] =>
        Units.mapEquiv τ.toMulEquiv (integerUnitsModPrincipalUnitsEquivResidueUnits L x)) := by
  rw [integerUnitsModPrincipalUnitsResidueNorm_residue]
  exact residueUnitsMap_residueField_norm_eq_prod_algEquiv K L
    (integerUnitsModPrincipalUnitsEquivResidueUnits L x)

theorem

residueAlgEquiv_card_eq_finrank

L299 ↗

LocalFieldTheory.residueAlgEquiv_card_eq_finrank

Documentation

The residue-field automorphism group has order the finite residue-field extension degree.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueAlgEquiv_card_eq_finrank (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Nat.card (𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L]) = Module.finrank 𝓀[K] 𝓀[L]

theorem

maximalIdeal_inertiaDeg_eq_residue_finrank

L310 ↗

LocalFieldTheory.maximalIdeal_inertiaDeg_eq_residue_finrank

Documentation

The mathlib inertia degree of the maximal ideals agrees with the concrete degree of the canonical residue-field extension supplied by a valuation extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_inertiaDeg_eq_residue_finrank (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    (𝓂[L] : Ideal 𝒪[L]).inertiaDeg 𝒪[K] =
      Module.finrank 𝓀[K] 𝓀[L]

theorem

residueAlgEquiv_card_eq_maximalIdeal_inertiaDeg

L322 ↗

LocalFieldTheory.residueAlgEquiv_card_eq_maximalIdeal_inertiaDeg

Documentation

The residue-field automorphism group has order the mathlib inertia degree of the maximal ideals for the canonical valuation-ring extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueAlgEquiv_card_eq_maximalIdeal_inertiaDeg (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Nat.card (𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L]) =
      (𝓂[L] : Ideal 𝒪[L]).inertiaDeg 𝒪[K]

theorem

integerRing_moduleFinite_of_isIntegralClosure

L335 ↗

LocalFieldTheory.integerRing_moduleFinite_of_isIntegralClosure

Documentation

Finite separable extensions whose valuation ring is the integral closure of the base valuation ring give a finite module extension of valuation integer rings.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRing_moduleFinite_of_isIntegralClosure (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [Algebra K L] [FiniteDimensional K L]
    [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Module.Finite 𝒪[K] 𝒪[L]

theorem

integerRing_algebra_isIntegral_of_isIntegralClosure

L347 ↗

LocalFieldTheory.integerRing_algebra_isIntegral_of_isIntegralClosure

Documentation

If the extension valuation ring is the integral closure of the base valuation ring, then the induced extension of valuation integer rings is integral.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerRing_algebra_isIntegral_of_isIntegralClosure (K L : Type u)
    [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Algebra.IsIntegral 𝒪[K] 𝒪[L]

theorem

maximalIdeal_ramificationIdx_mul_inertiaDeg_eq_finrank

L357 ↗

LocalFieldTheory.maximalIdeal_ramificationIdx_mul_inertiaDeg_eq_finrank

Documentation

The actual ramification index and inertia degree of the valuation-integer ring extension satisfy the local ramification identity.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_ramificationIdx_mul_inertiaDeg_eq_finrank (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    Ideal.ramificationIdx' (𝓂[K] : Ideal 𝒪[K]) (𝓂[L] : Ideal 𝒪[L]) *
      (𝓂[L] : Ideal 𝒪[L]).inertiaDeg 𝒪[K] =
        Module.finrank K L

theorem

maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank

L383 ↗

LocalFieldTheory.maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank

Documentation

The local ramification identity with the inertia degree rewritten as the finite-dimensional degree of the canonical residue-field extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    Ideal.ramificationIdx' (𝓂[K] : Ideal 𝒪[K]) (𝓂[L] : Ideal 𝒪[L]) *
      Module.finrank 𝓀[K] 𝓀[L] =
        Module.finrank K L

theorem

maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank_of_isIntegralClosure

L402 ↗

LocalFieldTheory.maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank_of_isIntegralClosure

Documentation

finite extensions of discrete valuations, finite-extension degree formula with module-finiteness generated from the actual integral-closure hypothesis.

This is the source-producing form used by later local CFT files: the finite 𝒪[K]-module structure on 𝒪[L] is produced from integral closure and separability, not exposed as a separate theorem-shaped input.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem maximalIdeal_ramificationIdx_mul_residue_finrank_eq_finrank_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    Ideal.ramificationIdx' (𝓂[K] : Ideal 𝒪[K]) (𝓂[L] : Ideal 𝒪[L]) *
      Module.finrank 𝓀[K] 𝓀[L] =
        Module.finrank K L

theorem

residue_finrank_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure

L422 ↗

LocalFieldTheory.residue_finrank_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure

Documentation

finite extensions of discrete valuations: in an unramified finite valuation extension, the residue degree is the full field degree.

The ramification-index-one input is the mathematical unramified datum. The finite 𝒪[K]-module structure is still generated from integral closure and separability, rather than being exposed as a separate hypothesis.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residue_finrank_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (h :
      Ideal.ramificationIdx' (𝓂[K] : Ideal 𝒪[K]) (𝓂[L] : Ideal 𝒪[L]) = 1) :
    Module.finrank 𝓀[K] 𝓀[L] = Module.finrank K L

theorem

residueAlgEquiv_card_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure

L440 ↗

LocalFieldTheory.residueAlgEquiv_card_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure

Documentation

The residue-field automorphism group has order the full field degree in an unramified finite valuation extension, with finite valuation-ring module-finiteness generated from integral closure.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueAlgEquiv_card_eq_finrank_of_ramificationIdx_eq_one_of_isIntegralClosure
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (h :
      Ideal.ramificationIdx' (𝓂[K] : Ideal 𝒪[K]) (𝓂[L] : Ideal 𝒪[L]) = 1) :
    Nat.card (𝓀[L] ≃ₐ[𝓀[K]] 𝓀[L]) = Module.finrank K L

theorem

residueFieldAlgebra_isSeparable_of_valuationExtension

L454 ↗

LocalFieldTheory.residueFieldAlgebra_isSeparable_of_valuationExtension

Documentation

The residue-field extension supplied by a local-field valuation extension is separable.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueFieldAlgebra_isSeparable_of_valuationExtension (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Algebra.IsSeparable 𝓀[K] 𝓀[L]

theorem

residueField_trace_surjective_of_valuationExtension

L464 ↗

LocalFieldTheory.residueField_trace_surjective_of_valuationExtension

Documentation

The trace map for the canonical residue-field extension supplied by a valuation extension is surjective.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueField_trace_surjective_of_valuationExtension (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Function.Surjective (Algebra.trace 𝓀[K] 𝓀[L])

theorem

residueField_units_norm_surjective_of_valuationExtension

L476 ↗

LocalFieldTheory.residueField_units_norm_surjective_of_valuationExtension

Documentation

The finite-field norm on residue-field units is surjective for the canonical residue extension induced by a valuation extension.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueField_units_norm_surjective_of_valuationExtension (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Function.Surjective (Units.map (Algebra.norm 𝓀[K] (S := 𝓀[L])))

theorem

residueField_units_norm_surjective_of_valuationExtension_apply

L487 ↗

LocalFieldTheory.residueField_units_norm_surjective_of_valuationExtension_apply

Documentation

The chosen right inverse to the residue-field unit norm maps back to the prescribed residue unit.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem residueField_units_norm_surjective_of_valuationExtension_apply
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (u : 𝓀[K]ˣ) :
    ∃ v : 𝓀[L]ˣ, Units.map (Algebra.norm 𝓀[K] (S := 𝓀[L])) v = u

theorem

integerUnitsModPrincipalUnitsResidueNorm_surjective_of_valuationExtension

L498 ↗

LocalFieldTheory.integerUnitsModPrincipalUnitsResidueNorm_surjective_of_valuationExtension

Documentation

The residue norm on integer units modulo first principal units is surjective.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel

Lean source · statement

theorem integerUnitsModPrincipalUnitsResidueNorm_surjective_of_valuationExtension
    (K L : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    Function.Surjective
      (integerUnitsModPrincipalUnitsResidueNormOfValuationExtension K L)

Module documentation

Residue extensions

Declarations