PadicMultiplicativeArtinComparison.lean

def padicCompletedChangedUniformizerNegativePrimeUnit
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicCompletedChangedUniformizerFixedField p u n)ˣ

theorem padicCompletedChangedUniformizerNegativePrimeUnit_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicCompletedChangedUniformizerNegativePrimeUnit p n u :
      padicCompletedChangedUniformizerFixedField p u n) =
      -padicCompletedChangedUniformizerPrimeElement p u n

theorem padicCompletedChangedUniformizerNegativePrimeUnit_norm
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    normUnits ℚ_[p]
        (padicCompletedChangedUniformizerFixedField p u n)
        (padicCompletedChangedUniformizerNegativePrimeUnit p n u) =
      standardLubinTateChangedUniformizerUnit
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u

theorem padicCompletedChangedUniformizerNegativePrimeUnit_valuationMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let D := padicCompletedChangedUniformizerFixedField p u n
    letI : NontriviallyNormedField D :=
      finiteExtensionSpectralNormedField ℚ_[p] D
    letI : ValuativeRel D :=
      finiteExtensionSpectralValuativeRel ℚ_[p] D
    letI : IsNonarchimedeanLocalField D :=
      finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] D
    IsNonarchimedeanLocalField.valuationMap D
        (Additive.ofMul
          (padicCompletedChangedUniformizerNegativePrimeUnit p n u)) =
      -1 := by
  let D := padicCompletedChangedUniformizerFixedField p u n
  let M := padicCompletedStandardChangedCompositum p u n
  let : NontriviallyNormedField D :=
    finiteExtensionSpectralNormedField ℚ_[p] D
  let : ValuativeRel D :=
    finiteExtensionSpectralValuativeRel ℚ_[p] D
  let : IsNonarchimedeanLocalField D :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] D
  let : NontriviallyNormedField M :=
    finiteExtensionSpectralNormedField ℚ_[p] M
  let : ValuativeRel M :=
    finiteExtensionSpectralValuativeRel ℚ_[p] M
  let : IsNonarchimedeanLocalField M :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] M
  obtain ⟨htheta, _⟩ :=
    padicCompletedChangedUniformizerPrimeElement_isUniformizer_in_changedField_and_compositum
      p u n
  have hnegative :
      (localCompleteDVF D).valuation.IsUniformizer
        (-padicCompletedChangedUniformizerPrimeElement p u n : D) := by
    simpa only [Valuation.IsUniformizer.iff,
      (localCompleteDVF D).valuation.map_neg] using htheta
  let negativeInteger : (localCompleteDVF D).valuationSubring :=
    ⟨-padicCompletedChangedUniformizerPrimeElement p u n,
      hnegative.val_lt_one.le⟩
  have hunit :
      padicCompletedChangedUniformizerNegativePrimeUnit p n u =
        IsNonarchimedeanLocalField.uniformizerFieldUnit
          D negativeInteger hnegative := by
    apply Units.ext
    rfl
  rw [hunit]
  exact
    IsNonarchimedeanLocalField.valuationMap_uniformizerFieldUnit
      D negativeInteger hnegative

theorem
    padicCompletedChangedUniformizerRelativeArtin_negativePrime
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let D := padicCompletedChangedUniformizerFixedField p u n
    let M := padicCompletedStandardChangedCompositum p u n
    letI : NontriviallyNormedField D :=
      finiteExtensionSpectralNormedField ℚ_[p] D
    letI : ValuativeRel D :=
      finiteExtensionSpectralValuativeRel ℚ_[p] D
    letI : IsNonarchimedeanLocalField D :=
      finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] D
    letI : NontriviallyNormedField M :=
      finiteExtensionSpectralNormedField ℚ_[p] M
    letI : ValuativeRel M :=
      finiteExtensionSpectralValuativeRel ℚ_[p] M
    letI : IsNonarchimedeanLocalField M :=
      finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] M
    letI :
        Valuation.HasExtension (ValuativeRel.valuation D)
          (ValuativeRel.valuation M) :=
      finiteExtensionSpectralValuation_hasExtension_of_tower ℚ_[p] D M
    letI :
        IsNonarchimedeanLocalField.IsUnramifiedValuedExtension D M :=
      padicCompletedStandardChangedCompositum_isUnramifiedValuedExtension
        p u n
    abelianLocalArtinMonoidHom D M
        (padicCompletedChangedUniformizerNegativePrimeUnit p n u) =
      padicCompletedChangedUniformizerRelativeArtinCandidate p u n := by
  let D := padicCompletedChangedUniformizerFixedField p u n
  let M := padicCompletedStandardChangedCompositum p u n
  let : NontriviallyNormedField D :=
    finiteExtensionSpectralNormedField ℚ_[p] D
  let : ValuativeRel D :=
    finiteExtensionSpectralValuativeRel ℚ_[p] D
  let : IsNonarchimedeanLocalField D :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] D
  let : NontriviallyNormedField M :=
    finiteExtensionSpectralNormedField ℚ_[p] M
  let : ValuativeRel M :=
    finiteExtensionSpectralValuativeRel ℚ_[p] M
  let : IsNonarchimedeanLocalField M :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] M
  let :
      Valuation.HasExtension (ValuativeRel.valuation D)
        (ValuativeRel.valuation M) :=
    finiteExtensionSpectralValuation_hasExtension_of_tower ℚ_[p] D M
  let :
      IsNonarchimedeanLocalField.IsUnramifiedValuedExtension D M :=
    padicCompletedStandardChangedCompositum_isUnramifiedValuedExtension
      p u n
  calc
    abelianLocalArtinMonoidHom D M
        (padicCompletedChangedUniformizerNegativePrimeUnit p n u) =
        (arithmeticFrobeniusOfUnramifiedValuation D M) ^
          IsNonarchimedeanLocalField.valuationMap D
            (Additive.ofMul
              (padicCompletedChangedUniformizerNegativePrimeUnit p n u)) :=
      abelianLocalArtinMonoidHom_eq_frobenius_zpow D M _
    _ = (arithmeticFrobeniusOfUnramifiedValuation D M) ^ (-1 : ℤ) := by
      rw [padicCompletedChangedUniformizerNegativePrimeUnit_valuationMap]
    _ = (arithmeticFrobeniusOfUnramifiedValuation D M)⁻¹ := by
      rw [zpow_neg_one]
    _ = padicCompletedChangedUniformizerRelativeArtinCandidate p u n :=
      (padicCompletedChangedUniformizerRelativeArtinCandidate_eq_inverseArithmeticFrobenius
        p u n).symm

theorem padicArtinStandardLevel_normal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Normal ℚ_[p]
      (standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n)

theorem
    padicCompletedChangedUniformizerRelativeArtinCandidate_restrict_standardLevel
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let T := standardLubinTateLevelField hπ n
    let M := padicCompletedStandardChangedCompositum p u n
    letI : Algebra T M :=
      (padicStandardLevelToCompletedChangedCompositum
        p u n).toRingHom.toAlgebra
    letI : IsScalarTower ℚ_[p] T M :=
      IsScalarTower.of_algebraMap_eq'
        (padicStandardLevelToCompletedChangedCompositum p u n).comp_algebraMap.symm
    ((AlgEquiv.restrictNormalHom T).comp
        (AlgEquiv.restrictScalarsHom ℚ_[p]))
        (padicCompletedChangedUniformizerRelativeArtinCandidate
          p u n) =
      standardLubinTateUnitParameterEquivGal
        (padicLocalField p) hπ n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let T := standardLubinTateLevelField hπ n
  let M := padicCompletedStandardChangedCompositum p u n
  let : Algebra T M :=
    (padicStandardLevelToCompletedChangedCompositum
      p u n).toRingHom.toAlgebra
  let : IsScalarTower ℚ_[p] T M :=
    IsScalarTower.of_algebraMap_eq'
      (padicStandardLevelToCompletedChangedCompositum p u n).comp_algebraMap.symm
  apply AlgEquiv.ext
  intro x
  apply (algebraMap T M).injective
  rw [MonoidHom.comp_apply, AlgEquiv.restrictScalarsHom_apply]
  change
    algebraMap T M
        (AlgEquiv.restrictNormal
          ((AlgEquiv.restrictScalarsHom ℚ_[p])
            (padicCompletedChangedUniformizerRelativeArtinCandidate p u n)) T x) =
      algebraMap T M
        (standardLubinTateUnitParameterEquivGal
          (padicLocalField p) hπ n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) x)
  rw [AlgEquiv.restrictNormal_commutes]
  change
    padicCompletedChangedUniformizerRelativeArtinCandidate p u n
        (padicStandardLevelToCompletedChangedCompositum p u n x) =
      padicStandardLevelToCompletedChangedCompositum p u n
        (standardLubinTateUnitParameterEquivGal
          (padicLocalField p) hπ n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) x)
  rw [
    padicCompletedChangedUniformizerRelativeArtinCandidate_apply,
    padicCompletedChangedUniformizerArtinCandidate_standardLevel]
  exact congrArg
    (fun σ : Gal(T / ℚ_[p]) =>
      padicStandardLevelToCompletedChangedCompositum p u n (σ x))
    (standardLubinTateUnitParameterEquivGal_apply (padicLocalField p) hπ n
      (standardLubinTateUnitParameterClass (padicLocalField p) n u)).symm

theorem padicMultiplicativeAbelianLocalArtin_baseUniformizer
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateBaseUniformizerUnit hπ) =
      1 := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois
      (padicLocalField p) hπ n
  have hnorm :=
    standardLubinTateBaseUniformizerUnit_mem_normSubgroup hπ n
  change
    standardLubinTateBaseUniformizerUnit hπ ∈
      localNormSubgroup ℚ_[p] L at hnorm
  rw [← abelianLocalArtinMonoidHom_ker, MonoidHom.mem_ker] at hnorm
  exact hnorm

theorem padicMultiplicativeAbelianLocalArtin_eq_uniformizerUnitPart
    (p : ℕ) [Fact p.Prime] (n : ℕ) (x : ℚ_[p]ˣ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois F hπ n
    abelianLocalArtinMonoidHom ℚ_[p] L x =
      abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit F
          (CompleteDVF.higherPrincipalUnitGroup.fieldUnitUniformizerUnitPart
            F.toCompleteDVF hπ x)) := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois F hπ n
  let φ := abelianLocalArtinMonoidHom ℚ_[p] L
  let ϖ : ℚ_[p]ˣ := standardLubinTateBaseUniformizerUnit hπ
  let u : F.valuationSubringˣ :=
    CompleteDVF.higherPrincipalUnitGroup.fieldUnitUniformizerUnitPart
      F.toCompleteDVF hπ x
  let e : ℤ :=
    CompleteDVF.uniformizerValueExponent F.toCompleteDVF hπ x
  have hϖone : φ ϖ = 1 := by
    simpa only [φ, ϖ] using
      padicMultiplicativeAbelianLocalArtin_baseUniformizer p n
  have huField :
      standardLubinTateUnitFactorFieldUnit F u =
        x * ϖ ^ (-e) := by
    apply Units.ext
    simpa only [
      u, e, ϖ,
      standardLubinTateUnitFactorFieldUnit_coe,
      CompleteDVF.coe_valuationSubringUnitsToFieldUnits_apply,
      CompleteDVF.higherPrincipalUnitGroup.coe_valuationSubringUnitFieldUnitHom_apply,
      standardLubinTateBaseUniformizerUnit] using
      congrArg (fun z : ℚ_[p]ˣ => (z : ℚ_[p]))
        (valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
          F.toCompleteDVF hπ x)
  calc
    φ x = φ x * φ ϖ ^ (-e) := by
      rw [hϖone, one_zpow, mul_one]
    _ = φ (x * ϖ ^ (-e)) := by
      rw [map_mul, map_zpow]
    _ = φ (standardLubinTateUnitFactorFieldUnit F u) := by
      rw [huField]

theorem padicMultiplicativeAbelianLocalArtin_changedUniformizer
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateChangedUniformizerUnit hπ u) =
      abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) := by
  let F := padicLocalField p
  let π : F.valuationSubring :=
    padicIntEquivValuationSubring p (p : ℤ_[p])
  let hπ : F.toCompleteDVF.valuation.IsUniformizer (π : ℚ_[p]) :=
    padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField (F := F) (π := π) hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois
      F hπ n
  have hchanged :
      standardLubinTateChangedUniformizerUnit hπ u =
        standardLubinTateUnitFactorFieldUnit F u *
          standardLubinTateBaseUniformizerUnit hπ :=
    standardLubinTateChangedUniformizerUnit_eq_unit_mul (F := F) hπ u
  calc
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateChangedUniformizerUnit hπ u) =
        abelianLocalArtinMonoidHom ℚ_[p] L
          (standardLubinTateUnitFactorFieldUnit F u *
            standardLubinTateBaseUniformizerUnit hπ) :=
      congrArg (abelianLocalArtinMonoidHom ℚ_[p] L) hchanged
    _ = abelianLocalArtinMonoidHom ℚ_[p] L
          (standardLubinTateUnitFactorFieldUnit F u) := by
      rw [map_mul, padicMultiplicativeAbelianLocalArtin_baseUniformizer p n,
        mul_one]

theorem padicMultiplicativeAbelianLocalArtin_eq_unitParameter
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] T :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] T
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) =
      standardLubinTateUnitParameterEquivGal
        (padicLocalField p) hπ n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let T := standardLubinTateLevelField hπ n
  let D := padicCompletedChangedUniformizerFixedField p u n
  let M := padicCompletedStandardChangedCompositum p u n
  let : FiniteDimensional ℚ_[p] T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] T :=
    standardLubinTateLevelField_isAbelianGalois
      (padicLocalField p) hπ n
  let : Algebra T M :=
    (padicStandardLevelToCompletedChangedCompositum
      p u n).toRingHom.toAlgebra
  let : IsScalarTower ℚ_[p] T M :=
    IsScalarTower.of_algebraMap_eq'
      (padicStandardLevelToCompletedChangedCompositum p u n).comp_algebraMap.symm
  let : FiniteDimensional D M :=
    FiniteDimensional.right ℚ_[p] D M
  let : NontriviallyNormedField D :=
    finiteExtensionSpectralNormedField ℚ_[p] D
  let : ValuativeRel D :=
    finiteExtensionSpectralValuativeRel ℚ_[p] D
  let : IsNonarchimedeanLocalField D :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] D
  let : NontriviallyNormedField M :=
    finiteExtensionSpectralNormedField ℚ_[p] M
  let : ValuativeRel M :=
    finiteExtensionSpectralValuativeRel ℚ_[p] M
  let : IsNonarchimedeanLocalField M :=
    finiteExtensionSpectralIsNonarchimedeanLocalField ℚ_[p] M
  let :
      Valuation.HasExtension (ValuativeRel.valuation ℚ_[p])
        (ValuativeRel.valuation D) :=
    finiteExtensionSpectralValuation_hasExtension ℚ_[p] D
  let :
      Valuation.HasExtension (ValuativeRel.valuation D)
        (ValuativeRel.valuation M) :=
    finiteExtensionSpectralValuation_hasExtension_of_tower
      ℚ_[p] D M
  let :
      IsNonarchimedeanLocalField.IsUnramifiedValuedExtension D M :=
    padicCompletedStandardChangedCompositum_isUnramifiedValuedExtension
      p u n
  have hnormRestriction :=
    DFunLike.congr_fun
      (abelianLocalArtinMonoidHom_norm_restriction
        ℚ_[p] D T M)
      (padicCompletedChangedUniformizerNegativePrimeUnit p n u)
  have hrelative :
      abelianLocalArtinMonoidHom D M
          (padicCompletedChangedUniformizerNegativePrimeUnit p n u) =
        padicCompletedChangedUniformizerRelativeArtinCandidate p u n :=
    padicCompletedChangedUniformizerRelativeArtin_negativePrime p n u
  have hrestrict :
      ((AlgEquiv.restrictNormalHom T).comp
          (AlgEquiv.restrictScalarsHom ℚ_[p]))
          (padicCompletedChangedUniformizerRelativeArtinCandidate p u n) =
        standardLubinTateUnitParameterEquivGal
          (padicLocalField p) hπ n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) :=
    padicCompletedChangedUniformizerRelativeArtinCandidate_restrict_standardLevel
      p n u
  have hnorm :
      normUnits ℚ_[p] D
          (padicCompletedChangedUniformizerNegativePrimeUnit p n u) =
        standardLubinTateChangedUniformizerUnit hπ u :=
    padicCompletedChangedUniformizerNegativePrimeUnit_norm p n u
  have hchanged :
      abelianLocalArtinMonoidHom ℚ_[p] T
          (standardLubinTateChangedUniformizerUnit hπ u) =
        abelianLocalArtinMonoidHom ℚ_[p] T
          (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) :=
    padicMultiplicativeAbelianLocalArtin_changedUniformizer p n u
  have h :
      standardLubinTateUnitParameterEquivGal
          (padicLocalField p) hπ n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) =
        abelianLocalArtinMonoidHom ℚ_[p] T
          (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) := by
    simpa only [MonoidHom.comp_apply, hrelative, hrestrict, hnorm, hchanged] using
      hnormRestriction
  exact h.symm

theorem padicMultiplicativeAbelianLocalArtin_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let T := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] T :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] T :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] T
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u)
        (padicMultiplicativePrimitiveRoot p n) =
      (padicMultiplicativePrimitiveRoot p n) ^
        (PadicInt.toZModPow (n + 1)
          ((padicIntEquivValuationSubring p).symm
            (u : (padicLocalField p).valuationSubring))).val := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let T := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] T :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] T :=
    standardLubinTateLevelField_isAbelianGalois F hπ n
  have hArtin :
      abelianLocalArtinMonoidHom ℚ_[p] T
          (standardLubinTateUnitFactorFieldUnit F u) =
        standardLubinTateUnitParameterEquivGal F hπ n
          (standardLubinTateUnitParameterClass F n u) :=
    padicMultiplicativeAbelianLocalArtin_eq_unitParameter p n u
  exact
    (congrArg (fun σ : Gal(T / ℚ_[p]) =>
      σ (padicMultiplicativePrimitiveRoot p n)) hArtin).trans
      (padicMultiplicativePrimitiveRoot_unitParameterGaloisAction p n u)

theorem
    padicMultiplicativeAbelianLocalArtin_eq_one_of_mem_higherPrincipalUnitGroup
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup
        (padicLocalField p).toCompleteDVF (n + 1)) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) =
      1 := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois
      (padicLocalField p) hπ n
  have hnorm :=
    standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_mem_higher
      hπ u n hu
  change
    standardLubinTateUnitFactorFieldUnit (padicLocalField p) u ∈
      localNormSubgroup ℚ_[p] L at hnorm
  rw [← abelianLocalArtinMonoidHom_ker, MonoidHom.mem_ker] at hnorm
  exact hnorm

def padicMultiplicativeArtinUnitParameterHom
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTateUnitParameter (padicLocalField p) n →*
      Gal((standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) / ℚ_[p])

theorem padicMultiplicativeArtinUnitParameterHom_apply_class
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois F hπ n
    padicMultiplicativeArtinUnitParameterHom p n
        (standardLubinTateUnitParameterClass F n u) =
      abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit F u) := by
  dsimp only
  rfl

theorem padicMultiplicativeArtinUnitParameterHom_surjective
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Function.Surjective (padicMultiplicativeArtinUnitParameterHom p n)

def padicMultiplicativeArtinUnitParameterEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    standardLubinTateUnitParameter (padicLocalField p) n ≃*
      Gal((standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) / ℚ_[p])

theorem padicMultiplicativeArtinUnitParameterEquiv_apply_class
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois F hπ n
    padicMultiplicativeArtinUnitParameterEquiv p n
        (standardLubinTateUnitParameterClass F n u) =
      abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit F u) := by
  dsimp only
  rfl

def
    padicMultiplicativeUniformizerHigherPrincipalUnitSubgroup
    (p : ℕ) [Fact p.Prime] (n : ℕ) : Subgroup ℚ_[p]ˣ

theorem padicMultiplicativeAbelianLocalArtin_ker
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois F hπ n
    (abelianLocalArtinMonoidHom ℚ_[p] L).ker =
      padicMultiplicativeUniformizerHigherPrincipalUnitSubgroup p n := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois F hπ n
  let φ := abelianLocalArtinMonoidHom ℚ_[p] L
  let ϖ : ℚ_[p]ˣ := standardLubinTateBaseUniformizerUnit hπ
  let H : Subgroup F.valuationSubringˣ :=
    CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)
  let j : F.valuationSubringˣ →* ℚ_[p]ˣ :=
    CompleteDVF.valuationSubringUnitsToFieldUnits F.toCompleteDVF
  change φ.ker = Subgroup.zpowers ϖ ⊔ H.map j
  apply le_antisymm
  · intro x hx
    let u : F.valuationSubringˣ :=
      CompleteDVF.higherPrincipalUnitGroup.fieldUnitUniformizerUnitPart
        F.toCompleteDVF hπ x
    let e : ℤ :=
      CompleteDVF.uniformizerValueExponent F.toCompleteDVF hπ x
    have hxArtin : φ x = 1 :=
      MonoidHom.mem_ker.mp hx
    have hreduce :
        φ x = φ (standardLubinTateUnitFactorFieldUnit F u) := by
      simpa only [φ, u] using
        padicMultiplicativeAbelianLocalArtin_eq_uniformizerUnitPart
          p n x
    have huArtin :
        φ (standardLubinTateUnitFactorFieldUnit F u) = 1 :=
      hreduce.symm.trans hxArtin
    have huClass :
        standardLubinTateUnitParameterClass F n u = 1 := by
      apply (padicMultiplicativeArtinUnitParameterEquiv p n).injective
      rw [
        padicMultiplicativeArtinUnitParameterEquiv_apply_class,
        map_one]
      exact huArtin
    have hu : u ∈ H := by
      exact
        (QuotientGroup.eq_one_iff (N := H) u).1 huClass
    have huMap : j u ∈ H.map j :=
      ⟨u, hu, rfl⟩
    have hunit :
        j u ∈ Subgroup.zpowers ϖ ⊔ H.map j :=
      (show H.map j ≤ Subgroup.zpowers ϖ ⊔ H.map j from le_sup_right)
        huMap
    have hpow :
        ϖ ^ e ∈ Subgroup.zpowers ϖ ⊔ H.map j :=
      (show Subgroup.zpowers ϖ ≤
          Subgroup.zpowers ϖ ⊔ H.map j from le_sup_left)
        (Subgroup.zpow_mem_zpowers ϖ e)
    have huField :
        j u = x * ϖ ^ (-e) := by
      apply Units.ext
      simpa only [
        j, u, e, ϖ,
        CompleteDVF.coe_valuationSubringUnitsToFieldUnits_apply,
        CompleteDVF.higherPrincipalUnitGroup.coe_valuationSubringUnitFieldUnitHom_apply,
        standardLubinTateBaseUniformizerUnit] using
        congrArg (fun z : ℚ_[p]ˣ => (z : ℚ_[p]))
          (valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
            F.toCompleteDVF hπ x)
    have hxDecomposition :
        x = j u * ϖ ^ e := by
      rw [huField]
      simp [mul_assoc]
    rw [hxDecomposition]
    exact
      (Subgroup.zpowers ϖ ⊔ H.map j).mul_mem hunit hpow
  · apply sup_le
    · apply Subgroup.zpowers_le_of_mem
      rw [MonoidHom.mem_ker]
      simpa only [φ, ϖ] using
        padicMultiplicativeAbelianLocalArtin_baseUniformizer p n
    · rintro _ ⟨u, hu, rfl⟩
      rw [MonoidHom.mem_ker]
      change
        abelianLocalArtinMonoidHom ℚ_[p] L
            (standardLubinTateUnitFactorFieldUnit F u) =
          1
      exact
        padicMultiplicativeAbelianLocalArtin_eq_one_of_mem_higherPrincipalUnitGroup
          p n u hu

theorem
    padicMultiplicativeLocalNormSubgroup_eq_uniformizerHigherPrincipalUnitSubgroup
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois F hπ n
    localNormSubgroup ℚ_[p] L =
      padicMultiplicativeUniformizerHigherPrincipalUnitSubgroup p n := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois F hπ n
  calc
    localNormSubgroup ℚ_[p] L =
        (abelianLocalArtinMonoidHom ℚ_[p] L).ker :=
      (abelianLocalArtinMonoidHom_ker ℚ_[p] L).symm
    _ = padicMultiplicativeUniformizerHigherPrincipalUnitSubgroup p n :=
      padicMultiplicativeAbelianLocalArtin_ker p n

theorem
    padicMultiplicativeAbelianLocalArtin_eq_unitParameter_of_mem_higherPrincipalUnitGroup
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup
        (padicLocalField p).toCompleteDVF (n + 1)) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) =
      (standardLubinTateUnitParameterEquivGal
        (padicLocalField p) hπ n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u))⁻¹ := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois
      (padicLocalField p) hπ n
  have hArtin :
      abelianLocalArtinMonoidHom ℚ_[p] L
          (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) =
        1 :=
    padicMultiplicativeAbelianLocalArtin_eq_one_of_mem_higherPrincipalUnitGroup
      p n u hu
  have hParameter :
      standardLubinTateUnitParameterClass (padicLocalField p) n u = 1 := by
    exact
      (QuotientGroup.eq_one_iff
        (N :=
          CompleteDVF.higherPrincipalUnitGroup
            (padicLocalField p).toCompleteDVF (n + 1)) u).2 hu
  calc
    abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u) = 1 :=
      hArtin
    _ = (standardLubinTateUnitParameterEquivGal
        (padicLocalField p) hπ n
        (standardLubinTateUnitParameterClass
          (padicLocalField p) n u))⁻¹ := by
      rw [hParameter, map_one, inv_one]

theorem
    padicMultiplicativeAbelianLocalArtin_primitiveRoot_of_mem_higherPrincipalUnitGroup
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup
        (padicLocalField p).toCompleteDVF (n + 1)) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    let L := standardLubinTateLevelField hπ n
    letI : FiniteDimensional ℚ_[p] L :=
      standardLubinTateLevelField_finiteDimensional hπ n
    letI : IsAbelianGalois ℚ_[p] L :=
      standardLubinTateLevelField_isAbelianGalois
        (padicLocalField p) hπ n
    (abelianLocalArtinMonoidHom ℚ_[p] L
        (standardLubinTateUnitFactorFieldUnit (padicLocalField p) u))
        (padicMultiplicativePrimitiveRoot p n) =
      padicMultiplicativePrimitiveRoot p n ^
        (PadicInt.toZModPow (p := p) (n + 1)
          ((padicIntEquivValuationSubring p).symm
            ((u⁻¹ : (padicLocalField p).valuationSubringˣ) :
              (padicLocalField p).valuationSubring))).val := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois
      (padicLocalField p) hπ n
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let : FiniteDimensional ℚ_[p] L :=
    standardLubinTateLevelField_finiteDimensional hπ n
  let : IsAbelianGalois ℚ_[p] L :=
    standardLubinTateLevelField_isAbelianGalois F hπ n
  have hArtin :
      abelianLocalArtinMonoidHom ℚ_[p] L
          (standardLubinTateUnitFactorFieldUnit F u) =
        (standardLubinTateUnitParameterEquivGal F hπ n
          (standardLubinTateUnitParameterClass F n u))⁻¹ :=
    padicMultiplicativeAbelianLocalArtin_eq_unitParameter_of_mem_higherPrincipalUnitGroup
      p n u hu
  exact
    (congrArg (fun σ : Gal(L / ℚ_[p]) =>
      σ (padicMultiplicativePrimitiveRoot p n)) hArtin).trans
      (padicMultiplicativePrimitiveRoot_galoisAction p n u)