Grothendieck

📁 Source: Mathlib/CategoryTheory/Grothendieck.lean

Statistics

Metric	Count
Definitions base, fiber, base, comp, compAsSmallFunctorEquivalence, compAsSmallFunctorEquivalenceFunctor, compAsSmallFunctorEquivalenceInverse, fiber, forget, functor, functorFrom, grothendieckTypeToCat, grothendieckTypeToCatFunctor, grothendieckTypeToCatInverse, id, instCategory, instInhabitedHom, isoMk, map, mapCompIso, mapIdIso, mapWhiskerLeftIsoConjPreMap, mapWhiskerRightAsSmallFunctor, pre, preEquivalence, preInv, preNatIso, preUnitIso, toTransport, transport, transportIso, ι, ιCompFunctorFrom, ιCompMap, ιNatTrans	35
Theorems base_eqToHom, compAsSmallFunctorEquivalenceFunctor_map_base, compAsSmallFunctorEquivalenceFunctor_map_fiber, compAsSmallFunctorEquivalenceFunctor_obj_base, compAsSmallFunctorEquivalenceFunctor_obj_fiber, compAsSmallFunctorEquivalenceInverse_map_base, compAsSmallFunctorEquivalenceInverse_map_fiber, compAsSmallFunctorEquivalenceInverse_obj_base, compAsSmallFunctorEquivalenceInverse_obj_fiber, compAsSmallFunctorEquivalence_counitIso, compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse, compAsSmallFunctorEquivalence_unitIso, comp_base, comp_fiber, eqToHom_eq, ext, faithful_ι, fiber_eqToHom, forget_map, forget_obj, functorFrom_map, functorFrom_obj, functor_comp_forget, grothendieckTypeToCatFunctor_map_coe, grothendieckTypeToCatFunctor_obj_fst, grothendieckTypeToCatFunctor_obj_snd, grothendieckTypeToCatInverse_map_base, grothendieckTypeToCatInverse_obj_base, grothendieckTypeToCatInverse_obj_fiber_as, grothendieckTypeToCat_counitIso_hom_app_coe, grothendieckTypeToCat_counitIso_inv_app_coe, grothendieckTypeToCat_functor_map_coe, grothendieckTypeToCat_functor_obj_fst, grothendieckTypeToCat_functor_obj_snd, grothendieckTypeToCat_inverse_map_base, grothendieckTypeToCat_inverse_obj_base, grothendieckTypeToCat_inverse_obj_fiber_as, grothendieckTypeToCat_unitIso_hom_app_base, grothendieckTypeToCat_unitIso_hom_app_fiber, grothendieckTypeToCat_unitIso_inv_app_base, grothendieckTypeToCat_unitIso_inv_app_fiber, id_base, id_fiber, isoMk_hom_base, isoMk_hom_fiber, isoMk_inv_base, isoMk_inv_fiber, map_comp_eq, map_id_eq, map_map, map_map_base, map_map_fiber, map_obj, map_obj_base, map_obj_fiber, pre_comp, pre_comp_map, pre_comp_map_assoc, pre_id, pre_map_base, pre_map_fiber, pre_obj_base, pre_obj_fiber, toTransport_base, toTransport_fiber, transportIso_hom_base, transportIso_hom_fiber, transportIso_inv_base, transportIso_inv_fiber, transport_base, transport_fiber, ιCompMap_hom_app_base, ιCompMap_hom_app_fiber, ιCompMap_inv_app_base, ιCompMap_inv_app_fiber, ιNatTrans_app_base, ιNatTrans_app_fiber, ι_map, ι_obj	80
Total	115

CategoryTheory.Grothendieck

Definitions

Name	Category	Theorems
base 📖	CompOp	68 math math: base_eqToHom, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, ιNatTrans_app_fiber, transportIso_hom_base, compAsSmallFunctorEquivalenceFunctor_map_fiber, grothendieckTypeToCatFunctor_obj_snd, grothendieckTypeToCat_unitIso_hom_app_fiber, isoMk_inv_base, comp_base, isoMk_inv_fiber, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, grothendieckTypeToCat_unitIso_inv_app_fiber, id_fiber, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right, comp_fiber, map_map, grothendieckTypeToCat_unitIso_inv_app_base, grothendieckTypeToCat_functor_obj_fst, grothendieckTypeToCat_unitIso_hom_app_base, fiber_eqToHom, eqToHom_eq, CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left, compAsSmallFunctorEquivalenceFunctor_obj_fiber, grothendieckTypeToCat_inverse_obj_base, grothendieckTypeToCatFunctor_map_coe, compAsSmallFunctorEquivalenceInverse_obj_fiber, pre_map_fiber, forget_obj, id_base, toTransport_fiber, pre_obj_base, CategoryTheory.CostructuredArrow.grothendieckProj_map, grothendieckTypeToCatFunctor_obj_fst, CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app, isoMk_hom_base, map_obj_fiber, compAsSmallFunctorEquivalenceFunctor_obj_base, transportIso_inv_base, compAsSmallFunctorEquivalenceFunctor_map_base, transport_base, functorFrom_obj, transportIso_inv_fiber, map_obj, compAsSmallFunctorEquivalenceInverse_obj_base, CategoryTheory.CostructuredArrow.grothendieckProj_obj, map_obj_base, CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv, compAsSmallFunctorEquivalenceInverse_map_fiber, functorFrom_map, transport_fiber, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app, map_map_fiber, map_map_base, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, compAsSmallFunctorEquivalenceInverse_map_base, grothendieckTypeToCatInverse_obj_base, congr, grothendieckTypeToCat_functor_map_coe, isoMk_hom_fiber, grothendieckTypeToCat_functor_obj_snd, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom, transportIso_hom_fiber, pre_map_base, ι_map
comp 📖	CompOp	—
compAsSmallFunctorEquivalence 📖	CompOp	4 math math: compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse, compAsSmallFunctorEquivalence_unitIso, compAsSmallFunctorEquivalence_counitIso
compAsSmallFunctorEquivalenceFunctor 📖	CompOp	6 math math: compAsSmallFunctorEquivalenceFunctor_map_fiber, compAsSmallFunctorEquivalenceFunctor_obj_fiber, compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalenceFunctor_obj_base, compAsSmallFunctorEquivalenceFunctor_map_base, compAsSmallFunctorEquivalence_counitIso
compAsSmallFunctorEquivalenceInverse 📖	CompOp	6 math math: compAsSmallFunctorEquivalenceInverse_obj_fiber, compAsSmallFunctorEquivalence_inverse, compAsSmallFunctorEquivalenceInverse_obj_base, compAsSmallFunctorEquivalenceInverse_map_fiber, compAsSmallFunctorEquivalenceInverse_map_base, compAsSmallFunctorEquivalence_counitIso
fiber 📖	CompOp	49 math math: CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, ιNatTrans_app_fiber, compAsSmallFunctorEquivalenceFunctor_map_fiber, grothendieckTypeToCatFunctor_obj_snd, isoMk_inv_fiber, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber, id_fiber, comp_fiber, map_map, fiber_eqToHom, eqToHom_eq, CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv_assoc, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left, compAsSmallFunctorEquivalenceFunctor_obj_fiber, grothendieckTypeToCatFunctor_map_coe, compAsSmallFunctorEquivalenceInverse_obj_fiber, pre_map_fiber, toTransport_fiber, CategoryTheory.CostructuredArrow.grothendieckProj_map, CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app, map_obj_fiber, compAsSmallFunctorEquivalenceFunctor_map_base, functorFrom_obj, transportIso_inv_fiber, map_obj, CategoryTheory.CostructuredArrow.grothendieckProj_obj, CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv, compAsSmallFunctorEquivalenceInverse_map_fiber, grothendieckTypeToCat_inverse_obj_fiber_as, functorFrom_map, transport_fiber, CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit_ι_app, map_map_fiber, map_map_base, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, compAsSmallFunctorEquivalenceInverse_map_base, pre_obj_fiber, congr, grothendieckTypeToCat_functor_map_coe, isoMk_hom_fiber, grothendieckTypeToCat_functor_obj_snd, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, grothendieckTypeToCatInverse_obj_fiber_as, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom, transportIso_hom_fiber, pre_map_base, ι_map
forget 📖	CompOp	4 math math: functor_comp_forget, forget_obj, CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit_app, forget_map
functor 📖	CompOp	—
functorFrom 📖	CompOp	2 math math: functorFrom_obj, functorFrom_map
grothendieckTypeToCat 📖	CompOp	12 math math: grothendieckTypeToCat_inverse_map_base, grothendieckTypeToCat_counitIso_inv_app_coe, grothendieckTypeToCat_unitIso_hom_app_fiber, grothendieckTypeToCat_unitIso_inv_app_fiber, grothendieckTypeToCat_unitIso_inv_app_base, grothendieckTypeToCat_functor_obj_fst, grothendieckTypeToCat_unitIso_hom_app_base, grothendieckTypeToCat_inverse_obj_base, grothendieckTypeToCat_counitIso_hom_app_coe, grothendieckTypeToCat_inverse_obj_fiber_as, grothendieckTypeToCat_functor_map_coe, grothendieckTypeToCat_functor_obj_snd
grothendieckTypeToCatFunctor 📖	CompOp	9 math math: grothendieckTypeToCat_counitIso_inv_app_coe, grothendieckTypeToCatFunctor_obj_snd, grothendieckTypeToCat_unitIso_hom_app_fiber, grothendieckTypeToCat_unitIso_inv_app_fiber, grothendieckTypeToCat_unitIso_inv_app_base, grothendieckTypeToCat_unitIso_hom_app_base, grothendieckTypeToCatFunctor_map_coe, grothendieckTypeToCat_counitIso_hom_app_coe, grothendieckTypeToCatFunctor_obj_fst
grothendieckTypeToCatInverse 📖	CompOp	9 math math: grothendieckTypeToCat_counitIso_inv_app_coe, grothendieckTypeToCat_unitIso_hom_app_fiber, grothendieckTypeToCat_unitIso_inv_app_fiber, grothendieckTypeToCat_unitIso_inv_app_base, grothendieckTypeToCat_unitIso_hom_app_base, grothendieckTypeToCat_counitIso_hom_app_coe, grothendieckTypeToCatInverse_obj_base, grothendieckTypeToCatInverse_map_base, grothendieckTypeToCatInverse_obj_fiber_as
id 📖	CompOp	—
instCategory 📖	CompOp	118 math math: base_eqToHom, ιCompMap_hom_app_fiber, CategoryTheory.Functor.instHasColimitGrothendieckFunctorCompGrothendieckProj, map_comp_eq, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, pre_comp_map_assoc, ιNatTrans_app_fiber, grothendieckTypeToCat_inverse_map_base, grothendieckTypeToCat_counitIso_inv_app_coe, transportIso_hom_base, compAsSmallFunctorEquivalenceFunctor_map_fiber, grothendieckTypeToCatFunctor_obj_snd, functor_comp_forget, grothendieckTypeToCat_unitIso_hom_app_fiber, isoMk_inv_base, comp_base, isoMk_inv_fiber, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_functor, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv_assoc, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_fiber, grothendieckTypeToCat_unitIso_inv_app_fiber, CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app, id_fiber, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom, CategoryTheory.Limits.fiberwiseColim_obj, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_right, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base, ιNatTrans_app_base, comp_fiber, map_map, grothendieckTypeToCat_unitIso_inv_app_base, ιCompMap_inv_app_fiber, grothendieckTypeToCat_functor_obj_fst, grothendieckTypeToCat_unitIso_hom_app_base, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, fiber_eqToHom, CategoryTheory.Limits.preservesLimitsOfShape_colim_grothendieck, eqToHom_eq, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_left, compAsSmallFunctorEquivalenceFunctor_obj_fiber, grothendieckTypeToCat_inverse_obj_base, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_hom_assoc, grothendieckTypeToCatFunctor_map_coe, compAsSmallFunctorEquivalenceInverse_obj_fiber, pre_map_fiber, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, map_id_eq, forget_obj, CategoryTheory.instIsFilteredOrEmptyGrothendieckOfαCategoryObjCat, grothendieckTypeToCat_counitIso_hom_app_coe, compAsSmallFunctorEquivalence_functor, id_base, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_unitIso, CategoryTheory.Limits.fiberwiseColim_map_app, CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app, pre_obj_base, CategoryTheory.CostructuredArrow.grothendieckProj_map, grothendieckTypeToCatFunctor_obj_fst, compAsSmallFunctorEquivalence_inverse, pre_comp_map, isoMk_hom_base, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_inverse, map_obj_fiber, final_map, compAsSmallFunctorEquivalenceFunctor_obj_base, transportIso_inv_base, compAsSmallFunctorEquivalenceFunctor_map_base, ιCompMap_inv_app_base, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app, pre_comp, functorFrom_obj, transportIso_inv_fiber, map_obj, compAsSmallFunctorEquivalenceInverse_obj_base, CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorEquivalence_counitIso, CategoryTheory.CostructuredArrow.grothendieckProj_obj, map_obj_base, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, final_pre, compAsSmallFunctorEquivalenceInverse_map_fiber, compAsSmallFunctorEquivalence_unitIso, grothendieckTypeToCat_inverse_obj_fiber_as, CategoryTheory.Limits.fiberwiseColimCompColimIso_inv_app, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app, functorFrom_map, CategoryTheory.Limits.hasColimitsOfShape_grothendieck, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, map_map_fiber, map_map_base, ι_obj, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, ιCompMap_hom_app_base, compAsSmallFunctorEquivalenceInverse_map_base, pre_obj_fiber, grothendieckTypeToCatInverse_obj_base, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app, pre_id, grothendieckTypeToCatInverse_map_base, grothendieckTypeToCat_functor_map_coe, CategoryTheory.instIsFilteredGrothendieckOfαCategoryObjCat, isoMk_hom_fiber, grothendieckTypeToCat_functor_obj_snd, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_obj_base, compAsSmallFunctorEquivalence_counitIso, CategoryTheory.Functor.ι_colimitIsoColimitGrothendieck_inv, grothendieckTypeToCatInverse_obj_fiber_as, forget_map, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_obj_hom, transportIso_hom_fiber, pre_map_base, ι_map, faithful_ι
instInhabitedHom 📖	CompOp	—
isoMk 📖	CompOp	4 math math: isoMk_inv_base, isoMk_inv_fiber, isoMk_hom_base, isoMk_hom_fiber
map 📖	CompOp	16 math math: ιCompMap_hom_app_fiber, map_comp_eq, pre_comp_map_assoc, functor_comp_forget, map_map, ιCompMap_inv_app_fiber, map_id_eq, pre_comp_map, map_obj_fiber, final_map, ιCompMap_inv_app_base, map_obj, map_obj_base, map_map_fiber, map_map_base, ιCompMap_hom_app_base
mapCompIso 📖	CompOp	—
mapIdIso 📖	CompOp	—
mapWhiskerLeftIsoConjPreMap 📖	CompOp	—
mapWhiskerRightAsSmallFunctor 📖	CompOp	—
pre 📖	CompOp	9 math math: pre_comp_map_assoc, pre_map_fiber, pre_obj_base, pre_comp_map, pre_comp, final_pre, pre_obj_fiber, pre_id, pre_map_base
preEquivalence 📖	CompOp	—
preInv 📖	CompOp	—
preNatIso 📖	CompOp	—
preUnitIso 📖	CompOp	—
toTransport 📖	CompOp	2 math math: toTransport_fiber, toTransport_base
transport 📖	CompOp	8 math math: transportIso_hom_base, toTransport_fiber, transportIso_inv_base, transport_base, transportIso_inv_fiber, toTransport_base, transport_fiber, transportIso_hom_fiber
transportIso 📖	CompOp	4 math math: transportIso_hom_base, transportIso_inv_base, transportIso_inv_fiber, transportIso_hom_fiber
ι 📖	CompOp	23 math math: ιCompMap_hom_app_fiber, ιNatTrans_app_fiber, CategoryTheory.Limits.fiberwiseColimitLimitIso_hom_app, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_inv_app, CategoryTheory.Functor.hasColimit_map_comp_ι_comp_grothendieckProj, ιNatTrans_app_base, ιCompMap_inv_app_fiber, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_inv_app, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app, CategoryTheory.Limits.fiberwiseColim_map_app, CategoryTheory.Limits.fiberwiseColimitLimitIso_inv_app, ιCompMap_inv_app_base, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_hom_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app, CategoryTheory.Limits.fiberwiseColimCompEvaluationIso_inv_app, CategoryTheory.CostructuredArrow.ιCompGrothendieckPrecompFunctorToCommaCompFst_hom_app, ι_obj, ιCompMap_hom_app_base, CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app, ι_map, faithful_ι
ιCompFunctorFrom 📖	CompOp	—
ιCompMap 📖	CompOp	4 math math: ιCompMap_hom_app_fiber, ιCompMap_inv_app_fiber, ιCompMap_inv_app_base, ιCompMap_hom_app_base
ιNatTrans 📖	CompOp	3 math math: CategoryTheory.Limits.fiberwiseColimit_map, ιNatTrans_app_fiber, ιNatTrans_app_base

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_eqToHom 📖	mathematical	—	Hom.base CategoryTheory.eqToHom CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory base	—	—
compAsSmallFunctorEquivalenceFunctor_map_base 📖	mathematical	—	Hom.base base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor CategoryTheory.Functor.obj CategoryTheory.AsSmall CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.down fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceFunctor	—	—
compAsSmallFunctorEquivalenceFunctor_map_fiber 📖	mathematical	—	Hom.fiber base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor CategoryTheory.Functor.obj CategoryTheory.AsSmall CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.down fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceFunctor	—	—
compAsSmallFunctorEquivalenceFunctor_obj_base 📖	mathematical	—	base CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalenceFunctor	—	—
compAsSmallFunctorEquivalenceFunctor_obj_fiber 📖	mathematical	—	fiber CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalenceFunctor CategoryTheory.AsSmall CategoryTheory.Bundled.α CategoryTheory.Category base CategoryTheory.Cat.str CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.down	—	—
compAsSmallFunctorEquivalenceInverse_map_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.up fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceInverse	—	—
compAsSmallFunctorEquivalenceInverse_map_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.up fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceInverse CategoryTheory.Cat.Hom.toFunctor Hom.base CategoryTheory.AsSmall.down	—	—
compAsSmallFunctorEquivalenceInverse_obj_base 📖	mathematical	—	base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceInverse	—	—
compAsSmallFunctorEquivalenceInverse_obj_fiber 📖	mathematical	—	fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory compAsSmallFunctorEquivalenceInverse CategoryTheory.Bundled.α CategoryTheory.Category base CategoryTheory.Cat.str CategoryTheory.AsSmall CategoryTheory.instSmallCategoryAsSmall CategoryTheory.AsSmall.up	—	—
compAsSmallFunctorEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category compAsSmallFunctorEquivalenceInverse compAsSmallFunctorEquivalenceFunctor	—	—
compAsSmallFunctorEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalence compAsSmallFunctorEquivalenceFunctor	—	—
compAsSmallFunctorEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalence compAsSmallFunctorEquivalenceInverse	—	—
compAsSmallFunctorEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.asSmallFunctor instCategory compAsSmallFunctorEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
comp_base 📖	mathematical	—	Hom.base CategoryTheory.CategoryStruct.comp CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory base	—	—
comp_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.CategoryStruct.comp CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map Hom.base fiber CategoryTheory.eqToHom	—	—
eqToHom_eq 📖	mathematical	—	CategoryTheory.eqToHom CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory base CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber	—	—
ext 📖	—	Hom.base CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber CategoryTheory.eqToHom Hom.fiber	—	—	CategoryTheory.Category.id_comp
faithful_ι 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory ι	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.instIsIsoEqToHom
fiber_eqToHom 📖	mathematical	—	Hom.fiber CategoryTheory.eqToHom CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map Hom.base fiber	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory forget Hom.base	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory forget base	—	—
functorFrom_map 📖	mathematical	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerLeft	CategoryTheory.Grothendieck instCategory functorFrom base fiber Hom.base CategoryTheory.NatTrans.app Hom.fiber	—	—
functorFrom_obj 📖	mathematical	CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.eqToHom CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.whiskerLeft	CategoryTheory.Grothendieck instCategory functorFrom base fiber	—	—
functor_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Grothendieck instCategory map forget	—	—
grothendieckTypeToCatFunctor_map_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Discrete.as fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor Hom.base	—	—
grothendieckTypeToCatFunctor_obj_fst 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor base	—	—
grothendieckTypeToCatFunctor_obj_snd 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor CategoryTheory.Discrete.as base fiber	—	—
grothendieckTypeToCatInverse_map_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory grothendieckTypeToCatInverse Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
grothendieckTypeToCatInverse_obj_base 📖	mathematical	—	base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory grothendieckTypeToCatInverse	—	—
grothendieckTypeToCatInverse_obj_fiber_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory grothendieckTypeToCatInverse	—	—
grothendieckTypeToCat_counitIso_hom_app_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory grothendieckTypeToCatInverse grothendieckTypeToCatFunctor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso grothendieckTypeToCat CategoryTheory.CategoryStruct.id	—	—
grothendieckTypeToCat_counitIso_inv_app_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory grothendieckTypeToCatInverse grothendieckTypeToCatFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso grothendieckTypeToCat CategoryTheory.CategoryStruct.id	—	—
grothendieckTypeToCat_functor_map_coe 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.types base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Discrete.as fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.functor grothendieckTypeToCat Hom.base	—	—
grothendieckTypeToCat_functor_obj_fst 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.functor grothendieckTypeToCat base	—	—
grothendieckTypeToCat_functor_obj_snd 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Equivalence.functor grothendieckTypeToCat CategoryTheory.Discrete.as base fiber	—	—
grothendieckTypeToCat_inverse_map_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory CategoryTheory.Equivalence.inverse grothendieckTypeToCat Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
grothendieckTypeToCat_inverse_obj_base 📖	mathematical	—	base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory CategoryTheory.Equivalence.inverse grothendieckTypeToCat	—	—
grothendieckTypeToCat_inverse_obj_fiber_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Functor.obj CategoryTheory.types fiber CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements CategoryTheory.Grothendieck instCategory CategoryTheory.Equivalence.inverse grothendieckTypeToCat	—	—
grothendieckTypeToCat_unitIso_hom_app_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.id CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor grothendieckTypeToCatInverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso grothendieckTypeToCat CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct base	—	—
grothendieckTypeToCat_unitIso_hom_app_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.id CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor grothendieckTypeToCatInverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso grothendieckTypeToCat CategoryTheory.eqToHom CategoryTheory.Discrete base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.discreteCategory CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Discrete.as	—	—
grothendieckTypeToCat_unitIso_inv_app_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor grothendieckTypeToCatInverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso grothendieckTypeToCat CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct base	—	—
grothendieckTypeToCat_unitIso_inv_app_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.typeToCat CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.Elements CategoryTheory.categoryOfElements grothendieckTypeToCatFunctor grothendieckTypeToCatInverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso grothendieckTypeToCat CategoryTheory.eqToHom CategoryTheory.Discrete base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.of CategoryTheory.discreteCategory CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Discrete.as	—	—
id_base 📖	mathematical	—	Hom.base CategoryTheory.CategoryStruct.id CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory base	—	—
id_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.CategoryStruct.id CategoryTheory.Grothendieck CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.eqToHom CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map Hom.base fiber	—	—
isoMk_hom_base 📖	mathematical	—	Hom.base CategoryTheory.Iso.hom CategoryTheory.Grothendieck instCategory isoMk base	—	—
isoMk_hom_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Iso.hom CategoryTheory.Grothendieck instCategory isoMk CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber	—	—
isoMk_inv_base 📖	mathematical	—	Hom.base CategoryTheory.Iso.inv CategoryTheory.Grothendieck instCategory isoMk base	—	—
isoMk_inv_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Iso.inv CategoryTheory.Grothendieck instCategory isoMk CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber CategoryTheory.Iso.hom CategoryTheory.eqToHom	—	—
map_comp_eq 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Grothendieck instCategory	—	CategoryTheory.Functor.ext CategoryTheory.Functor.congr_obj CategoryTheory.NatTrans.naturality map_map CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans CategoryTheory.eqToHom_app CategoryTheory.Functor.map_comp CategoryTheory.eqToHom_map CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_id_eq 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Grothendieck instCategory	—	CategoryTheory.Functor.ext CategoryTheory.NatTrans.naturality map_map CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
map_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory map CategoryTheory.Functor.obj Hom.base CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor fiber CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.eqToHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.NatTrans.naturality Hom.fiber	—	ext CategoryTheory.NatTrans.naturality CategoryTheory.Functor.congr_obj map_map_fiber CategoryTheory.Category.id_comp CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans CategoryTheory.eqToHom_app
map_map_base 📖	mathematical	—	Hom.base base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory map	—	—
map_map_fiber 📖	mathematical	—	Hom.fiber base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Hom.base CategoryTheory.eqToHom CategoryTheory.Functor.congr_obj CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Cat.Hom	—	CategoryTheory.Functor.congr_obj CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans CategoryTheory.eqToHom_app
map_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory map base CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app fiber	—	—
map_obj_base 📖	mathematical	—	base CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory map	—	—
map_obj_fiber 📖	mathematical	—	fiber CategoryTheory.Functor.obj CategoryTheory.Grothendieck instCategory map CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app	—	—
pre_comp 📖	mathematical	—	pre CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Cat CategoryTheory.Cat.category instCategory	—	—
pre_comp_map 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Cat CategoryTheory.Cat.category instCategory pre map CategoryTheory.Functor.whiskerLeft	—	—
pre_comp_map_assoc 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Cat CategoryTheory.Cat.category instCategory pre map CategoryTheory.Functor.whiskerLeft	—	—
pre_id 📖	mathematical	—	pre CategoryTheory.Functor.id CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category instCategory	—	—
pre_map_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.obj base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory pre	—	—
pre_map_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.obj base CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category fiber CategoryTheory.Functor.map CategoryTheory.Grothendieck instCategory pre	—	—
pre_obj_base 📖	mathematical	—	base CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category instCategory pre	—	—
pre_obj_fiber 📖	mathematical	—	fiber CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category instCategory pre	—	—
toTransport_base 📖	mathematical	—	Hom.base transport toTransport	—	—
toTransport_fiber 📖	mathematical	—	Hom.fiber transport toTransport CategoryTheory.CategoryStruct.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber	—	—
transportIso_hom_base 📖	mathematical	—	Hom.base transport CategoryTheory.Iso.hom base CategoryTheory.Grothendieck instCategory transportIso CategoryTheory.Iso.inv	—	—
transportIso_hom_fiber 📖	mathematical	—	Hom.fiber transport CategoryTheory.Iso.hom base CategoryTheory.Grothendieck instCategory transportIso CategoryTheory.eqToHom CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Iso.inv fiber	—	CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
transportIso_inv_base 📖	mathematical	—	Hom.base transport CategoryTheory.Iso.hom base CategoryTheory.Iso.inv CategoryTheory.Grothendieck instCategory transportIso	—	—
transportIso_inv_fiber 📖	mathematical	—	Hom.fiber transport CategoryTheory.Iso.hom base CategoryTheory.Iso.inv CategoryTheory.Grothendieck instCategory transportIso CategoryTheory.CategoryStruct.id CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Category.toCategoryStruct CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map fiber	—	—
transport_base 📖	mathematical	—	base transport	—	—
transport_fiber 📖	mathematical	—	fiber transport CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category base CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map	—	—
ιCompMap_hom_app_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.comp ι map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category ιCompMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ιCompMap_hom_app_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.comp ι map CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category ιCompMap CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id	—	—
ιCompMap_inv_app_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app ι map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ιCompMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ιCompMap_inv_app_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.NatTrans.app ι map CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category ιCompMap CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id	—	—
ιNatTrans_app_base 📖	mathematical	—	Hom.base CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory ι CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app ιNatTrans	—	—
ιNatTrans_app_fiber 📖	mathematical	—	Hom.fiber CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory ι CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.NatTrans.app ιNatTrans CategoryTheory.CategoryStruct.id base CategoryTheory.Category.toCategoryStruct fiber	—	—
ι_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory ι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct base CategoryTheory.CategoryStruct.comp CategoryTheory.Cat.Hom.toFunctor fiber CategoryTheory.eqToHom	—	—
ι_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck instCategory ι	—	—

CategoryTheory.Grothendieck.Hom

Definitions

Name	Category	Theorems
base 📖	CompOp	34 math math: CategoryTheory.Grothendieck.base_eqToHom, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, CategoryTheory.Grothendieck.grothendieckTypeToCat_inverse_map_base, CategoryTheory.Grothendieck.transportIso_hom_base, CategoryTheory.Grothendieck.isoMk_inv_base, CategoryTheory.Grothendieck.comp_base, CategoryTheory.Grothendieck.id_fiber, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_base, CategoryTheory.Grothendieck.ιNatTrans_app_base, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.map_map, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_base, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_base, CategoryTheory.Grothendieck.fiber_eqToHom, CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe, CategoryTheory.Grothendieck.id_base, CategoryTheory.CostructuredArrow.grothendieckProj_map, CategoryTheory.Grothendieck.isoMk_hom_base, CategoryTheory.Grothendieck.transportIso_inv_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_base, CategoryTheory.Grothendieck.ιCompMap_inv_app_base, CategoryTheory.Grothendieck.toTransport_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.Grothendieck.functorFrom_map, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.Grothendieck.map_map_base, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_right, CategoryTheory.Grothendieck.ιCompMap_hom_app_base, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base, CategoryTheory.Grothendieck.grothendieckTypeToCatInverse_map_base, CategoryTheory.Grothendieck.congr, CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_map_coe, CategoryTheory.Grothendieck.forget_map, CategoryTheory.Grothendieck.pre_map_base
fiber 📖	CompOp	23 math math: CategoryTheory.Grothendieck.ιCompMap_hom_app_fiber, CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma_map_left, CategoryTheory.Grothendieck.ιNatTrans_app_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_hom_app_fiber, CategoryTheory.Grothendieck.isoMk_inv_fiber, CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor_map_fiber, CategoryTheory.Grothendieck.grothendieckTypeToCat_unitIso_inv_app_fiber, CategoryTheory.Grothendieck.id_fiber, CategoryTheory.Grothendieck.comp_fiber, CategoryTheory.Grothendieck.map_map, CategoryTheory.Grothendieck.ιCompMap_inv_app_fiber, CategoryTheory.Grothendieck.fiber_eqToHom, CategoryTheory.Grothendieck.pre_map_fiber, CategoryTheory.Grothendieck.toTransport_fiber, CategoryTheory.CostructuredArrow.grothendieckProj_map, CategoryTheory.Grothendieck.transportIso_inv_fiber, CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_fiber, CategoryTheory.Grothendieck.functorFrom_map, CategoryTheory.Grothendieck.map_map_fiber, CategoryTheory.Grothendieck.congr, CategoryTheory.Grothendieck.isoMk_hom_fiber, CategoryTheory.Grothendieck.transportIso_hom_fiber

---

← Back to Index