Free

📁 Source: Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

Statistics

Metric	Count
Definitions free, freeAdjunction, freeAdjunctionUnit, freeHomEquiv, freeObj, freeObjDesc	6
Theorems freeAdjunctionUnit_app, freeAdjunction_homEquiv, freeAdjunction_unit_app, freeObjDesc_app, freeObj_map, freeObj_obj, free_hom_ext, free_map_app, free_obj	9
Total	15

PresheafOfModules

Definitions

Name	Category	Theorems
free 📖	CompOp	7 math math: free_map_app, freeYonedaEquiv_symm_app, free_obj, pullbackObjIsDefined_free_yoneda, freeAdjunction_unit_app, freeYonedaEquiv_comp, freeAdjunction_homEquiv
freeAdjunction 📖	CompOp	2 math math: freeAdjunction_unit_app, freeAdjunction_homEquiv
freeAdjunctionUnit 📖	CompOp	2 math math: freeAdjunctionUnit_app, freeAdjunction_unit_app
freeHomEquiv 📖	CompOp	1 math math: freeAdjunction_homEquiv
freeObj 📖	CompOp	6 math math: free_map_app, freeObj_map, freeObj_obj, freeAdjunctionUnit_app, free_obj, freeObjDesc_app
freeObjDesc 📖	CompOp	1 math math: freeObjDesc_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeAdjunctionUnit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory presheaf freeObj CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier freeAdjunctionUnit ModuleCat.freeMk RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory RingCat.ring	—	—
freeAdjunction_homEquiv 📖	mathematical	—	CategoryTheory.Adjunction.homEquiv CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category PresheafOfModules instCategory free CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory toPresheaf CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier freeAdjunction freeHomEquiv	—	CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
freeAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp PresheafOfModules instCategory free Ab AddCommGrpCat.instCategory toPresheaf CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Adjunction.unit freeAdjunction freeAdjunctionUnit	—	—
freeObjDesc_app 📖	mathematical	—	Hom.app freeObj freeObjDesc ModuleCat.freeDesc RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.types obj CategoryTheory.NatTrans.app CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory presheaf CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier	—	—
freeObj_map 📖	mathematical	—	map freeObj ModuleCat.freeDesc RingCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring CategoryTheory.types ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars RingCat.Hom.hom CategoryTheory.Functor.map ModuleCat.free ModuleCat.freeMk	—	—
freeObj_obj 📖	mathematical	—	obj freeObj CategoryTheory.Functor.obj CategoryTheory.types ModuleCat RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.free	—	—
free_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory presheaf freeObj CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Functor.obj PresheafOfModules instCategory toPresheaf freeAdjunctionUnit CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.map	—	—	Equiv.injective
free_map_app 📖	mathematical	—	Hom.app freeObj CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category PresheafOfModules instCategory free ModuleCat RingCat.carrier CategoryTheory.Functor.obj RingCat RingCat.instCategory RingCat.ring ModuleCat.moduleCategory ModuleCat.free CategoryTheory.NatTrans.app	—	—
free_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category PresheafOfModules instCategory free freeObj	—	—

---

← Back to Index