AbstractUnramified.lean

theorem residueFieldModule_eq_algebraModule
    (R S : Type) [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)] :
    (IsLocalRing.ResidueField.instModule :
      Module (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)) =
      (Algebra.toModule :
        Module (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))

theorem residueFieldAlgebra_eq_of_isIntegral
    (R S : Type) [CommRing R] [IsLocalRing R]
    [CommRing S] [IsLocalRing S] [Algebra R S]
    [IsLocalHom (algebraMap R S)]
    [Algebra.IsIntegral R (IsLocalRing.ResidueField S)] :
    (IsLocalRing.ResidueField.instAlgebra :
      Algebra (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)) =
      (IsLocalRing.ResidueField.algebraOfIsIntegral :
        Algebra (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))

theorem ramificationIdx_mul_residue_finrank_eq_finrank_compatible
    (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] [Algebra.IsSeparable K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K] *
        @Module.finrank 𝓀[K] 𝓀[L] _ _
          (IsLocalRing.ResidueField.instModule
            (R := 𝒪[K]) (S := 𝒪[L])) =
      Module.finrank K L

theorem baseFixingExtensionSubgroup_index_eq_finrank
    (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
    (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E] :
    (extensionSubgroup
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
      (closedFixingSubgroup K Ω E)
      (fixingSubgroupLeBase K Ω E)).index =
        Module.finrank K E

theorem finiteAbstractField_residueDegree_eq_relativeResidueDegree
    {G : Type u} [Group G] [TopologicalSpace G]
    (D : DegreeData G) (H : FiniteAbstractField G) :
    (H.residueDegree D : ℕ) =
      (H.toFiniteAbstractExtension.residueDegree D : ℕ)

theorem finiteAbstractField_degree_eq_abstractFixedField_finrank
    (K : Type) [Field K]
    (H : FiniteAbstractField
      (Gal(SeparableClosure K/K)))
    (hnormal :
      (extensionSubgroup
        (baseField (Gal(SeparableClosure K/K))) H.field
        (le_baseField H.field)).Normal) :
    let E :=
      abstractFixedField K (SeparableClosure K) H.field
    letI : FiniteDimensional K E :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : IsGalois K E :=
      abstractFixedField_isGalois_of_base_normal K H.field hnormal
    (H.toFiniteAbstractExtension.degree : ℕ) =
      Module.finrank K E := by
  let E :=
    abstractFixedField K (SeparableClosure K) H.field
  let : FiniteDimensional K E :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  let : IsGalois K E :=
    abstractFixedField_isGalois_of_base_normal K H.field hnormal
  calc
    (H.toFiniteAbstractExtension.degree : ℕ) =
        (extensionSubgroup
          (baseField (Gal(SeparableClosure K/K))) H.field
          (le_baseField H.field)).index :=
      H.toFiniteAbstractExtension.extensionSubgroup_index_eq_degree.symm
    _ = H.field.toSubgroup.index := by
      symm
      rw [← Subgroup.relIndex_top_right]
      rfl
    _ = E.fixingSubgroup.index := by
      exact congrArg Subgroup.index
        (InfiniteGalois.fixingSubgroup_fixedField H.field).symm
    _ = Module.finrank K E :=
      (IntermediateField.finrank_eq_fixingSubgroup_index (SeparableClosure K) E).symm

theorem abstractFixedField_isUnramifiedValuedExtension
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      (Gal(SeparableClosure K/K)))
    (hnormal :
      (extensionSubgroup
        (baseField (Gal(SeparableClosure K/K))) H.field
        (le_baseField H.field)).Normal)
    (hunramified :
      H.toFiniteAbstractExtension.IsUnramified
        (localResidueDatum K)) :
    let E :=
      abstractFixedField K (SeparableClosure K) H.field
    letI : FiniteDimensional K E :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : IsGalois K E :=
      abstractFixedField_isGalois_of_base_normal K H.field hnormal
    letI : NontriviallyNormedField K :=
      localFieldNontriviallyNormedField K
    letI : IsUltrametricDist K :=
      localFieldIsUltrametricDist K
    letI : CompleteSpace K := inferInstance
    letI : NontriviallyNormedField E :=
      finiteExtensionSpectralNormedField K E
    letI : ValuativeRel E :=
      finiteExtensionSpectralValuativeRel K E
    letI : IsNonarchimedeanLocalField E :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K E
    letI : Valuation.HasExtension
        (ValuativeRel.valuation K) (ValuativeRel.valuation E) :=
      finiteExtensionSpectralValuation_hasExtension K E
    letI : IsIntegralClosure 𝒪[E] 𝒪[K] E :=
      localCompleteDVF_integerRing_isIntegralClosure K E
    letI : Module.Finite 𝒪[K] 𝒪[E] :=
      localCompleteDVF_integerRing_moduleFinite K E
    LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
      K E := by
  let E :=
    abstractFixedField K (SeparableClosure K) H.field
  let : FiniteDimensional K E :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  let : IsGalois K E :=
    abstractFixedField_isGalois_of_base_normal K H.field hnormal
  let : NontriviallyNormedField K :=
    localFieldNontriviallyNormedField K
  let : IsUltrametricDist K :=
    localFieldIsUltrametricDist K
  let : CompleteSpace K := inferInstance
  let : NontriviallyNormedField E :=
    finiteExtensionSpectralNormedField K E
  let : ValuativeRel E :=
    finiteExtensionSpectralValuativeRel K E
  let : IsNonarchimedeanLocalField E :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K E
  let : Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation E) :=
    finiteExtensionSpectralValuation_hasExtension K E
  let : IsIntegralClosure 𝒪[E] 𝒪[K] E :=
    localCompleteDVF_integerRing_isIntegralClosure K E
  let : Module.Finite 𝒪[K] 𝒪[E] :=
    localCompleteDVF_integerRing_moduleFinite K E
  let f : ℕ :=
    @Module.finrank 𝓀[K] 𝓀[E] _ _
      (IsLocalRing.ResidueField.instModule
        (R := 𝒪[K]) (S := 𝒪[E]))
  have hresidueDegree :
      f = Module.finrank K E := by
    calc
      f =
          (H.residueDegree (localResidueDatum K) : ℕ) :=
        (localResidueDatum_residueDegree_eq_residueFinrank K H).symm
      _ =
          (H.toFiniteAbstractExtension.residueDegree
            (localResidueDatum K) : ℕ) :=
        finiteAbstractField_residueDegree_eq_relativeResidueDegree
          (localResidueDatum K) H
      _ = (H.toFiniteAbstractExtension.degree : ℕ) :=
        H.toFiniteAbstractExtension.residueDegree_eq_degree_of_isUnramified
          (localResidueDatum K) hunramified
      _ = Module.finrank K E :=
        finiteAbstractField_degree_eq_abstractFixedField_finrank
          K H hnormal
  have hdegree' :
      (𝓂[E] : Ideal 𝒪[E]).ramificationIdx 𝒪[K] *
          f =
        Module.finrank K E :=
    ramificationIdx_mul_residue_finrank_eq_finrank_compatible K E
  have hpos : 0 < f := by
    rw [hresidueDegree]
    exact Module.finrank_pos
  apply
    LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension.mk
  apply Nat.eq_of_mul_eq_mul_right hpos
  calc
    (𝓂[E] : Ideal 𝒪[E]).ramificationIdx 𝒪[K] *
        f =
      Module.finrank K E := hdegree'
    _ = f := hresidueDegree.symm
    _ = 1 * f := (one_mul _).symm

theorem localUpperRamificationGroup_abstractFixedField_eq_bot
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (H : FiniteAbstractField
      (Gal(SeparableClosure K/K)))
    (hnormal :
      (extensionSubgroup
        (baseField (Gal(SeparableClosure K/K))) H.field
        (le_baseField H.field)).Normal)
    (hunramified :
      H.toFiniteAbstractExtension.IsUnramified
        (localResidueDatum K))
    (t : ℝ) (ht : 0 ≤ t) :
    let E :=
      abstractFixedField K (SeparableClosure K) H.field
    letI : FiniteDimensional K E :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : IsGalois K E :=
      abstractFixedField_isGalois_of_base_normal K H.field hnormal
    localUpperRamificationGroup K E t = ⊥ := by
  let E :=
    abstractFixedField K (SeparableClosure K) H.field
  let : FiniteDimensional K E :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  let : IsGalois K E :=
    abstractFixedField_isGalois_of_base_normal K H.field hnormal
  let : NontriviallyNormedField K :=
    localFieldNontriviallyNormedField K
  let : IsUltrametricDist K :=
    localFieldIsUltrametricDist K
  let : CompleteSpace K := inferInstance
  let : NontriviallyNormedField E :=
    finiteExtensionSpectralNormedField K E
  let : ValuativeRel E :=
    finiteExtensionSpectralValuativeRel K E
  let : IsNonarchimedeanLocalField E :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K E
  let : Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation E) :=
    finiteExtensionSpectralValuation_hasExtension K E
  let : IsIntegralClosure 𝒪[E] 𝒪[K] E :=
    localCompleteDVF_integerRing_isIntegralClosure K E
  let : Module.Finite 𝒪[K] 𝒪[E] :=
    localCompleteDVF_integerRing_moduleFinite K E
  let :
      LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
        K E :=
    abstractFixedField_isUnramifiedValuedExtension
      K H hnormal hunramified
  exact
    localUpperRamificationGroup_eq_bot_of_unramifiedValuation
      K E t ht

def localFiniteUnramifiedAbstractField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    FiniteAbstractField (intrinsicAbsoluteGalois K)

theorem localFiniteUnramifiedAbstractField_field
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    (localFiniteUnramifiedAbstractField K d hd).field =
      (localFiniteUnramifiedAbelianSubextension K d hd).field

theorem localFiniteUnramifiedAbstractField_normal
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    (extensionSubgroup
      (baseField (intrinsicAbsoluteGalois K))
      (localFiniteUnramifiedAbstractField K d hd).field
    (le_baseField
        (localFiniteUnramifiedAbstractField K d hd).field)).Normal

theorem localFiniteUnramifiedAbstractField_isUnramified
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) :
    (localFiniteUnramifiedAbstractField K d hd).toFiniteAbstractExtension.IsUnramified
      (localResidueDatum K)

theorem localUpperRamificationGroup_finiteUnramifiedAbelianExtension_eq_bot
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) (t : ℝ) (ht : 0 ≤ t) :
    let H := localFiniteUnramifiedAbstractField K d hd
    let E :=
      abstractFixedField K (SeparableClosure K) H.field
    letI : FiniteDimensional K E :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : IsGalois K E :=
      abstractFixedField_isGalois_of_base_normal K H.field
        (localFiniteUnramifiedAbstractField_normal K d hd)
    localUpperRamificationGroup K E t = ⊥ := by
  exact
    localUpperRamificationGroup_abstractFixedField_eq_bot
      K (localFiniteUnramifiedAbstractField K d hd)
        (localFiniteUnramifiedAbstractField_normal K d hd)
        (localFiniteUnramifiedAbstractField_isUnramified K d hd)
        t ht

theorem
    artinPrincipalUnitStepGroup_finiteUnramifiedAbelianExtension_eq_bot
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) (t : ℝ) :
    let H := localFiniteUnramifiedAbstractField K d hd
    let E :=
      abstractFixedField K (SeparableClosure K) H.field
    letI : FiniteDimensional K E :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) H.field H.finite
    letI : IsAbelianGalois K E := by
      change IsAbelianGalois K
        (abstractFixedField K (SeparableClosure K)
          (localFiniteUnramifiedAbelianSubextension K d hd).field)
      exact finiteAbelianSubextension_fixedField_isAbelianGalois K
        (localFiniteUnramifiedAbelianSubextension K d hd)
    artinPrincipalUnitStepGroup K E t = ⊥ := by
  let H := localFiniteUnramifiedAbstractField K d hd
  let E :=
    abstractFixedField K (SeparableClosure K) H.field
  let : FiniteDimensional K E :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) H.field H.finite
  let : IsAbelianGalois K E := by
    change IsAbelianGalois K
      (abstractFixedField K (SeparableClosure K)
        (localFiniteUnramifiedAbelianSubextension K d hd).field)
    exact finiteAbelianSubextension_fixedField_isAbelianGalois K
      (localFiniteUnramifiedAbelianSubextension K d hd)
  let : NontriviallyNormedField K :=
    localFieldNontriviallyNormedField K
  let : IsUltrametricDist K :=
    localFieldIsUltrametricDist K
  let : CompleteSpace K := inferInstance
  let : NontriviallyNormedField E :=
    finiteExtensionSpectralNormedField K E
  let : ValuativeRel E :=
    finiteExtensionSpectralValuativeRel K E
  let : IsNonarchimedeanLocalField E :=
    finiteExtensionSpectralIsNonarchimedeanLocalField K E
  let : Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation E) :=
    finiteExtensionSpectralValuation_hasExtension K E
  let :
      LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
        K E :=
    abstractFixedField_isUnramifiedValuedExtension
      K H
        (localFiniteUnramifiedAbstractField_normal K d hd)
        (localFiniteUnramifiedAbstractField_isUnramified K d hd)
  exact
    artinPrincipalUnitStepGroup_eq_bot_of_unramifiedValuation
      K E t