English
Equality of two local properties: targetAffineLocally(affineAnd(Q)) equals IsAffineHom ∧ affineLocally(Q).
Русский
Равенство двух локальных свойств: targetAffineLocally(affineAnd(Q)) равно IsAffineHom ∧ affineLocally(Q).
LaTeX
$$$\\operatorname{targetAffineLocally}(\\operatorname{affineAnd}(Q)) = (\\operatorname{IsAffineHom} \\wedge \\operatorname{affineLocally}(Q))$$$
Lean4
theorem SpecMap_iff_of_affineAnd {P : MorphismProperty Scheme.{u}} (hP : HasAffineProperty P (affineAnd Q))
(hQi : RingHom.RespectsIso Q) {R S : CommRingCat.{u}} (f : R ⟶ S) : P (Spec.map f) ↔ Q f.hom :=
by
have := RingHom.toMorphismProperty_respectsIso_iff.mp hQi
rw [HasAffineProperty.iff_of_isAffine (P := P), affineAnd, and_iff_right]
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty Q) (arrowIsoΓSpecOfIsAffine f).symm,
inferInstance]