iff_isInteger_or_isInteger — Mathlib

English

The five properties listed are equivalent: ValuationRing R; the integer criterion for fractions; total divisibility; total ideals; local Bézout domain.

Русский

Пять перечисленных свойств эквивалентны: Валюационное кольцо; критерий целых для дробей; полная делимость; полный порядок идеалов; локальное Bezout-область.

LaTeX

$$$\\text{TFAE}\ (R) :\\; \\text{ValuationRing } R \\iff \\forall x\\in \\mathrm{FractionRing } R\\, (\\text{IsLocalization.IsInteger } R x \\lor \\text{IsLocalization.IsInteger } R x^{-1}) \\iff IsTotal R(\\cdot \\mid \\cdot) \\iff IsTotal (\\mathrm{Ideal } R)(\\le) \\iff (\\text{IsLocalRing } R \\land \\text{IsBezout } R)$$$

Lean4

theorem iff_isInteger_or_isInteger :
    ValuationRing R ↔ ∀ x : K, IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹ :=
  by
  constructor
  · intro H x
    obtain ⟨x : R, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) x
    have := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr (nonZeroDivisors.ne_zero hy)
    obtain ⟨s, rfl | rfl⟩ := ValuationRing.cond x y
    · exact Or.inr ⟨s, eq_inv_of_mul_eq_one_left <| by rwa [mul_div, div_eq_one_iff_eq, map_mul, mul_comm]⟩
    · exact Or.inl ⟨s, by rwa [eq_div_iff, map_mul, mul_comm]⟩
  · intro H
    suffices PreValuationRing R from mk
    constructor
    intro a b
    by_cases ha : a = 0; · subst ha; exact ⟨0, Or.inr <| mul_zero b⟩
    by_cases hb : b = 0; · subst hb; exact ⟨0, Or.inl <| mul_zero a⟩
    replace ha := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr ha
    replace hb := (map_ne_zero_iff _ (IsFractionRing.injective R K)).mpr hb
    obtain ⟨c, e⟩ | ⟨c, e⟩ := H (algebraMap R K a / algebraMap R K b)
    · rw [eq_div_iff hb, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm] at e
      exact ⟨c, Or.inr e⟩
    · rw [inv_div, eq_div_iff ha, ← map_mul, (IsFractionRing.injective R K).eq_iff, mul_comm c] at e
      exact ⟨c, Or.inl e⟩

Похожие утверждения