# Documentation

Mathlib.AlgebraicGeometry.Morphisms.Basic

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

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

Instances For

IsIso as a MorphismProperty.

Instances For

IsIso as an AffineTargetMorphismProperty.

Instances For

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

Instances For
theorem AlgebraicGeometry.affine_cancel_left_isIso (f : X Y) (g : Y Z) :
P X Z () inst✝ P Y Z g inst✝
theorem AlgebraicGeometry.affine_cancel_right_isIso (f : X Y) (g : Y Z) :
P X Z () inst✝ P X Y f inst✝¹
theorem AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk (h₁ : {X Y Z : AlgebraicGeometry.Scheme} → (e : X Y) → (f : Y Z) → [inst : ] → P Y Z f instP X Z () inst) (h₂ : {X Y Z : AlgebraicGeometry.Scheme} → (e : Y Z) → (f : X Y) → [h : ] → P X Y f hP X Z () (_ : )) :

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.

Instances For
• P as a morphism property respects isomorphisms

• toBasicOpen : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : ] (f : X Y) (r : ↑(Y.presheaf.obj ())), P fP ()

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

• ofBasicOpenCover : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : ] (f : X Y) (s : Finset ↑(Y.presheaf.obj ())), = (∀ (r : { x // x s }), P ()) → 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.
Instances For
theorem AlgebraicGeometry.targetAffineLocallyOfOpenCover (f : X Y) [∀ (i : 𝒰.J), ] (h𝒰 : (i : ) → P () () CategoryTheory.Limits.pullback.snd (inst✝ i)) :
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE (f : X Y) :
List.TFAE [, 𝒰 x, (i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd , (𝒰 : ) → [inst : ∀ (i : 𝒰.J), ] → (i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd , {U : AlgebraicGeometry.Scheme} → (g : U Y) → [inst : ] → [inst_1 : ] → P () 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))))) () (f ∣_ U i) (_ : )]
theorem AlgebraicGeometry.AffineTargetMorphismProperty.isLocalOfOpenCoverImply (H : {X Y : AlgebraicGeometry.Scheme} → (f : X Y) → (𝒰 x, (i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd ) → {U : AlgebraicGeometry.Scheme} → (g : U Y) → [inst : ] → [inst_1 : ] → P () U CategoryTheory.Limits.pullback.snd inst) :
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_iff (f : X Y) [h𝒰 : ∀ (i : 𝒰.J), ] :
(i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd (h𝒰 i)
• RespectsIso :

P respects isomorphisms.

• restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace), P fP (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) (𝒰 : ), (∀ (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.
Instances For
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_TFAE (f : X Y) :
List.TFAE [P X Y f, 𝒰, (i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd, (𝒰 : ) → (i : 𝒰.J) → P () () 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)))) () (f ∣_ U), {U : AlgebraicGeometry.Scheme} → (g : U Y) → [inst : ] → P () 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))))) () (f ∣_ U i)]
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff (f : X Y) :
P X Y f (i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd

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.

Instances For

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

Instances For
theorem AlgebraicGeometry.diagonalTargetAffineLocallyOfOpenCover (f : X Y) [∀ (i : 𝒰.J), ] (𝒰' : ) [∀ (i : 𝒰.J) (j : (𝒰' i).J), ] (h𝒰' : (i : 𝒰.J) → (j k : (𝒰' i).J) → P (CategoryTheory.Limits.pullback () ()) (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd)) (CategoryTheory.Limits.pullback.mapDesc () () CategoryTheory.Limits.pullback.snd) (_ : AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd)))) :
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE (f : X Y) :
List.TFAE [, 𝒰 x, ∀ (i : 𝒰.J), AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : ) [inst : ∀ (i : 𝒰.J), ] (i : 𝒰.J), AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : ] [inst_1 : ], AlgebraicGeometry.AffineTargetMorphismProperty.diagonal P CategoryTheory.Limits.pullback.snd, 𝒰 x 𝒰' x_1, (i : 𝒰.J) → (j k : (𝒰' i).J) → P (CategoryTheory.Limits.pullback () ()) (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd)) (CategoryTheory.Limits.pullback.mapDesc () () CategoryTheory.Limits.pullback.snd) (_ : AlgebraicGeometry.IsAffine (CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd)))]
theorem AlgebraicGeometry.universallyIsLocalAtTarget (hP : {X Y : AlgebraicGeometry.Scheme} → (f : X Y) → (𝒰 : ) → ((i : 𝒰.J) → P () () CategoryTheory.Limits.pullback.snd) → P X Y f) :
theorem AlgebraicGeometry.universallyIsLocalAtTargetOfMorphismRestrict (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))))) () (f ∣_ U i)) → P X Y f) :
def AlgebraicGeometry.MorphismProperty.topologically (P : {α β : Type u} → [inst : ] → [inst : ] → (αβ) → Prop) :

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

Instances For