Theorems · Definition · category theory

PresheafOfModules.casesOn

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {motive : PresheafOfModules R → Sort u_1} →
        (t : PresheafOfModules R) →
          ((obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)) →
              (map :
                  {X Y : Cᵒᵖ} →
                    (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj Y)) →
                (map_id :
                    ∀ (X : Cᵒᵖ),
                      map (CategoryTheory.CategoryStruct.id X) =
                        (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X)))
                                ⋯).inv.app
                          (obj X)) →
                  (map_comp :
                      ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
                        map (CategoryTheory.CategoryStruct.comp f g) =
                          CategoryTheory.CategoryStruct.comp (map f)
                            (CategoryTheory.CategoryStruct.comp
                              ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map g))
                              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                                (obj Z)))) →
                    motive { obj := obj, map := map, map_id := map_id, map_comp := map_comp }) →
            motive t

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category