Core.lean

theorem uniformizerPowerIdeal_primeElement_eq_exponentialMaxIdeal_pow_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n =
      (exponentialMaxIdeal v) ^ n

theorem uniformizerPowerIdeal_primeElement_eq_maximalIdeal_pow_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n =
      (IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n

def residue_addEquiv_maximalIdeal_pow_quotient
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    (exponentialValuationSubring v ⧸
      IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ≃+
      Ideal.map
        (Ideal.Quotient.mk
          ((IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ (n + 1)))
        ((IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n)

def residue_addEquiv_uniformizerPowerIdeal_quotient
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    (exponentialValuationSubring v ⧸
      uniformizerPowerIdeal (primeElementInValuationSubring v hπ) 1) ≃+
      Ideal.map
        (Ideal.Quotient.mk
          (uniformizerPowerIdeal (primeElementInValuationSubring v hπ) (n + 1)))
        (uniformizerPowerIdeal (primeElementInValuationSubring v hπ) n)

def uniformizerGradedPiece {O : Type*} [CommRing O] (π : O) (n : ℕ) : Type _

instance uniformizerGradedPieceAddCommGroup
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    AddCommGroup (uniformizerGradedPiece π n)

instance uniformizerGradedPieceModule
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    Module O (uniformizerGradedPiece π n)

def uniformizerGradedPieceConcreteLinearEquiv
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    uniformizerGradedPiece π n ≃ₗ[O]
      ((uniformizerPowerIdeal π n) ⧸
        (Submodule.comap (uniformizerPowerIdeal π n).subtype
          (uniformizerPowerIdeal π (n + 1) : Submodule O O) :
            Submodule O (uniformizerPowerIdeal π n)))

def uniformizerGradedPieceMk
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    uniformizerPowerIdeal π n →ₗ[O] uniformizerGradedPiece π n

theorem uniformizerGradedPieceConcreteLinearEquiv_mk
    {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (a : uniformizerPowerIdeal π n) :
    uniformizerGradedPieceConcreteLinearEquiv π n
        (uniformizerGradedPieceMk π n a) =
      Submodule.Quotient.mk a

theorem uniformizerGradedPieceMk_surjective
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    Function.Surjective (uniformizerGradedPieceMk π n)

theorem uniformizerGradedPiece.inductionOn
    {O : Type*} [CommRing O] (π : O) (n : ℕ)
    {motive : uniformizerGradedPiece π n → Prop}
    (q : uniformizerGradedPiece π n)
    (h : ∀ a : uniformizerPowerIdeal π n,
      motive (uniformizerGradedPieceMk π n a)) :
    motive q

def uniformizerGradedPieceLinearLift
    {O M : Type*} [CommRing O] [AddCommGroup M] [Module O M]
    (π : O) (n : ℕ)
    (f : uniformizerPowerIdeal π n →ₗ[O] M)
    (h :
      (Submodule.comap (uniformizerPowerIdeal π n).subtype
        (uniformizerPowerIdeal π (n + 1) : Submodule O O) :
          Submodule O (uniformizerPowerIdeal π n)) ≤ f.ker) :
    uniformizerGradedPiece π n →ₗ[O] M

theorem uniformizerGradedPieceLinearLift_mk
    {O M : Type*} [CommRing O] [AddCommGroup M] [Module O M]
    (π : O) (n : ℕ)
    (f : uniformizerPowerIdeal π n →ₗ[O] M)
    (h :
      (Submodule.comap (uniformizerPowerIdeal π n).subtype
        (uniformizerPowerIdeal π (n + 1) : Submodule O O) :
          Submodule O (uniformizerPowerIdeal π n)) ≤ f.ker)
    (a : uniformizerPowerIdeal π n) :
    uniformizerGradedPieceLinearLift π n f h
        (uniformizerGradedPieceMk π n a) = f a

theorem uniformizerGradedPieceMk_eq_zero_iff
    {O : Type*} [CommRing O] (π : O) (n : ℕ)
    (a : uniformizerPowerIdeal π n) :
    uniformizerGradedPieceMk π n a = 0 ↔
      a ∈
        (Submodule.comap (uniformizerPowerIdeal π n).subtype
          (uniformizerPowerIdeal π (n + 1) : Submodule O O) :
            Submodule O (uniformizerPowerIdeal π n))

def HigherUnit {O : Type*} [CommRing O] (π : O) (n : ℕ) (u : Oˣ) : Prop

theorem higherUnit_iff_sub_one_mem_powerIdeal {O : Type*} [CommRing O]
    (π : O) (n : ℕ) (u : Oˣ) :
    HigherUnit π n u ↔ (u : O) - 1 ∈ uniformizerPowerIdeal π n

def higherUnitSubgroup {O : Type*} [CommRing O] (π : O) (n : ℕ) : Subgroup Oˣ where
  carrier := {u | HigherUnit π n u}
  one_mem' := by
    use 0
    simp
  mul_mem' := by
    rintro u v ⟨a, ha⟩ ⟨b, hb⟩
    use a + b + π ^ n * a * b
    calc
      ((u * v : Oˣ) : O) = (u : O) * (v : O) := rfl
      _ = (1 + π ^ n * a) * (1 + π ^ n * b) := by rw [ha, hb]
      _ = 1 + π ^ n * (a + b + π ^ n * a * b) := by ring
  inv_mem' := by
    rintro u ⟨a, ha⟩
    use -((u⁻¹ : Oˣ) : O) * a
    have hmul : ((u⁻¹ : Oˣ) : O) * (u : O) = 1 := by
      simp
    calc
      ((u⁻¹ : Oˣ) : O) =
          ((u⁻¹ : Oˣ) : O) * (u : O) -
            ((u⁻¹ : Oˣ) : O) * ((u : O) - 1) := by
        ring
      _ = 1 - ((u⁻¹ : Oˣ) : O) * ((u : O) - 1) := by
        rw [hmul]
      _ = 1 + π ^ n * (-((u⁻¹ : Oˣ) : O) * a) := by
        rw [ha]
        ring

theorem mem_higherUnitSubgroup {O : Type*} [CommRing O]
    {π : O} {n : ℕ} {u : Oˣ} :
    u ∈ higherUnitSubgroup π n ↔ HigherUnit π n u

theorem mem_higherUnitSubgroup_iff_sub_one_mem_powerIdeal
    {O : Type*} [CommRing O] {π : O} {n : ℕ} {u : Oˣ} :
    u ∈ higherUnitSubgroup π n ↔ (u : O) - 1 ∈ uniformizerPowerIdeal π n

theorem mem_higherUnitSubgroup_primeElement_iff_sub_one_mem_maximalIdeal_pow
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) {n : ℕ}
    {u : (exponentialValuationSubring v)ˣ} :
    u ∈ higherUnitSubgroup (primeElementInValuationSubring v hπ) n ↔
      (u : exponentialValuationSubring v) - 1 ∈
        (IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n

theorem higherUnit_coeff_unique {O : Type*} [CommRing O] [IsDomain O]
    {π : O} {n : ℕ} (hπ0 : π ≠ 0) {u : Oˣ} {a b : O}
    (ha : (u : O) = 1 + π ^ n * a)
    (hb : (u : O) = 1 + π ^ n * b) :
    a = b

def chosenHigherUnitCoeff {O : Type*} [CommRing O]
    (π : O) (n : ℕ) (u : higherUnitSubgroup π n) : O

theorem chosenHigherUnitCoeff_spec {O : Type*} [CommRing O]
    (π : O) (n : ℕ) (u : higherUnitSubgroup π n) :
    ((u : Oˣ) : O) = 1 + π ^ n * chosenHigherUnitCoeff π n u

theorem chosenHigherUnitCoeff_eq_of_repr {O : Type*} [CommRing O] [IsDomain O]
    {π : O} {n : ℕ} (hπ0 : π ≠ 0) {u : higherUnitSubgroup π n} {a : O}
    (ha : ((u : Oˣ) : O) = 1 + π ^ n * a) :
    chosenHigherUnitCoeff π n u = a

theorem higherUnitSubgroup_succ_le {O : Type*} [CommRing O]
    (π : O) (n : ℕ) :
    higherUnitSubgroup π (n + 1) ≤ higherUnitSubgroup π n

theorem higherUnitSubgroup_zero_eq_top {O : Type*} [CommRing O]
    (π : O) :
    higherUnitSubgroup π 0 = ⊤

theorem higherUnitSubgroup_le_of_le {O : Type*} [CommRing O]
    (π : O) {m n : ℕ} (hmn : m ≤ n) :
    higherUnitSubgroup π n ≤ higherUnitSubgroup π m

theorem isUnit_one_add_of_mem_maximalIdeal {O : Type*} [CommRing O] [IsLocalRing O]
    {x : O} (hx : x ∈ IsLocalRing.maximalIdeal O) :
    IsUnit (1 + x)

def unitReduction {O : Type*} [CommRing O] (I : Ideal O) : Oˣ →* (O ⧸ I)ˣ

theorem unitReduction_apply {O : Type*} [CommRing O] (I : Ideal O) (u : Oˣ) :
    (unitReduction I u : O ⧸ I) = Ideal.Quotient.mk I (u : O)

theorem unitReduction_ker_powerIdeal {O : Type*} [CommRing O]
    (π : O) (n : ℕ) :
    (unitReduction (uniformizerPowerIdeal π n)).ker = higherUnitSubgroup π n

theorem unitReduction_ker_maximalIdeal_pow_primeElement_of_normalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ) :
    (unitReduction
      ((IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n)).ker =
      higherUnitSubgroup (primeElementInValuationSubring v hπ) n

theorem unitReduction_surjective_of_isLocalHom {O : Type*} [CommRing O]
    (I : Ideal O) [IsLocalHom (Ideal.Quotient.mk I)] :
    Function.Surjective (unitReduction I)

theorem unitReduction_isLocalHom_maximalIdeal_pow_of_pos
    {K : Type*} [Field K] (v : ExponentialValuation K)
    {n : ℕ} (hn : 1 ≤ n) :
    IsLocalHom
      (Ideal.Quotient.mk
        ((IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n))

def unitsModPowerIdealEquivOfSurjective {O : Type*} [CommRing O]
    (π : O) (n : ℕ)
    (hsurj : Function.Surjective (unitReduction (uniformizerPowerIdeal π n))) :
    Oˣ ⧸ higherUnitSubgroup π n ≃* (O ⧸ uniformizerPowerIdeal π n)ˣ

def unitsModPowerIdealEquivOfIsLocalHom {O : Type*} [CommRing O]
    (π : O) (n : ℕ) [IsLocalHom (Ideal.Quotient.mk (uniformizerPowerIdeal π n))] :
    Oˣ ⧸ higherUnitSubgroup π n ≃* (O ⧸ uniformizerPowerIdeal π n)ˣ

def unitsModMaximalIdealPowEquivOfSurjectiveNormalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) (n : ℕ)
    (hsurj : Function.Surjective
      (unitReduction
        ((IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n))) :
    ((exponentialValuationSubring v)ˣ ⧸
        higherUnitSubgroup (primeElementInValuationSubring v hπ) n) ≃*
      (exponentialValuationSubring v ⧸
        (IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n)ˣ

def unitsModMaximalIdealPowEquivOfNormalized
    {K : Type*} [Field K] {v : ExponentialValuation K}
    (hv : NormalizedExponentialValuation v) {π : K}
    (hπ : PrimeElementFor v π) {n : ℕ} (hn : 1 ≤ n) :
    ((exponentialValuationSubring v)ˣ ⧸
        higherUnitSubgroup (primeElementInValuationSubring v hπ) n) ≃*
      (exponentialValuationSubring v ⧸
        (IsLocalRing.maximalIdeal (exponentialValuationSubring v)) ^ n)ˣ

theorem uniformizerPowerIdeal_le_span_singleton {O : Type*} [CommRing O]
    {π : O} {n : ℕ} (hn : 1 ≤ n) :
    uniformizerPowerIdeal π n ≤ Ideal.span ({π} : Set O)

theorem uniformizerPowerIdeal_le_jacobson_bot {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    uniformizerPowerIdeal π n ≤ Ideal.jacobson (⊥ : Ideal O)

theorem unitReduction_isLocalHom_of_dvr {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    IsLocalHom (Ideal.Quotient.mk (uniformizerPowerIdeal π n))

def higherUnitCoeffModHom {O : Type*}
    [CommRing O] [IsDomain O] {π : O} (hπ0 : π ≠ 0) (n : ℕ) (hn : 1 ≤ n) :
    higherUnitSubgroup π n →*
      Multiplicative (O ⧸ Ideal.span ({π} : Set O)) where
  toFun u :=
    Multiplicative.ofAdd
      (Ideal.Quotient.mk (Ideal.span ({π} : Set O)) (chosenHigherUnitCoeff π n u))
  map_one' := by
    apply Multiplicative.ofAdd.injective
    change Ideal.Quotient.mk (Ideal.span ({π} : Set O))
        (chosenHigherUnitCoeff π n (1 : higherUnitSubgroup π n)) = 0
    have hcoeff :
        chosenHigherUnitCoeff π n (1 : higherUnitSubgroup π n) = 0 := by
      apply chosenHigherUnitCoeff_eq_of_repr hπ0
      simp
    rw [hcoeff]
    simp
  map_mul' u v := by
    apply Multiplicative.ofAdd.injective
    let I : Ideal O := Ideal.span ({π} : Set O)
    let cu : O := chosenHigherUnitCoeff π n u
    let cv : O := chosenHigherUnitCoeff π n v
    let cuv : O := chosenHigherUnitCoeff π n (u * v)
    have hu : ((u : Oˣ) : O) = 1 + π ^ n * cu :=
      chosenHigherUnitCoeff_spec π n u
    have hv : ((v : Oˣ) : O) = 1 + π ^ n * cv :=
      chosenHigherUnitCoeff_spec π n v
    have hrepr : (((u * v : higherUnitSubgroup π n) : Oˣ) : O) =
        1 + π ^ n * (cu + cv + π ^ n * cu * cv) := by
      calc
        (((u * v : higherUnitSubgroup π n) : Oˣ) : O) =
            ((u : Oˣ) : O) * ((v : Oˣ) : O) := rfl
        _ = (1 + π ^ n * cu) * (1 + π ^ n * cv) := by rw [hu, hv]
        _ = 1 + π ^ n * (cu + cv + π ^ n * cu * cv) := by ring
    have hcuv : cuv = cu + cv + π ^ n * cu * cv :=
      chosenHigherUnitCoeff_eq_of_repr hπ0 hrepr
    change Ideal.Quotient.mk I cuv =
      Ideal.Quotient.mk I cu + Ideal.Quotient.mk I cv
    rw [hcuv]
    change Ideal.Quotient.mk I (cu + cv + π ^ n * cu * cv) =
      Ideal.Quotient.mk I (cu + cv)
    apply Ideal.Quotient.eq.mpr
    have hpow_mem : π ^ n * cu * cv ∈ I := by
      have hbase : π ^ n ∈ uniformizerPowerIdeal π n :=
        Ideal.subset_span (by simp)
      have hmem' : π ^ n * (cu * cv) ∈ I :=
        uniformizerPowerIdeal_le_span_singleton (π := π) hn
          ((uniformizerPowerIdeal π n).mul_mem_right (cu * cv) hbase)
      simpa [mul_assoc] using hmem'
    have hdiff : (cu + cv + π ^ n * cu * cv) - (cu + cv) = π ^ n * cu * cv := by
      ring
    simpa [I, hdiff]
      using hpow_mem

theorem higherUnitCoeffModHom_ker {O : Type*}
    [CommRing O] [IsDomain O] {π : O} (hπ0 : π ≠ 0) (n : ℕ) (hn : 1 ≤ n) :
    (higherUnitCoeffModHom (O := O) hπ0 n hn).ker =
      Subgroup.comap (higherUnitSubgroup π n).subtype
        (higherUnitSubgroup π (n + 1))

theorem higherUnitCoeffModHom_surjective {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) :
    Function.Surjective (higherUnitCoeffModHom (O := O) hπ.ne_zero n hn)

def higherUnitOneAdd {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) (a : O) :
    higherUnitSubgroup π n

theorem higherUnitOneAdd_val {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) (a : O) :
    (((higherUnitOneAdd hπ n hn a : higherUnitSubgroup π n) : Oˣ) : O) =
      1 + π ^ n * a

theorem chosenHigherUnitCoeff_oneAdd {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) (a : O) :
    chosenHigherUnitCoeff π n (higherUnitOneAdd hπ n hn a) = a

theorem higherUnitCoeffModHom_oneAdd {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) (a : O) :
    higherUnitCoeffModHom (O := O) hπ.ne_zero n hn
      (higherUnitOneAdd hπ n hn a) =
        Multiplicative.ofAdd
          (Ideal.Quotient.mk (Ideal.span ({π} : Set O)) a)

theorem higherUnitCoeffModHom_apply_of_repr {O : Type*}
    [CommRing O] [IsDomain O] {π : O} (hπ0 : π ≠ 0)
    {n : ℕ} (hn : 1 ≤ n) {u : higherUnitSubgroup π n} {a : O}
    (ha : ((u : Oˣ) : O) = 1 + π ^ n * a) :
    higherUnitCoeffModHom (O := O) hπ0 n hn u =
      Multiplicative.ofAdd
        (Ideal.Quotient.mk (Ideal.span ({π} : Set O)) a)

def higherUnitGradedPieceMulEquivResidue {O : Type*}
    [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) (n : ℕ) (hn : 1 ≤ n) :
    ((higherUnitSubgroup π n) ⧸
      Subgroup.comap (higherUnitSubgroup π n).subtype
        (higherUnitSubgroup π (n + 1))) ≃*
      Multiplicative (O ⧸ Ideal.span ({π} : Set O))

theorem units_reduction_kernel
    {O : Type*} [CommRing O] (π : O) (n : ℕ) :
    (unitReduction (uniformizerPowerIdeal π n)).ker = higherUnitSubgroup π n

theorem units_reduction_surjective
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    Function.Surjective (unitReduction (uniformizerPowerIdeal π n))

def units_quotient_equiv
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    Oˣ ⧸ higherUnitSubgroup π n ≃* (O ⧸ uniformizerPowerIdeal π n)ˣ

theorem units_quotient_equiv_mk
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) (u : Oˣ) :
    units_quotient_equiv hπ hn (QuotientGroup.mk u) =
      unitReduction (uniformizerPowerIdeal π n) u

theorem higher_unit_coeff_kernel
    {O : Type*} [CommRing O] [IsDomain O]
    {π : O} (hπ0 : π ≠ 0) {n : ℕ} (hn : 1 ≤ n) :
    (higherUnitCoeffModHom (O := O) hπ0 n hn).ker =
      Subgroup.comap (higherUnitSubgroup π n).subtype
        (higherUnitSubgroup π (n + 1))

theorem higher_unit_coeff_surjective
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    Function.Surjective (higherUnitCoeffModHom (O := O) hπ.ne_zero n hn)

def higher_unit_graded_equiv
    {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
    {π : O} (hπ : Irreducible π) {n : ℕ} (hn : 1 ≤ n) :
    Additive
      ((higherUnitSubgroup π n) ⧸
        Subgroup.comap (higherUnitSubgroup π n).subtype
          (higherUnitSubgroup π (n + 1))) ≃+
      (O ⧸ Ideal.span ({π} : Set O))