Documentation

TauCeti.AlgebraicGeometry.Modules.Differentials.Restriction

Restriction of relative differentials #

The sheaf of relative differentials commutes with restriction along an open immersion over an affine base. The canonical isomorphism sends the differential of a local function to the differential of its restriction. This permits affine computations of differentials to be used on arbitrary schemes. The isomorphism is relativeDifferentialsRestrictIso, characterized by relativeDifferentialsRestrictIso_hom_app_d and relativeDifferentialsRestrictIso_inv_app_d.

References #

source
def TauCeti.AlgebraicGeometry.pushforwardDerivation (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] {M : X.Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) :
AlgebraicGeometry.Scheme.Modules.Derivation R ((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M)

A derivation of the structure sheaf of X induces a derivation into its pushforward on Y, by differentiating the pullbacks of local functions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.pushforwardDerivation_d (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] {M : X.Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) (U : Y.Opens) (a : ↑(Y.presheaf.obj (Opposite.op U))) :
    (pushforwardDerivation R f d).d a = d.d ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U)) a)

    The pushed derivation differentiates the pullback of a local function.

    source
    noncomputable def TauCeti.AlgebraicGeometry.restrictDerivation (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsOpenImmersion f] {M : Y.Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) :
    AlgebraicGeometry.Scheme.Modules.Derivation R (M.restrict f)

    On an open immersion, a derivation restricts by identifying the functions on each open with the functions on its image.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.restrictDerivation_d (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsOpenImmersion f] {M : Y.Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) (U : X.Opens) (a : ↑(X.presheaf.obj (Opposite.op U))) :
      (restrictDerivation R f d).d a = d.d ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) a)

      A restricted derivation differentiates the corresponding function on the image open.

      source
      noncomputable def TauCeti.AlgebraicGeometry.relativeDifferentialsRestrictIso (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsOpenImmersion f] :
      (AlgebraicGeometry.Scheme.relativeDifferentials R Y).restrict f ≅ AlgebraicGeometry.Scheme.relativeDifferentials R X

      Relative differentials commute with restriction along an open immersion over Spec R. The inverse sends d a on X to the differential of the corresponding function on Y.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem TauCeti.AlgebraicGeometry.relativeDifferentialsRestrictIso_hom_app_d (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) (a : ↑(Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)))) :
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (relativeDifferentialsRestrictIso R f).hom U)) ((AlgebraicGeometry.Scheme.universalDerivation R Y).d a) = (AlgebraicGeometry.Scheme.universalDerivation R X).d ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).hom) a)

        The restriction comparison carries the differential of a function on Y to the differential of that function on X.

        source
        @[simp]
        theorem TauCeti.AlgebraicGeometry.relativeDifferentialsRestrictIso_inv_app_d (R : Type u) [CommRing R] {X Y : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [Y.Over (AlgebraicGeometry.Spec ↧R)] (f : X ⟶ Y) [hf : AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens) (a : ↑(X.presheaf.obj (Opposite.op U))) :
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (relativeDifferentialsRestrictIso R f).inv U)) ((AlgebraicGeometry.Scheme.universalDerivation R X).d a) = (AlgebraicGeometry.Scheme.universalDerivation R Y).d ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) a)

        The inverse restriction comparison sends d a to the differential of the corresponding function on the image open.