LubinTateTransport.lean

def equalCharacteristicResidueRank
    {L : Type} [Field L] (F : LocalField L) : ℕ+

theorem equalCharacteristicResidueCard
    {L : Type} [Field L] (F : LocalField L) :
    Nat.card F.residueField =
      F.residueCharacteristic ^
        (equalCharacteristicResidueRank F : ℕ)

def equalCharacteristicTargetLocalField :
    LocalField K

theorem equalCharacteristicTargetLocalField_valuation_eq :
    (equalCharacteristicTargetLocalField K).valuation =
      ValuativeRel.valuation K

def equalCharacteristicTargetIntegerEquiv :
    𝒪[K] ≃+* (equalCharacteristicTargetLocalField K).valuationSubring where
  toFun x := ⟨x, by
    have hx := x.property
    change ValuativeRel.valuation K (x : K) ≤ 1 at hx
    change (equalCharacteristicTargetLocalField K).valuation (x : K) ≤ 1
    rw [equalCharacteristicTargetLocalField_valuation_eq]
    exact hx⟩
  invFun x := ⟨x, by
    have hx := x.property
    change (equalCharacteristicTargetLocalField K).valuation (x : K) ≤ 1 at hx
    rw [equalCharacteristicTargetLocalField_valuation_eq] at hx
    change ValuativeRel.valuation K (x : K) ≤ 1
    exact hx⟩
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl
  map_add' := fun _ _ => rfl
  map_mul' := fun _ _ => rfl

theorem equalCharacteristicTargetIntegerEquiv_apply_coe (x : 𝒪[K]) :
    (((equalCharacteristicTargetIntegerEquiv K x :
      (equalCharacteristicTargetLocalField K).valuationSubring)) : K) =
      (x : K)

theorem equalCharacteristicTargetIntegerEquiv_symm_apply_coe
    (x : (equalCharacteristicTargetLocalField K).valuationSubring) :
    ((((equalCharacteristicTargetIntegerEquiv K).symm x : 𝒪[K])) : K) =
      (x : K)

theorem equalCharacteristicTargetResidueCharacteristicCharP
    (p : ℕ) [Fact p.Prime] [CharP K p] :
    CharP K (equalCharacteristicTargetLocalField K).residueCharacteristic

theorem equalCharacteristicUniformizerRatio_valuationMap
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    valuationMap K
        (Additive.ofMul
          (ϖ / inverseIntegerRingUniformizerFieldUnit K)) = 0

def equalCharacteristicUniformizerRatioIntegerUnit
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    𝒪[K]ˣ

theorem integerUnitsToFieldUnits_equalCharacteristicUniformizerRatioIntegerUnit
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    integerUnitsToFieldUnits K
        (equalCharacteristicUniformizerRatioIntegerUnit K ϖ hϖ) =
      ϖ / inverseIntegerRingUniformizerFieldUnit K

def equalCharacteristicTargetUniformizerInteger
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) : 𝒪[K]

theorem equalCharacteristicTargetUniformizerInteger_irreducible
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    Irreducible
      (equalCharacteristicTargetUniformizerInteger K ϖ hϖ)

theorem equalCharacteristicTargetUniformizerInteger_coe
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    ((equalCharacteristicTargetUniformizerInteger K ϖ hϖ : 𝒪[K]) : K) =
      ((ϖ⁻¹ : Kˣ) : K)

def equalCharacteristicTargetUniformizer
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    (equalCharacteristicTargetLocalField K).valuationSubring

theorem equalCharacteristicTargetUniformizer_coe
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    ((equalCharacteristicTargetUniformizer K ϖ hϖ :
      (equalCharacteristicTargetLocalField K).valuationSubring) : K) =
      ((ϖ⁻¹ : Kˣ) : K)

theorem equalCharacteristicTargetUniformizer_isUniformizer
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    (equalCharacteristicTargetLocalField K).valuation.IsUniformizer
      (equalCharacteristicTargetUniformizer K ϖ hϖ : K)

def equalCharacteristicTargetLaurentRingEquiv
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    (equalCharacteristicTargetLocalField K).residueField⸨X⸩ ≃+* K

theorem equalCharacteristicTargetLaurentRingEquiv_uniformizer
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ
        (equalCharacteristicLaurentUniformizer
          (equalCharacteristicTargetLocalField K)) =
      ((ϖ⁻¹ : Kˣ) : K)

def equalCharacteristicTargetLaurentUnitsEquiv
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    (equalCharacteristicTargetLocalField K).residueField⸨X⸩ˣ ≃* Kˣ

theorem equalCharacteristicTargetLaurentUnitsEquiv_uniformizer
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ
        (equalCharacteristicLaurentUniformizerUnit
          (equalCharacteristicTargetLocalField K)) =
      ϖ⁻¹

theorem equalCharacteristicTargetLaurentUnitsEquiv_uniformizer_inv
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ
        (equalCharacteristicLaurentUniformizerUnit
          (equalCharacteristicTargetLocalField K))⁻¹ =
      ϖ

theorem equalCharacteristicTargetLaurentUnitsEquiv_mem_fieldPrincipalUnits_of_mem_higherUnit
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ)
    (a :
      (equalCharacteristicTargetLocalField K).residueField⟦X⟧ˣ)
    (ha :
      a ∈ equalCharacteristicLubinTateHigherUnitSubgroup
        (equalCharacteristicTargetLocalField K) m) :
    equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ
        (equalCharacteristicPowerSeriesUnitToLaurentFieldUnit
          (equalCharacteristicTargetLocalField K) a) ∈
      LocalFieldTheory.fieldPrincipalUnits K (m + 1)

theorem equalCharacteristicTargetLaurent_fieldPrincipalUnits_map_le
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    let B := F.residueField⸨X⸩
    letI : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
    (LocalFieldTheory.fieldPrincipalUnits B (m + 1)).map
        (equalCharacteristicTargetLaurentUnitsEquiv
          K p ϖ hϖ).toMonoidHom ≤
      LocalFieldTheory.fieldPrincipalUnits K (m + 1) := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  change
    (LocalFieldTheory.fieldPrincipalUnits B (m + 1)).map
        (equalCharacteristicTargetLaurentUnitsEquiv
          K p ϖ hϖ).toMonoidHom ≤
      LocalFieldTheory.fieldPrincipalUnits K (m + 1)
  rw [←
    equalCharacteristicLubinTateHigherUnitSubgroup_map_toLaurentField_eq
      F m]
  rintro x ⟨y, ⟨a, ha, rfl⟩, rfl⟩
  exact
    equalCharacteristicTargetLaurentUnitsEquiv_mem_fieldPrincipalUnits_of_mem_higherUnit
      K p ϖ hϖ m a ha

theorem equalCharacteristicTargetLaurent_uniformizerPrincipalSubgroup_map_le
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    let B := F.residueField⸨X⸩
    letI : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
    (LocalFieldTheory.uniformizerPrincipalSubgroup B
        (equalCharacteristicLaurentUniformizerUnit F)⁻¹
        1 (m + 1)).map
        (equalCharacteristicTargetLaurentUnitsEquiv
          K p ϖ hϖ).toMonoidHom ≤
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 (m + 1) := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  change
    (LocalFieldTheory.uniformizerPrincipalSubgroup B
        (equalCharacteristicLaurentUniformizerUnit F)⁻¹
        1 (m + 1)).map
        (equalCharacteristicTargetLaurentUnitsEquiv
          K p ϖ hϖ).toMonoidHom ≤
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 (m + 1)
  unfold LocalFieldTheory.uniformizerPrincipalSubgroup
  rw [Subgroup.map_sup, MonoidHom.map_zpowers]
  apply sup_le_sup
  · apply (Subgroup.zpowers_le).2
    rw [map_pow]
    change
      (equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ
        ((equalCharacteristicLaurentUniformizerUnit F)⁻¹)) ^ 1 ∈
        Subgroup.zpowers (ϖ ^ 1)
    rw [equalCharacteristicTargetLaurentUnitsEquiv_uniformizer_inv]
    exact Subgroup.mem_zpowers (ϖ ^ 1)
  · exact
      equalCharacteristicTargetLaurent_fieldPrincipalUnits_map_le
        K p ϖ hϖ m

def equalCharacteristicTransportedLubinTateLevelAlgebra
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    Algebra K (equalCharacteristicLubinTateLevelField F m) := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  letI : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  letI : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  letI : CharP K p := hKp
  exact RingHom.toAlgebra
    ((algebraMap B E).comp
      (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ).symm.toRingHom)

theorem equalCharacteristicTransportedLubinTateLevelAlgebra_comp
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    let B := F.residueField⸨X⸩
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let E := equalCharacteristicLubinTateLevelField F m
    letI : Algebra B E :=
      equalCharacteristicLubinTateLevelAlgebra F m
    letI : CharP K p := hKp
    letI : Algebra K E :=
      equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
    (algebraMap K E).comp
        (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ).toRingHom =
      (RingEquiv.refl E).toRingHom.comp (algebraMap B E) := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : CharP K p := hKp
  let : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  apply RingHom.ext
  intro x
  change
    (algebraMap B E)
        ((equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ).symm
          (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ x)) =
      (algebraMap B E) x
  rw [RingEquiv.symm_apply_apply]

theorem equalCharacteristicTransportedLubinTateLevel_finiteDimensional
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let E := equalCharacteristicLubinTateLevelField F m
    letI : CharP K p := hKp
    letI : Algebra K E :=
      equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
    letI : Module K E := Algebra.toModule
    Module.Finite K E := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  let algBE : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : Algebra B E := algBE
  let : Module B E := algBE.toModule
  let : Module.Finite B E :=
    equalCharacteristicLubinTateLevelField_finiteDimensional F m
  let : CharP K p := hKp
  let algKE : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  let : Algebra K E := algKE
  let : Module K E := algKE.toModule
  exact Module.Finite.of_equiv_equiv
    (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ)
    (RingEquiv.refl E)
    (equalCharacteristicTransportedLubinTateLevelAlgebra_comp
      K p ϖ hϖ m)

theorem equalCharacteristicTransportedLubinTateLevel_isGalois
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let E := equalCharacteristicLubinTateLevelField F m
    letI : CharP K p := hKp
    letI : Algebra K E :=
      equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
    IsGalois K E := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : IsGalois B E :=
    equalCharacteristicLubinTateLevelField_isGalois F m
  let : CharP K p := hKp
  let : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  exact IsGalois.of_equiv_equiv
    (F := B) («E» := E)
    (f := equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ)
    (g := RingEquiv.refl E)
    (equalCharacteristicTransportedLubinTateLevelAlgebra_comp
      K p ϖ hϖ m)

theorem equalCharacteristicTransportedLubinTateLevel_isAbelianGalois
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let E := equalCharacteristicLubinTateLevelField F m
    letI : CharP K p := hKp
    letI : Algebra K E :=
      equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
    IsAbelianGalois K E := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : IsAbelianGalois B E :=
    equalCharacteristicLubinTateLevelField_isAbelianGalois F m
  let : CharP K p := hKp
  let : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  let e := equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ
  have he (x : B) :
      algebraMap K E (e x) = algebraMap B E x := by
    have hcomp :=
      DFunLike.congr_fun
        (equalCharacteristicTransportedLubinTateLevelAlgebra_comp
          K p ϖ hϖ m) x
    simpa [e] using hcomp
  let : IsGalois K E :=
    equalCharacteristicTransportedLubinTateLevel_isGalois
      K p ϖ hϖ m
  let restrictToLaurent :
      Gal(E / K) →* Gal(E / B) :=
    { toFun := fun (σ : Gal(E / K)) =>
        show Gal(E / B) from
          { σ.toRingEquiv with
            commutes' := fun x => by
              rw [← he x]
              exact σ.commutes (e x) }
      map_one' := by
        ext x
        rfl
      map_mul' σ τ := by
        ext x
        rfl }
  have hrestrict :
      Function.Injective restrictToLaurent := by
    intro σ τ hστ
    apply AlgEquiv.ext
    intro x
    exact DFunLike.congr_fun hστ x
  refine { is_comm.comm := fun σ τ => hrestrict ?_ }
  exact
    (inferInstance : IsMulCommutative (Gal(E / B))).is_comm.comm
      (restrictToLaurent σ) (restrictToLaurent τ)

def equalCharacteristicTransportedLubinTateNormSubgroup
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) : Subgroup Kˣ

theorem equalCharacteristicTransported_normUnits
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ)
    (x :
      let F := equalCharacteristicTargetLocalField K
      letI : CharP K F.residueCharacteristic :=
        equalCharacteristicTargetResidueCharacteristicCharP K p
      (equalCharacteristicLubinTateLevelField F m)ˣ) :
    let F := equalCharacteristicTargetLocalField K
    let B := F.residueField⸨X⸩
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let E := equalCharacteristicLubinTateLevelField F m
    letI : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
    letI : CharP K p := hKp
    letI : Algebra K E :=
      equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
    equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ
        (LocalFieldTheory.normUnits B E x) =
      LocalFieldTheory.normUnits K E x := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  change Eˣ at x
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : CharP K p := hKp
  let : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  have hnorm :=
    Algebra.norm_eq_of_equiv_equiv
      (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ)
      (RingEquiv.refl E)
      (equalCharacteristicTransportedLubinTateLevelAlgebra_comp
        K p ϖ hϖ m)
      x.val
  apply Units.ext
  change
    equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ
        (Algebra.norm B x.val) =
      Algebra.norm K x.val
  rw [hnorm,
    (equalCharacteristicTargetLaurentRingEquiv K p ϖ hϖ).apply_symm_apply]
  rfl

theorem equalCharacteristicLubinTateNormSubgroup_map_eq_transported
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    let F := equalCharacteristicTargetLocalField K
    letI : CharP K F.residueCharacteristic :=
      equalCharacteristicTargetResidueCharacteristicCharP K p
    let N := equalCharacteristicLubinTateNormSubgroup F m
    letI : CharP K p := hKp
    N.map
        (equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ).toMonoidHom =
      equalCharacteristicTransportedLubinTateNormSubgroup K p ϖ hϖ m := by
  let F := equalCharacteristicTargetLocalField K
  let B := F.residueField⸨X⸩
  let : CharP K F.residueCharacteristic :=
    equalCharacteristicTargetResidueCharacteristicCharP K p
  let E := equalCharacteristicLubinTateLevelField F m
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F m
  let : CharP K p := hKp
  let : Algebra K E :=
    equalCharacteristicTransportedLubinTateLevelAlgebra K p ϖ hϖ m
  change
    (_root_.LocalFieldTheory.localNormSubgroup B E).map
        (equalCharacteristicTargetLaurentUnitsEquiv K p ϖ hϖ).toMonoidHom =
      _root_.LocalFieldTheory.localNormSubgroup K E
  ext x
  constructor
  · rintro ⟨y, ⟨z, rfl⟩, rfl⟩
    exact
      ⟨z,
        (equalCharacteristicTransported_normUnits K p ϖ hϖ m z).symm⟩
  · rintro ⟨z, rfl⟩
    refine ⟨LocalFieldTheory.normUnits B E z, ⟨z, rfl⟩, ?_⟩
    exact equalCharacteristicTransported_normUnits K p ϖ hϖ m z

theorem equalCharacteristicTransportedLubinTateNormSubgroup_le_uniformizerPrincipalSubgroup
    (p : ℕ) [Fact p.Prime] [hKp : CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (m : ℕ) :
    equalCharacteristicTransportedLubinTateNormSubgroup K p ϖ hϖ m ≤
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 (m + 1)

theorem equalCharacteristicTransportedLubinTateNormSubgroup_le_of_pos
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (ϖ : Kˣ)
    (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (n : ℕ) (hn : 1 ≤ n) :
    equalCharacteristicTransportedLubinTateNormSubgroup
        K p ϖ hϖ (n - 1) ≤
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 n