Module

ModulesProjectionMorphism.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesProjectionMorphism

4 declarations indexed from sourceView source ↗

Module documentation

Projection morphisms for module sheaves

The monoidal pullback comparison and adjunction counit define a projection morphism and its mate under the pullback-pushforward adjunction.

Imports2

Imported by8

def

projectionMorphismMate

L35 ↗

AlgebraicGeometry.Scheme.Modules.projectionMorphismMate

Documentation

The morphism from the pullback of i_* 𝟙 ⊗ F to i^* F obtained from the monoidal comparison, counit, and left unitor.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {Z X : Scheme.{u}} (i : Z ⟶ X)

Lean source · statement

def projectionMorphismMate (F : X.Modules) :
    (Modules.pullback i).obj ((Modules.pushforward i).obj (𝟙_ Z.Modules) ⊗ F) ⟶ (Modules.pullback
        i).obj F

def

projectionMorphism

L43 ↗

AlgebraicGeometry.Scheme.Modules.projectionMorphism

Documentation

The projection morphism i_* 𝟙 ⊗ F ⟶ i_* i^* F, adjoint to projectionMorphismMate i F.

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {Z X : Scheme.{u}} (i : Z ⟶ X)

Lean source · statement

def projectionMorphism (F : X.Modules) :
    (Modules.pushforward i).obj (𝟙_ Z.Modules) ⊗ F ⟶ (Modules.pushforward i).obj ((Modules.pullback
        i).obj F)

theorem

projectionMorphism_def

L48 ↗

AlgebraicGeometry.Scheme.Modules.projectionMorphism_def

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {Z X : Scheme.{u}} (i : Z ⟶ X)

Lean source · statement

theorem projectionMorphism_def (F : X.Modules) :
    projectionMorphism i F = ((pullbackPushforwardAdjunction i).homEquiv _ _)
        (projectionMorphismMate i F)

theorem

projectionMorphismMate_def

L52 ↗

AlgebraicGeometry.Scheme.Modules.projectionMorphismMate_def

Source context 5 commands

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

universe u
open CategoryTheory MonoidalCategory
noncomputable section
namespace AlgebraicGeometry.Scheme.Modules
variable {Z X : Scheme.{u}} (i : Z ⟶ X)

Lean source · statement

theorem projectionMorphismMate_def (F : X.Modules) :
    projectionMorphismMate i F =
      (Functor.Monoidal.μIso (Modules.pullback i) ((Modules.pushforward i).obj (𝟙_ Z.Modules))
          F).inv ≫
        ((pullbackPushforwardAdjunction i).counit.app (𝟙_ Z.Modules) ▷ (Modules.pullback i).obj F) ≫
        (λ_ ((Modules.pullback i).obj F)).hom

Module documentation

Projection morphisms for module sheaves

Declarations

projectionMorphismMate

projectionMorphism

projectionMorphism_def

projectionMorphismMate_def