homEquiv — Mathlib

English

There is a canonical equivalence (fully faithful) between morphisms of affine schemes and ring homomorphisms: Spec S → Spec R corresponds to a ring hom R → S, giving a natural isomorphism (fully faithful).

Русский

Существует каноническое соответствие между морфизмами аффинных схем и гомоморфизмами колец: Spec S → Spec R эквивалентно гомоморфизмам колец R → S, образующее естественную эквиваленцию (полная верность).

LaTeX

$$$(\mathrm{Spec}S \to \mathrm{Spec}R) \cong \mathrm{Hom}_{\mathrm{CommRing}}(R,S).$$$

Lean4

/-- Spec is fully faithful -/
@[simps]
def homEquiv {R S : CommRingCat} : (Spec S ⟶ Spec R) ≃ (R ⟶ S)
    where
  toFun := Spec.preimage
  invFun := Spec.map
  left_inv := Spec.map_preimage
  right_inv := Spec.preimage_map

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