Documentation

TauCeti.AlgebraicGeometry.IdealSheaf.Functor

The functor of ideal sheaves on base changes #

Let f : X ⟶ S be a morphism of schemes. For a scheme T over S, write X_T = T ×_S X for the base change of X. A morphism T' ⟶ T over S induces X_{T'} ⟶ X_T, and pulling back ideal sheaves along it makes T ↦ {ideal sheaves on X_T} a functor (Over S)ᵒᵖ ⥤ Type.

The base change X_T = T ×_S X and the induced morphisms ((Over.pullback f).map φ).left are those used by TauCeti.AlgebraicGeometry.rigidifiedPicardFunctor.

Main declarations #

source
noncomputable def TauCeti.AlgebraicGeometry.baseChangeIdealSheafFunctor {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) :
CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ (Type u)

The functor of closed subschemes of the base changes of f : X ⟶ S: it sends a scheme T over S to the ideal sheaves on X_T = T ×_S X, and a morphism T' ⟶ T over S to pullback of ideal sheaves along the induced morphism X_{T'} ⟶ X_T.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.AlgebraicGeometry.baseChangeIdealSheafFunctor_obj {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (T : (CategoryTheory.Over S)ᵒᵖ) :
    (baseChangeIdealSheafFunctor f).obj T = (CategoryTheory.Limits.pullback (Opposite.unop T).hom f).IdealSheafData

    The value of baseChangeIdealSheafFunctor f at T is the type of ideal sheaves on T ×_S X.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeIdealSheafFunctor_map_apply {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (I : (baseChangeIdealSheafFunctor f).obj T) :
    (CategoryTheory.ConcreteCategory.hom ((baseChangeIdealSheafFunctor f).map φ)) I = AlgebraicGeometry.Scheme.IdealSheafData.comap I (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map φ.unop))

    baseChangeIdealSheafFunctor f acts by pullback of ideal sheaves along the induced morphism of base changes.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.baseChangeIdealSheafFunctor_map_top {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') :
    (CategoryTheory.ConcreteCategory.hom ((baseChangeIdealSheafFunctor f).map φ)) ⊤ = ⊤

    Base change preserves the unit ideal sheaf, that is, the empty closed subscheme.