DescentData

📁 Source: Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

Statistics

Metric	Count
Definitions DescentData, hom, hom, instCategory, iso, isoMk, obj, ofObj, pullFunctor, pullFunctorCompIso, pullFunctorEquivalence, pullFunctorIdIso, pullFunctorIso, pullFunctorObj, pullFunctorObjHom, subtypeCompatibleHomEquiv, toDescentDataCompPullFunctorIso, IsPrestackFor, fullyFaithful, IsStackFor, fullyFaithfulToDescentData, toDescentData	22
Theorems comm, comm_assoc, ext, ext_iff, comp_hom, comp_hom_assoc, exists_equivalence_of_sieve_eq, hom_comp, hom_comp_assoc, hom_ext, hom_ext_iff, hom_self, id_hom, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, isEquivalence_toDescentData_iff_of_sieve_eq, isoMk_hom_hom, isoMk_inv_hom, iso_hom, iso_inv, nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, ofObj_hom, ofObj_obj, pullFunctorCompIso_hom_app_hom, pullFunctorCompIso_inv_app_hom, pullFunctorEquivalence_counitIso, pullFunctorEquivalence_functor, pullFunctorEquivalence_inverse, pullFunctorEquivalence_unitIso, pullFunctorIdIso_hom_app_hom, pullFunctorIdIso_inv_app_hom, pullFunctorIso_hom_app_hom, pullFunctorIso_inv_app_hom, pullFunctorObjHom_eq, pullFunctorObjHom_eq_assoc, pullFunctorObj_hom, pullFunctorObj_obj, pullFunctor_map_hom, pullFunctor_obj, pullHom_hom, subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, of_isPrestackFor, isSheafFor', nonempty_fullyFaithful, IsPrestackFor_generate_iff, essSurj, isEquivalence, isPrestackFor, IsStackFor_generate_iff, bijective_toDescentData_map_iff, isPrestackFor, isPrestackFor', isPrestackFor_iff, isPrestackFor_iff_isSheafFor, isPrestackFor_iff_isSheafFor', isPrestackFor_iff_of_sieve_eq, isPrestackFor_ofArrows_iff, isStackFor_iff, isStackFor_iff_of_sieve_eq, isStackFor_ofArrows_iff, toDescentData_map_hom, toDescentData_obj	61
Total	83

CategoryTheory.Pseudofunctor

Definitions

Name	Category	Theorems
DescentData 📖	CompData	36 math math: DescentData.isEquivalence_toDescentData_of_sieve_le, DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, DescentData.pullFunctorCompIso_inv_app_hom, isEquivalence_toDescentData, DescentData.pullFunctorIso_inv_app_hom, DescentData.pullFunctor_map_hom, DescentData.isoMk_inv_hom, DescentData.comp_hom, isStackFor_ofArrows_iff, DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, DescentData.pullFunctorEquivalence_inverse, isPrestackFor_ofArrows_iff, isStackFor_iff, bijective_toDescentData_map_iff, DescentData.pullFunctorEquivalence_functor, DescentData.pullFunctorIso_hom_app_hom, IsStack.essSurj_of_sieve, toDescentData_obj, isPrestackFor_iff, IsStackFor.isEquivalence, DescentData.full_pullFunctor, toDescentData_map_hom, IsStackFor.essSurj, DescentData.exists_equivalence_of_sieve_eq, DescentData.pullFunctorIdIso_inv_app_hom, DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, DescentData.pullFunctorIdIso_hom_app_hom, DescentData.id_hom, DescentData.pullFunctorCompIso_hom_app_hom, DescentData.isoMk_hom_hom, DescentData.comp_hom_assoc, DescentData.pullFunctorEquivalence_counitIso, DescentData.faithful_pullFunctor, DescentData.pullFunctorEquivalence_unitIso, DescentData.pullFunctor_obj, IsPrestackFor.nonempty_fullyFaithful
IsPrestackFor 📖	CompData	9 math math: isPrestackFor', isPrestackFor_ofArrows_iff, isPrestackFor_iff_isSheafFor, IsStackFor.isPrestackFor, isPrestackFor_iff, IsPrestackFor_generate_iff, isPrestackFor, isPrestackFor_iff_isSheafFor', isPrestackFor_iff_of_sieve_eq
IsStackFor 📖	CompData	6 math math: isStackFor_ofArrows_iff, isStackFor, IsStackFor_generate_iff, isStackFor_iff_of_sieve_eq, isStackFor_iff, isStackFor'
fullyFaithfulToDescentData 📖	CompOp	—
toDescentData 📖	CompOp	17 math math: DescentData.isEquivalence_toDescentData_of_sieve_le, DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, isEquivalence_toDescentData, isStackFor_ofArrows_iff, DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, isPrestackFor_ofArrows_iff, isStackFor_iff, bijective_toDescentData_map_iff, IsStack.essSurj_of_sieve, toDescentData_obj, isPrestackFor_iff, IsStackFor.isEquivalence, toDescentData_map_hom, IsStackFor.essSurj, DescentData.exists_equivalence_of_sieve_eq, DescentData.isEquivalence_toDescentData_iff_of_sieve_eq, IsPrestackFor.nonempty_fullyFaithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsPrestackFor_generate_iff 📖	mathematical	—	IsPrestackFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate	—	isPrestackFor_iff_of_sieve_eq CategoryTheory.Sieve.generate_sieve
IsStackFor_generate_iff 📖	mathematical	—	IsStackFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.generate	—	isStackFor_iff_of_sieve_eq CategoryTheory.Sieve.generate_sieve
bijective_toDescentData_map_iff 📖	mathematical	—	Function.Bijective Quiver.Hom CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory CategoryTheory.Functor.obj toDescentData CategoryTheory.Functor.map CategoryTheory.Presieve.IsSheafFor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CategoryStruct.id presheafHom CategoryTheory.Presieve.ofArrows CategoryTheory.Over.homMk	—	CategoryTheory.Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible Function.Bijective.of_comp_iff' Equiv.bijective Function.Bijective.of_comp_iff DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv
isPrestackFor 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.generate	IsPrestackFor	—	isPrestackFor_iff CategoryTheory.Sieve.ofArrows_category'
isPrestackFor' 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	IsPrestackFor CategoryTheory.Sieve.arrows	—	isPrestackFor CategoryTheory.Sieve.generate_sieve
isPrestackFor_iff 📖	mathematical	—	IsPrestackFor CategoryTheory.Functor.FullyFaithful CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom DescentData.instCategory toDescentData	—	—
isPrestackFor_iff_isSheafFor 📖	mathematical	—	IsPrestackFor CategoryTheory.Sieve.arrows CategoryTheory.Presieve.IsSheafFor CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct presheafHom DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Sieve.overEquiv	—	isPrestackFor_iff CategoryTheory.Functor.FullyFaithful.nonempty_iff_map_bijective bijective_toDescentData_map_iff le_antisymm CategoryTheory.Over.mk_surjective CategoryTheory.Category.comp_id CategoryTheory.Over.OverMorphism.ext CategoryTheory.Over.w
isPrestackFor_iff_isSheafFor' 📖	mathematical	—	IsPrestackFor CategoryTheory.Sieve.arrows CategoryTheory.Presieve.IsSheafFor CategoryTheory.Over CategoryTheory.instCategoryOver presheafHom DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Sieve.overEquiv	—	isPrestackFor_iff_isSheafFor le_antisymm CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Over.w CategoryTheory.Over.OverMorphism.ext CategoryTheory.Functor.congr_map CategoryTheory.Sieve.downward_closed CategoryTheory.Presieve.isSheafFor_over_map_op_comp_iff CategoryTheory.Presieve.isSheafFor_iff_of_iso
isPrestackFor_iff_of_sieve_eq 📖	mathematical	CategoryTheory.Sieve.generate	IsPrestackFor	—	CategoryTheory.Presieve.exists_eq_ofArrows DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq CategoryTheory.Sieve.ofArrows_category'
isPrestackFor_ofArrows_iff 📖	mathematical	—	IsPrestackFor CategoryTheory.Presieve.ofArrows CategoryTheory.Functor.FullyFaithful CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory toDescentData	—	DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq CategoryTheory.Sieve.ofArrows_category'
isStackFor_iff 📖	mathematical	—	IsStackFor CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom DescentData.instCategory toDescentData	—	—
isStackFor_iff_of_sieve_eq 📖	mathematical	CategoryTheory.Sieve.generate	IsStackFor	—	CategoryTheory.Presieve.exists_eq_ofArrows DescentData.isEquivalence_toDescentData_iff_of_sieve_eq CategoryTheory.Sieve.ofArrows_category'
isStackFor_ofArrows_iff 📖	mathematical	—	IsStackFor CategoryTheory.Presieve.ofArrows CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory toDescentData	—	DescentData.isEquivalence_toDescentData_iff_of_sieve_eq CategoryTheory.Sieve.ofArrows_category'
toDescentData_map_hom 📖	mathematical	—	DescentData.Hom.hom DescentData.ofObj CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory toDescentData CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	—
toDescentData_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct toPrelaxFunctor Opposite.op CategoryTheory.Cat.str DescentData DescentData.instCategory toDescentData DescentData.ofObj	—	—

CategoryTheory.Pseudofunctor.DescentData

Definitions

Name	Category	Theorems
hom 📖	CompOp	15 math math: ofObj_hom, pullFunctorIso_inv_app_hom, iso_hom, iso_inv, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, Hom.comm_assoc, hom_comp_assoc, pullHom_hom, pullFunctorIso_hom_app_hom, pullFunctorObjHom_eq_assoc, pullFunctorObj_hom, pullFunctorObjHom_eq, hom_self, hom_comp, Hom.comm
instCategory 📖	CompOp	36 math math: isEquivalence_toDescentData_of_sieve_le, subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv, pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.isEquivalence_toDescentData, pullFunctorIso_inv_app_hom, pullFunctor_map_hom, isoMk_inv_hom, comp_hom, CategoryTheory.Pseudofunctor.isStackFor_ofArrows_iff, nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq, pullFunctorEquivalence_inverse, CategoryTheory.Pseudofunctor.isPrestackFor_ofArrows_iff, CategoryTheory.Pseudofunctor.isStackFor_iff, CategoryTheory.Pseudofunctor.bijective_toDescentData_map_iff, pullFunctorEquivalence_functor, pullFunctorIso_hom_app_hom, CategoryTheory.Pseudofunctor.IsStack.essSurj_of_sieve, CategoryTheory.Pseudofunctor.toDescentData_obj, CategoryTheory.Pseudofunctor.isPrestackFor_iff, CategoryTheory.Pseudofunctor.IsStackFor.isEquivalence, full_pullFunctor, CategoryTheory.Pseudofunctor.toDescentData_map_hom, CategoryTheory.Pseudofunctor.IsStackFor.essSurj, exists_equivalence_of_sieve_eq, pullFunctorIdIso_inv_app_hom, isEquivalence_toDescentData_iff_of_sieve_eq, pullFunctorIdIso_hom_app_hom, id_hom, pullFunctorCompIso_hom_app_hom, isoMk_hom_hom, comp_hom_assoc, pullFunctorEquivalence_counitIso, faithful_pullFunctor, pullFunctorEquivalence_unitIso, pullFunctor_obj, CategoryTheory.Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful
iso 📖	CompOp	2 math math: iso_hom, iso_inv
isoMk 📖	CompOp	2 math math: isoMk_inv_hom, isoMk_hom_hom
obj 📖	CompOp	23 math math: pullFunctorCompIso_inv_app_hom, pullFunctor_map_hom, isoMk_inv_hom, comp_hom, iso_hom, iso_inv, instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom, Hom.comm_assoc, ofObj_obj, hom_comp_assoc, pullHom_hom, pullFunctorObj_obj, pullFunctorObjHom_eq_assoc, pullFunctorIdIso_inv_app_hom, pullFunctorIdIso_hom_app_hom, id_hom, pullFunctorCompIso_hom_app_hom, isoMk_hom_hom, pullFunctorObjHom_eq, hom_self, comp_hom_assoc, hom_comp, Hom.comm
ofObj 📖	CompOp	4 math math: ofObj_hom, ofObj_obj, CategoryTheory.Pseudofunctor.toDescentData_obj, CategoryTheory.Pseudofunctor.toDescentData_map_hom
pullFunctor 📖	CompOp	14 math math: pullFunctorCompIso_inv_app_hom, pullFunctorIso_inv_app_hom, pullFunctor_map_hom, pullFunctorEquivalence_inverse, pullFunctorEquivalence_functor, pullFunctorIso_hom_app_hom, full_pullFunctor, pullFunctorIdIso_inv_app_hom, pullFunctorIdIso_hom_app_hom, pullFunctorCompIso_hom_app_hom, pullFunctorEquivalence_counitIso, faithful_pullFunctor, pullFunctorEquivalence_unitIso, pullFunctor_obj
pullFunctorCompIso 📖	CompOp	4 math math: pullFunctorCompIso_inv_app_hom, pullFunctorCompIso_hom_app_hom, pullFunctorEquivalence_counitIso, pullFunctorEquivalence_unitIso
pullFunctorEquivalence 📖	CompOp	4 math math: pullFunctorEquivalence_inverse, pullFunctorEquivalence_functor, pullFunctorEquivalence_counitIso, pullFunctorEquivalence_unitIso
pullFunctorIdIso 📖	CompOp	4 math math: pullFunctorIdIso_inv_app_hom, pullFunctorIdIso_hom_app_hom, pullFunctorEquivalence_counitIso, pullFunctorEquivalence_unitIso
pullFunctorIso 📖	CompOp	4 math math: pullFunctorIso_inv_app_hom, pullFunctorIso_hom_app_hom, pullFunctorEquivalence_counitIso, pullFunctorEquivalence_unitIso
pullFunctorObj 📖	CompOp	4 math math: pullFunctor_map_hom, pullFunctorObj_obj, pullFunctorObj_hom, pullFunctor_obj
pullFunctorObjHom 📖	CompOp	3 math math: pullFunctorObjHom_eq_assoc, pullFunctorObj_hom, pullFunctorObjHom_eq
subtypeCompatibleHomEquiv 📖	CompOp	1 math math: subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv
toDescentDataCompPullFunctorIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj Hom.hom CategoryTheory.Pseudofunctor.DescentData instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
exists_equivalence_of_sieve_eq 📖	mathematical	CategoryTheory.Sieve.ofArrows	CategoryTheory.Iso CategoryTheory.Functor CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Pseudofunctor.toDescentData CategoryTheory.Equivalence.functor	—	CategoryTheory.Category.comp_id
hom_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj hom	—	—
hom_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_comp
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_self 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	hom CategoryTheory.CategoryStruct.id CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj	—	—
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj hom	—	CategoryTheory.Iso.isIso_hom
isEquivalence_toDescentData_iff_of_sieve_eq 📖	mathematical	CategoryTheory.Sieve.ofArrows	CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.toDescentData	—	exists_equivalence_of_sieve_eq CategoryTheory.Functor.isEquivalence_iff_of_iso CategoryTheory.Functor.isEquivalence_trans CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Functor.isEquivalence_of_comp_right
isoMk_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.hom CategoryTheory.Pseudofunctor.DescentData instCategory isoMk CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
isoMk_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.DescentData instCategory isoMk CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str obj	—	—
iso_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Iso.hom CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj iso hom	—	—
iso_inv 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	CategoryTheory.Iso.inv CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj iso hom	—	—
nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq 📖	mathematical	CategoryTheory.Sieve.ofArrows	CategoryTheory.Functor.FullyFaithful CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Pseudofunctor.toDescentData	—	exists_equivalence_of_sieve_eq
ofObj_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	hom ofObj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.mapComp' CategoryTheory.Iso.hom	—	—
ofObj_obj 📖	mathematical	—	obj ofObj CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	—
pullFunctorCompIso_hom_app_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Functor.comp pullFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorCompIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp' obj	—	—
pullFunctorCompIso_inv_app_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorCompIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.hom CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapComp' obj	—	—
pullFunctorEquivalence_counitIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.inv	CategoryTheory.Equivalence.counitIso CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctorEquivalence CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp pullFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Functor.id pullFunctorCompIso CategoryTheory.Iso.hom_inv_id pullFunctorIso pullFunctorIdIso	—	—
pullFunctorEquivalence_functor 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.inv	CategoryTheory.Equivalence.functor CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctorEquivalence pullFunctor	—	—
pullFunctorEquivalence_inverse 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.inv	CategoryTheory.Equivalence.inverse CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctorEquivalence pullFunctor	—	—
pullFunctorEquivalence_unitIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.inv	CategoryTheory.Equivalence.unitIso CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctorEquivalence CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id pullFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Functor.comp CategoryTheory.Iso.symm pullFunctorIdIso pullFunctorIso pullFunctorCompIso CategoryTheory.Iso.inv_hom_id	—	—
pullFunctorIdIso_hom_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorIdIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId obj	—	—
pullFunctorIdIso_inv_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory CategoryTheory.Functor.id pullFunctor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorIdIso CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Cat.instQuiver CategoryTheory.Cat.Hom.instCategory CategoryTheory.Pseudofunctor.mapId obj	—	—
pullFunctorIso_hom_app_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorIso hom	—	—
pullFunctorIso_inv_app_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pullFunctorIso hom	—	—
pullFunctorObjHom_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	pullFunctorObjHom CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.mapComp' hom CategoryTheory.Iso.hom	—	CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp
pullFunctorObjHom_eq_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj pullFunctorObjHom CategoryTheory.NatTrans.app CategoryTheory.Cat.Hom₂.toNatTrans CategoryTheory.Iso.inv CategoryTheory.Pseudofunctor.mapComp' hom CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullFunctorObjHom_eq
pullFunctorObj_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	hom pullFunctorObj pullFunctorObjHom	—	—
pullFunctorObj_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	obj pullFunctorObj CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op	—	—
pullFunctor_map_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Hom.hom pullFunctorObj CategoryTheory.Functor.map CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op obj	—	—
pullFunctor_obj 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj CategoryTheory.Pseudofunctor.DescentData instCategory pullFunctor pullFunctorObj	—	—
pullHom_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom obj hom	—	—
subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Presieve.Arrows.Compatible CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Pseudofunctor.presheafHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Over.homMk Quiver.Hom CategoryTheory.Pseudofunctor.DescentData CategoryTheory.CategoryStruct.toQuiver instCategory CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.toDescentData EquivLike.toFunLike Equiv.instEquivLike subtypeCompatibleHomEquiv CategoryTheory.Presieve.Arrows.toCompatible CategoryTheory.types CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv CategoryTheory.Functor.map	—	hom_ext CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app CategoryTheory.locallyDiscreteBicategory.strict CategoryTheory.Category.assoc CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app CategoryTheory.Category.comp_id CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc

CategoryTheory.Pseudofunctor.DescentData.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	17 math math: CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_inv_app_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom, CategoryTheory.Pseudofunctor.DescentData.isoMk_inv_hom, CategoryTheory.Pseudofunctor.DescentData.comp_hom, CategoryTheory.Pseudofunctor.DescentData.hom_ext_iff, comm_assoc, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIso_hom_app_hom, CategoryTheory.Pseudofunctor.toDescentData_map_hom, ext_iff, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom, CategoryTheory.Pseudofunctor.DescentData.id_hom, CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom, CategoryTheory.Pseudofunctor.DescentData.isoMk_hom_hom, CategoryTheory.Pseudofunctor.DescentData.comp_hom_assoc, comm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Pseudofunctor.DescentData.obj CategoryTheory.Functor.map hom CategoryTheory.Pseudofunctor.DescentData.hom	—	—
comm_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Functor.obj CategoryTheory.Cat.Hom.toFunctor Prefunctor.map Quiver.Hom.toLoc CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.Pseudofunctor.DescentData.obj CategoryTheory.Functor.map hom CategoryTheory.Pseudofunctor.DescentData.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext

CategoryTheory.Pseudofunctor.IsPrestack

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isPrestackFor 📖	mathematical	CategoryTheory.Pseudofunctor.IsPrestackFor CategoryTheory.Sieve.arrows	CategoryTheory.Pseudofunctor.IsPrestack	—	CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.Over.mk_surjective CategoryTheory.Pseudofunctor.IsPrestackFor.isSheafFor'

CategoryTheory.Pseudofunctor.IsPrestackFor

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheafFor' 📖	mathematical	CategoryTheory.Pseudofunctor.IsPrestackFor CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Sieve.arrows DFunLike.coe Equiv CategoryTheory.Sieve CategoryTheory.Over CategoryTheory.instCategoryOver EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Sieve.overEquiv	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Pseudofunctor.presheafHom	—	CategoryTheory.Over.mk_surjective Equiv.symm_apply_apply CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor'
nonempty_fullyFaithful 📖	mathematical	CategoryTheory.Pseudofunctor.IsPrestackFor	CategoryTheory.Functor.FullyFaithful CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.toDescentData	—	—

CategoryTheory.Pseudofunctor.IsStackFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSurj 📖	mathematical	CategoryTheory.Pseudofunctor.IsStackFor	CategoryTheory.Functor.EssSurj CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.toDescentData	—	isEquivalence CategoryTheory.Functor.IsEquivalence.essSurj
isEquivalence 📖	mathematical	CategoryTheory.Pseudofunctor.IsStackFor	CategoryTheory.Functor.IsEquivalence CategoryTheory.Bundled.α CategoryTheory.Category Prefunctor.obj CategoryTheory.LocallyDiscrete Opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.locallyDiscreteBicategory CategoryTheory.Category.opposite CategoryTheory.Cat CategoryTheory.Cat.bicategory CategoryTheory.PrelaxFunctorStruct.toPrefunctor Quiver.Hom CategoryTheory.Category.toCategoryStruct CategoryTheory.Bicategory.homCategory CategoryTheory.PrelaxFunctor.toPrelaxFunctorStruct CategoryTheory.Pseudofunctor.toPrelaxFunctor Opposite.op CategoryTheory.Cat.str CategoryTheory.Pseudofunctor.DescentData CategoryTheory.Presieve.category CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.hom CategoryTheory.Pseudofunctor.DescentData.instCategory CategoryTheory.Pseudofunctor.toDescentData	—	—
isPrestackFor 📖	mathematical	CategoryTheory.Pseudofunctor.IsStackFor	CategoryTheory.Pseudofunctor.IsPrestackFor	—	CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Pseudofunctor.isStackFor_iff CategoryTheory.Functor.IsEquivalence.faithful

---

← Back to Index