Theorems · Theorem · category theory

CategoryTheory.equivEssImageOfReflective_counitIso

∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i],
  CategoryTheory.equivEssImageOfReflective.counitIso =
    CategoryTheory.Functor.fullyFaithfulCancelRight i.essImage.ι
      (CategoryTheory.NatIso.ofComponents
        (fun X => (CategoryTheory.asIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)).symm) ⋯)

Defined in

Mathlib.CategoryTheory.Adjunction.Reflective

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Reflective