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.

Equations
Instances For

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

    Equations
    Instances For
      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 fP (CategoryTheory.CategoryStruct.comp e.hom f)) (h₂ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (e : Y Z) (f : X Y) [h : AlgebraicGeometry.IsAffine Y], P fP (CategoryTheory.CategoryStruct.comp f e.hom)) :
      P.toProperty.RespectsIso

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

          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 fP (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

          @[simp]

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

          theorem AlgebraicGeometry.targetAffineLocallyOfOpenCover {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) :
          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) (hP : 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

          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 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) (𝒰 : 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.

          Instances For

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

            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.
            Instances For
              theorem AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_respectsIso (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.toProperty.RespectsIso) :
              P.diagonal.toProperty.RespectsIso
              theorem AlgebraicGeometry.diagonalTargetAffineLocallyOfOpenCover (P : AlgebraicGeometry.AffineTargetMorphismProperty) (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (𝒰' : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) [∀ (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)) :
              theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.diagonal_affine_openCover_TFAE {P : AlgebraicGeometry.AffineTargetMorphismProperty} (hP : P.IsLocal) {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) :
              [(AlgebraicGeometry.targetAffineLocally P).diagonal f, ∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), P.diagonal CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : Y.OpenCover) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), P.diagonal CategoryTheory.Limits.pullback.snd, ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : AlgebraicGeometry.IsAffine U] [inst_1 : AlgebraicGeometry.IsOpenImmersion g], P.diagonal CategoryTheory.Limits.pullback.snd, ∃ (𝒰 : Y.OpenCover) (x : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)) (𝒰' : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) (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)].TFAE
              theorem AlgebraicGeometry.universallyIsLocalAtTarget (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) (𝒰 : Y.OpenCover), (∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd)P f) :
              theorem AlgebraicGeometry.universallyIsLocalAtTargetOfMorphismRestrict (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) (hP₁ : P.RespectsIso) (hP₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) {ι : Type u} (U : ιTopologicalSpace.Opens Y.toPresheafedSpace), iSup U = (∀ (i : ι), P (f ∣_ U i))P f) :

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

              Equations
              Instances For