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.targetAffineLocallyIsLocal : 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.

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

IsIso as a MorphismProperty.

def AlgebraicGeometry.Scheme.affineTargetIsIso : AlgebraicGeometry.AffineTargetMorphismProperty

IsIso as an AffineTargetMorphismProperty.

instance AlgebraicGeometry.instInhabitedAffineTargetMorphismProperty : Inhabited AlgebraicGeometry.AffineTargetMorphismProperty

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

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

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

theorem AlgebraicGeometry.affine_cancel_right_isIso {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P)) {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 X Z (CategoryTheory.CategoryStruct.comp f g) inst✝ ↔ P X Y f inst✝¹

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

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.

theorem AlgebraicGeometry.IsAffineOpen.map_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)

theorem AlgebraicGeometry.targetAffineLocally_respectsIso {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P)) : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.targetAffineLocally P)

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

• RespectsIso : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P)

  P as a morphism property respects isomorphisms

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

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

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.

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

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.targetAffineLocally P f, ∃ 𝒰 x, (i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) CategoryTheory.Limits.pullback.snd (_ : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)), (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) → [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] → (i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) CategoryTheory.Limits.pullback.snd (_ : AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)), {U : AlgebraicGeometry.Scheme} → (g : U ⟶ Y) → [inst : AlgebraicGeometry.IsAffine U] → [inst_1 : AlgebraicGeometry.IsOpenImmersion g] → P (CategoryTheory.Limits.pullback f g) U CategoryTheory.Limits.pullback.snd inst, ∃ ι U x hU', (i : ι) → P (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (U i))))) (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (U i)))) (f ∣_ U i) (_ : AlgebraicGeometry.IsAffineOpen (U i))]

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

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

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

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

• RespectsIso : CategoryTheory.MorphismProperty.RespectsIso P

  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) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y), (∀ (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.

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.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) : 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) : List.TFAE [P X Y f, ∃ 𝒰, (i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) CategoryTheory.Limits.pullback.snd, (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) → (i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) CategoryTheory.Limits.pullback.snd, (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) → P (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj U)))) (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion U))) (f ∣_ U), {U : AlgebraicGeometry.Scheme} → (g : U ⟶ Y) → [inst : AlgebraicGeometry.IsOpenImmersion g] → P (CategoryTheory.Limits.pullback f g) U CategoryTheory.Limits.pullback.snd, ∃ ι U x, (i : ι) → P (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (U i))))) (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (U i)))) (f ∣_ U i)]

theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (hP : AlgebraicGeometry.PropertyIsLocalAtTarget P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) : P X Y f ↔ (i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) 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.

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

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

def AlgebraicGeometry.AffineTargetMorphismProperty.diagonal (P : AlgebraicGeometry.AffineTargetMorphismProperty) : AlgebraicGeometry.AffineTargetMorphismProperty

The AffineTargetMorphismProperty associated to (targetAffineLocally P).diagonal. See diagonal_targetAffineLocally_eq_targetAffineLocally.

theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P)) : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty (AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P))

theorem AlgebraicGeometry.diagonalTargetAffineLocallyOfOpenCover (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (𝒰' : (i : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) [∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj (𝒰' i) j)] (h𝒰' : (i : 𝒰.J) → (j k : (𝒰' i).J) → P (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k)) (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd)) (CategoryTheory.Limits.pullback.mapDesc (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd) (_ : AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd)))) : CategoryTheory.MorphismProperty.diagonal (AlgebraicGeometry.targetAffineLocally P) f

theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonalOfTargetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {U : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : U ⟶ Y) [AlgebraicGeometry.IsAffine U] [AlgebraicGeometry.IsOpenImmersion g] (H : CategoryTheory.MorphismProperty.diagonal (AlgebraicGeometry.targetAffineLocally P) f) : AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [CategoryTheory.MorphismProperty.diagonal (AlgebraicGeometry.targetAffineLocally P) f, ∃ 𝒰 x, ∀ (i : 𝒰.J), AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (i : 𝒰.J), AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst_1 : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∃ 𝒰 x 𝒰' x_1, (i : 𝒰.J) → (j k : (𝒰' i).J) → P (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k)) (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd)) (CategoryTheory.Limits.pullback.mapDesc (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd) (_ : AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) k) CategoryTheory.Limits.pullback.snd)))]

theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal (AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P)

theorem AlgebraicGeometry.diagonal_targetAffineLocally_eq_targetAffineLocally (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) : CategoryTheory.MorphismProperty.diagonal (AlgebraicGeometry.targetAffineLocally P) = AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P)

theorem AlgebraicGeometry.universallyIsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) → ((i : 𝒰.J) → P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i) CategoryTheory.Limits.pullback.snd) → P X Y f) : AlgebraicGeometry.PropertyIsLocalAtTarget (CategoryTheory.MorphismProperty.universally P)

theorem AlgebraicGeometry.universallyIsLocalAtTargetOfMorphismRestrict (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP₁ : CategoryTheory.MorphismProperty.RespectsIso P) (hP₂ : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → {ι : Type u} → (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) → iSup U = ⊤ → ((i : ι) → P (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj (U i))))) (AlgebraicGeometry.Scheme.restrict Y (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion (U i)))) (f ∣_ U i)) → P X Y f) : AlgebraicGeometry.PropertyIsLocalAtTarget (CategoryTheory.MorphismProperty.universally P)

def AlgebraicGeometry.MorphismProperty.topologically (P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop) : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme

topologically P holds for a morphism if the underlying topological map satisfies P.