StandardFixedFieldComparison.lean

theorem artinPrincipalUnitStepGroup_map_standardFixedFieldEquiv
    (L M : Type) [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsAbelianGalois K L] [IsAbelianGalois K M]
    (e : L ≃ₐ[K] M) (t : ℝ) :
    Subgroup.map (AlgEquiv.autCongr e).toMonoidHom
        (artinPrincipalUnitStepGroup K L t) =
      artinPrincipalUnitStepGroup K M t

theorem standardLubinTateFiniteAbelianSubextension_filteredLocalReciprocity
    (m : ℕ) (t : ℝ) (ht : 0 ≤ t) :
    let T := standardLubinTateFiniteAbelianSubextension K m
    let M :=
      abstractFixedField K (SeparableClosure K) T.field
    letI : FiniteDimensional K M :=
      abstractFixedField_finiteDimensional
        K (SeparableClosure K) T.field
          (finiteAbelianSubextension_finite_over_absoluteBase K T)
    letI : IsAbelianGalois K M :=
      finiteAbelianSubextension_fixedField_isAbelianGalois K T
    artinPrincipalUnitStepGroup K M t =
      localUpperRamificationGroup K M t := 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 T := standardLubinTateFiniteAbelianSubextension K m
  let M :=
    abstractFixedField K (SeparableClosure K) T.field
  let : FiniteDimensional K M :=
    abstractFixedField_finiteDimensional
      K (SeparableClosure K) T.field
        (finiteAbelianSubextension_finite_over_absoluteBase K T)
  let : IsAbelianGalois K M :=
    finiteAbelianSubextension_fixedField_isAbelianGalois K T
  let e : E ≃ₐ[K] M :=
    standardLubinTateFiniteAbelianSubextensionFixedFieldEquiv K m
  let q : Gal(E / K) ≃* Gal(M / K) :=
    AlgEquiv.autCongr e
  have hArtin :
      Subgroup.map q.toMonoidHom
          (artinPrincipalUnitStepGroup K E t) =
        artinPrincipalUnitStepGroup K M t :=
    artinPrincipalUnitStepGroup_map_standardFixedFieldEquiv
      K E M e t
  have hUpper :
      Subgroup.map q.toMonoidHom
          (localUpperRamificationGroup K E t) =
        localUpperRamificationGroup K M t :=
    localUpperRamificationGroup_map_autCongr K E M e t
  have hStandard :
      artinPrincipalUnitStepGroup K E t =
        localUpperRamificationGroup K E t :=
    standardLubinTateCanonicalArtinPrincipalUnitStepGroup_eq_localUpperRamificationGroup
      K m t ht
  calc
    artinPrincipalUnitStepGroup K M t =
        Subgroup.map q.toMonoidHom
          (artinPrincipalUnitStepGroup K E t) :=
      hArtin.symm
    _ =
        Subgroup.map q.toMonoidHom
          (localUpperRamificationGroup K E t) := by
      rw [hStandard]
    _ = localUpperRamificationGroup K M t := hUpper