Documentation

TauCeti.AlgebraicGeometry.Modules.Pushforward

Pushforward and restriction of modules on schemes #

Pushforward along a scheme isomorphism agrees with restriction along its inverse. This identification transports local properties of module sheaves through affine normalizations. Restriction of a pushforward to an open of the base agrees with pushforward of the restriction to its preimage. Both comparisons have formulas on sections.

These comparisons use Mathlib's module pushforward and restriction API.

source
noncomputable def TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) :
AlgebraicGeometry.Scheme.Modules.pushforward e.hom ≅ AlgebraicGeometry.Scheme.Modules.restrictFunctor e.inv

Pushforward along an isomorphism agrees with restriction along its inverse.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor_hom_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (M : X.Modules) (V : Y.Opens) (x : ↑(((AlgebraicGeometry.Scheme.Modules.pushforward e.hom).obj M).presheaf.obj (Opposite.op V))) :
    (CategoryTheory.ConcreteCategory.hom (((pushforwardIsoRestrictFunctor e).hom.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

    On sections, pushforward along an isomorphism is restriction along the equality between the image under its inverse and the preimage under the forward map.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.pushforwardIsoRestrictFunctor_inv_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (M : X.Modules) (V : Y.Opens) (x : ↑((M.restrict e.inv).presheaf.obj (Opposite.op V))) :
    (CategoryTheory.ConcreteCategory.hom (((pushforwardIsoRestrictFunctor e).inv.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

    The inverse pushforward--restriction comparison uses the inverse equality of opens.

    source
    noncomputable def TauCeti.AlgebraicGeometry.restrictPushforwardIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) :
    (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.restrictFunctor U.ι) ≅ (AlgebraicGeometry.Scheme.Modules.restrictFunctor ((TopologicalSpace.Opens.map f.base).obj U).ι).comp (AlgebraicGeometry.Scheme.Modules.pushforward (f ∣_ U))

    Restricting a pushforward to an open of the base agrees with pushing forward the restriction to its preimage, naturally in the module sheaf.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.restrictPushforwardIso_hom_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (M : X.Modules) (V : (↑U).Opens) (x : ↑((((AlgebraicGeometry.Scheme.Modules.pushforward f).obj M).restrict U.ι).presheaf.obj (Opposite.op V))) :
      (CategoryTheory.ConcreteCategory.hom (((restrictPushforwardIso f U).hom.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

      On sections, open restriction of pushforward is the restriction along the equality of the two inverse-image opens.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.restrictPushforwardIso_inv_app_val_app_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) (M : X.Modules) (V : (↑U).Opens) (x : ↑(((AlgebraicGeometry.Scheme.Modules.pushforward (f ∣_ U)).obj (M.restrict ((TopologicalSpace.Opens.map f.base).obj U).ι)).presheaf.obj (Opposite.op V))) :
      (CategoryTheory.ConcreteCategory.hom (((restrictPushforwardIso f U).inv.app M).val.app (Opposite.op V))) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (CategoryTheory.eqToHom ⋯).op)) x

      The inverse comparison restricts along the inverse equality of inverse-image opens.