Module

PullbackMonoidal.lean

Nyll.SchemeTheory.Modules.PullbackMonoidal

11 declarations indexed from sourceView source ↗

Module documentation

Tensor compatibility of module pullback on schemes

Pullback on module presheaves descends through module sheafification to a monoidal functor on module sheaves. Its tensor and unit comparison isomorphisms identify pullbacks of tensor products and structure modules with the corresponding tensor products and structure modules.

Imports5

Mathlib.CategoryTheory.Localization.Monoidal.Functor
Nyll.SchemeTheory.Modules.PresheafInternalHom
Nyll.SchemeTheory.Modules.SheafificationMonoidal
Nyll.SchemeTheory.Modules.Monoidal
Nyll.SchemeTheory.Modules.PresheafPullbackMonoidal

Imported by143

instance

preservesBinaryProducts_opensMap

L37 ↗

AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · full declaration

instance preservesBinaryProducts_opensMap :
    PreservesLimitsOfShape (Discrete WalkingPair) (Opens.map f.base) where
  preservesLimit {K} := ⟨fun {c} hc => ⟨
    { lift := fun s => homOfLE (by
        have hinf : K.obj ⟨.left⟩ ⊓ K.obj ⟨.right⟩ ≤ c.pt := leOfHom (hc.lift
          { pt := K.obj ⟨.left⟩ ⊓ K.obj ⟨.right⟩
            π := Discrete.natTrans (fun j => match j with
              | ⟨.left⟩ => homOfLE inf_le_left
              | ⟨.right⟩ => homOfLE inf_le_right) })
        have h₁ : s.pt ≤ (Opens.map f.base).obj (K.obj ⟨.left⟩) := leOfHom (s.π.app ⟨.left⟩)
        have h₂ : s.pt ≤ (Opens.map f.base).obj (K.obj ⟨.right⟩) := leOfHom (s.π.app ⟨.right⟩)
        exact (le_inf h₁ h₂).trans (leOfHom ((Opens.map f.base).map (homOfLE hinf))))
      fac := fun s j => Subsingleton.elim _ _
      uniq := fun s m _ => Subsingleton.elim _ _ }⟩⟩

instance

preservesTerminal_opensMap

L52 ↗

AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · full declaration

instance preservesTerminal_opensMap :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (Opens.map f.base) where
  preservesLimit {K} := ⟨fun {c} hc => ⟨
    { lift := fun s => homOfLE (by
        have htop : (⊤ : Y.Opens) ≤ c.pt := leOfHom (hc.lift
          { pt := ⊤, π := Discrete.natTrans (fun j => j.as.elim) })
        exact le_top.trans (leOfHom ((Opens.map f.base).map (homOfLE htop))))
      fac := fun s j => Subsingleton.elim _ _
      uniq := fun s m _ => Subsingleton.elim _ _ }⟩⟩

instance

preservesFiniteProducts_opensMap

L62 ↗

AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

instance preservesFiniteProducts_opensMap : PreservesFiniteProducts (Opens.map f.base)

abbrev

pullback₀

L66 ↗

AlgebraicGeometry.Scheme.Modules.pullback₀

Documentation

The pullback functor on module presheaves underlying the pullback of sheaves of modules.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

abbrev pullback₀ : Y.PresheafOfModules ⥤ X.PresheafOfModules

instance

pullback₀_monoidal

L69 ↗

AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

instance pullback₀_monoidal : (pullback₀ f).Monoidal

instance

(anonymous instance)

L73 ↗

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)

Lean source · statement

instance : (PresheafOfModules.pushforward.{u}
    (F := Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint

instance

sheafify_isLocalization'

L81 ↗

AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'

Source context 7 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
variable (Y) in

Lean source · statement

instance sheafify_isLocalization' : (Modules.sheafify Y).IsLocalization
    (SheafOfModules.presheafW (Opens.grothendieckTopology Y) Y.sheaf.obj)

instance

sheafifyPullback_lifting

L87 ↗

AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting

Source context 7 commands

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

universe u
open CategoryTheory MonoidalCategory Limits TopologicalSpace
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {X Y : Scheme.{u}} (f : X ⟶ Y)
local instance : (PresheafOfModules.pushforward.{u}
    (F := Opens.map f.base) f.toRingCatSheafHom.hom).IsRightAdjoint :=
  (PresheafOfModules.PullbackMonoidal.adj (Opens.map f.base)
    (R := X.sheaf.obj) (S := Y.sheaf.obj) f.c).isRightAdjoint
variable (Y) in

Lean source · statement

instance sheafifyPullback_lifting : Localization.Lifting (Modules.sheafify Y)
    (SheafOfModules.presheafW (Opens.grothendieckTopology Y) Y.sheaf.obj)
    (pullback₀ f ⋙ Modules.sheafify X) (Modules.pullback f)

instance