SpecMap_iff_of_affineAnd — Mathlib

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]

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