Theorems · Theorem · category theory

CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite

∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {A : Type w}
  [inst_2 : CategoryTheory.Category.{w', w} A]
  [inst_3 : ∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A]
  [CategoryTheory.Functor.IsDenseSubsite J K G] (Y : CategoryTheory.Sheaf J A) (U : C) (X : A),
  CategoryTheory.IsIso
    ((CategoryTheory.yoneda.map ((G.op.ranCounit.app Y.obj).app (Opposite.op U))).app (Opposite.op X))

Defined in

Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Functor.IsDenseSubsite