NYLL
Module

UnramifiedComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedComparison
18 declarations indexed from sourceView source ↗

Module documentation

Abstract and concrete unramified Frobenius

This module compares the residue-degree construction on a fixed separable closure with the ordinary unramified valuation extension and its arithmetic Frobenius.

Comparison of unramifiedness

Frobenius normalization

Imports5
Imported by5

Declarations

abbrev

absoluteGalois

L33 ↗
LocalClassFieldTheory.absoluteGalois
Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
Lean source · statement
abbrev absoluteGalois (K : Type) [Field K]
abbrev

abstractBase

L36 ↗
LocalClassFieldTheory.abstractBase
Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
Lean source · statement
abbrev abstractBase (K : Type) [Field K] :
    ClosedSubgroup (absoluteGalois K)
def

finiteResidueAbstractBase

L40 ↗
LocalClassFieldTheory.finiteResidueAbstractBase
Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
Lean source · statement
def finiteResidueAbstractBase
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    DegreeData.FiniteResidueAbstractField (localResidueDatum K)
theorem

intrinsicFiniteAbstractBase_residueDegree_eq_one

L53 ↗
LocalClassFieldTheory.intrinsicFiniteAbstractBase_residueDegree_eq_one
Documentation

The intrinsic finite abstract base has residue degree one for the local datum.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseResidueDegree
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem intrinsicFiniteAbstractBase_residueDegree_eq_one :
    ((intrinsicFiniteAbstractBase K).residueDegree (localResidueDatum K) : ℕ) = 1
theorem

finiteResidueAbstractBase_residueDegree_eq_one

L59 ↗
LocalClassFieldTheory.finiteResidueAbstractBase_residueDegree_eq_one
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseResidueDegree
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem finiteResidueAbstractBase_residueDegree_eq_one :
    ((finiteResidueAbstractBase K).residueDegree : ℕ) = 1
def

abstractBaseFrobeniusLift

L72 ↗
LocalClassFieldTheory.abstractBaseFrobeniusLift
Documentation

The chosen degree-one lift used in the abstract unramified Frobenius.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseFrobeniusLift
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def abstractBaseFrobeniusLift :
    (abstractBase K).toSubgroup
theorem

abstractBaseFrobeniusLift_normalizedDegree

L79 ↗
LocalClassFieldTheory.abstractBaseFrobeniusLift_normalizedDegree
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseFrobeniusLift
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem abstractBaseFrobeniusLift_normalizedDegree :
    (localResidueDatum K).normalizedDegree
        (finiteResidueAbstractBase K)
        (abstractBaseFrobeniusLift K) =
      Multiplicative.ofAdd (1 : ZHat)
theorem

abstractBaseFrobeniusLift_degree

L89 ↗
LocalClassFieldTheory.abstractBaseFrobeniusLift_degree
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseFrobeniusLift
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem abstractBaseFrobeniusLift_degree :
    localResidueDegree K (abstractBaseFrobeniusLift K).1 =
      Multiplicative.ofAdd (1 : ZHat)
theorem

localSeparableResidueAlgAction_eq_frobenius_of_degree_one

L103 ↗
LocalClassFieldTheory.localSeparableResidueAlgAction_eq_frobenius_of_degree_one
Documentation

A degree-one element of the local absolute Galois group acts by the arithmetic Frobenius on the selected residue algebraic closure.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section BaseFrobeniusLift
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localSeparableResidueAlgAction_eq_frobenius_of_degree_one
    (sigma : Gal((SeparableClosure K)/K))
    (hsigma : localResidueDegree K sigma =
      Multiplicative.ofAdd (1 : ZHat)) :
    localSeparableResidueAlgAction K sigma =
      FiniteField.frobeniusAlgEquivOfAlgebraic
        (decompositionResidueField K (localSeparableValuationSubring K))
        (selectedResidueField (localSeparableValuationSubring K))
instance

comparisonIntegerRingIsIntegralClosure

L138 ↗
LocalClassFieldTheory.comparisonIntegerRingIsIntegralClosure
Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
Lean source · statement
instance comparisonIntegerRingIsIntegralClosure :
    IsIntegralClosure 𝒪[L] 𝒪[K] L
instance

finiteGaloisLocalField_integerRing_moduleFinite

L145 ↗
LocalClassFieldTheory.finiteGaloisLocalField_integerRing_moduleFinite
Documentation

A finite Galois extension of nonarchimedean local fields has a finite extension of valuation integer rings. The integral-closure proof is derived from the chosen valuation extension, rather than exposed as an assumption.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
Lean source · statement
instance finiteGaloisLocalField_integerRing_moduleFinite :
    Module.Finite 𝒪[K] 𝒪[L]
theorem

localSeparableValuationSubring_comap_embedding

L163 ↗
LocalClassFieldTheory.localSeparableValuationSubring_comap_embedding
Documentation

Pulling the selected extension valuation on Kˢᵉᵖ back along a finite separable embedding gives the given local valuation on the source field.

Source context 13 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
omit [TopologicalSpace L] [IsNonarchimedeanLocalField L] [IsGalois K L]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] in
open _root_.ValuationTheory.DiscreteValuationField.Valuation
  (hasExtension_valuation_of_valuationSubring_pullback) in
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (exists_integralClosure_standard_fundamental_identity
   target_valuationSubring_eq_of_finite_separable) in
Lean source · statement
theorem localSeparableValuationSubring_comap_embedding
    [Algebra.IsSeparable K L] :
    (localSeparableValuationSubring K).comap i.toRingHom =
      (ValuativeRel.valuation L).valuationSubring
def

finiteGaloisResidueEmbeddingOfEmbedding

L206 ↗
LocalClassFieldTheory.finiteGaloisResidueEmbeddingOfEmbedding
Documentation

Reduction of an embedded finite extension into the selected residue algebraic closure used by localResidueDatum.

Source context 11 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
omit [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] in
Lean source · statement
def finiteGaloisResidueEmbeddingOfEmbedding :
    𝓀[L] →+*
      selectedResidueField (localSeparableValuationSubring K)
theorem

finiteGaloisResidueEmbeddingOfEmbedding_residue

L226 ↗
LocalClassFieldTheory.finiteGaloisResidueEmbeddingOfEmbedding_residue
Documentation

The residue embedding is reduction of the original field embedding.

Source context 11 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
omit [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] in
Lean source · full declaration
theorem finiteGaloisResidueEmbeddingOfEmbedding_residue
    (x : 𝒪[L]) :
    finiteGaloisResidueEmbeddingOfEmbedding K L i
        (IsLocalRing.residue 𝒪[L] x) =
      IsLocalRing.residue (localSeparableValuationSubring K)
        (⟨i (x : L), by
          have hx : (x : L) ∈
              (localSeparableValuationSubring K).comap i.toRingHom := by
            rw [localSeparableValuationSubring_comap_embedding K L i]
            exact x.property
          exact hx⟩ : localSeparableValuationSubring K) := by
  simp only [finiteGaloisResidueEmbeddingOfEmbedding]
  rfl
theorem

finiteGaloisResidueEmbeddingOfEmbedding_equivariant

L243 ↗
LocalClassFieldTheory.finiteGaloisResidueEmbeddingOfEmbedding_equivariant
Documentation

The concrete residue action is the restriction of the selected absolute residue action along the chosen finite Galois embedding.

Source context 11 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
omit [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] in
Lean source · statement
theorem finiteGaloisResidueEmbeddingOfEmbedding_equivariant
    (τ : (abstractBase K).toSubgroup) (x : 𝓀[L]) :
    finiteGaloisResidueEmbeddingOfEmbedding K L i
        (galoisGroupResidueAlgEquivOfIsIntegralClosure K L
          (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i
            (QuotientGroup.mk τ)) x) =
      localSeparableResidueAlgAction K τ.1
        (finiteGaloisResidueEmbeddingOfEmbedding K L i x)
theorem

finiteGaloisAbstractExtensionOfEmbedding_isUnramified

L301 ↗
LocalClassFieldTheory.finiteGaloisAbstractExtensionOfEmbedding_isUnramified
Documentation

An actually unramified finite Galois extension gives an unramified extension for the abstract local residue datum.

Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
Lean source · statement
theorem finiteGaloisAbstractExtensionOfEmbedding_isUnramified :
    (finiteGaloisAbstractExtensionOfEmbedding K L i).IsUnramified
      (localResidueDatum K)
theorem

finiteGaloisResidueBaseExtension_normal

L365 ↗
LocalClassFieldTheory.finiteGaloisResidueBaseExtension_normal
Source context 12 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
section AbstractUnramifiedFrobenius
omit [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] in
Lean source · statement
theorem finiteGaloisResidueBaseExtension_normal :
    (extensionSubgroup (finiteResidueAbstractBase K).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).below).Normal
theorem

finiteGaloisAbstractUnramifiedFrobenius_eq_arithmeticFrobenius

L376 ↗
LocalClassFieldTheory.finiteGaloisAbstractUnramifiedFrobenius_eq_arithmeticFrobenius
Documentation

Under the field-facing quotient equivalence, the abstract degree-one unramified Frobenius is the actual arithmetic Frobenius of the unramified valuation extension.

Source context 12 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open RamificationTheory.HilbertRamification.ValuationSubring
section
variable (K L : Type)
  [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)]
variable
  [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
variable (i : L →ₐ[K] SeparableClosure K)
section AbstractUnramifiedFrobenius
attribute [local instance] finiteGaloisResidueBaseExtension_normal
Lean source · statement
theorem finiteGaloisAbstractUnramifiedFrobenius_eq_arithmeticFrobenius :
    finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i
        ((localResidueDatum K).unramifiedFrobenius
          (finiteResidueAbstractBase K)
          (finiteGaloisAbstractExtensionOfEmbedding K L i).field
          (finiteGaloisAbstractExtensionOfEmbedding K L i).below) =
      arithmeticFrobeniusOfUnramifiedValuation K L

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