equivInteger — Mathlib

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⟩)

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