Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff

∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y X' Y' : AlgebraicGeometry.Scheme}
  {f : X ⟶ Y} {f' : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f')
  {h : AlgebraicGeometry.IsAffine Y}, P f ↔ P f'

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

4 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.MorphismProperty.RespectsIso