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.stableUnderBaseChange_mk: If Q is stable under affine base change, then P is stable under arbitrary base change.

class AlgebraicGeometry.IsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover), P f ↔ ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.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.respectsIso {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocalAtTarget P] : P.RespectsIso

P respects isomorphisms.

theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) : P f ↔ ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.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 AlgebraicGeometry.Scheme} [P.RespectsIso] (restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)) (of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) : AlgebraicGeometry.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 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] [AlgebraicGeometry.IsLocalAtTarget Q] : AlgebraicGeometry.IsLocalAtTarget (P ⊓ Q)

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsLocalAtTarget.of_isPullback {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {UX : AlgebraicGeometry.Scheme} {UY : AlgebraicGeometry.Scheme} {iY : UY ⟶ Y} [AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hf : P f) (U : Y.Opens) : P (f ∣_ U)

theorem AlgebraicGeometry.IsLocalAtTarget.of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) (H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)) : P f

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

class AlgebraicGeometry.IsLocalAtSource (P : CategoryTheory.MorphismProperty AlgebraicGeometry.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 : AlgebraicGeometry.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.respectsIso {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocalAtSource P] : P.RespectsIso

P respects isomorphisms.

theorem AlgebraicGeometry.IsLocalAtSource.iff_of_openCover' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [P.RespectsIso] (restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (CategoryTheory.CategoryStruct.comp U.ι f)) (of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i).ι f)) → P f) : AlgebraicGeometry.IsLocalAtSource 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.IsLocalAtSource.inf (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtSource P] [AlgebraicGeometry.IsLocalAtSource Q] : AlgebraicGeometry.IsLocalAtSource (P ⊓ Q)

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.IsLocalAtSource.of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [P.ContainsIdentities] [AlgebraicGeometry.IsOpenImmersion f] : P f

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

theorem AlgebraicGeometry.IsLocalAtSource.resLE {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsLocalAtTarget P] {U : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hf : P f) : P (AlgebraicGeometry.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 AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.IsLocalAtTarget P] [P.RespectsRight @AlgebraicGeometry.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 (AlgebraicGeometry.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) → [inst : AlgebraicGeometry.IsAffine Y] → Prop)

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

def AlgebraicGeometry.AffineTargetMorphismProperty.of (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : AlgebraicGeometry.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 : AlgebraicGeometry.AffineTargetMorphismProperty) : CategoryTheory.MorphismProperty AlgebraicGeometry.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 : AlgebraicGeometry.AffineTargetMorphismProperty) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [i : AlgebraicGeometry.IsAffine Y] : P.toProperty f ↔ P f

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

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

@[deprecated AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso]

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

Alias of AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso.

@[deprecated AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso]

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

Alias of AlgebraicGeometry.AffineTargetMorphismProperty.cancel_right_of_respectsIso.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.arrow_mk_iso_iff (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {X' : AlgebraicGeometry.Scheme} {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'

theorem AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk {P : AlgebraicGeometry.AffineTargetMorphismProperty} (h₁ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : AlgebraicGeometry.IsAffine Z], P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) (h₂ : ∀ {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

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

Equations

• ⋯ = ⋯

class AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal (P : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.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

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] : P.toProperty.RespectsIso

P as a morphism property respects isomorphisms

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpen {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.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.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.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 AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] : (AlgebraicGeometry.AffineTargetMorphismProperty.of P).IsLocal

Equations

• ⋯ = ⋯

def AlgebraicGeometry.AffineTargetMorphismProperty.StableUnderBaseChange (P : AlgebraicGeometry.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.StableUnderBaseChange.mk (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] (H : ∀ ⦃X Y S : AlgebraicGeometry.Scheme⦄ [inst : AlgebraicGeometry.IsAffine S] [inst_1 : AlgebraicGeometry.IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)) : P.StableUnderBaseChange

def AlgebraicGeometry.targetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) : CategoryTheory.MorphismProperty AlgebraicGeometry.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 : AlgebraicGeometry.AffineTargetMorphismProperty} [P.IsLocal] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {UX : AlgebraicGeometry.Scheme} {UY : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine UY] {f : X ⟶ Y} {iY : UY ⟶ Y} [AlgebraicGeometry.IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY} (h : CategoryTheory.IsPullback iX f' f iY) (hf : AlgebraicGeometry.targetAffineLocally P f) : P f'

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

Equations

• ⋯ = ⋯

class AlgebraicGeometry.HasAffineProperty (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (Q : outParam AlgebraicGeometry.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 : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal Q
• eq_targetAffineLocally' : P = AlgebraicGeometry.targetAffineLocally Q

theorem AlgebraicGeometry.HasAffineProperty.isLocal_affineProperty (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty} [self : AlgebraicGeometry.HasAffineProperty P Q] : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal Q

theorem AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty} [self : AlgebraicGeometry.HasAffineProperty P Q] : P = AlgebraicGeometry.targetAffineLocally Q

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.HasAffineProperty.of_isLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocalAtTarget P] : AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.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 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} {Q' : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] (e : P = P') (e' : Q = Q') : AlgebraicGeometry.HasAffineProperty P' Q'

theorem AlgebraicGeometry.HasAffineProperty.of_isPullback {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {UX : AlgebraicGeometry.Scheme} {UY : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine UY] {iY : UY ⟶ Y} [AlgebraicGeometry.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 AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hf : P f) (U : ↑Y.affineOpens) : Q (f ∣_ ↑U)

@[instance 900]

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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 AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (h𝒰 : ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)) : P f

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

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

@[instance 900]

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

Equations

• ⋯ = ⋯

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

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

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