Properties of morphisms between Schemes

We provide the basic framework for talking about properties of morphisms between Schemes.

A MorphismProperty Scheme is a predicate on morphisms between schemes. For properties local at the target, its behaviour is entirely determined by its definition on morphisms into affine schemes, which we call an AffineTargetMorphismProperty. In this file, we provide API lemmas for properties local at the target, and special support for those properties whose AffineTargetMorphismProperty takes on a more simple form. We also provide API lemmas for properties local at the target. The main interfaces of the API are the typeclasses IsLocalAtTarget, IsLocalAtSource and HasAffineProperty, which we describle in detail below.

IsLocalAtTarget

• AlgebraicGeometry.IsLocalAtTarget: We say that IsLocalAtTarget P for P : MorphismProperty Scheme if

1. P respects isomorphisms.
2. P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

For a morphism property P local at the target and f : X ⟶ Y, we provide these API lemmas:

• AlgebraicGeometry.IsLocalAtTarget.of_isPullback: P is preserved under pullback along open immersions.
• AlgebraicGeometry.IsLocalAtTarget.restrict: P f → P (f ∣_ U) for an open U of Y.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top: P f ↔ ∀ i, P (f ∣_ U i) for a family U i of open sets covering Y.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover: P f ↔ ∀ i, P (𝒰.pullbackHom f i) for 𝒰 : Y.openCover.

IsLocalAtSource

• AlgebraicGeometry.IsLocalAtSource: We say that IsLocalAtSource P for P : MorphismProperty Scheme if

1. P respects isomorphisms.
2. P holds for 𝒰.map i ≫ f for an open cover 𝒰 of X iff P holds for f : X ⟶ Y.

For a morphism property P local at the source and f : X ⟶ Y, we provide these API lemmas:

• AlgebraicGeometry.IsLocalAtTarget.comp: P is preserved under composition with open immersions at the source.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top: P f ↔ ∀ i, P (U.ι ≫ f) for a family U i of open sets covering X.
• AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover: P f ↔ ∀ i, P (𝒰.map i ≫ f) for 𝒰 : X.openCover.
• AlgebraicGeometry.IsLocalAtTarget.of_isOpenImmersion: If P contains identities then P holds for open immersions.

AffineTargetMorphismProperty

• AlgebraicGeometry.AffineTargetMorphismProperty: The type of predicates on f : X ⟶ Y with Y affine.
• AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal: We say that P.IsLocal if P satisfies the assumptions of the affine communication lemma (AlgebraicGeometry.of_affine_open_cover). That is,
  1. P respects isomorphisms.
  2. If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basicOpen r for any global section r.
  3. If P holds for f ∣_ Y.basicOpen r for all r in a spanning set of the global sections, then P holds for f.

HasAffineProperty

• AlgebraicGeometry.HasAffineProperty: HasAffineProperty P Q is a type class asserting that P is local at the target, and over affine schemes, it is equivalent to Q : AffineTargetMorphismProperty.

For HasAffineProperty P Q and f : X ⟶ Y, we provide these API lemmas:

• AlgebraicGeometry.HasAffineProperty.of_isPullback: P is preserved under pullback along open immersions from affine schemes.
• AlgebraicGeometry.HasAffineProperty.restrict: P f → Q (f ∣_ U) for affine U of Y.
• AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top: P f ↔ ∀ i, Q (f ∣_ U i) for a family U i of affine open sets covering Y.
• AlgebraicGeometry.HasAffineProperty.iff_of_openCover: P f ↔ ∀ i, P (𝒰.pullbackHom f i) for affine open covers 𝒰 of Y.
• AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange_mk: If Q is stable under affine base change, then P is stable under arbitrary base change.

class AlgebraicGeometry.IsLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) : Prop

We say that P : MorphismProperty Scheme is local at the target if

1. P respects isomorphisms.
2. P holds for f ∣_ U for an open cover U of Y if and only if P holds for f. Also see IsLocalAtTarget.mk' for a convenient constructor.

• respectsIso : P.RespectsIso

  P respects isomorphisms.

• iff_of_openCover' {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) : P f ↔ ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)

  P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

theorem AlgebraicGeometry.IsLocalAtTarget.mk' {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] (restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)) (of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) : IsLocalAtTarget P

P is local at the target if

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.
3. If P holds for f ∣_ U for an open cover U of Y, then P holds for f.

instance AlgebraicGeometry.IsLocalAtTarget.inf (P Q : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] [IsLocalAtTarget Q] : IsLocalAtTarget (P ⊓ Q)

The intersection of two morphism properties that are local at the target is again local at the target.

theorem AlgebraicGeometry.IsLocalAtTarget.of_isPullback {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} {UX UY : Scheme} {iY : UY ⟶ Y} [IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : CategoryTheory.IsPullback iX f' f iY) (H : P f) : P f'

theorem AlgebraicGeometry.IsLocalAtTarget.restrict {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} (hf : P f) (U : Y.Opens) : P (f ∣_ U)

theorem AlgebraicGeometry.IsLocalAtTarget.of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → Y.Opens) (hU : iSup U = ⊤) (H : ∀ (i : ι), P (f ∣_ U i)) : P f

theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → Y.Opens) (hU : iSup U = ⊤) : P f ↔ ∀ (i : ι), P (f ∣_ U i)

theorem AlgebraicGeometry.IsLocalAtTarget.of_openCover {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) (H : ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)) : P f

theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) : P f ↔ ∀ (i : 𝒰.1), P (Scheme.Cover.pullbackHom 𝒰 f i)

theorem AlgebraicGeometry.IsLocalAtTarget.of_range_subset_iSup {P : CategoryTheory.MorphismProperty Scheme} [hP : IsLocalAtTarget P] {X Y : Scheme} {f : X ⟶ Y} [P.RespectsRight IsOpenImmersion] {ι : Type u_1} (U : ι → Y.Opens) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⊆ ↑(⨆ (i : ι), U i)) (hf : ∀ (i : ι), P (f ∣_ U i)) : P f

instance AlgebraicGeometry.IsLocalAtTarget.top : IsLocalAtTarget ⊤

class AlgebraicGeometry.IsLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) : Prop

We say that P : MorphismProperty Scheme is local at the source if

1. P respects isomorphisms.
2. P holds for 𝒰.map i ≫ f for an open cover 𝒰 of X iff P holds for f : X ⟶ Y. Also see IsLocalAtSource.mk' for a convenient constructor.

• respectsIso : P.RespectsIso

  P respects isomorphisms.

• iff_of_openCover' {X Y : Scheme} (f : X ⟶ Y) (𝒰 : X.OpenCover) : P f ↔ ∀ (i : 𝒰.J), P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)

  P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

theorem AlgebraicGeometry.IsLocalAtSource.mk' {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] (restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (CategoryTheory.CategoryStruct.comp U.ι f)) (of_sSup_eq_top : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) → P f) : IsLocalAtSource P

P is local at the source if

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for U.ι ≫ f for any U.
3. If P holds for U.ι ≫ f for an open cover U of X, then P holds for f.

instance AlgebraicGeometry.IsLocalAtSource.inf (P Q : CategoryTheory.MorphismProperty Scheme) [IsLocalAtSource P] [IsLocalAtSource Q] : IsLocalAtSource (P ⊓ Q)

The intersection of two morphism properties that are local at the target is again local at the target.

theorem AlgebraicGeometry.IsLocalAtSource.comp {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} {UX : Scheme} (H : P f) (i : UX ⟶ X) [IsOpenImmersion i] : P (CategoryTheory.CategoryStruct.comp i f)

instance AlgebraicGeometry.IsLocalAtSource.respectsLeft_isOpenImmersion {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] : P.RespectsLeft IsOpenImmersion

If P is local at the source, then it respects composition on the left with open immersions.

theorem AlgebraicGeometry.IsLocalAtSource.of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → X.Opens) (hU : iSup U = ⊤) (H : ∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) : P f

theorem AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → X.Opens) (hU : iSup U = ⊤) : P f ↔ ∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)

theorem AlgebraicGeometry.IsLocalAtSource.of_openCover {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : X.OpenCover) (H : ∀ (i : 𝒰.J), P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)) : P f

theorem AlgebraicGeometry.IsLocalAtSource.iff_of_openCover {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : X.OpenCover) : P f ↔ ∀ (i : 𝒰.J), P (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)

theorem AlgebraicGeometry.IsLocalAtSource.of_isOpenImmersion {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} (f : X ⟶ Y) [P.ContainsIdentities] [IsOpenImmersion f] : P f

theorem AlgebraicGeometry.IsLocalAtSource.isLocalAtTarget {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] [P.IsMultiplicative] (hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (CategoryTheory.CategoryStruct.comp f g) → P f) : IsLocalAtTarget P

theorem AlgebraicGeometry.IsLocalAtSource.sigmaDesc {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X : Scheme} {ι : Type v} [Small.{u, v} ι] {Y : ι → Scheme} {f : (i : ι) → Y i ⟶ X} (hf : ∀ (i : ι), P (f i)) : P (CategoryTheory.Limits.Sigma.desc f)

instance AlgebraicGeometry.IsLocalAtSource.top : IsLocalAtSource ⊤

theorem AlgebraicGeometry.IsLocalAtSource.resLE {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} [IsLocalAtTarget P] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hf : P f) : P (Scheme.Hom.resLE f U V e)

If P is local at the source and the target, then restriction on both source and target preserves P.

theorem AlgebraicGeometry.IsLocalAtSource.iff_exists_resLE {P : CategoryTheory.MorphismProperty Scheme} [IsLocalAtSource P] {X Y : Scheme} {f : X ⟶ Y} [IsLocalAtTarget P] [P.RespectsRight IsOpenImmersion] : P f ↔ ∀ (x : ↑↑X.toPresheafedSpace), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), P (Scheme.Hom.resLE f U V e)

If P is local at the source, local at the target and is stable under post-composition with open immersions, then P can be checked locally around points.

def AlgebraicGeometry.AffineTargetMorphismProperty : Type (u_1 + 1)

An AffineTargetMorphismProperty is a class of morphisms from an arbitrary scheme into an affine scheme.

Equations

• AlgebraicGeometry.AffineTargetMorphismProperty = (⦃X Y : AlgebraicGeometry.Scheme⦄ → (X ⟶ Y) → [AlgebraicGeometry.IsAffine Y] → Prop)

theorem AlgebraicGeometry.AffineTargetMorphismProperty.ext {P Q : AffineTargetMorphismProperty} (H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f) : P = Q

theorem AlgebraicGeometry.AffineTargetMorphismProperty.ext_iff {P Q : AffineTargetMorphismProperty} : P = Q ↔ ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f

def AlgebraicGeometry.AffineTargetMorphismProperty.of (P : CategoryTheory.MorphismProperty Scheme) : AffineTargetMorphismProperty

The restriction of a MorphismProperty Scheme to morphisms with affine target.

Equations

• AlgebraicGeometry.AffineTargetMorphismProperty.of P f = P f

def AlgebraicGeometry.AffineTargetMorphismProperty.toProperty (P : AffineTargetMorphismProperty) : CategoryTheory.MorphismProperty Scheme

An AffineTargetMorphismProperty can be extended to a MorphismProperty such that it never holds when the target is not affine

Equations

• P.toProperty f = ∃ (h : AlgebraicGeometry.IsAffine x✝), P f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply (P : AffineTargetMorphismProperty) {X Y : Scheme} (f : X ⟶ Y) [i : IsAffine Y] : P.toProperty f ↔ P f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] [IsAffine Z] : P (CategoryTheory.CategoryStruct.comp f g) ↔ P g

theorem AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] [IsAffine Z] [IsAffine Y] : P (CategoryTheory.CategoryStruct.comp f g) ↔ P f

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

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

instance AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_of (P : CategoryTheory.MorphismProperty Scheme) [P.RespectsIso] : (of P).toProperty.RespectsIso

class AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal (P : AffineTargetMorphismProperty) : Prop

We say that P : AffineTargetMorphismProperty is a local property if

1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basicOpen r for any global section r.
3. If P holds for f ∣_ Y.basicOpen r for all r in a spanning set of the global sections, then P holds for f.

• respectsIso : P.toProperty.RespectsIso

  P as a morphism property respects isomorphisms

• to_basicOpen {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : P f → P (f ∣_ Y.basicOpen r)

  P is stable under restriction to basic open set of global sections.

• of_basicOpenCover {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))) : Ideal.span ↑s = ⊤ → (∀ (r : { x : ↑(Y.presheaf.obj (Opposite.op ⊤)) // x ∈ s }), P (f ∣_ Y.basicOpen ↑r)) → P f

  P for f if P holds for f restricted to basic sets of a spanning set of the global sections

instance AlgebraicGeometry.AffineTargetMorphismProperty.instIsLocalOfOfIsLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] : (of P).IsLocal

def AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange (P : AffineTargetMorphismProperty) : Prop

A P : AffineTargetMorphismProperty is stable under base change if P holds for Y ⟶ S implies that P holds for X ×ₛ Y ⟶ X with X and S affine schemes.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] (H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)) : P.IsStableUnderBaseChange

def AlgebraicGeometry.targetAffineLocally (P : AffineTargetMorphismProperty) : CategoryTheory.MorphismProperty Scheme

For a P : AffineTargetMorphismProperty, targetAffineLocally P holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of Y.

Equations

• AlgebraicGeometry.targetAffineLocally P f = ∀ (U : ↑Y.affineOpens), P (f ∣_ ↑U)

theorem AlgebraicGeometry.of_targetAffineLocally_of_isPullback {P : AffineTargetMorphismProperty} [P.IsLocal] {X Y UX UY : Scheme} [IsAffine UY] {f : X ⟶ Y} {iY : UY ⟶ Y} [IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : CategoryTheory.IsPullback iX f' f iY) (hf : targetAffineLocally P f) : P f'

instance AlgebraicGeometry.instRespectsIsoSchemeTargetAffineLocallyOfToProperty (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso] : (targetAffineLocally P).RespectsIso

class AlgebraicGeometry.HasAffineProperty (P : CategoryTheory.MorphismProperty Scheme) (Q : outParam AffineTargetMorphismProperty) : Prop

HasAffineProperty P Q is a type class asserting that P is local at the target, and over affine schemes, it is equivalent to Q : AffineTargetMorphismProperty. To make the proofs easier, we state it instead as

1. Q is local at the target
2. P f if and only if ∀ U, Q (f ∣_ U) ranging over all affine opens of U. See HasAffineProperty.iff.

• isLocal_affineProperty : AffineTargetMorphismProperty.IsLocal Q
• eq_targetAffineLocally' : P = targetAffineLocally Q

instance AlgebraicGeometry.HasAffineProperty.instTargetAffineLocallyOfIsLocal (Q : AffineTargetMorphismProperty) [Q.IsLocal] : HasAffineProperty (targetAffineLocally Q) Q

theorem AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally (P : CategoryTheory.MorphismProperty Scheme) {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] : P = targetAffineLocally Q

theorem AlgebraicGeometry.HasAffineProperty.of_isLocalAtTarget (P : CategoryTheory.MorphismProperty Scheme) [IsLocalAtTarget P] : HasAffineProperty P (AffineTargetMorphismProperty.of P)

Every property local at the target can be associated with an affine target property. This is not an instance as the associated property can often take on simpler forms.

theorem AlgebraicGeometry.HasAffineProperty.copy {P P' : CategoryTheory.MorphismProperty Scheme} {Q Q' : AffineTargetMorphismProperty} [HasAffineProperty P Q] (e : P = P') (e' : Q = Q') : HasAffineProperty P' Q'

theorem AlgebraicGeometry.HasAffineProperty.of_isPullback {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} {UX UY : Scheme} [IsAffine UY] {iY : UY ⟶ Y} [IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : CategoryTheory.IsPullback iX f' f iY) (hf : P f) : Q f'

theorem AlgebraicGeometry.HasAffineProperty.restrict {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} (hf : P f) (U : ↑Y.affineOpens) : Q (f ∣_ ↑U)

@[instance 900]

instance AlgebraicGeometry.HasAffineProperty.instRespectsIsoScheme {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] : P.RespectsIso

theorem AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → ↑Y.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) (hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))) : P f

theorem AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} {ι : Sort u_1} (U : ι → ↑Y.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) : P f ↔ ∀ (i : ι), Q (f ∣_ ↑(U i))

theorem AlgebraicGeometry.HasAffineProperty.of_openCover {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] (h𝒰 : ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)) : P f

theorem AlgebraicGeometry.HasAffineProperty.iff_of_openCover {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] : P f ↔ ∀ (i : 𝒰.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

theorem AlgebraicGeometry.HasAffineProperty.iff_of_isAffine {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] {X Y : Scheme} {f : X ⟶ Y} [IsAffine Y] : P f ↔ Q f

@[instance 900]

instance AlgebraicGeometry.HasAffineProperty.instIsLocalAtTarget {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] : IsLocalAtTarget P

theorem AlgebraicGeometry.HasAffineProperty.iff {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} : HasAffineProperty P Q ↔ IsLocalAtTarget P ∧ Q = AffineTargetMorphismProperty.of P

theorem AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] (hP' : Q.IsStableUnderBaseChange) : P.IsStableUnderBaseChange

theorem AlgebraicGeometry.HasAffineProperty.isLocalAtSource {P : CategoryTheory.MorphismProperty Scheme} {Q : AffineTargetMorphismProperty} [HasAffineProperty P Q] (H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)) : IsLocalAtSource P

theorem AlgebraicGeometry.hasOfPostcompProperty_isOpenImmersion_of_morphismRestrict (P : CategoryTheory.MorphismProperty Scheme) [P.RespectsIso] (H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)) : P.HasOfPostcompProperty IsOpenImmersion

instance AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange (P : CategoryTheory.MorphismProperty Scheme) [P.IsStableUnderBaseChange] : P.HasOfPostcompProperty IsOpenImmersion