FullyFaithful

📁 Source: Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Statistics

Metric	Count
Definitions `counitSplitMonoOfRFull`, `fullyFaithfulLOfIsIsoUnit`, `fullyFaithfulROfIsIsoCounit`, `unitSplitEpiOfLFull`, `whiskerLeftLCounitIsoOfIsIsoUnit`, `whiskerLeftRUnitIsoOfIsIsoCounit`	6
Theorems `counit_epi_of_R_faithful`, `counit_isIso_of_R_fully_faithful`, `counit_isSplitMono_of_R_full`, `faithful_L_of_mono_unit_app`, `faithful_R_of_epi_counit_app`, `full_L_of_isSplitEpi_unit_app`, `full_R_of_isSplitMono_counit_app`, `instIsIsoAppCounitObjOfFaithfulOfFull`, `instIsIsoAppCounitOfFullOfFaithful`, `instIsIsoAppUnitObjOfFaithfulOfFull`, `instIsIsoAppUnitOfFullOfFaithful`, `instIsIsoFunctorCounitOfIsEquivalence`, `instIsIsoFunctorCounitOfIsEquivalence_1`, `instIsIsoFunctorUnitOfIsEquivalence`, `instIsIsoFunctorUnitOfIsEquivalence_1`, `instIsIsoMapAppCounitOfFaithfulOfFull`, `instIsIsoMapAppUnitOfFaithfulOfFull`, `inv_counit_map`, `inv_map_unit`, `isEquivalence_left_of_isEquivalence_right`, `isEquivalence_right_of_isEquivalence_left`, `isIso_counit_app_iff_mem_essImage`, `isIso_counit_app_of_iso`, `isIso_unit_app_iff_mem_essImage`, `isIso_unit_app_of_iso`, `mem_essImage_of_counit_isIso`, `mem_essImage_of_unit_isIso`, `unit_isIso_of_L_fully_faithful`, `unit_isSplitEpi_of_L_full`, `unit_mono_of_L_faithful`, `whiskerLeftLCounitIsoOfIsIsoUnit_hom_app`, `whiskerLeftLCounitIsoOfIsIsoUnit_inv_app`, `whiskerLeftRUnitIsoOfIsIsoCounit_hom_app`, `whiskerLeftRUnitIsoOfIsIsoCounit_inv_app`, `whiskerLeft_counit_iso_of_L_fully_faithful`, `whiskerLeft_unit_iso_of_R_fully_faithful`, `whiskerRight_counit_iso_of_L_fully_faithful`, `whiskerRight_unit_iso_of_R_fully_faithful`	38
Total	44

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
`counitSplitMonoOfRFull` 📖	CompOp	—
`fullyFaithfulLOfIsIsoUnit` 📖	CompOp	—
`fullyFaithfulROfIsIsoCounit` 📖	CompOp	—
`unitSplitEpiOfLFull` 📖	CompOp	—
`whiskerLeftLCounitIsoOfIsIsoUnit` 📖	CompOp	2 math math: `whiskerLeftLCounitIsoOfIsIsoUnit_hom_app`, `whiskerLeftLCounitIsoOfIsIsoUnit_inv_app`
`whiskerLeftRUnitIsoOfIsIsoCounit` 📖	CompOp	2 math math: `whiskerLeftRUnitIsoOfIsIsoCounit_hom_app`, `whiskerLeftRUnitIsoOfIsIsoCounit_inv_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counit_epi_of_R_faithful` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	—	`CategoryTheory.Functor.map_injective` `Equiv.injective` `homEquiv_counit` `counit_naturality`
`counit_isIso_of_R_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `counit`	—	`CategoryTheory.NatIso.isIso_of_isIso_app` `instIsIsoAppCounitOfFullOfFaithful`
`counit_isSplitMono_of_R_full` 📖	mathematical	—	`CategoryTheory.IsSplitMono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	—	—
`faithful_L_of_mono_unit_app` 📖	mathematical	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	`CategoryTheory.Functor.Faithful`	—	`CategoryTheory.Mono.right_cancellation` `Equiv.injective` `homEquiv_counit` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `left_triangle_components` `CategoryTheory.Category.comp_id`
`faithful_R_of_epi_counit_app` 📖	mathematical	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	`CategoryTheory.Functor.Faithful`	—	`CategoryTheory.Epi.left_cancellation` `Equiv.injective` `homEquiv_unit` `CategoryTheory.Functor.map_comp` `right_triangle_components_assoc`
`full_L_of_isSplitEpi_unit_app` 📖	mathematical	`CategoryTheory.IsSplitEpi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	`CategoryTheory.Functor.Full`	—	`CategoryTheory.Category.comp_id` `left_triangle_components` `CategoryTheory.IsSplitEpi.id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `homEquiv_unit` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `counit_naturality` `left_triangle_components_assoc`
`full_R_of_isSplitMono_counit_app` 📖	mathematical	`CategoryTheory.IsSplitMono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	`CategoryTheory.Functor.Full`	—	`CategoryTheory.Category.id_comp` `right_triangle_components` `CategoryTheory.Category.assoc` `CategoryTheory.IsSplitMono.id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `homEquiv_counit` `CategoryTheory.Functor.map_comp` `unit_naturality_assoc`
`instIsIsoAppCounitObjOfFaithfulOfFull` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	—	`CategoryTheory.isIso_of_hom_comp_eq_id` `CategoryTheory.Functor.map_isIso` `instIsIsoAppUnitOfFullOfFaithful` `left_triangle_components`
`instIsIsoAppCounitOfFullOfFaithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	—	`CategoryTheory.isIso_of_epi_of_isSplitMono` `counit_isSplitMono_of_R_full` `counit_epi_of_R_faithful`
`instIsIsoAppUnitObjOfFaithfulOfFull` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	—	`CategoryTheory.isIso_of_comp_hom_eq_id` `CategoryTheory.Functor.map_isIso` `instIsIsoAppCounitOfFullOfFaithful` `right_triangle_components`
`instIsIsoAppUnitOfFullOfFaithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	—	`CategoryTheory.isIso_of_mono_of_isSplitEpi` `unit_mono_of_L_faithful` `unit_isSplitEpi_of_L_full`
`instIsIsoFunctorCounitOfIsEquivalence` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `counit`	—	`isIso_counit_app_of_iso` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.Functor.IsEquivalence.essSurj` `CategoryTheory.NatIso.isIso_of_isIso_app`
`instIsIsoFunctorCounitOfIsEquivalence_1` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `counit`	—	`isEquivalence_left_of_isEquivalence_right` `instIsIsoFunctorCounitOfIsEquivalence`
`instIsIsoFunctorUnitOfIsEquivalence` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit`	—	`isIso_unit_app_of_iso` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.Functor.IsEquivalence.essSurj` `CategoryTheory.NatIso.isIso_of_isIso_app`
`instIsIsoFunctorUnitOfIsEquivalence_1` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit`	—	`isEquivalence_right_of_isEquivalence_left` `instIsIsoFunctorUnitOfIsEquivalence`
`instIsIsoMapAppCounitOfFaithfulOfFull` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `counit`	—	`CategoryTheory.isIso_of_hom_comp_eq_id` `instIsIsoAppUnitOfFullOfFaithful` `right_triangle_components`
`instIsIsoMapAppUnitOfFaithfulOfFull` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `unit`	—	`CategoryTheory.isIso_of_comp_hom_eq_id` `instIsIsoAppCounitOfFullOfFaithful` `left_triangle_components`
`inv_counit_map` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `counit` `CategoryTheory.Functor.map_isIso` `unit`	—	`CategoryTheory.IsIso.inv_eq_of_inv_hom_id` `CategoryTheory.Functor.map_isIso` `right_triangle_components`
`inv_map_unit` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.Functor.map_isIso` `counit`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `CategoryTheory.Functor.map_isIso` `left_triangle_components`
`isEquivalence_left_of_isEquivalence_right` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence`	—	`CategoryTheory.Equivalence.isEquivalence_functor` `CategoryTheory.NatIso.isIso_app_of_isIso` `instIsIsoFunctorUnitOfIsEquivalence` `instIsIsoAppCounitOfFullOfFaithful` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.Functor.IsEquivalence.faithful`
`isEquivalence_right_of_isEquivalence_left` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence`	—	`CategoryTheory.Equivalence.isEquivalence_inverse` `instIsIsoAppUnitOfFullOfFaithful` `CategoryTheory.Functor.IsEquivalence.full` `CategoryTheory.Functor.IsEquivalence.faithful` `CategoryTheory.NatIso.isIso_app_of_isIso` `instIsIsoFunctorCounitOfIsEquivalence`
`isIso_counit_app_iff_mem_essImage` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit` `CategoryTheory.Functor.essImage`	—	`CategoryTheory.NatTrans.isIso_app_iff_of_iso` `instIsIsoAppCounitObjOfFaithfulOfFull`
`isIso_counit_app_of_iso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `counit`	—	`isIso_counit_app_iff_mem_essImage`
`isIso_unit_app_iff_mem_essImage` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit` `CategoryTheory.Functor.essImage`	—	`CategoryTheory.NatTrans.isIso_app_iff_of_iso` `instIsIsoAppUnitObjOfFaithfulOfFull`
`isIso_unit_app_of_iso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	—	`isIso_unit_app_iff_mem_essImage`
`mem_essImage_of_counit_isIso` 📖	mathematical	—	`CategoryTheory.Functor.essImage`	—	—
`mem_essImage_of_unit_isIso` 📖	mathematical	—	`CategoryTheory.Functor.essImage`	—	—
`unit_isIso_of_L_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `unit`	—	`CategoryTheory.NatIso.isIso_of_isIso_app` `instIsIsoAppUnitOfFullOfFaithful`
`unit_isSplitEpi_of_L_full` 📖	mathematical	—	`CategoryTheory.IsSplitEpi` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	—	—
`unit_mono_of_L_faithful` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `unit`	—	`CategoryTheory.Functor.map_injective` `Equiv.injective` `homEquiv_unit` `unit_naturality`
`whiskerLeftLCounitIsoOfIsIsoUnit_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `whiskerLeftLCounitIsoOfIsIsoUnit` `CategoryTheory.Functor.id` `counit` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatIso.isIso_inv_app` `CategoryTheory.Functor.map_inv` `inv_map_unit` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`whiskerLeftLCounitIsoOfIsIsoUnit_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `whiskerLeftLCounitIsoOfIsIsoUnit` `CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `unit`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`whiskerLeftRUnitIsoOfIsIsoCounit_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `whiskerLeftRUnitIsoOfIsIsoCounit` `CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `counit`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`whiskerLeftRUnitIsoOfIsIsoCounit_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `whiskerLeftRUnitIsoOfIsIsoCounit` `CategoryTheory.Functor.id` `unit` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.isIso_app_of_isIso` `CategoryTheory.NatIso.isIso_inv_app` `CategoryTheory.Functor.map_inv` `inv_counit_map` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`whiskerLeft_counit_iso_of_L_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerLeft` `counit`	—	`left_triangle` `CategoryTheory.Functor.isIso_whiskerRight` `unit_isIso_of_L_fully_faithful` `CategoryTheory.IsIso.eq_inv_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.inv_isIso` `CategoryTheory.IsIso.id`
`whiskerLeft_unit_iso_of_R_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerLeft` `unit`	—	`right_triangle` `CategoryTheory.Functor.isIso_whiskerRight` `counit_isIso_of_R_fully_faithful` `CategoryTheory.IsIso.eq_comp_inv` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.IsIso.inv_isIso`
`whiskerRight_counit_iso_of_L_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerRight` `counit`	—	`right_triangle` `CategoryTheory.Functor.isIso_whiskerLeft` `unit_isIso_of_L_fully_faithful` `CategoryTheory.IsIso.eq_inv_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.inv_isIso` `CategoryTheory.IsIso.id`
`whiskerRight_unit_iso_of_R_fully_faithful` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Functor.whiskerRight` `unit`	—	`left_triangle` `CategoryTheory.Functor.isIso_whiskerLeft` `counit_isIso_of_R_fully_faithful` `CategoryTheory.IsIso.eq_comp_inv` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.id` `CategoryTheory.IsIso.inv_isIso`

---

← Back to Index