StandardLubinTate.lean

def standardLubinTateFiniteAbelianSubextension
    (m : ℕ) :
    FiniteAbelianSubextension (intrinsicAbstractBase K)

def standardLubinTateFiniteAbelianSubextensionFixedFieldEquiv
    (m : ℕ) :
    let hπ := standardLocalFieldUniformizer_isUniformizer K
    let E := standardLubinTateLevelField hπ m
    E ≃ₐ[K]
      abstractFixedField K (SeparableClosure K)
        (standardLubinTateFiniteAbelianSubextension K m).field := by
  let hπ := standardLocalFieldUniformizer_isUniformizer K
  let E := standardLubinTateLevelField hπ m
  letI : FiniteDimensional K E :=
    standardLubinTateLevelField_finiteDimensional hπ m
  letI : IsAbelianGalois K E :=
    standardLubinTateLevelField_isAbelianGalois
      (standardLocalField K) hπ m
  let i : E →ₐ[K] SeparableClosure K := E.val
  let T := standardLubinTateFiniteAbelianSubextension K m
  have hfixed :
      abstractFixedField K (SeparableClosure K) T.field =
        finiteGaloisFieldRangeOfEmbedding K E i := by
    change
      IntermediateField.fixedField
          (finiteGaloisFieldRangeOfEmbedding K E i).fixingSubgroup =
        finiteGaloisFieldRangeOfEmbedding K E i
    exact
      InfiniteGalois.fixedField_fixingSubgroup
        (finiteGaloisFieldRangeOfEmbedding K E i)
  rw [hfixed]
  exact finiteGaloisFieldRangeEquivOfEmbedding K E i

theorem
    standardLubinTateFiniteAbelianSubextension_normSubgroup_map_eq
    (m : ℕ) :
    let T := standardLubinTateFiniteAbelianSubextension K m
    (T.normSubgroup (intrinsicAbsoluteUnits K)).map
        (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom =
      (LocalFieldTheory.uniformizerPrincipalSubgroup K
        (inverseIntegerRingUniformizerFieldUnit K) 1 (m + 1)).toAddSubgroup := by
  let hπ := standardLocalFieldUniformizer_isUniformizer K
  let E := standardLubinTateLevelField hπ m
  let : FiniteDimensional K E :=
    standardLubinTateLevelField_finiteDimensional hπ m
  let : IsAbelianGalois K E :=
    standardLubinTateLevelField_isAbelianGalois
      (standardLocalField K) hπ m
  let i : E →ₐ[K] SeparableClosure K := E.val
  let T := standardLubinTateFiniteAbelianSubextension K m
  calc
    (T.normSubgroup (intrinsicAbsoluteUnits K)).map
          (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom =
        CyclicCohomology.additiveNormSubgroup K E := by
      simpa [T, standardLubinTateFiniteAbelianSubextension, i, E, hπ] using
        map_finiteAbelianAbstractExtension_normSubgroup_eq K E i
    _ =
        (LocalFieldTheory.uniformizerPrincipalSubgroup K
          (inverseIntegerRingUniformizerFieldUnit K)
          1 (m + 1)).toAddSubgroup := by
      simpa [CyclicCohomology.additiveNormSubgroup, E, hπ,
        standardLubinTateNormSubgroup] using
          congrArg Subgroup.toAddSubgroup
            (standardLubinTateCanonicalNormSubgroup_eq_normalizedUniformizerPrincipalSubgroup
              K m)

def standardLubinTateFiniteAbelianCompositum
    (d n : ℕ) (hd : 0 < d) :
    FiniteAbelianSubextension (intrinsicAbstractBase K)

theorem standardLubinTateFiniteAbelianCompositum_fixedField_eq_sup
    (d n : ℕ) (hd : 0 < d) :
    abstractFixedField K (SeparableClosure K)
        (standardLubinTateFiniteAbelianCompositum K d n hd).field =
      abstractFixedField K (SeparableClosure K)
          (localFiniteUnramifiedAbelianSubextension K d hd).field ⊔
        abstractFixedField K (SeparableClosure K)
          (standardLubinTateFiniteAbelianSubextension K (n - 1)).field

theorem standardLubinTateFiniteAbelianCompositum_nativeNormSubgroup_le
    (H : Subgroup Kˣ) (d n : ℕ)
    (hd : 0 < d) (hn : 0 < n)
    (hstandard :
      LocalFieldTheory.uniformizerPrincipalSubgroup K
          (inverseIntegerRingUniformizerFieldUnit K) d n ≤
        H) :
    finiteAbelianNormSubgroup K
        (standardLubinTateFiniteAbelianCompositum K d n hd) ≤
      H