PrincipalUnits.lean

def integerRingEquivPadicInt :
    𝒪[ℚ_[p]] ≃+* ℤ_[p] where
  toFun x := ⟨x, (integer_mem_iff_norm_le_one p x).1 x.property⟩
  invFun x := ⟨x, (integer_mem_iff_norm_le_one p x).2 x.property⟩
  left_inv _ := Subtype.ext rfl
  right_inv _ := Subtype.ext rfl
  map_add' _ _ := Subtype.ext rfl
  map_mul' _ _ := Subtype.ext rfl

theorem integerRingEquivPadicInt_coe (x : 𝒪[ℚ_[p]]) :
    ((integerRingEquivPadicInt p x : ℤ_[p]) : ℚ_[p]) = (x : ℚ_[p])

def integerRingEquivPadicDVRValuationSubring :
    𝒪[ℚ_[p]] ≃+*
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring

theorem integerRingEquivPadicDVRValuationSubring_coe
    (x : 𝒪[ℚ_[p]]) :
    ((integerRingEquivPadicDVRValuationSubring p x :
        (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring) :
      ℚ_[p]) = (x : ℚ_[p])

theorem unitsMapEquiv_mem_higherPrincipalUnitGroup_iff
    (n : ℕ) (u : 𝒪[ℚ_[p]]ˣ) :
    Units.mapEquiv (integerRingEquivPadicDVRValuationSubring p).toMulEquiv u ∈
        DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
          (DiscreteValuationField.Examples.Qp.padicCompleteDVF p) n ↔
      u ∈ principalUnits ℚ_[p] n

theorem principalUnits_map_eq_higherPrincipalUnitGroup (n : ℕ) :
    (principalUnits ℚ_[p] n).map
        (Units.mapEquiv
          (integerRingEquivPadicDVRValuationSubring p).toMulEquiv).toMonoidHom =
      DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
        (DiscreteValuationField.Examples.Qp.padicCompleteDVF p) n

def integerUnitsPrincipalQuotEquivPadicDVR (n : ℕ) :
    IntegerUnitsPrincipalQuot ℚ_[p] n ≃*
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubringˣ ⧸
        DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
          (DiscreteValuationField.Examples.Qp.padicCompleteDVF p) n

def padicDVRQuotientEquivZMod (n : ℕ) :
    (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicCompleteDVF p).valuationSubring ⧸
        (DiscreteValuationField.Examples.Qp.padicCompleteDVF p).maximalIdeal ^ n ≃+*
      ZMod (p ^ n)

theorem nat_card_integerUnitsPrincipalQuot_padic_succ (k : ℕ) :
    Nat.card (IntegerUnitsPrincipalQuot ℚ_[p] (k + 1)) =
      (p - 1) * p ^ k

def padicPrimeUnit : ℚ_[p]ˣ

def padicPrimeInteger : 𝒪[ℚ_[p]]

theorem padicPrimeInteger_coe :
    ((padicPrimeInteger p : 𝒪[ℚ_[p]]) : ℚ_[p]) = (p : ℚ_[p])

theorem padicPrimeInteger_irreducible :
    Irreducible (padicPrimeInteger p)

theorem valuationMap_padicPrimeUnit :
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap ℚ_[p]
        (Additive.ofMul (padicPrimeUnit p)) = -1

theorem valuationMap_padicPrimeUnit_inv :
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap ℚ_[p]
        (Additive.ofMul (padicPrimeUnit p)⁻¹) = 1

theorem nat_card_fieldUnitsUniformizerPrincipalQuot_padic_succ
    (k : ℕ) :
    Nat.card (ℚ_[p]ˣ ⧸ LocalFieldTheory.uniformizerPrincipalSubgroup ℚ_[p]
      (padicPrimeUnit p)⁻¹ 1 (k + 1)) = (p - 1) * p ^ k

theorem padicInt_exists_degree_root_of_mem_maximalIdeal_pow_succ
    (k : ℕ) (z : ℤ_[p])
    (hz : z ∈ IsLocalRing.maximalIdeal ℤ_[p] ^ (k + 1)) :
    ∃ b : ℤ_[p],
      b ∈ IsLocalRing.maximalIdeal ℤ_[p] ∧
      ((p - 1) * p ^ k) • b = z

instance padicDVR_residueField_finite :
    Finite (IsLocalRing.ResidueField
      (DiscreteValuationField.Examples.Qp.padicDVRValuation p).valuationSubring)

theorem padicDVR_residueCharacteristic :
    (LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
      (DiscreteValuationField.Examples.Qp.padicDVRValuation p)).residueCharacteristic = p

theorem padicDVR_valuation_p :
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p (p : ℚ_[p]) =
      WithZero.exp (-1 : ℤ)

theorem padicDVR_ramificationIndex_eq_one :
    LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
      (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p) = 1

theorem padicDVR_logExp_level_one_of_odd (hp2 : p ≠ 2) :
    (LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
          (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p) : ℚ) /
        (((LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
          (DiscreteValuationField.Examples.Qp.padicDVRValuation p)).residueCharacteristic : ℚ) -
            1) <
      (1 : ℚ)

theorem padicDVR_logExp_level_succ_of_odd
    (hp2 : p ≠ 2) (k : ℕ) :
    (LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
          (LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p) : ℚ) /
        (((LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
          (DiscreteValuationField.Examples.Qp.padicDVRValuation p)).residueCharacteristic : ℚ) -
            1) <
      (k + 1 : ℚ)

def expLogMulEquivOfWithZeroValuation
    {K : Type*} [Field K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v) (n : ℕ)
    (hlevel :
      (DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation v : ℚ) /
          (((DiscreteValuationField.LocalField.ofWithZeroValuation v).residueCharacteristic : ℚ)
            - 1) <
        (n : ℚ)) :
    Multiplicative
        ((DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation
          v).maximalIdeal ^ n :
          Ideal
            (completeDVFOfWithZeroValuation v).valuationSubring) ≃*
      DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
        (DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation v)
        n

theorem expLogMulEquivOfWithZeroValuation_fieldVal
    {K : Type*} [Field K]
    (v : Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v) (n : ℕ)
    (hlevel :
      (DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation v : ℚ) /
          (((DiscreteValuationField.LocalField.ofWithZeroValuation v).residueCharacteristic : ℚ)
            - 1) <
        (n : ℚ))
    (a : Multiplicative
      ((DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation
        v).maximalIdeal ^ n :
        Ideal
          (DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation
          v).valuationSubring)) :
    let F :=
      DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation v
    let E := expLogMulEquivOfWithZeroValuation v hv n hlevel
    ((((E a : DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F n) :
      F.valuationSubringˣ) :
        F.valuationSubring) : K) =
      DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesFieldOfWithZeroValuation
        v (((a.toAdd : F.valuationSubring) : K))
          (fun m =>
            Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let p : ℕ :=
    (LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation v).residueCharacteristic
  let _ : Fact p.Prime := by
    dsimp [p]
    infer_instance
  simp only [expLogMulEquivOfWithZeroValuation]
  simp only [
    DiscreteValuationField.MultiplicativeIntegerValuation.chosenExpLogContinuousMulEquiv,
    principalUnitExpLogContinuousMulEquivOfExact_ofWithZeroValuationScaled,
    principalUnitExpLogMulEquivOfExact_ofWithZeroValuationScaled]
  apply
    principalUnitExpSeries_maximalIdealPow_val_ofWithZeroValuationScaled
      (v := v) (p := p)
      (LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation v)
      n
  case hπval =>
    exact Classical.choose_spec
      (exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective
        v hv)
  case hπ =>
    exact
      DiscreteValuationField.WithZeroValuation.isUniformizer_of_valuation_eq_exp_neg_one
        v _
        (Classical.choose_spec
          (exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective
            v hv))
  case hlevel => exact hlevel
  case hnval =>
    intro m
    exact
      valuation_natCast_factorial_eq_exp_neg_ramificationIndex_mul_padicValNat
        v m
  case hcomplete =>
    exact
      DiscreteValuationField.WithZeroValuationTopology.completeSpace_ofWithZeroValuation
        v

theorem padicDVR_higherPrincipalUnit_degree_is_power_odd
    (hp2 : p ≠ 2) (k : ℕ) :
    let v := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p
    let F :=
      DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation v
    ∀ u : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F (k + 1),
      ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 1,
        (r : F.valuationSubringˣ) ^ ((p - 1) * p ^ k) =
          (u : F.valuationSubringˣ) := by
  let v := LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicDVRValuation p
  let F :=
    DiscreteValuationField.MultiplicativeIntegerValuation.completeDVFOfWithZeroValuation v
  change ∀ u : DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F (k + 1),
    ∃ r : LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 1,
      (r : F.valuationSubringˣ) ^ ((p - 1) * p ^ k) =
        (u : F.valuationSubringˣ)
  have hv : Function.Surjective v :=
    (IsDiscreteValuationRing.maximalIdeal ℤ_[p]).valuation_surjective ℚ_[p]
  let E1 := expLogMulEquivOfWithZeroValuation v hv 1
    (padicDVR_logExp_level_one_of_odd p hp2)
  let En := expLogMulEquivOfWithZeroValuation v hv (k + 1) (by
        simpa [Nat.cast_add, Nat.cast_one] using
          padicDVR_logExp_level_succ_of_odd p hp2 k)
  let eO : ℤ_[p] ≃+* F.valuationSubring :=
    LocalFieldTheory.DiscreteValuationField.Examples.Qp.padicIntEquivValuationSubring p
  intro u
  let a : Multiplicative (F.maximalIdeal ^ (k + 1) : Ideal F.valuationSubring) :=
    En.symm u
  let z : ℤ_[p] := eO.symm (a.toAdd : F.valuationSubring)
  have hz : z ∈ IsLocalRing.maximalIdeal ℤ_[p] ^ (k + 1) := by
    apply (ringEquiv_mem_maximalIdeal_pow_iff eO (k + 1) z).1
    simp [z]
  obtain ⟨b, hb, hdb⟩ :=
    padicInt_exists_degree_root_of_mem_maximalIdeal_pow_succ p k z hz
  have hbO : eO b ∈ F.maximalIdeal := by
    rw [← pow_one F.maximalIdeal]
    exact (ringEquiv_mem_maximalIdeal_pow_iff eO 1 b).2 (by simpa using hb)
  let b1 : (F.maximalIdeal ^ 1 : Ideal F.valuationSubring) :=
    ⟨eO b, by simpa using hbO⟩
  have hdbO : ((p - 1) * p ^ k) • (eO b) = (a.toAdd : F.valuationSubring) := by
    rw [← map_nsmul eO ((p - 1) * p ^ k) b, hdb]
    simp [z]
  let r : DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 1 := E1
    (Multiplicative.ofAdd b1)
  refine ⟨r, ?_⟩
  have hua : En a = u := En.apply_symm_apply u
  have hrpow :
      r ^ ((p - 1) * p ^ k) =
        E1 ((Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k)) := by
    change E1 (Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k) =
      E1 ((Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k))
    exact (map_pow E1 (Multiplicative.ofAdd b1) ((p - 1) * p ^ k)).symm
  change ((r ^ ((p - 1) * p ^ k) : DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F
    1) :
      F.valuationSubringˣ) = (u : F.valuationSubringˣ)
  rw [hrpow, ← hua]
  apply Units.ext
  apply Subtype.ext
  have hleft := expLogMulEquivOfWithZeroValuation_fieldVal v hv 1
    (padicDVR_logExp_level_one_of_odd p hp2)
    ((Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k))
  have hright := expLogMulEquivOfWithZeroValuation_fieldVal v hv (k + 1)
    (by
      simpa [Nat.cast_add, Nat.cast_one] using
        padicDVR_logExp_level_succ_of_odd p hp2 k) a
  have hleft' :
      ((((E1 ((Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k)) :
          DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F 1) : F.valuationSubringˣ) :
          F.valuationSubring) : ℚ_[p]) =
        DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesFieldOfWithZeroValuation
          v ((((Multiplicative.ofAdd b1) ^ ((p - 1) * p ^ k)).toAdd :
            F.valuationSubring) : ℚ_[p])
            (fun m =>
              Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)) := by
    exact hleft
  have hright' :
      ((((En a : DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F (k + 1)) :
        F.valuationSubringˣ) :
          F.valuationSubring) : ℚ_[p]) =
        DiscreteValuationField.MultiplicativeIntegerValuation.expSeriesFieldOfWithZeroValuation
          v ((a.toAdd : F.valuationSubring) : ℚ_[p])
            (fun m =>
              Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)) := by
    exact hright
  rw [hleft', hright']
  congr 2