Theorems · Theorem · category theory

PresheafOfModules.mk.sizeOf_spec

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} [inst_1 : SizeOf C]
  (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 :
    autoParam
      (∀ (X : Cᵒᵖ),
        map (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj X))
      PresheafOfModules.map_id._autoParam)
  (map_comp :
    autoParam
      (∀ {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))))
      PresheafOfModules.map_comp._autoParam),
  sizeOf { obj := obj, map := map, map_id := map_id, map_comp := map_comp } = 1

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySizeOf