RationalLocalization.lean

def LocalizationAt (p : ℕ) : Subring ℚ where
  carrier := {q : ℚ | q.den.Coprime p}
  mul_mem' {a b} ha hb :=
    Nat.Coprime.coprime_dvd_left (Rat.mul_den_dvd a b) (ha.mul_left hb)
  one_mem' := by simp
  add_mem' {a b} ha hb :=
    Nat.Coprime.coprime_dvd_left (Rat.add_den_dvd a b) (ha.mul_left hb)
  zero_mem' := by simp
  neg_mem' {a} ha := by simpa using ha

theorem mem_iff_den_coprime {p : ℕ} (q : ℚ) :
    q ∈ Rat.LocalizationAt p ↔ q.den.Coprime p

theorem mem_iff_not_dvd_den {p : ℕ} (hp : p.Prime) (q : ℚ) :
    q ∈ Rat.LocalizationAt p ↔ ¬p ∣ q.den

theorem isUnit_iff_not_dvd_num {p : ℕ} (hp : p.Prime) (x : Rat.LocalizationAt p) :
    IsUnit x ↔ ¬p ∣ (x : ℚ).num.natAbs

theorem isLocalization {p : ℕ} (hp : p.Prime)
    [(Ideal.span {(p : ℤ)}).IsPrime] :
    IsLocalization.AtPrime (Rat.LocalizationAt p) (Ideal.span {(p : ℤ)})

def denominatorMonoid (p : ℕ) : Submonoid ℤ where
  carrier := {z : ℤ | z ≠ 0 ∧ ((z : ℚ)⁻¹ ∈ Rat.LocalizationAt p)}
  one_mem' := by
    refine ⟨one_ne_zero, ?_⟩
    rw [Int.cast_one, inv_one, mem_iff_den_coprime]
    simp
  mul_mem' := by
    rintro a b ⟨ha0, ha⟩ ⟨hb0, hb⟩
    refine ⟨mul_ne_zero ha0 hb0, ?_⟩
    rw [Int.cast_mul, mul_inv]
    exact mul_mem ha hb

lemma natCast_den_mem_denominatorMonoid {p : ℕ} {q : ℚ}
    (hq : q ∈ Rat.LocalizationAt p) : (q.den : ℤ) ∈ denominatorMonoid p

instance denominatorMonoid_isLocalization (p : ℕ) :
    IsLocalization (denominatorMonoid p) (Rat.LocalizationAt p)

theorem isFractionRing (p : ℕ) : IsFractionRing (Rat.LocalizationAt p) ℚ

theorem isPrincipalIdealRing (p : ℕ) : IsPrincipalIdealRing (Rat.LocalizationAt p)

theorem denominatorMonoid_eq_primeCompl {p : ℕ} (hp : p.Prime)
    [(Ideal.span {(p : ℤ)}).IsPrime] :
    denominatorMonoid p = (Ideal.span {(p : ℤ)}).primeCompl

theorem isDiscreteValuationRing (p : ℕ) (hp : p.Prime) :
    IsDiscreteValuationRing (Rat.LocalizationAt p)

theorem irreducible_natCast (p : ℕ) (hp : p.Prime) :
    Irreducible ((p : ℕ) : Rat.LocalizationAt p)