Subobject

📁 Source: Mathlib/CategoryTheory/Subfunctor/Subobject.lean

Statistics

Metric	Count
Definitions equivalenceMonoOver, orderIsoSubobject, equivalenceMonoOver, orderIsoSubobject	4
Theorems range_subobjectMk_ι, subobjectMk_range_arrow, equivalenceMonoOver_counitIso, equivalenceMonoOver_functor_map, equivalenceMonoOver_functor_obj, equivalenceMonoOver_inverse_map, equivalenceMonoOver_inverse_obj, equivalenceMonoOver_unitIso, orderIsoSubobject_apply, orderIsoSubobject_symm_apply, range_subobjectMk_ι, subobjectMk_range_arrow	12
Total	16

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
equivalenceMonoOver 📖	CompOp	6 math math: equivalenceMonoOver_inverse_map, equivalenceMonoOver_functor_map, equivalenceMonoOver_inverse_obj, equivalenceMonoOver_functor_obj, equivalenceMonoOver_unitIso, equivalenceMonoOver_counitIso
orderIsoSubobject 📖	CompOp	2 math math: orderIsoSubobject_apply, orderIsoSubobject_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalenceMonoOver_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Subfunctor CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono equivalenceMonoOver CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp range CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoOver.arrow CategoryTheory.homOfLE toFunctor ι instMonoFunctorTypeι CategoryTheory.MonoOver.homMk homOfLe CategoryTheory.MonoOver.isoMk CategoryTheory.Functor.obj CategoryTheory.Iso.symm CategoryTheory.asIso toRange	—	instMonoFunctorTypeι
equivalenceMonoOver_functor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Subfunctor Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Equivalence.functor equivalenceMonoOver CategoryTheory.MonoOver.homMk toFunctor ι instMonoFunctorTypeι homOfLe	—	instMonoFunctorTypeι
equivalenceMonoOver_functor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Subfunctor Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Equivalence.functor equivalenceMonoOver toFunctor ι instMonoFunctorTypeι	—	—
equivalenceMonoOver_inverse_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Subfunctor Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Equivalence.inverse equivalenceMonoOver CategoryTheory.homOfLE range CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoOver.arrow	—	—
equivalenceMonoOver_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono CategoryTheory.Subfunctor Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.Equivalence.inverse equivalenceMonoOver range CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoOver.arrow	—	—
equivalenceMonoOver_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Subfunctor CategoryTheory.MonoOver CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.isMono equivalenceMonoOver CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toFunctor ι instMonoFunctorTypeι CategoryTheory.MonoOver.homMk homOfLe range CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.MonoOver.arrow CategoryTheory.homOfLE CategoryTheory.eqToIso CategoryTheory.Functor.obj	—	instMonoFunctorTypeι
orderIsoSubobject_apply 📖	mathematical	—	DFunLike.coe RelIso CategoryTheory.Subfunctor CategoryTheory.Subobject CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubfunctor CategoryTheory.instPartialOrderSubobject RelIso.instFunLike orderIsoSubobject toFunctor ι instMonoFunctorTypeι	—	—
orderIsoSubobject_symm_apply 📖	mathematical	—	DFunLike.coe RelIso CategoryTheory.Subobject CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Subfunctor Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.instPartialOrderSubfunctor RelIso.instFunLike RelIso.symm orderIsoSubobject range CategoryTheory.Functor.obj Preorder.smallCategory CategoryTheory.Subobject.underlying CategoryTheory.Subobject.arrow	—	—
range_subobjectMk_ι 📖	mathematical	—	range CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying toFunctor ι instMonoFunctorTypeι CategoryTheory.Subobject.arrow	—	CategoryTheory.MonoOver.isThin CategoryTheory.Iso.to_eq
subobjectMk_range_arrow 📖	mathematical	—	CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category toFunctor range CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subobject.arrow ι instMonoFunctorTypeι	—	CategoryTheory.Iso.to_eq CategoryTheory.MonoOver.isThin

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
equivalenceMonoOver 📖	CompOp	—
orderIsoSubobject 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_subobjectMk_ι 📖	mathematical	—	CategoryTheory.Subfunctor.range CategoryTheory.Functor.obj CategoryTheory.Subobject CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.ι CategoryTheory.Subfunctor.instMonoFunctorTypeι CategoryTheory.Subobject.arrow	—	CategoryTheory.Subfunctor.range_subobjectMk_ι
subobjectMk_range_arrow 📖	mathematical	—	CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Subfunctor.toFunctor CategoryTheory.Subfunctor.range CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Subobject.arrow CategoryTheory.Subfunctor.ι CategoryTheory.Subfunctor.instMonoFunctorTypeι	—	CategoryTheory.Subfunctor.subobjectMk_range_arrow

---

← Back to Index