Theorems · Definition · category theory

PresheafOfModules.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {P : Sort u_1} →
        {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} →
                {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} →
                        { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
                            { obj := obj', map := map', map_id := map_id', map_comp := map_comp' } →
                          (obj ≍ obj' → map ≍ map' → P) → P

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf

Cited by

1 results in Mathlib

Foundations

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