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 #

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

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

    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

      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.AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal P) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :

        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

          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
            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)))) :
            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)))]

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

            Instances For