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. For properties local at the target, its behaviour is entirely determined by its definition on morphisms into affine schemes, which we call an AffineTargetMorphismProperty. In this file, we provide API lemmas for properties local at the target, and special support for those properties whose AffineTargetMorphismProperty takes on a more simple form. We also provide API lemmas for properties local at the target. The main interfaces of the API are the typeclasses IsLocalAtTarget, IsLocalAtSource and HasAffineProperty, which we describle in detail below.

IsLocalAtTarget #

  1. P respects isomorphisms.
  2. P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

For a morphism property P local at the target and f : X ⟶ Y, we provide these API lemmas:

IsLocalAtSource #

  1. P respects isomorphisms.
  2. P holds for 𝒰.map i ≫ f for an open cover 𝒰 of X iff P holds for f : X ⟶ Y.

For a morphism property P local at the source and f : X ⟶ Y, we provide these API lemmas:

AffineTargetMorphismProperty #

HasAffineProperty #

For HasAffineProperty P Q and f : X ⟶ Y, we provide these API lemmas:

We say that P : MorphismProperty Scheme is local at the target if

  1. P respects isomorphisms.
  2. P holds for f ∣_ U for an open cover U of Y if and only if P holds for f. Also see IsLocalAtTarget.mk' for a convenient constructor.
  • respectsIso : P.RespectsIso

    P respects isomorphisms.

  • iff_of_openCover' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) (𝒰 : Y.OpenCover), P f ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)

    P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

Instances
    theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (𝒰 : Y.OpenCover) :
    P f ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)

    P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

    theorem AlgebraicGeometry.IsLocalAtTarget.mk' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] (restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) (U : Y.Opens), P fP (f ∣_ U)) (of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) {ι : Type u} (U : ιY.Opens), iSup U = (∀ (i : ι), P (f ∣_ U i))P f) :

    P 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.IsLocalAtTarget.of_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} (𝒰 : Y.OpenCover) (H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)) :
    P f
    theorem AlgebraicGeometry.IsLocalAtTarget.iff_of_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [hP : AlgebraicGeometry.IsLocalAtTarget P] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} (𝒰 : Y.OpenCover) :
    P f ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)

    We say that P : MorphismProperty Scheme is local at the source if

    1. P respects isomorphisms.
    2. P holds for 𝒰.map i ≫ f for an open cover 𝒰 of X iff P holds for f : X ⟶ Y. Also see IsLocalAtSource.mk' for a convenient constructor.
    Instances

      P holds for f ∣_ U for an open cover U of Y if and only if P holds for f.

      theorem AlgebraicGeometry.IsLocalAtSource.mk' {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] (restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) (U : X.Opens), P fP (CategoryTheory.CategoryStruct.comp U f)) (of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) {ι : Type u} (U : ιX.Opens), iSup U = (∀ (i : ι), P (CategoryTheory.CategoryStruct.comp (U i) f))P f) :

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

      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

          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

            P as a morphism property respects isomorphisms

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

            theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCover {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X Y) (s : Finset (Y.presheaf.obj (Opposite.op ))) :
            Ideal.span s = (∀ (r : { x : (Y.presheaf.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

            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

              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

                HasAffineProperty P Q is a type class asserting that P is local at the target, and over affine schemes, it is equivalent to Q : AffineTargetMorphismProperty. To make the proofs easier, we state it instead as

                1. Q is local at the target
                2. P f if and only if ∀ U, Q (f ∣_ U) ranging over all affine opens of U. See HasAffineProperty.iff.
                Instances

                  Every property local at the target can be associated with an affine target property. This is not an instance as the associated property can often take on simpler forms.

                  theorem AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} {ι : Sort u_1} (U : ιY.affineOpens) (hU : ⨆ (i : ι), (U i) = ) (hU' : ∀ (i : ι), Q (f ∣_ (U i))) :
                  P f
                  theorem AlgebraicGeometry.HasAffineProperty.of_openCover {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : AlgebraicGeometry.AffineTargetMorphismProperty} [AlgebraicGeometry.HasAffineProperty P Q] {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (h𝒰 : ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)) :
                  P f