Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk

∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
  (∀ {X Y Z : AlgebraicGeometry.Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : AlgebraicGeometry.IsAffine Z],
      P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) →
    (∀ {X Y Z : AlgebraicGeometry.Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y],
        P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) →
      P.toProperty.RespectsIso

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

1 results in Mathlib

Foundations

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