Theorems · Definition · category theory

SheafOfModules.pushforwardId

{D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {K : CategoryTheory.GrothendieckTopology D} →
      (R : CategoryTheory.Sheaf K RingCat) →
        SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (SheafOfModules R)

The pushforward functor by the identity morphism identifies to the identify functor of the category of sheaves of modules.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Cited by

5 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category