Theorems · Theorem · category theory

CategoryTheory.presheafHom_map_app_op_mk_id

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {F G : CategoryTheory.Functor Cᵒᵖ A} {X Y : C} (g : Y ⟶ X) (α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)),
  ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.presheafHom F G).map g.op)) α).app
      (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y))) =
    α.app (Opposite.op (CategoryTheory.Over.mk g))

Defined in

Mathlib.CategoryTheory.Sites.SheafHom

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category