iff_of_isAffine — Mathlib

English

If X and Y are affine, then SurjectiveOnStalks f is equivalent to the surjectivity of the induced ring homomorphism on global sections.

Русский

Если X и Y аффинны, то SurjectiveOnStalks f эквивалентна суръективности гомоморфизма колец на глобальных секциях.

LaTeX

$$iff_of_isAffine [IsAffine X] [IsAffine Y] : SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (f.app ⊤).hom$$

Lean4

theorem iff_of_isAffine [IsAffine X] [IsAffine Y] : SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (f.app ⊤).hom :=
  by rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)]

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