UnramifiedLubinTateDiagonal.lean

theorem standardLubinTateLevel_spectral_inertiaDeg_eq_one
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : ℕ) :
    let hπ := standardLocalFieldUniformizer_isUniformizer K
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional K T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : NontriviallyNormedField T :=
      finiteExtensionSpectralNormedField K T
    letI : ValuativeRel T :=
      finiteExtensionSpectralValuativeRel K T
    letI : IsNonarchimedeanLocalField T :=
      finiteExtensionSpectralIsNonarchimedeanLocalField K T
    letI : Valuation.HasExtension (ValuativeRel.valuation K)
        (ValuativeRel.valuation T) :=
      finiteExtensionSpectralValuation_hasExtension K T
    letI :
        (LocalFieldTheory.localCompleteDVF K).valuation.HasExtension
          (LocalFieldTheory.localCompleteDVF T).valuation :=
      localCompleteDVFValuation_hasExtension K T
    (LocalFieldTheory.localCompleteDVF T).maximalIdeal.inertiaDeg
      (LocalFieldTheory.localCompleteDVF K).valuationSubring = 1 := by
  simpa only using lubinTateLevel_spectral_inertiaDeg_eq_one K
    (standardLocalFieldUniformizer_isUniformizer K) n

theorem localFiniteUnramifiedField_inf_standardLubinTateLevelField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    localFiniteUnramifiedField K d hd ⊓
        standardLubinTateLevelField
          (standardLocalFieldUniformizer_isUniformizer K) n =
      ⊥

theorem localFiniteUnramifiedField_linearDisjoint_standardLubinTateLevelField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (d : ℕ) (hd : 0 < d) (n : ℕ) :
    (localFiniteUnramifiedField K d hd).LinearDisjoint
      (standardLubinTateLevelField
        (standardLocalFieldUniformizer_isUniformizer K) n)

abbrev standardLubinTateDiagonalCompositumField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IntermediateField K (SeparableClosure K)

theorem standardLubinTateDiagonalCompositumField_finiteDimensional
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    FiniteDimensional K
      (standardLubinTateDiagonalCompositumField K n u)

theorem standardLubinTateDiagonalCompositumField_isGalois
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IsGalois K (standardLubinTateDiagonalCompositumField K n u)

abbrev standardLubinTateDiagonalAutomorphism
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    Gal((standardLubinTateDiagonalCompositumField K n u) / K)

abbrev standardLubinTateDiagonalFixedField
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    IntermediateField K
      (standardLubinTateDiagonalCompositumField K n u)

theorem standardLubinTateDiagonalFixedField_finrank
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    Module.finrank K (standardLubinTateDiagonalFixedField K n u) =
      Module.finrank K
        (standardLubinTateLevelField
          (standardLocalFieldUniformizer_isUniformizer K) n)