English
If 𝒪 is a domain with a valuation ring structure (ValuationRing 𝒪) inside K, then IsFractionRing 𝒪 K holds if and only if every x ∈ K can be written as algebraMap 𝒪 K(a) or its inverse, and the map algebraMap 𝒪 K is injective.
Русский
Если 𝒪 является доменом, внутри K имеет валюационное кольцо (ValuationRing 𝒪), то IsFractionRing 𝒪 K выполняется тогда и только тогда, когда каждый элемент x ∈ K можно записать в виде algebraMap 𝒪 K(a) или его обратного, и отображение algebraMap 𝒪 K инъективно.
LaTeX
$$$\text{IsFractionRing}(\mathcal{O}, K) \iff \Big( \forall x \in K, \exists a \in \mathcal{O}, x = \alpha(a) \lor x^{-1} = \alpha(a) \Big) \land \operatorname{Injective}(\alpha)$, где $\alpha = \operatorname{algebraMap}_{\mathcal{O},K}$$$
Lean4
theorem isFractionRing_iff [IsDomain 𝒪] [ValuationRing 𝒪] :
IsFractionRing 𝒪 K ↔
(∀ (x : K), ∃ a : 𝒪, x = algebraMap 𝒪 K a ∨ x⁻¹ = algebraMap 𝒪 K a) ∧ Function.Injective (algebraMap 𝒪 K) :=
by
refine ⟨fun h ↦ ⟨fun x ↦ ?_, IsFractionRing.injective _ _⟩, fun h ↦ ?_⟩
· obtain (⟨a, e⟩ | ⟨a, e⟩) := isInteger_or_isInteger 𝒪 x
exacts [⟨a, .inl e.symm⟩, ⟨a, .inr e.symm⟩]
· exact isFractionRing_of_exists_eq_algebraMap_or_inv_eq_algebraMap_of_injective h.1 h.2
