arrow_mk_iso_iff — Mathlib

English

If there is an isomorphism between arrows f and f' with target affine, then P holds for f iff it holds for f'.

Русский

Если существует изоморфизм между стрелами f и f' с аффинной целью, то P(f) выполняется тогда и только тогда, когда выполняется P(f').

LaTeX

$$$\forall {f,f'} (e : f \cong f') [h: IsAffine Y], P(f) \iff P(f').$$$

Lean4

theorem arrow_mk_iso_iff (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y X' Y' : Scheme} {f : X ⟶ Y}
    {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') {h : IsAffine Y} :
    letI : IsAffine Y' := .of_isIso (Y := Y) e.inv.right
    P f ↔ P f' :=
  by rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]

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