Module

PushforwardRestrict.lean

Nyll.SchemeTheory.Modules.PushforwardRestrict

4 declarations indexed from sourceView source ↗

Module documentation

Restriction of direct images to open subschemes

The comparison uses the actual preimage-open equality and native scheme restriction maps. The former AlgebraicCurves owner reexports this shared owner.

Imports2

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Tactic.Ext

Imported by3

lemma

topSheaf_comp_hom

L29 ↗

AlgebraicGeometry.Scheme.Modules.topSheaf_comp_hom

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

lemma topSheaf_comp_hom {Z : TopCat.{u}}
    {A B C : Z.Sheaf RingCat.{u}} (f : A ⟶ B) (g : B ⟶ C) :
    (f ≫ g).hom = f.hom ≫ g.hom

def

restrictPushforwardOpensIso

L37 ↗

AlgebraicGeometry.Scheme.Modules.restrictPushforwardOpensIso

Documentation

The two actual target-open indexing functors agree by the preimage formula for morphismRestrict.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (g : X ⟶ Y) (W : Y.Opens)

Lean source · statement

def restrictPushforwardOpensIso :
    (Opens.map (g ∣_ W).base ⋙ (g ⁻¹ᵁ W).ι.opensFunctor : W.toScheme.Opens ⥤ X.Opens) ≅
      W.ι.opensFunctor ⋙ Opens.map g.base

def

pushforwardRestrictIso

L44 ↗

AlgebraicGeometry.Scheme.Modules.pushforwardRestrictIso

Documentation

Restriction to an open subscheme commutes with the actual direct image. The ring-map comparison is proved from morphismRestrict_app'.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (g : X ⟶ Y) (W : Y.Opens)

Lean source · statement

def pushforwardRestrictIso :
    restrictFunctor (g ⁻¹ᵁ W).ι ⋙ pushforward (g ∣_ W) ≅ pushforward g ⋙ restrictFunctor W.ι

lemma

pushforwardRestrictIso_hom_app_app

L109 ↗

AlgebraicGeometry.Scheme.Modules.pushforwardRestrictIso_hom_app_app

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory AlgebraicGeometry Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (g : X ⟶ Y) (W : Y.Opens)

Lean source · statement

lemma pushforwardRestrictIso_hom_app_app (M : X.Modules) (U : W.toScheme.Opens) :
    ((pushforwardRestrictIso g W).hom.app M).app U =
      M.presheaf.map (eqToHom (image_morphismRestrict_preimage g W U).symm).op

Module documentation

Restriction of direct images to open subschemes

Declarations

topSheaf_comp_hom

restrictPushforwardOpensIso

pushforwardRestrictIso

pushforwardRestrictIso_hom_app_app