Restrict

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

Statistics

Metric	Count
Definitions restrictFullyFaithful	1
Theorems map_restrictFullyFaithful_counit_app, map_restrictFullyFaithful_counit_app_assoc, map_restrictFullyFaithful_unit_app, map_restrictFullyFaithful_unit_app_assoc, restrictFullyFaithful_homEquiv_apply	5
Total	6

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
restrictFullyFaithful 📖	CompOp	5 math math: map_restrictFullyFaithful_unit_app_assoc, map_restrictFullyFaithful_counit_app, map_restrictFullyFaithful_counit_app_assoc, restrictFullyFaithful_homEquiv_apply, map_restrictFullyFaithful_unit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_restrictFullyFaithful_counit_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.NatTrans.app counit restrictFullyFaithful CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp homEquiv_counit CategoryTheory.Category.comp_id CategoryTheory.Functor.FullyFaithful.map_preimage
map_restrictFullyFaithful_counit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id counit restrictFullyFaithful CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_restrictFullyFaithful_counit_app
map_restrictFullyFaithful_unit_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatTrans.app unit restrictFullyFaithful CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id homEquiv_unit CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Functor.FullyFaithful.map_preimage
map_restrictFullyFaithful_unit_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp unit restrictFullyFaithful CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_restrictFullyFaithful_unit_app
restrictFullyFaithful_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj EquivLike.toFunLike Equiv.instEquivLike homEquiv restrictFullyFaithful CategoryTheory.Functor.FullyFaithful.preimage CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.id unit CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category	—	CategoryTheory.Functor.FullyFaithful.map_injective CategoryTheory.Functor.map_comp map_restrictFullyFaithful_unit_app CategoryTheory.Category.assoc CategoryTheory.Functor.FullyFaithful.map_preimage CategoryTheory.NatTrans.naturality

---

← Back to Index