NYLL
Module

UnramifiedFrobenius.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.UnramifiedFrobenius
26 declarations indexed from sourceView source ↗

Module documentation

Actual unramified Frobenius

The arithmetic Frobenius is first defined as finite-field Frobenius on the residue extension, then lifted to Gal(L / K) through the canonical residue-action isomorphism for a finite unramified extension.

Imports6
Imported by12

Declarations

def

residueExtensionArithmeticFrobeniusOfValuationExtension

L36 ↗
LocalFieldTheory.residueExtensionArithmeticFrobeniusOfValuationExtension
Documentation

Arithmetic Frobenius of the actual residue-field extension supplied by a valuation extension. This is finite Galois ramification theory's finite-field Frobenius, applied to the canonical residue extension 𝓀[L]/𝓀[K].

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def residueExtensionArithmeticFrobeniusOfValuationExtension
    (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] ≃ₐ[𝓀[K]] 𝓀[L]
theorem

residueExtensionArithmeticFrobeniusOfValuationExtension_apply

L48 ↗
LocalFieldTheory.residueExtensionArithmeticFrobeniusOfValuationExtension_apply
Documentation

The arithmetic Frobenius of a finite residue extension raises each residue element to the size of the base residue field.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem residueExtensionArithmeticFrobeniusOfValuationExtension_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)]
    (x : 𝓀[L]) :
    residueExtensionArithmeticFrobeniusOfValuationExtension K L x =
      x ^ Nat.card 𝓀[K]
theorem

residueExtensionArithmeticFrobeniusOfValuationExtension_preserves_base

L64 ↗
LocalFieldTheory.residueExtensionArithmeticFrobeniusOfValuationExtension_preserves_base
Documentation

Arithmetic Frobenius fixes the image of the base residue field.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem residueExtensionArithmeticFrobeniusOfValuationExtension_preserves_base
    (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 : 𝓀[K]) :
    residueExtensionArithmeticFrobeniusOfValuationExtension K L
        (algebraMap 𝓀[K] 𝓀[L] x) =
      algebraMap 𝓀[K] 𝓀[L] x
theorem

orderOf_residueExtensionArithmeticFrobeniusOfValuationExtension

L79 ↗
LocalFieldTheory.orderOf_residueExtensionArithmeticFrobeniusOfValuationExtension
Documentation

The order of residue arithmetic Frobenius is the degree of the finite residue-field extension.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem orderOf_residueExtensionArithmeticFrobeniusOfValuationExtension
    (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)] :
    orderOf (residueExtensionArithmeticFrobeniusOfValuationExtension K L) =
      Module.finrank 𝓀[K] 𝓀[L]
theorem

orderOf_residueExtensionArithmeticFrobeniusOfUnramifiedValuation

L94 ↗
LocalFieldTheory.orderOf_residueExtensionArithmeticFrobeniusOfUnramifiedValuation
Documentation

For an unramified valued extension, residue arithmetic Frobenius has order equal to the field-extension degree.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem orderOf_residueExtensionArithmeticFrobeniusOfUnramifiedValuation
    (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]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    orderOf (residueExtensionArithmeticFrobeniusOfValuationExtension K L) =
      Module.finrank K L
theorem

residueExtensionArithmeticFrobeniusOfValuationExtension_generates

L108 ↗
LocalFieldTheory.residueExtensionArithmeticFrobeniusOfValuationExtension_generates
Documentation

Arithmetic Frobenius generates the automorphism group of a finite residue-field extension.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem residueExtensionArithmeticFrobeniusOfValuationExtension_generates
    (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] ≃ₐ[𝓀[K]] 𝓀[L],
      σ ∈ Subgroup.zpowers (residueExtensionArithmeticFrobeniusOfValuationExtension K L)
def

arithmeticFrobeniusOfUnramifiedValuation

L129 ↗
LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation
Documentation

Actual arithmetic Frobenius in Gal(L / K), obtained by lifting the residue finite-field Frobenius through the already constructed unramified residue-action isomorphism.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def arithmeticFrobeniusOfUnramifiedValuation
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Gal(L / K)
theorem

galoisGroupEquivResidueAlgEquivOfUnramifiedValuationOfIsIntegralClosure_arithmeticFrobenius

L144 ↗
LocalFieldTheory.galoisGroupEquivResidueAlgEquivOfUnramifiedValuationOfIsIntegralClosure_arithmeticFrobenius
Documentation

The unramified Galois-residue equivalence lifts residue arithmetic Frobenius to field arithmetic Frobenius.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroupEquivResidueAlgEquivOfUnramifiedValuationOfIsIntegralClosure_arithmeticFrobenius
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    galoisGroupEquivResidueAlgEquivOfUnramifiedValuationOfIsIntegralClosure K L
        (arithmeticFrobeniusOfUnramifiedValuation K L) =
      residueExtensionArithmeticFrobeniusOfValuationExtension K L
theorem

galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius

L159 ↗
LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius
Documentation

The residue action of field arithmetic Frobenius is residue arithmetic Frobenius.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    galoisGroupResidueAlgEquivOfIsIntegralClosure K L
        (arithmeticFrobeniusOfUnramifiedValuation K L) =
      residueExtensionArithmeticFrobeniusOfValuationExtension K L
theorem

galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius_apply

L177 ↗
LocalFieldTheory.galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius_apply
Documentation

Field arithmetic Frobenius acts on residues by raising them to the size of the base residue field.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroupResidueAlgEquivOfIsIntegralClosure_arithmeticFrobenius_apply
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (x : 𝓀[L]) :
    galoisGroupResidueAlgEquivOfIsIntegralClosure K L
        (arithmeticFrobeniusOfUnramifiedValuation K L) x =
      x ^ Nat.card 𝓀[K]
theorem

eq_of_simple_roots_of_residue_eq

L193 ↗
LocalFieldTheory.eq_of_simple_roots_of_residue_eq
Documentation

Two simple roots over a local domain with the same residue are equal.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem eq_of_simple_roots_of_residue_eq
    {R : Type*} [CommRing R] [IsDomain R] [IsLocalRing R]
    {f : Polynomial R} {a b : R}
    (ha : f.IsRoot a) (hb : f.IsRoot b)
    (hres : IsLocalRing.residue R b = IsLocalRing.residue R a)
    (hderiv : IsUnit (f.derivative.eval a)) :
    b = a
theorem

arithmeticFrobeniusOfUnramifiedValuation_apply_primitiveRoot

L239 ↗
LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation_apply_primitiveRoot
Documentation

Arithmetic Frobenius sends a primitive root of unity of order prime to the base residue cardinality to its residue-cardinality power.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem arithmeticFrobeniusOfUnramifiedValuation_apply_primitiveRoot
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    {n : Nat} {ζ : L} (hζ : IsPrimitiveRoot ζ n)
    (hcoprime : (Nat.card 𝓀[K]).Coprime n) :
    arithmeticFrobeniusOfUnramifiedValuation K L ζ =
      ζ ^ Nat.card 𝓀[K]
theorem

orderOf_arithmeticFrobeniusOfUnramifiedValuation

L348 ↗
LocalFieldTheory.orderOf_arithmeticFrobeniusOfUnramifiedValuation
Documentation

Arithmetic Frobenius in an unramified Galois extension has order equal to the extension degree.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem orderOf_arithmeticFrobeniusOfUnramifiedValuation
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    orderOf (arithmeticFrobeniusOfUnramifiedValuation K L) =
      Module.finrank K L
theorem

arithmeticFrobeniusOfUnramifiedValuation_generates

L367 ↗
LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation_generates
Documentation

Arithmetic Frobenius generates the Galois group of a finite unramified extension.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem arithmeticFrobeniusOfUnramifiedValuation_generates
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    ∀ σ : Gal(L / K),
      σ ∈ Subgroup.zpowers (arithmeticFrobeniusOfUnramifiedValuation K L)
theorem

arithmeticFrobeniusOfUnramifiedValuation_zpowers_eq_top

L388 ↗
LocalFieldTheory.arithmeticFrobeniusOfUnramifiedValuation_zpowers_eq_top
Documentation

The subgroup of integral powers of arithmetic Frobenius is the full Galois group.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem arithmeticFrobeniusOfUnramifiedValuation_zpowers_eq_top
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Subgroup.zpowers (arithmeticFrobeniusOfUnramifiedValuation K L) = ⊤
theorem

isCyclic_galoisGroup_of_unramifiedValuation

L401 ↗
LocalFieldTheory.isCyclic_galoisGroup_of_unramifiedValuation
Documentation

The Galois group of a finite unramified extension is cyclic.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem isCyclic_galoisGroup_of_unramifiedValuation
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    IsCyclic Gal(L / K)
theorem

galoisGroup_card_eq_finrank_of_unramifiedValuation

L417 ↗
LocalFieldTheory.galoisGroup_card_eq_finrank_of_unramifiedValuation
Documentation

The order of the actual unramified Galois group is the degree. This is the cardinality consequence of the normalized Frobenius construction: arithmetic Frobenius has order [L : K] and generates Gal(L/K).

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroup_card_eq_finrank_of_unramifiedValuation
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Nat.card Gal(L / K) = Module.finrank K L
def

galoisGroupEquivZModOfUnramifiedValuation

L434 ↗
LocalFieldTheory.galoisGroupEquivZModOfUnramifiedValuation
Documentation

A ZMod model of the unramified Galois group obtained from cyclicity and the order of arithmetic Frobenius. This equivalence does not prescribe which generator maps to 1; the normalized model below does.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def galoisGroupEquivZModOfUnramifiedValuation
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Gal(L / K) ≃* Multiplicative (ZMod (Module.finrank K L))
def

zmodAddEquivOfGenerator

L451 ↗
LocalFieldTheory.zmodAddEquivOfGenerator
Documentation

Internal quotient construction for a specified additive generator. The public local-field API below supplies horder and hgen from the already proved Frobenius source lemmas, so these hypotheses are not exposed as new endpoints.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def zmodAddEquivOfGenerator {A : Type*} [AddGroup A]
    (g : A) {n : Nat} (horder : addOrderOf g = n)
    (hgen : AddSubgroup.zmultiples g = ⊤) :
    ZMod n ≃+ A
theorem

zmodAddEquivOfGenerator_apply_one

L473 ↗
LocalFieldTheory.zmodAddEquivOfGenerator_apply_one
Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem zmodAddEquivOfGenerator_apply_one {A : Type*} [AddGroup A]
    (g : A) {n : Nat} (horder : addOrderOf g = n)
    (hgen : AddSubgroup.zmultiples g = ⊤) :
    zmodAddEquivOfGenerator g horder hgen (1 : ZMod n) = g
lemma

additive_zmultiples_eq_top_of_zpowers_eq_top

L489 ↗
LocalFieldTheory.additive_zmultiples_eq_top_of_zpowers_eq_top
Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
lemma additive_zmultiples_eq_top_of_zpowers_eq_top {G : Type*} [Group G]
    (g : G) (hgen : Subgroup.zpowers g = ⊤) :
    AddSubgroup.zmultiples (Additive.ofMul g) = ⊤
def

zmodCyclicMulEquivOfGenerator

L503 ↗
LocalFieldTheory.zmodCyclicMulEquivOfGenerator
Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def zmodCyclicMulEquivOfGenerator {G : Type*} [Group G]
    (g : G) {n : Nat} (horder : orderOf g = n)
    (hgen : Subgroup.zpowers g = ⊤) :
    Multiplicative (ZMod n) ≃* G
theorem

zmodCyclicMulEquivOfGenerator_apply_one

L512 ↗
LocalFieldTheory.zmodCyclicMulEquivOfGenerator_apply_one
Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem zmodCyclicMulEquivOfGenerator_apply_one {G : Type*} [Group G]
    (g : G) {n : Nat} (horder : orderOf g = n)
    (hgen : Subgroup.zpowers g = ⊤) :
    zmodCyclicMulEquivOfGenerator g horder hgen
      (Multiplicative.ofAdd (1 : ZMod n)) = g
def

galoisGroupEquivZModOfUnramifiedValuationNormalized

L529 ↗
LocalFieldTheory.galoisGroupEquivZModOfUnramifiedValuationNormalized
Documentation

The generator-normalized ZMod model of the actual unramified Galois group. Unlike galoisGroupEquivZModOfUnramifiedValuation, this quotient construction uses the specified arithmetic Frobenius as the generator, following the normalized Frobenius construction before the uniformizer/Frobenius calculation.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
def galoisGroupEquivZModOfUnramifiedValuationNormalized
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    Gal(L / K) ≃* Multiplicative (ZMod (Module.finrank K L))
theorem

galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius

L546 ↗
LocalFieldTheory.galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius
Documentation

The normalized equivalence from the unramified Galois group to ZMod sends arithmetic Frobenius to one.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    galoisGroupEquivZModOfUnramifiedValuationNormalized K L
        (arithmeticFrobeniusOfUnramifiedValuation K L) =
      Multiplicative.ofAdd (1 : ZMod (Module.finrank K L))
theorem

galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius_zpow

L574 ↗
LocalFieldTheory.galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius_zpow
Documentation

Power form of the generator-normalized Frobenius model. This is the Frobenius-side model used before composing with the valuation quotient.

Source context 5 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open _root_.LocalFieldTheory.IsNonarchimedeanLocalField
Lean source · statement
theorem galoisGroupEquivZModOfUnramifiedValuationNormalized_arithmeticFrobenius_zpow
    (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] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] (m : Int) :
    galoisGroupEquivZModOfUnramifiedValuationNormalized K L
        ((arithmeticFrobeniusOfUnramifiedValuation K L) ^ m) =
      Multiplicative.ofAdd (m : ZMod (Module.finrank K L))

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