Module

PullbackUnitComposition.lean

Nyll.SchemeTheory.Modules.PullbackUnitComposition

1 declaration indexed from sourceView source ↗

Module documentation

Units and composition of pullback functors

The unit for a composite scheme morphism agrees with the successive units after the canonical pullback composition comparison.

Imports1

Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by10

theorem

unit_app_comp_pullbackComp_inv

L30 ↗

AlgebraicGeometry.Scheme.Modules.unit_app_comp_pullbackComp_inv

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_unit_app_comp_pullbackComp_inv
universe u
open CategoryTheory AlgebraicGeometry Opposite AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.unit_app_comp_pullbackComp_inv
    {X Y Z : Scheme.{u}} (g : Z ⟶ Y) (f : Y ⟶ X) (M : X.Modules) (U : X.Opens) :
    ((Scheme.Modules.pullbackPushforwardAdjunction (g ≫ f)).unit.app M).app U ≫
        ((Scheme.Modules.pullbackComp g f).inv.app M).app ((g ≫ f) ⁻¹ᵁ U) =
      ((Scheme.Modules.pullbackPushforwardAdjunction f).unit.app M).app U ≫
        ((Scheme.Modules.pullbackPushforwardAdjunction g).unit.app
          ((Scheme.Modules.pullback f).obj M)).app (f ⁻¹ᵁ U)

Module documentation

Units and composition of pullback functors

Declarations

unit_app_comp_pullbackComp_inv