NYLL
Module

RelativeUnramifiedFixedField.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.RelativeUnramifiedFixedField
17 declarations indexed from sourceView source ↗

Module documentation

Relative unramified extensions inside a fixed separable closure

The relative unramified extension is realized as a named fixed field. Its inclusion and algebra structure are compared with the relative field, and its degree, residue degree, Galois property, and unramified valuation extension are recorded.

Imports15
Imported by2

Declarations

theorem

valuationInteger_scalarTower

L39 ↗
LocalClassFieldTheory.valuationInteger_scalarTower
Source context 5 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
Lean source · statement
theorem valuationInteger_scalarTower
    (A B C : Type) [Field A] [Field B] [Field C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    [ValuativeRel A] [ValuativeRel B] [ValuativeRel C]
    [Valuation.HasExtension (ValuativeRel.valuation A) (ValuativeRel.valuation B)]
    [Valuation.HasExtension (ValuativeRel.valuation B) (ValuativeRel.valuation C)]
    [Valuation.HasExtension (ValuativeRel.valuation A) (ValuativeRel.valuation C)] :
    IsScalarTower 𝒪[A] 𝒪[B] 𝒪[C]
theorem

valuationResidue_scalarTower

L51 ↗
LocalClassFieldTheory.valuationResidue_scalarTower
Source context 5 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
Lean source · statement
theorem valuationResidue_scalarTower
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
    [IsLocalRing A] [IsLocalRing B] [IsLocalRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    [IsLocalHom (algebraMap A B)] [IsLocalHom (algebraMap B C)]
    [IsLocalHom (algebraMap A C)] :
    IsScalarTower (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)
      (IsLocalRing.ResidueField C)
theorem

valuationResidue_finrank_mul

L60 ↗
LocalClassFieldTheory.valuationResidue_finrank_mul
Source context 5 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
Lean source · statement
theorem valuationResidue_finrank_mul
    (A B C : Type*) [CommRing A] [CommRing B] [CommRing C]
    [IsLocalRing A] [IsLocalRing B] [IsLocalRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
    [IsLocalHom (algebraMap A B)] [IsLocalHom (algebraMap B C)]
    [IsLocalHom (algebraMap A C)] :
    (@Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B) _ _
      (IsLocalRing.ResidueField.instModule (R := A) (S := B))) *
    (@Module.finrank (IsLocalRing.ResidueField B) (IsLocalRing.ResidueField C) _ _
      (IsLocalRing.ResidueField.instModule (R := B) (S := C))) =
    (@Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField C) _ _
      (IsLocalRing.ResidueField.instModule (R := A) (S := C)))
abbrev

relativeUnramifiedFiniteExtension

L85 ↗
LocalClassFieldTheory.relativeUnramifiedFiniteExtension
Documentation

The canonical unramified degree kernel over an absolutely finite field, with finiteness of its upper endpoint obtained from the actual quotient tower.

Source context 6 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
abbrev relativeUnramifiedFiniteExtension
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    FiniteAbstractFieldExtension (Gal(SeparableClosure K / K))
abbrev

relativeUnramifiedFixedField

L96 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField
Documentation

The actual fixed field, retained in the original K-separable closure.

Source context 6 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
abbrev relativeUnramifiedFixedField
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) : IntermediateField K (SeparableClosure K)
def

relativeUnramifiedFixedField_inclusion

L103 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_inclusion
Documentation

The canonical inclusion of the lower fixed field in the unramified field.

Source context 6 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def relativeUnramifiedFixedField_inclusion
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    abstractFixedField K (SeparableClosure K) H.field →ₐ[K]
      relativeUnramifiedFixedField K H m hm
def

relativeUnramifiedFixedField_algebra

L114 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_algebra
Documentation

The lower-field scalar structure is exactly the actual field inclusion.

Source context 6 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def relativeUnramifiedFixedField_algebra
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    Algebra (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)
def

relativeUnramifiedFixedField_equivRelative

L121 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_equivRelative
Source context 6 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
def relativeUnramifiedFixedField_equivRelative
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    letI := relativeUnramifiedFixedField_algebra K H m hm
    relativeUnramifiedFixedField K H m hm ≃ₐ[
      abstractFixedField K (SeparableClosure K) H.field]
      abstractRelativeFixedField K (SeparableClosure K) (K := H.field)
        (relativeUnramifiedFiniteExtension K H m hm).below := by
  letI := relativeUnramifiedFixedField_algebra K H m hm
  exact {
    toFun := fun x => ⟨x.1, x.2⟩
    invFun := fun x => ⟨x.1, x.2⟩
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl
    commutes' := fun _ => rfl }
theorem

relativeUnramifiedFixedField_scalarTower

L141 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_scalarTower
Source context 7 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
Lean source · statement
theorem relativeUnramifiedFixedField_scalarTower
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    IsScalarTower K (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)
theorem

relativeUnramifiedFixedField_absoluteFiniteDimensional

L151 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_absoluteFiniteDimensional
Documentation

The fixed field is an actual finite extension of the original local field.

Source context 8 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
Lean source · statement
theorem relativeUnramifiedFixedField_absoluteFiniteDimensional
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    FiniteDimensional K (relativeUnramifiedFixedField K H m hm)
theorem

relativeUnramifiedFixedField_finiteDimensional

L160 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_finiteDimensional
Documentation

The relative unramified fixed field is an actual finite extension.

Source context 8 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
Lean source · statement
theorem relativeUnramifiedFixedField_finiteDimensional
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    FiniteDimensional (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)
theorem

relativeUnramifiedFixedField_finrank

L171 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_finrank
Documentation

The actual relative fixed field has exactly the prescribed degree.

Source context 8 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
Lean source · statement
theorem relativeUnramifiedFixedField_finrank
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    Module.finrank (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm) = m
theorem

relativeUnramifiedFixedField_isGalois

L192 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_isGalois
Documentation

Normality of the actual reduction kernel makes its relative fixed field Galois.

Source context 8 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
Lean source · statement
theorem relativeUnramifiedFixedField_isGalois
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    IsGalois (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)
theorem

relativeUnramifiedFixedField_integer_isLocalHom

L206 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_integer_isLocalHom
Source context 8 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
Lean source · statement
theorem relativeUnramifiedFixedField_integer_isLocalHom
    (H : FiniteAbstractField (Gal(SeparableClosure K/K))) (m : ℕ) (hm : 0 < m)
    [ValuativeRel (abstractFixedField K (SeparableClosure K) H.field)]
    [ValuativeRel (relativeUnramifiedFixedField K H m hm)]
    [Valuation.HasExtension
      (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))
      (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))] :
    IsLocalHom (algebraMap
      𝒪[abstractFixedField K (SeparableClosure K) H.field]
      𝒪[relativeUnramifiedFixedField K H m hm])
theorem

relativeUnramifiedFixedField_faithfulSMul

L245 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_faithfulSMul
Source context 12 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
attribute [local instance] relativeUnramifiedFixedField_integer_isLocalHom
section Residue
variable (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
  (m : ℕ) (hm : 0 < m)
variable [ValuativeRel (abstractFixedField K (SeparableClosure K) H.field)]
  [TopologicalSpace (abstractFixedField K (SeparableClosure K) H.field)]
  [IsNonarchimedeanLocalField (abstractFixedField K (SeparableClosure K) H.field)]
  [ValuativeRel (relativeUnramifiedFixedField K H m hm)]
  [TopologicalSpace (relativeUnramifiedFixedField K H m hm)]
  [IsNonarchimedeanLocalField (relativeUnramifiedFixedField K H m hm)]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
  [Valuation.HasExtension
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
Lean source · statement
theorem relativeUnramifiedFixedField_faithfulSMul
    (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
    (m : ℕ) (hm : 0 < m) :
    FaithfulSMul (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)
theorem

relativeUnramifiedFixedField_residue_finrank

L260 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_residue_finrank
Documentation

The residue field of the actual relative degree-kernel extension also has exactly the prescribed degree, for its compatible local valuations.

Source context 13 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
attribute [local instance] relativeUnramifiedFixedField_integer_isLocalHom
section Residue
variable (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
  (m : ℕ) (hm : 0 < m)
variable [ValuativeRel (abstractFixedField K (SeparableClosure K) H.field)]
  [TopologicalSpace (abstractFixedField K (SeparableClosure K) H.field)]
  [IsNonarchimedeanLocalField (abstractFixedField K (SeparableClosure K) H.field)]
  [ValuativeRel (relativeUnramifiedFixedField K H m hm)]
  [TopologicalSpace (relativeUnramifiedFixedField K H m hm)]
  [IsNonarchimedeanLocalField (relativeUnramifiedFixedField K H m hm)]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
  [Valuation.HasExtension
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
attribute [local instance] relativeUnramifiedFixedField_faithfulSMul
Lean source · statement
theorem relativeUnramifiedFixedField_residue_finrank :
    @Module.finrank 𝓀[abstractFixedField K (SeparableClosure K) H.field]
      𝓀[relativeUnramifiedFixedField K H m hm] _ _
        (IsLocalRing.ResidueField.instModule
          (R := 𝒪[abstractFixedField K (SeparableClosure K) H.field])
          (S := 𝒪[relativeUnramifiedFixedField K H m hm])) = m
theorem

relativeUnramifiedFixedField_isUnramifiedValuedExtension

L316 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_isUnramifiedValuedExtension
Documentation

The relative degree-kernel fixed field is unramified for the compatible local valuations, as witnessed by its actual maximal-ideal ramification index.

Source context 13 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open ClassFormation LocalFieldTheory CyclicCohomology
open LocalFieldTheory.IsNonarchimedeanLocalField
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_algebra
attribute [local instance] relativeUnramifiedFixedField_scalarTower
attribute [local instance] relativeUnramifiedFixedField_integer_isLocalHom
section Residue
variable (H : FiniteAbstractField (Gal(SeparableClosure K/K)))
  (m : ℕ) (hm : 0 < m)
variable [ValuativeRel (abstractFixedField K (SeparableClosure K) H.field)]
  [TopologicalSpace (abstractFixedField K (SeparableClosure K) H.field)]
  [IsNonarchimedeanLocalField (abstractFixedField K (SeparableClosure K) H.field)]
  [ValuativeRel (relativeUnramifiedFixedField K H m hm)]
  [TopologicalSpace (relativeUnramifiedFixedField K H m hm)]
  [IsNonarchimedeanLocalField (relativeUnramifiedFixedField K H m hm)]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
  [Valuation.HasExtension
    (ValuativeRel.valuation (abstractFixedField K (SeparableClosure K) H.field))
    (ValuativeRel.valuation (relativeUnramifiedFixedField K H m hm))]
attribute [local instance] relativeUnramifiedFixedField_faithfulSMul
Lean source · statement
theorem relativeUnramifiedFixedField_isUnramifiedValuedExtension
    [FiniteDimensional (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)]
    [Module.Finite 𝒪[(abstractFixedField K (SeparableClosure K) H.field)]
      𝒪[(relativeUnramifiedFixedField K H m hm)]] :
    IsUnramifiedValuedExtension (abstractFixedField K (SeparableClosure K) H.field)
      (relativeUnramifiedFixedField K H m hm)

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