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, and an AffineTargetMorphismProperty is a predicate on morphisms into affine schemes. Given a P : AffineTargetMorphismProperty, we may construct a MorphismProperty called targetAffineLocally P that holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of Y.

Main definitions

• 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.

• AlgebraicGeometry.PropertyIsLocalAtTarget: We say that PropertyIsLocalAtTarget P for P : MorphismProperty Scheme 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.

Main results

• AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE: If P.IsLocal, then targetAffineLocally P f iff there exists an affine cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ.
• AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply: If the existence of an affine cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ implies targetAffineLocally P f, then P.IsLocal.
• AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_target_iff: If Y is affine and f : X ⟶ Y, then targetAffineLocally P f ↔ P f provided P.IsLocal.
• AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal : If P.IsLocal, then PropertyIsLocalAtTarget (targetAffineLocally P).
• AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_TFAE: If PropertyIsLocalAtTarget P, then P f iff there exists an open cover { Uᵢ } of Y such that P holds for f ∣_ Uᵢ.

These results should not be used directly, and should be ported to each property that is local.

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)

def AlgebraicGeometry.Scheme.isIso : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

IsIso as a MorphismProperty.

Equations

• AlgebraicGeometry.Scheme.isIso = @CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory

def AlgebraicGeometry.Scheme.affineTargetIsIso : AlgebraicGeometry.AffineTargetMorphismProperty

IsIso as an AffineTargetMorphismProperty.

Equations

• AlgebraicGeometry.Scheme.affineTargetIsIso f = CategoryTheory.IsIso f

instance AlgebraicGeometry.instInhabitedAffineTargetMorphismProperty : Inhabited AlgebraicGeometry.AffineTargetMorphismProperty

Equations

• AlgebraicGeometry.instInhabitedAffineTargetMorphismProperty = { default := AlgebraicGeometry.Scheme.affineTargetIsIso }

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.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.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.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) [h : AlgebraicGeometry.IsAffine Y], P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) : P.toProperty.RespectsIso

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.IsAffineOpen.preimage_of_isIso {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [CategoryTheory.IsIso f] : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)

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

Equations

• ⋯ = ⋯

structure 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

• toBasicOpen : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj { unop := ⊤ })), P f → P (f ∣_ Y.basicOpen r)

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

• ofBasicOpenCover : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj { unop := ⊤ })), Ideal.span ↑s = ⊤ → (∀ (r : { x : ↑(Y.presheaf.obj { unop := ⊤ }) // 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.toBasicOpen {P : AlgebraicGeometry.AffineTargetMorphismProperty} (self : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (r : ↑(Y.presheaf.obj { unop := ⊤ })) : P f → P (f ∣_ Y.basicOpen r)

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

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.ofBasicOpenCover {P : AlgebraicGeometry.AffineTargetMorphismProperty} (self : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) (s : Finset ↑(Y.presheaf.obj { unop := ⊤ })) : Ideal.span ↑s = ⊤ → (∀ (r : { x : ↑(Y.presheaf.obj { unop := ⊤ }) // 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.CommRingCat.id_apply (R : CommRingCat) (x : ↑R) : (CategoryTheory.CategoryStruct.id R) x = x

Specialization of ConcreteCategory.id_apply because simp can't see through the defeq.

theorem AlgebraicGeometry.targetAffineLocally_of_openCover {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (h𝒰 : ∀ (i : (𝒰.pullbackCover f).J), P CategoryTheory.Limits.pullback.snd) : AlgebraicGeometry.targetAffineLocally P f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : [AlgebraicGeometry.targetAffineLocally P f, ∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst_1 : AlgebraicGeometry.IsOpenImmersion g], P CategoryTheory.Limits.pullback.snd, ∃ (ι : Type u) (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (_ : iSup U = ⊤) (hU' : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)), ∀ (i : ι), P (f ∣_ U i)].TFAE

theorem AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso] (H : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst_1 : AlgebraicGeometry.IsOpenImmersion g], P CategoryTheory.Limits.pullback.snd) : P.IsLocal

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_iff {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) [h𝒰 : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] : AlgebraicGeometry.targetAffineLocally P f ↔ ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_target_iff {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] : AlgebraicGeometry.targetAffineLocally P f ↔ P f

structure AlgebraicGeometry.PropertyIsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) : Prop

We say that P : MorphismProperty Scheme 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.

• RespectsIso : P.RespectsIso

  P respects isomorphisms.

• restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), P f → P (f ∣_ U)

  If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.

• of_openCover : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover), (∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → P f

  If P holds for f ∣_ U for an open cover U of Y, then P holds for f.

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.RespectsIso {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (self : AlgebraicGeometry.PropertyIsLocalAtTarget P) : P.RespectsIso

P respects isomorphisms.

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.restrict {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (self : AlgebraicGeometry.PropertyIsLocalAtTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) : P f → P (f ∣_ U)

If P holds for f : X ⟶ Y, then P holds for f ∣_ U for any U.

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.of_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (self : AlgebraicGeometry.PropertyIsLocalAtTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) : (∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → P f

If P holds for f ∣_ U for an open cover U of Y, then P holds for f.

theorem AlgebraicGeometry.propertyIsLocalAtTarget_of_morphismRestrict (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [P.RespectsIso] (hP₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), P f → P (f ∣_ U)) (hP₃ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f) : AlgebraicGeometry.PropertyIsLocalAtTarget P

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) : AlgebraicGeometry.PropertyIsLocalAtTarget (AlgebraicGeometry.targetAffineLocally P)

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_TFAE {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (hP : AlgebraicGeometry.PropertyIsLocalAtTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : [P f, ∃ (𝒰 : Y.OpenCover), ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), P (f ∣_ U), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion g], P CategoryTheory.Limits.pullback.snd, ∃ (ι : Type u) (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (_ : iSup U = ⊤), ∀ (i : ι), P (f ∣_ U i)].TFAE

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (hP : AlgebraicGeometry.PropertyIsLocalAtTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) : P f ↔ ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd

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.IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) (hP' : P.StableUnderBaseChange) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsAffine S] (H : P g) : AlgebraicGeometry.targetAffineLocally P CategoryTheory.Limits.pullback.fst

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.stableUnderBaseChange {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) (hP' : P.StableUnderBaseChange) : (AlgebraicGeometry.targetAffineLocally P).StableUnderBaseChange

@[deprecated AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal]

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) : AlgebraicGeometry.PropertyIsLocalAtTarget (AlgebraicGeometry.targetAffineLocally P)

Alias of AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_isLocal.

@[deprecated AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange]

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyPullbackFstOfRightOfStableUnderBaseChange {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) (hP' : P.StableUnderBaseChange) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsAffine S] (H : P g) : AlgebraicGeometry.targetAffineLocally P CategoryTheory.Limits.pullback.fst

Alias of AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocally_pullback_fst_of_right_of_stableUnderBaseChange.