SpecMap_iff — Mathlib

English

(Repeat of the Spec.map equivalence) The integral-ness of Spec.map φ is equivalent to φ itself being integral.

Русский

Повторение эквивалентности: интегральность Spec.map φ эквивалентна интегральности φ.

LaTeX

$$$IsIntegralHom(\mathrm{Spec.map}\ φ) \iff (φ.hom).IsIntegral$$$

Lean4

theorem SpecMap_iff {R S : CommRingCat} {φ : R ⟶ S} : IsIntegralHom (Spec.map φ) ↔ φ.hom.IsIntegral :=
  by
  have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso
  rw [HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom), and_iff_right]
  exacts
    [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral) (arrowIsoΓSpecOfIsAffine φ).symm,
    inferInstance]

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