Documentation

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Functorial constructions of ideal sheaves #

We define the pullback and pushforward of ideal sheaves in this file.

Main definitions #

source
noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.comap {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
X.IdealSheafData

The pullback of an ideal sheaf.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.comapIso {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
    (I.comap f).subscheme ≅ CategoryTheory.Limits.pullback f I.subschemeι

    The subscheme associated to the pullback ideal sheaf is isomorphic to the fibred product.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (I.comapIso f).inv (I.comap f).subschemeι = CategoryTheory.Limits.pullback.fst f I.subschemeι
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι_assoc {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : Scheme} (h : X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (I.comapIso f).inv (CategoryTheory.CategoryStruct.comp (I.comap f).subschemeι h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f I.subschemeι) h
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.Limits.pullback.fst f I.subschemeι) = (I.comap f).subschemeι
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst_assoc {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : Scheme} (h : X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f I.subschemeι) h) = CategoryTheory.CategoryStruct.comp (I.comap f).subschemeι h
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_comp {X Y Z : Scheme} (I : Z.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z) :
      I.comap (CategoryTheory.CategoryStruct.comp f g) = (I.comap g).comap f
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_id {Z : Scheme} (I : Z.IdealSheafData) :
      I.comap (CategoryTheory.CategoryStruct.id Z) = I
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.IdealSheafData.support_comap {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
      (I.comap f).support = I.support.preimage ⋯
      source
      theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion {X Y Z : Scheme} (i : Z ⟶ Y) (f : X ⟶ Y) [IsClosedImmersion i] :
      Hom.ker (CategoryTheory.Limits.pullback.fst f i) = (Hom.ker i).comap f
      source
      theorem AlgebraicGeometry.isPullback_of_isClosedImmersion {ZX ZY X Y : Scheme} (iX : ZX ⟶ X) (iY : ZY ⟶ Y) (Zf : ZX ⟶ ZY) (f : X ⟶ Y) [IsClosedImmersion iX] [IsClosedImmersion iY] (h : CategoryTheory.CategoryStruct.comp iX f = CategoryTheory.CategoryStruct.comp Zf iY) (h' : (Scheme.Hom.ker iY).comap f = Scheme.Hom.ker iX) :
      CategoryTheory.IsPullback iX Zf f iY

      To show that the pullback of the closed immersion iX along f is the closed immersion iY, it suffices to check that the preimage of ker iY under f is ker iX.

      source
      noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.map {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) :
      Y.IdealSheafData

      The pushforward of an ideal sheaf.

      Equations
      Instances For
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_le {X Y : Scheme} {I : X.IdealSheafData} {f : X ⟶ Y} {J : Y.IdealSheafData} :
        J ≤ I.map f ↔ J.comap f ≤ I
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_gc {X Y : Scheme} (f : X ⟶ Y) :
        GaloisConnection (fun (x : Y.IdealSheafData) => x.comap f) fun (x : X.IdealSheafData) => x.map f

        Pushforward and pullback of ideal sheaves forms a Galois connection.

        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_mono {X Y : Scheme} (f : X ⟶ Y) :
        Monotone fun (x : X.IdealSheafData) => x.map f
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_mono {X Y : Scheme} (f : X ⟶ Y) :
        Monotone fun (x : Y.IdealSheafData) => x.comap f
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.le_map_comap {X Y : Scheme} (J : Y.IdealSheafData) (f : X ⟶ Y) :
        J ≤ (J.comap f).map f
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) :
        (I.map f).comap f ≤ I
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_top {X Y : Scheme} (f : X ⟶ Y) :
        ⊤.map f = ⊤
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_bot {X Y : Scheme} (f : X ⟶ Y) :
        ⊥.comap f = ⊥
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_inf {X Y : Scheme} (I₁ I₂ : X.IdealSheafData) (f : X ⟶ Y) :
        (I₁ ⊓ I₂).map f = I₁.map f ⊓ I₂.map f
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_sup {X Y : Scheme} (J₁ J₂ : Y.IdealSheafData) (f : X ⟶ Y) :
        (J₁ ⊔ J₂).comap f = J₁.comap f ⊔ J₂.comap f
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_bot {X Y : Scheme} (f : X ⟶ Y) :
        ⊥.map f = Hom.ker f
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_top {X Y : Scheme} (f : X ⟶ Y) :
        ⊤.comap f = ⊤
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_comp {X Y Z : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) (g : Y ⟶ Z) :
        I.map (CategoryTheory.CategoryStruct.comp f g) = (I.map f).map g
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_id {Z : Scheme} (I : Z.IdealSheafData) :
        I.map (CategoryTheory.CategoryStruct.id Z) = I
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ker {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
        (Hom.ker f).map g = Hom.ker (CategoryTheory.CategoryStruct.comp f g)
        source
        theorem AlgebraicGeometry.Scheme.Hom.ker_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) :
        ker (CategoryTheory.CategoryStruct.comp f g) = (ker f).map g
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal {X Y : Scheme} (f : X ⟶ Y) (Z : TopologicalSpace.Closeds ↥X) :
        (vanishingIdeal Z).map f = vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.IdealSheafData.support_map {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [QuasiCompact f] :
        (I.map f).support = TopologicalSpace.Closeds.closure (⇑f '' ↑I.support)
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_map {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [QuasiCompact f] (U : ↑Y.affineOpens) (H : IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj ↑U)) :
        (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, H⟩)
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_map_of_isAffineHom {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [IsAffineHom f] (U : ↑Y.affineOpens) :
        (I.map f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.app f ↑U)) (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, ⋯⟩)
        source
        theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) [IsOpenImmersion f] (U : ↑X.affineOpens) :
        (I.comap f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) (I.ideal ⟨(Hom.opensFunctor f).obj ↑U, ⋯⟩)
        source
        noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap {X Y : Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) :
        I.subscheme ⟶ J.subscheme

        If J ≤ I.map f, then f restricts to a map I ⟶ J between the closed subschemes.

        Equations
        Instances For
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι {X Y : Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) :
          CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) J.subschemeι = CategoryTheory.CategoryStruct.comp I.subschemeι f
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap_subschemeι_assoc {X Y : Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f : X ⟶ Y) (H : J ≤ I.map f) {Z : Scheme} (h : Y ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (I.subschemeMap J f H) (CategoryTheory.CategoryStruct.comp J.subschemeι h) = CategoryTheory.CategoryStruct.comp I.subschemeι (CategoryTheory.CategoryStruct.comp f h)
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) :
          CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.Limits.pullback.snd f I.subschemeι) = (I.comap f).subschemeMap I f ⋯
          source
          @[simp]
          theorem AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd_assoc {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) {Z : Scheme} (h : I.subscheme ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (I.comapIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f I.subschemeι) h) = CategoryTheory.CategoryStruct.comp ((I.comap f).subschemeMap I f ⋯) h