Theorems · Theorem · category theory
CategoryTheory.Functor.essImage.counit_isIso
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
{j : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Coreflective j] {A : D},
j.essImage A → CategoryTheory.IsIso ((CategoryTheory.coreflectorAdjunction j).counit.app A)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.NatTrans.appstatement · cited by 7,406
- CategoryTheory.Functor.compstatement · cited by 6,529
- CategoryTheory.Functor.idstatement · cited by 3,333
- CategoryTheory.IsIsostatement · cited by 1,156
- CategoryTheory.Adjunction.counitstatement · cited by 376
- CategoryTheory.Functor.essImagestatement and proof · cited by 82
- CategoryTheory.Coreflectivestatement and proof · cited by 9
- CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImageproof · cited by 4
- CategoryTheory.coreflectorstatement · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.mem_essImage_of_counit_isSplitEpiproof · cited by 0