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.

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

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

• AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P 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] : AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P f ↔ P f

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 (CategoryTheory.CategoryStruct.comp f g) ↔ P g

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

Equations

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

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 (f⁻¹ᵁ 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

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 : 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.toPrefunctor.obj (Opposite.op ⊤))), 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.toPrefunctor.obj (Opposite.op ⊤))), Ideal.span ↑s = ⊤ → (∀ (r : { x : ↑(Y.presheaf.toPrefunctor.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

@[simp]

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.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 (𝒰.obj i)] (h𝒰 : ∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J), P CategoryTheory.Limits.pullback.snd) : 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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [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)]

theorem AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : CategoryTheory.MorphismProperty.RespectsIso (AlgebraicGeometry.AffineTargetMorphismProperty.toProperty P)) (H : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), (∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (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) : 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 (𝒰.obj i)] : AlgebraicGeometry.targetAffineLocally P f ↔ ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd

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

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 f, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y), ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (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)]

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 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.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 g) : 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.

Equations

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

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 (𝒰.obj i)] (𝒰' : (i : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (CategoryTheory.Limits.pullback f (𝒰.map i))) [∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)] (h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), P (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map 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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.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, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)) (𝒰' : (i : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (CategoryTheory.Limits.pullback f (𝒰.map i))) (x_1 : ∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)), ∀ (i : 𝒰.J) (j k : (𝒰' i).J), P (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map 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.snd) → P 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 (f ∣_ U i)) → P 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.

Equations

• AlgebraicGeometry.MorphismProperty.topologically P f = P ⇑f.val.base