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.

source

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

Instances For

source

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

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

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)

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 (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' ↑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 (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' ↑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

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

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

Documentation

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Functorial constructions of ideal sheaves #

Main definitions #