FreeGroupoidOfCategory

📁 Source: Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean

Statistics

Metric	Count
Definitions functorEquiv, homMk, homRel, liftNatIso, map, mapComp, mapCompLift, mapId, mk, of, ofCompMapIso, strictUniversalPropertyFixedTarget, free, freeForgetAdjunction, instReflectiveCatForgetToCat, instGroupoidFreeGroupoid	16
Theorems eq_mk, functorEquiv_apply, functorEquiv_symm_apply, instIsLocalizationOfTopMorphismProperty, liftNatIso_hom_app, liftNatIso_inv_app, lift_comp, lift_id_comp_of, lift_map_homMk, lift_obj_mk, lift_spec, lift_unique, mapCompLift_hom_app, mapCompLift_inv_app, mapComp_hom_app, mapComp_inv_app, mapId_hom_app, mapId_inv_app, map_comp, map_comp_lift, map_id, map_map_homMk, map_obj_mk, of_comp_map, of_obj_bijective, freeForgetAdjunction_counit_app, freeForgetAdjunction_homEquiv_apply, freeForgetAdjunction_homEquiv_symm_apply, freeForgetAdjunction_unit_app, free_map, free_obj, instNonemptyFreeGroupoid	32
Total	48

CategoryTheory

Definitions

Name	Category	Theorems
instGroupoidFreeGroupoid 📖	CompOp	25 math math: FreeGroupoid.map_comp_lift, FreeGroupoid.lift_comp, FreeGroupoid.functorEquiv_apply, FreeGroupoid.mapComp_hom_app, FreeGroupoid.mapId_hom_app, FreeGroupoid.lift_map_homMk, FreeGroupoid.liftNatIso_hom_app, FreeGroupoid.mapCompLift_inv_app, FreeGroupoid.lift_obj_mk, FreeGroupoid.map_id, FreeGroupoid.map_map_homMk, Grpd.freeForgetAdjunction_homEquiv_symm_apply, FreeGroupoid.mapComp_inv_app, FreeGroupoid.mapId_inv_app, FreeGroupoid.liftNatIso_inv_app, FreeGroupoid.lift_id_comp_of, Grpd.freeForgetAdjunction_homEquiv_apply, FreeGroupoid.of_obj_bijective, FreeGroupoid.map_obj_mk, FreeGroupoid.functorEquiv_symm_apply, FreeGroupoid.instIsLocalizationOfTopMorphismProperty, FreeGroupoid.of_comp_map, FreeGroupoid.lift_spec, FreeGroupoid.mapCompLift_hom_app, FreeGroupoid.map_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyFreeGroupoid 📖	mathematical	—	FreeGroupoid	—	—

CategoryTheory.FreeGroupoid

Definitions

Name	Category	Theorems
functorEquiv 📖	CompOp	2 math math: functorEquiv_apply, functorEquiv_symm_apply
homMk 📖	CompOp	2 math math: lift_map_homMk, map_map_homMk
homRel 📖	CompData	1 math math: eq_mk
liftNatIso 📖	CompOp	2 math math: liftNatIso_hom_app, liftNatIso_inv_app
map 📖	CompOp	14 math math: map_comp_lift, CategoryTheory.Grpd.free_map, mapComp_hom_app, mapId_hom_app, mapCompLift_inv_app, map_id, map_map_homMk, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply, mapComp_inv_app, mapId_inv_app, map_obj_mk, of_comp_map, mapCompLift_hom_app, map_comp
mapComp 📖	CompOp	2 math math: mapComp_hom_app, mapComp_inv_app
mapCompLift 📖	CompOp	2 math math: mapCompLift_inv_app, mapCompLift_hom_app
mapId 📖	CompOp	2 math math: mapId_hom_app, mapId_inv_app
mk 📖	CompOp	—
of 📖	CompOp	10 math math: functorEquiv_apply, liftNatIso_hom_app, liftNatIso_inv_app, lift_id_comp_of, CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply, of_obj_bijective, instIsLocalizationOfTopMorphismProperty, of_comp_map, lift_spec, CategoryTheory.Grpd.freeForgetAdjunction_unit_app
ofCompMapIso 📖	CompOp	—
strictUniversalPropertyFixedTarget 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_mk 📖	mathematical	—	CategoryTheory.Quotient.as CategoryTheory.Paths Quiver.Symmetrify CategoryTheory.Paths.categoryPaths Quiver.symmetrifyQuiver CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Quiver.FreeGroupoid.redStep Quiver.FreeGroupoid Quiver.FreeGroupoid.instCategory homRel	—	—
functorEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid EquivLike.toFunLike Equiv.instEquivLike functorEquiv CategoryTheory.Functor.comp of	—	—
functorEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor CategoryTheory.Groupoid.toCategory CategoryTheory.FreeGroupoid CategoryTheory.instGroupoidFreeGroupoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm functorEquiv lift	—	—
instIsLocalizationOfTopMorphismProperty 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid of Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.Functor.IsLocalization.mk'
liftNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso CategoryTheory.Functor.comp of	—	instIsLocalizationOfTopMorphismProperty CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
liftNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category liftNatIso CategoryTheory.Functor.comp of	—	instIsLocalizationOfTopMorphismProperty CategoryTheory.Localization.liftNatTrans_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
lift_comp 📖	mathematical	—	lift CategoryTheory.Functor.comp CategoryTheory.Groupoid.toCategory CategoryTheory.FreeGroupoid CategoryTheory.instGroupoidFreeGroupoid	—	lift_unique CategoryTheory.Functor.assoc lift_spec
lift_id_comp_of 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid lift CategoryTheory.Functor.id of	—	lift_unique CategoryTheory.Functor.assoc lift_spec CategoryTheory.Functor.id_comp CategoryTheory.Functor.comp_id
lift_map_homMk 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid lift homMk	—	CategoryTheory.Functor.congr_obj lift_spec CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.congr_hom
lift_obj_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid lift	—	—
lift_spec 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid of lift	—	CategoryTheory.Functor.toPrefunctor_injective CategoryTheory.Quotient.lift_spec Quiver.FreeGroupoid.lift_spec
lift_unique 📖	mathematical	CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid of	lift	—	CategoryTheory.Quotient.lift_unique Quiver.FreeGroupoid.lift_unique
mapCompLift_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.Functor.comp map lift CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapCompLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	liftNatIso_hom_app
mapCompLift_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid lift CategoryTheory.Functor.comp map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapCompLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	liftNatIso_inv_app
mapComp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid map CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	liftNatIso_hom_app
mapComp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.Functor.comp map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	liftNatIso_inv_app
mapId_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid map CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category mapId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	liftNatIso_hom_app
mapId_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.Functor.id map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category mapId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	liftNatIso_inv_app
map_comp 📖	mathematical	—	map CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid	—	lift_unique
map_comp_lift 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid map lift	—	lift_unique CategoryTheory.Functor.assoc of_comp_map lift_spec
map_id 📖	mathematical	—	map CategoryTheory.Functor.id CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid	—	lift_unique
map_map_homMk 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid map homMk CategoryTheory.Functor.obj	—	—
map_obj_mk 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid map	—	—
of_comp_map 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid of map	—	—
of_obj_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.FreeGroupoid CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid of	—	—

CategoryTheory.Grpd

Definitions

Name	Category	Theorems
free 📖	CompOp	6 math math: free_obj, free_map, freeForgetAdjunction_homEquiv_symm_apply, freeForgetAdjunction_counit_app, freeForgetAdjunction_homEquiv_apply, freeForgetAdjunction_unit_app
freeForgetAdjunction 📖	CompOp	4 math math: freeForgetAdjunction_homEquiv_symm_apply, freeForgetAdjunction_counit_app, freeForgetAdjunction_homEquiv_apply, freeForgetAdjunction_unit_app
instReflectiveCatForgetToCat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeForgetAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Grpd category CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category forgetToCat free CategoryTheory.Functor.id CategoryTheory.Adjunction.counit freeForgetAdjunction of CategoryTheory.FreeGroupoid.lift CategoryTheory.Groupoid.toCategory	—	—
freeForgetAdjunction_homEquiv_apply 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Cat.of CategoryTheory.Functor.obj CategoryTheory.Grpd category CategoryTheory.Cat CategoryTheory.Cat.category forgetToCat of DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct free EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv freeForgetAdjunction CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.Groupoid.toCategory CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.FreeGroupoid.of	—	—
freeForgetAdjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Cat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.category CategoryTheory.Cat.of CategoryTheory.Functor.obj CategoryTheory.Grpd category forgetToCat of free EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv freeForgetAdjunction CategoryTheory.Functor.toCatHom CategoryTheory.Groupoid.toCategory CategoryTheory.Functor.comp CategoryTheory.FreeGroupoid CategoryTheory.instGroupoidFreeGroupoid CategoryTheory.FreeGroupoid.map CategoryTheory.FreeGroupoid.lift CategoryTheory.Functor.id	—	—
freeForgetAdjunction_unit_app 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.id CategoryTheory.Cat.of CategoryTheory.Functor.comp CategoryTheory.Grpd category free forgetToCat CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit freeForgetAdjunction CategoryTheory.FreeGroupoid.of	—	—
free_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grpd category free CategoryTheory.FreeGroupoid.map CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor	—	—
free_obj 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grpd category free CategoryTheory.FreeGroupoid CategoryTheory.Category CategoryTheory.Cat.str	—	—

---

← Back to Index