NYLL
Module

Scheme_Modules_pullback_map_projectionMorphism_comp_counit.lean

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

Module documentation

The counit and the projection morphism

Pulling back the projection morphism and composing with the counit gives its adjoint mate.

Imports3
Imported by2

Declarations

theorem

pullback_map_projectionMorphism_comp_counit

L35 ↗
AlgebraicGeometry.Scheme.Modules.pullback_map_projectionMorphism_comp_counit
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_pullback_map_projectionMorphism_comp_counit
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.Modules.pullback_map_projectionMorphism_comp_counit
    {Z X : Scheme.{u}} (i : Z ⟶ X) (F : X.Modules) :
    (Scheme.Modules.pullback i).map (Scheme.Modules.projectionMorphism i F) ≫
        (Scheme.Modules.pullbackPushforwardAdjunction i).counit.app ((Scheme.Modules.pullback i).obj
            F) =
      Scheme.Modules.projectionMorphismMate i F

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