Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.uliftYonedaCompSheafToPresheaf_inv_app_app_hom_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ)
  (a :
    (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).comp
              (CategoryTheory.sheafToPresheaf J (Type (max v w)))).obj
          X).obj
      X_1),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaCompSheafToPresheaf.inv.app X).app X_1)) a = a

Defined in

Mathlib.CategoryTheory.Sites.Canonical

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GrothendieckTopology.Subcanonical