English
If every x ∈ K is either algebraMap(𝒪) mapped or the inverse of such an algebraMap, and algebraMap 𝒪 K is injective, then 𝒪 is a fraction ring of K.
Русский
Если для каждого x ∈ K существует a ∈ 𝒪, такой что x = algebraMap 𝒪 K a или x⁻¹ = algebraMap 𝒪 K a, и алгебраMap 𝒪 K инъективна, тогда 𝒪 является дробно-кольцом K.
LaTeX
$$$IsFractionRing 𝒪 K$$$
Lean4
theorem _root_.isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective
(h : ∀ (x : K), ∃ a : 𝒪, x = algebraMap 𝒪 K a ∨ x⁻¹ = algebraMap 𝒪 K a)
(hinj : Function.Injective (algebraMap 𝒪 K)) : IsFractionRing 𝒪 K :=
by
have : IsDomain 𝒪 := hinj.isDomain
constructor
· intro a
simpa using hinj.ne_iff.mpr (nonZeroDivisors.ne_zero a.2)
· intro x
obtain ⟨a, ha⟩ := h x
by_cases h0 : a = 0
· refine ⟨⟨0, 1⟩, by simpa [h0, eq_comm] using ha⟩
· have : algebraMap 𝒪 K a ≠ 0 := by simpa using hinj.ne_iff.mpr h0
rw [inv_eq_iff_eq_inv, ← one_div, eq_div_iff this] at ha
cases ha with
| inl ha => exact ⟨⟨a, 1⟩, by simpa⟩
| inr ha => exact ⟨⟨1, ⟨a, mem_nonZeroDivisors_of_ne_zero h0⟩⟩, by simpa using ha⟩
· intro _ _ hab
exact ⟨1, by simp only [OneMemClass.coe_one, hinj hab, one_mul]⟩
