Documentation

TauCeti.AlgebraicGeometry.IdealSheaf.BaseChange

Base change of ideal sheaves #

This file identifies the closed subscheme of an ideal sheaf pulled back along a fibre-product projection with the corresponding base change. It also records the resulting preservation of flatness for the closed subscheme, and the affine-local form of that flatness: over affine opens W ⊆ S and U ⊆ f⁻¹ W, the quotient Γ(X, U) ⧸ I(U) is flat over Γ(S, W) (flat_appLE_comp_ofHom_quotient_mk).

source
noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) :
(I.comap (CategoryTheory.Limits.pullback.fst f g)).subscheme ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp I.subschemeι f) g

The closed subscheme cut out by the pullback of an ideal sheaf along a fibre-product projection is the base change of its original closed subscheme.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_hom_fst {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp I.subschemeι f) g) = (I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeMap I (CategoryTheory.Limits.pullback.fst f g) ⋯

    The base-change comparison preserves the projection to the original closed subscheme.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_hom_fst_assoc {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) {Z : Scheme} (h : I.subscheme ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp I.subschemeι f) g) h) = CategoryTheory.CategoryStruct.comp ((I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeMap I (CategoryTheory.Limits.pullback.fst f g) ⋯) h

    The base-change comparison preserves the projection to the original closed subscheme.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_inv_fst {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).inv ((I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeMap I (CategoryTheory.Limits.pullback.fst f g) ⋯) = CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp I.subschemeι f) g

    The inverse base-change comparison preserves the projection to the original closed subscheme.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_inv_fst_assoc {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) {Z : Scheme} (h : I.subscheme ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp ((I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeMap I (CategoryTheory.Limits.pullback.fst f g) ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp I.subschemeι f) g) h

    The inverse base-change comparison preserves the projection to the original closed subscheme.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_hom_snd {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp I.subschemeι f) g) = CategoryTheory.CategoryStruct.comp (I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeι (CategoryTheory.Limits.pullback.snd f g)

    The base-change comparison preserves the projection to the new base.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.IdealSheafData.comapPullbackFstIso_hom_snd_assoc {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) {Z : Scheme} (h : T ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (I.comapPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp I.subschemeι f) g) h) = CategoryTheory.CategoryStruct.comp (I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)

    The base-change comparison preserves the projection to the new base.

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.flat_comap_subschemeι_comp_snd {S T X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) (g : T ⟶ S) [Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)] :
    Flat (CategoryTheory.CategoryStruct.comp (I.comap (CategoryTheory.Limits.pullback.fst f g)).subschemeι (CategoryTheory.Limits.pullback.snd f g))

    Flatness of the closed subscheme over the base is preserved by arbitrary base change.

    source
    theorem AlgebraicGeometry.Scheme.IdealSheafData.flat_appLE_comp_ofHom_quotient_mk {S X : Scheme} (I : X.IdealSheafData) (f : X ⟶ S) [Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)] {W : S.Opens} (hW : IsAffineOpen W) (U : ↑X.affineOpens) (hUW : ↑U ≤ (TopologicalSpace.Opens.map f.base).obj W) :
    (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (Hom.appLE f W (↑U) hUW) (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))).Flat

    If the closed subscheme of I is flat over S, then over an affine open W of S, the quotient Γ(X, U) ⧸ I(U) is flat over Γ(S, W) for every affine open U ⊆ f⁻¹ W.