Functorial constructions of ideal sheaves

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

Main definitions

• AlgebraicGeometry.Scheme.IdealSheafData.comap: The pullback of an ideal sheaf.
• AlgebraicGeometry.Scheme.IdealSheafData.map: The pushforward of an ideal sheaf.
• AlgebraicGeometry.Scheme.IdealSheafData.map_gc: The Galois connection between pullback and pushforward.

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

The pullback of an ideal sheaf.

Equations

• I.comap f = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Limits.pullback.fst f I.subschemeι)

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

• I.comapIso f = (CategoryTheory.asIso (AlgebraicGeometry.Scheme.Hom.toImage (CategoryTheory.Limits.pullback.fst f I.subschemeι))).symm

@[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ι

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

@[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ι

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_id {Z : Scheme} (I : Z.IdealSheafData) : I.comap (CategoryTheory.CategoryStruct.id Z) = I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_comap {X Y : Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) : (I.comap f).support = I.support.preimage ⋯

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

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.

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

The pushforward of an ideal sheaf.

Equations

• I.map f = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp I.subschemeι f)

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

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.

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_mono {X Y : Scheme} (f : X ⟶ Y) : Monotone fun (x : X.IdealSheafData) => x.map f

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_mono {X Y : Scheme} (f : X ⟶ Y) : Monotone fun (x : Y.IdealSheafData) => x.comap f

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_map_comap {X Y : Scheme} (J : Y.IdealSheafData) (f : X ⟶ Y) : J ≤ (J.comap f).map f

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_map_le {X Y : Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) : (I.map f).comap f ≤ I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_top {X Y : Scheme} (f : X ⟶ Y) : ⊤.map f = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_bot {X Y : Scheme} (f : X ⟶ Y) : ⊥.comap f = ⊥

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

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_bot {X Y : Scheme} (f : X ⟶ Y) : ⊥.map f = Hom.ker f

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_top {X Y : Scheme} (f : X ⟶ Y) : ⊤.comap f = ⊤

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_id {Z : Scheme} (I : Z.IdealSheafData) : I.map (CategoryTheory.CategoryStruct.id Z) = I

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)

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

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

@[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)

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

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, ⋯⟩)

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, ⋯⟩)

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

• I.subschemeMap J f H = AlgebraicGeometry.IsClosedImmersion.lift J.subschemeι (CategoryTheory.CategoryStruct.comp I.subschemeι f) ⋯

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

@[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)

@[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 ⋯

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