English
There exists a ring isomorphism between A and the integer part (valuation A K).integer, i.e., ValuationRing.equivInteger A K: A ≃+* (valuation A K).integer.
Русский
Существует кольцевой изоморфизм между A и кольцом целых оценки (valuation A K).integer, то есть ValuationRing.equivInteger A K: A ≃+* (valuation A K).integer.
LaTeX
$$$A \\cong_{\\text{ring}} (\\operatorname{valuation} A K).\\operatorname{integer}$$$
Lean4
/-- The valuation ring `A` is isomorphic to the ring of integers of its associated valuation. -/
noncomputable def equivInteger : A ≃+* (valuation A K).integer :=
RingEquiv.ofBijective
(show A →ₙ+* (valuation A K).integer from
{ toFun := fun a => ⟨algebraMap A K a, (mem_integer_iff _ _ _).mpr ⟨a, rfl⟩⟩
map_mul' := fun _ _ => by ext1; exact (algebraMap A K).map_mul _ _
map_zero' := by ext1; exact (algebraMap A K).map_zero
map_add' := fun _ _ => by ext1; exact (algebraMap A K).map_add _ _ })
(by
constructor
· intro x y h
apply_fun (algebraMap (valuation A K).integer K) at h
exact IsFractionRing.injective _ _ h
· rintro ⟨-, ha⟩
rw [mem_integer_iff] at ha
obtain ⟨a, rfl⟩ := ha
exact ⟨a, rfl⟩)