Reflective

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

Statistics

Metric	Count
Definitions Coreflective, R, adj, comp, fullyFaithfulOfCoreflective, fullyFaithfulOfReflective, Reflective, L, adj, comp, coreflector, coreflectorAdjunction, equivEssImageOfReflective, reflector, reflectorAdjunction, unitCompPartialBijective, unitCompPartialBijectiveAux	17
Theorems toFaithful, toFull, counit_isIso, unit_isIso, essImage_ext_iff, toFaithful, toFull, counit_obj_eq_map_counit, equivEssImageOfReflective_counitIso, equivEssImageOfReflective_functor, equivEssImageOfReflective_inverse, equivEssImageOfReflective_unitIso, instIsIsoAppUnitReflectorAdjunctionObjEssImage, instIsLeftAdjointOfCoreflective, instIsLeftAdjointReflector, instIsRightAdjointCoreflector, instIsRightAdjointOfReflective, mem_essImage_of_counit_isSplitEpi, mem_essImage_of_unit_isSplitMono, unitCompPartialBijectiveAux_symm_apply, unitCompPartialBijective_natural, unitCompPartialBijective_symm_apply, unitCompPartialBijective_symm_natural, unit_obj_eq_map_unit	24
Total	41

CategoryTheory

Definitions

Name	Category	Theorems
Coreflective 📖	CompData	—
Reflective 📖	CompData	—
coreflector 📖	CompOp	6 math math: Functor.essImage.counit_isIso, Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, δ_iso_of_coreflective, counit_obj_eq_map_counit, instIsRightAdjointCoreflector, Coreflective.comparison_essSurj
coreflectorAdjunction 📖	CompOp	5 math math: Functor.essImage.counit_isIso, Coreflective.instIsIsoAppCounitCoreflectorAdjunctionA, δ_iso_of_coreflective, counit_obj_eq_map_counit, Coreflective.comparison_essSurj
equivEssImageOfReflective 📖	CompOp	4 math math: equivEssImageOfReflective_unitIso, equivEssImageOfReflective_functor, equivEssImageOfReflective_inverse, equivEssImageOfReflective_counitIso
reflector 📖	CompOp	20 math math: equivEssImageOfReflective_unitIso, prodComparison_iso, Limits.PreservesFiniteProducts.of_exponentialIdeal, preservesBinaryProducts_of_exponentialIdeal, bijection_natural, instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, bijection_symm_apply_id, unitCompPartialBijective_natural, Functor.essImage.unit_isIso, instIsIsoAppUnitReflectorAdjunctionObjEssImage, instIsLeftAdjointReflector, equivEssImageOfReflective_inverse, unitCompPartialBijective_symm_natural, μ_iso_of_reflective, unitCompPartialBijectiveAux_symm_apply, Reflective.comparison_essSurj, equivEssImageOfReflective_counitIso, unit_obj_eq_map_unit, Reflective.instIsIsoAppUnitReflectorAdjunctionA, unitCompPartialBijective_symm_apply
reflectorAdjunction 📖	CompOp	10 math math: equivEssImageOfReflective_unitIso, Functor.essImage.unit_isIso, instIsIsoAppUnitReflectorAdjunctionObjEssImage, μ_iso_of_reflective, unitCompPartialBijectiveAux_symm_apply, Reflective.comparison_essSurj, equivEssImageOfReflective_counitIso, unit_obj_eq_map_unit, Reflective.instIsIsoAppUnitReflectorAdjunctionA, unitCompPartialBijective_symm_apply
unitCompPartialBijective 📖	CompOp	3 math math: unitCompPartialBijective_natural, unitCompPartialBijective_symm_natural, unitCompPartialBijective_symm_apply
unitCompPartialBijectiveAux 📖	CompOp	1 math math: unitCompPartialBijectiveAux_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counit_obj_eq_map_counit 📖	mathematical	—	NatTrans.app Functor.comp coreflector Functor.id Adjunction.counit coreflectorAdjunction Functor.obj Functor.map	—	cancel_epi Functor.map_epi Functor.preservesEpimorphisms_of_isLeftAdjoint instIsLeftAdjointOfCoreflective epi_of_strongEpi strongEpi_of_isIso Adjunction.instIsIsoAppUnitOfFullOfFaithful Coreflective.toFull Coreflective.toFaithful Functor.map_comp Adjunction.left_triangle_components Adjunction.right_triangle_components Functor.map_id
equivEssImageOfReflective_counitIso 📖	mathematical	—	Equivalence.counitIso Functor.EssImageSubcategory ObjectProperty.FullSubcategory.category Functor.essImage equivEssImageOfReflective Functor.fullyFaithfulCancelRight Functor.comp ObjectProperty.ι reflector Functor.toEssImage Functor.id NatIso.ofComponents Iso.symm Functor.obj ObjectProperty.FullSubcategory.obj asIso NatTrans.app Adjunction.unit reflectorAdjunction instIsIsoAppUnitReflectorAdjunctionObjEssImage	—	—
equivEssImageOfReflective_functor 📖	mathematical	—	Equivalence.functor Functor.EssImageSubcategory ObjectProperty.FullSubcategory.category Functor.essImage equivEssImageOfReflective Functor.toEssImage	—	—
equivEssImageOfReflective_inverse 📖	mathematical	—	Equivalence.inverse Functor.EssImageSubcategory ObjectProperty.FullSubcategory.category Functor.essImage equivEssImageOfReflective Functor.comp ObjectProperty.ι reflector	—	—
equivEssImageOfReflective_unitIso 📖	mathematical	—	Equivalence.unitIso Functor.EssImageSubcategory ObjectProperty.FullSubcategory.category Functor.essImage equivEssImageOfReflective Iso.symm Functor Functor.category Functor.comp reflector Functor.id asIso Adjunction.counit reflectorAdjunction	—	—
instIsIsoAppUnitReflectorAdjunctionObjEssImage 📖	mathematical	—	IsIso Functor.obj Functor.id ObjectProperty.FullSubcategory.obj Functor.essImage Functor.comp reflector NatTrans.app Adjunction.unit reflectorAdjunction	—	Functor.essImage.unit_isIso ObjectProperty.FullSubcategory.property
instIsLeftAdjointOfCoreflective 📖	mathematical	—	Functor.IsLeftAdjoint	—	—
instIsLeftAdjointReflector 📖	mathematical	—	Functor.IsLeftAdjoint reflector	—	—
instIsRightAdjointCoreflector 📖	mathematical	—	Functor.IsRightAdjoint coreflector	—	—
instIsRightAdjointOfReflective 📖	mathematical	—	Functor.IsRightAdjoint	—	—
mem_essImage_of_counit_isSplitEpi 📖	mathematical	—	Functor.essImage	—	mono_of_mono NatTrans.naturality mono_comp IsSplitMono.mono instIsSplitMonoMap section_isSplitMono mono_of_strongMono strongMono_of_isIso Functor.essImage.counit_isIso Functor.obj_mem_essImage Adjunction.mem_essImage_of_counit_isIso isIso_of_mono_of_isSplitEpi
mem_essImage_of_unit_isSplitMono 📖	mathematical	—	Functor.essImage	—	epi_of_epi NatTrans.naturality epi_comp epi_of_strongEpi strongEpi_of_isIso Functor.essImage.unit_isIso Functor.obj_mem_essImage IsSplitEpi.epi instIsSplitEpiMap retraction_isSplitEpi Adjunction.mem_essImage_of_unit_isIso isIso_of_epi_of_isSplitMono
unitCompPartialBijectiveAux_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj reflector EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitCompPartialBijectiveAux CategoryStruct.comp Functor.id Functor.comp NatTrans.app Adjunction.unit reflectorAdjunction	—	Reflective.toFull Reflective.toFaithful Adjunction.homEquiv_unit Functor.FullyFaithful.map_preimage
unitCompPartialBijective_natural 📖	mathematical	Functor.essImage	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj reflector EquivLike.toFunLike Equiv.instEquivLike unitCompPartialBijective CategoryStruct.comp	—	Equiv.eq_symm_apply unitCompPartialBijective_symm_natural Equiv.symm_apply_apply
unitCompPartialBijective_symm_apply 📖	mathematical	Functor.essImage	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj reflector EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitCompPartialBijective CategoryStruct.comp Functor.id Functor.comp NatTrans.app Adjunction.unit reflectorAdjunction	—	Category.id_comp unitCompPartialBijectiveAux_symm_apply Category.assoc Iso.inv_hom_id Category.comp_id
unitCompPartialBijective_symm_natural 📖	mathematical	Functor.essImage	DFunLike.coe Equiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Functor.obj reflector EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitCompPartialBijective CategoryStruct.comp	—	unitCompPartialBijective_symm_apply Category.assoc
unit_obj_eq_map_unit 📖	mathematical	—	NatTrans.app Functor.id Functor.comp reflector Adjunction.unit reflectorAdjunction Functor.obj Functor.map	—	cancel_mono Functor.map_mono Functor.preservesMonomorphisms_of_isRightAdjoint instIsRightAdjointOfReflective mono_of_strongMono strongMono_of_isIso Adjunction.instIsIsoAppCounitOfFullOfFaithful Reflective.toFull Reflective.toFaithful Functor.map_comp Adjunction.right_triangle_components Adjunction.left_triangle_components Functor.map_id

CategoryTheory.Coreflective

Definitions

Name	Category	Theorems
R 📖	CompOp	—
adj 📖	CompOp	—
comp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFaithful 📖	mathematical	—	CategoryTheory.Functor.Faithful	—	—
toFull 📖	mathematical	—	CategoryTheory.Functor.Full	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
fullyFaithfulOfCoreflective 📖	CompOp	—
fullyFaithfulOfReflective 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essImage_ext_iff 📖	mathematical	—	map CategoryTheory.ObjectProperty.FullSubcategory essImage CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι	—	essImage_ext

CategoryTheory.Functor.essImage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counit_isIso 📖	mathematical	CategoryTheory.Functor.essImage	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.coreflector CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.coreflectorAdjunction	—	CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage CategoryTheory.Coreflective.toFaithful CategoryTheory.Coreflective.toFull
unit_isIso 📖	mathematical	CategoryTheory.Functor.essImage	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.reflector CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit CategoryTheory.reflectorAdjunction	—	CategoryTheory.Adjunction.isIso_unit_app_iff_mem_essImage CategoryTheory.Reflective.toFaithful CategoryTheory.Reflective.toFull

CategoryTheory.Reflective

Definitions

Name	Category	Theorems
L 📖	CompOp	—
adj 📖	CompOp	—
comp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFaithful 📖	mathematical	—	CategoryTheory.Functor.Faithful	—	—
toFull 📖	mathematical	—	CategoryTheory.Functor.Full	—	—

---

← Back to Index