NYLL
Module

Scheme_Modules_projectionMorphism_naturality.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_projectionMorphism_naturality
1 declaration indexed from sourceView source ↗

Module documentation

Naturality of the projection morphism

Projection morphisms commute with maps between the module sheaves being pulled back.

Imports3
Imported by2

Declarations

theorem

projectionMorphism_naturality

L33 ↗
AlgebraicGeometry.Scheme.Modules.projectionMorphism_naturality
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_projectionMorphism_naturality
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.projectionMorphism_naturality
    {Z X : Scheme.{u}} (i : Z ⟶ X) {F F' : X.Modules} (φ : F ⟶ F') :
    Scheme.Modules.projectionMorphism i F ≫
        (Scheme.Modules.pushforward i).map ((Scheme.Modules.pullback i).map φ) =
      ((Scheme.Modules.pushforward i).obj (𝟙_ Z.Modules) ◁ φ) ≫ Scheme.Modules.projectionMorphism i
          F'

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.