NYLL
Module

UnramifiedCommonExtension.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.UnramifiedCommonExtension
11 declarations indexed from sourceView source ↗

Module documentation

Unramified common extensions and fixed-field composita

The relative unramified fixed field is identified with the compositum of the chosen intermediate fields. The comparison supplies its degree, Galois structure, residue degree, and unramified valuation extension.

Imports16
Imported by2

Declarations

abbrev

finiteAbstractFieldOfGaloisIntermediateField

L44 ↗
LocalClassFieldTheory.finiteAbstractFieldOfGaloisIntermediateField
Documentation

An actual finite Galois intermediate field gives its finite abstract fixed subgroup, with finiteness supplied by the actual Galois quotient.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
Lean source · full declaration
abbrev finiteAbstractFieldOfGaloisIntermediateField
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F] :
    FiniteAbstractField (Gal(SeparableClosure K / K)) where
  field := closedFixingSubgroup K (SeparableClosure K) F
  finite := by
    apply Nat.finite_of_card_ne_zero
    change F.fixingSubgroup.relIndex ⊤ ≠ 0
    rw [Subgroup.relIndex_top_right,
      ← IntermediateField.finrank_eq_fixingSubgroup_index (F := K) (SeparableClosure K) F]
    exact Module.finrank_pos.ne'
theorem

fixedField_finiteAbstractFieldOfGaloisIntermediateField

L57 ↗
LocalClassFieldTheory.fixedField_finiteAbstractFieldOfGaloisIntermediateField
Documentation

The abstract package returns precisely the original intermediate field.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
Lean source · statement
theorem fixedField_finiteAbstractFieldOfGaloisIntermediateField
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F] :
    abstractFixedField K (SeparableClosure K)
      (finiteAbstractFieldOfGaloisIntermediateField K F).field = F
theorem

finrank_inclusion_congr

L64 ↗
LocalClassFieldTheory.finrank_inclusion_congr
Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
Lean source · full declaration
theorem finrank_inclusion_congr
    (A B C D : IntermediateField K (SeparableClosure K))
    (hAB : A = B) (hCD : C = D) (hAC : A ≤ C) (hBD : B ≤ D) :
    letI : Algebra A C := (IntermediateField.inclusion hAC).toRingHom.toAlgebra
    letI : Algebra B D := (IntermediateField.inclusion hBD).toRingHom.toAlgebra
    Module.finrank A C = Module.finrank B D := by
  subst B
  subst D
  rfl
theorem

relativeUnramifiedFixedField_actual_eq_sup

L78 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_actual_eq_sup
Documentation

The relative degree-kernel field over an actual finite Galois field is the compositum with the standard unramified field of degree f * m.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · statement
theorem relativeUnramifiedFixedField_actual_eq_sup
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (m : ℕ) (hm : 0 < m) :
    relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm =
        F ⊔ localFiniteUnramifiedField K
          (((finiteAbstractFieldOfGaloisIntermediateField K F).residueDegree
            (localResidueDatum K) : ℕ) * m)
          (Nat.mul_pos
            ((finiteAbstractFieldOfGaloisIntermediateField K F).residueDegree
              (localResidueDatum K)).property hm)
theorem

relativeUnramifiedFixedField_actual_isGalois

L97 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_actual_isGalois
Documentation

Normality of the two actual factors makes the common field Galois also over the original local base.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · statement
theorem relativeUnramifiedFixedField_actual_isGalois
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (m : ℕ) (hm : 0 < m) :
    IsGalois K (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)
theorem

le_relativeUnramifiedFixedField_actual

L108 ↗
LocalClassFieldTheory.le_relativeUnramifiedFixedField_actual
Documentation

The original actual field embeds in its unramified common extension.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · statement
theorem le_relativeUnramifiedFixedField_actual
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (m : ℕ) (hm : 0 < m) :
    F ≤ relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm
theorem

relativeUnramifiedFixedField_actual_finrank

L119 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_actual_finrank
Documentation

The degree over the original actual field is the prescribed m, for its literal intermediate-field inclusion.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · full declaration
theorem relativeUnramifiedFixedField_actual_finrank
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (m : ℕ) (hm : 0 < m) :
    letI : Algebra F (relativeUnramifiedFixedField K
        (finiteAbstractFieldOfGaloisIntermediateField K F) m hm) :=
      (IntermediateField.inclusion
        (le_relativeUnramifiedFixedField_actual K F m hm)).toRingHom.toAlgebra
    Module.finrank F (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm) = m := by
  let H := finiteAbstractFieldOfGaloisIntermediateField K F
  let N := relativeUnramifiedFixedField K H m hm
  have hF : abstractFixedField K (SeparableClosure K) H.field = F :=
    fixedField_finiteAbstractFieldOfGaloisIntermediateField K F
  have hF0N : abstractFixedField K (SeparableClosure K) H.field ≤ N :=
    abstractFixedField_le K (SeparableClosure K)
      (relativeUnramifiedFiniteExtension K H m hm).below
  have hdegree := finrank_inclusion_congr K
    (abstractFixedField K (SeparableClosure K) H.field) F N N hF rfl hF0N
    (le_relativeUnramifiedFixedField_actual K F m hm)
  exact hdegree.symm.trans (relativeUnramifiedFixedField_finrank K H m hm)
def

relativeUnramifiedFixedField_actual_algebra

L144 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_actual_algebra
Documentation

Scalars from the original field act through its actual inclusion.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
Lean source · statement
def relativeUnramifiedFixedField_actual_algebra
    (F : IntermediateField K (SeparableClosure K))
    [FiniteDimensional K F] [IsGalois K F]
    (m : ℕ) (hm : 0 < m) :
    Algebra F (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)
theorem

finiteAbstractFieldOfGaloisIntermediateField_residueDegree

L164 ↗
LocalClassFieldTheory.finiteAbstractFieldOfGaloisIntermediateField_residueDegree
Documentation

The abstract absolute residue degree is the residue degree of the original actual intermediate field.

Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_actual_algebra
section BaseValuations
variable (F : IntermediateField K (SeparableClosure K))
  [FiniteDimensional K F] [IsGalois K F]
  [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
Lean source · statement
theorem finiteAbstractFieldOfGaloisIntermediateField_residueDegree :
    ((finiteAbstractFieldOfGaloisIntermediateField K F).residueDegree
      (localResidueDatum K) : ℕ) =
        @Module.finrank 𝓀[K] 𝓀[F] _ _
          (IsLocalRing.ResidueField.instModule (R := 𝒪[K]) (S := 𝒪[F]))
theorem

relativeUnramifiedFixedField_ramification_eq_sup_sameDegree

L187 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_ramification_eq_sup_sameDegree
Documentation

Choosing the actual ramification index as relative unramified degree makes the absolute standard factor have exactly the degree of F/K.

Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_actual_algebra
section BaseValuations
variable (F : IntermediateField K (SeparableClosure K))
  [FiniteDimensional K F] [IsGalois K F]
  [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
Lean source · statement
theorem relativeUnramifiedFixedField_ramification_eq_sup_sameDegree :
    ∃ he : 0 < (𝓂[F] : Ideal 𝒪[F]).ramificationIdx 𝒪[K],
      relativeUnramifiedFixedField K
        (finiteAbstractFieldOfGaloisIntermediateField K F)
        ((𝓂[F] : Ideal 𝒪[F]).ramificationIdx 𝒪[K]) he =
      F ⊔ localFiniteUnramifiedField K (Module.finrank K F) Module.finrank_pos
theorem

relativeUnramifiedFixedField_actual_isUnramifiedValuedExtension

L244 ↗
LocalClassFieldTheory.relativeUnramifiedFixedField_actual_isUnramifiedValuedExtension
Documentation

Unramifiedness over the literal original field, for the compatible valuations and the canonical inclusion of that field.

Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open ClassFormation CyclicCohomology RamificationTheory LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
open scoped ValuativeRel
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
attribute [local instance] relativeUnramifiedFixedField_actual_algebra
section ActualValuations
variable (F : IntermediateField K (SeparableClosure K))
  [FiniteDimensional K F] [IsGalois K F] (m : ℕ) (hm : 0 < m)
  [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
  [ValuativeRel (relativeUnramifiedFixedField K
    (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)]
  [TopologicalSpace (relativeUnramifiedFixedField K
    (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)]
  [IsNonarchimedeanLocalField (relativeUnramifiedFixedField K
    (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
  [Valuation.HasExtension (ValuativeRel.valuation K)
    (ValuativeRel.valuation (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm))]
  [Valuation.HasExtension (ValuativeRel.valuation F)
    (ValuativeRel.valuation (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm))]
Lean source · statement
theorem relativeUnramifiedFixedField_actual_isUnramifiedValuedExtension
    [FiniteDimensional F (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)]
    [Module.Finite 𝒪[F] 𝒪[relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm]] :
    IsUnramifiedValuedExtension F (relativeUnramifiedFixedField K
      (finiteAbstractFieldOfGaloisIntermediateField K F) m hm)

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