Documentation Verification Report

LocallyDiscrete

📁 Source: Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

Statistics

Metric	Count
Definitions `IsLocallyDiscrete`, `LocallyDiscrete`, `as`, `categoryStruct`, `homSmallCategory`, `instDecidableEq`, `instInhabited`, `locallyDiscreteEquiv`, `locallyDiscreteBicategory`, `toLoc`	10
Theorems `instIsLocallyDiscreteLocallyDiscrete`, `instStrictOfIsLocallyDiscrete`, `toLoc`, `comp_as`, `eqToHom_toLoc`, `eq_of_hom`, `ext`, `ext_iff`, `id_as`, `locallyDiscreteEquiv_apply`, `locallyDiscreteEquiv_symm_apply_as`, `mk_as`, `subsingleton2Hom`, `strict`, `comp_toLoc`, `id_toLoc`, `toLoc_as`	17
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
`LocallyDiscrete` 📖	CompData	147 math math: `Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le`, `Pseudofunctor.DescentData.ofObj_hom`, `Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `Pseudofunctor.isEquivalence_toDescentData`, `Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.map_comp_eq`, `LocallyDiscrete.id_as`, `Pseudofunctor.DescentData.pullFunctor_map_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Functor.toPseudoFunctor'_obj`, `Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `LocallyDiscrete.comp_as`, `Pseudofunctor.DescentData.isoMk_inv_hom`, `Pseudofunctor.CoGrothendieck.map_map_base`, `Pseudofunctor.CoGrothendieck.map_map_fiber`, `Pseudofunctor.Grothendieck.map_id_eq`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `Pseudofunctor.DescentData.comp_hom`, `LocallyDiscrete.subsingleton2Hom`, `Pseudofunctor.Grothendieck.ext_iff`, `Functor.toOplaxFunctor'_obj`, `Pseudofunctor.isStackFor_ofArrows_iff`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app`, `GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app`, `Pseudofunctor.DescentData.iso_hom`, `Bicategory.instIsLocallyDiscreteLocallyDiscrete`, `Functor.toPseudoFunctor'_map`, `Pseudofunctor.presheafHom_obj`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData.iso_inv`, `Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CommSq.toLoc`, `Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj`, `Pseudofunctor.Grothendieck.map_id_map`, `Functor.toOplaxFunctor_obj`, `Functor.toPseudoFunctor_mapComp`, `Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `Pseudofunctor.CoGrothendieck.ι_map_base`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.isPrestackFor_ofArrows_iff`, `Pseudofunctor.CoGrothendieck.map_obj_fiber`, `Pseudofunctor.DescentData.Hom.comm_assoc`, `Functor.toPseudoFunctor_map`, `Pseudofunctor.Grothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.Hom.congr`, `FreeBicategory.preinclusion_map₂`, `Quiver.Hom.comp_toLoc`, `LocallyDiscrete.locallyDiscreteEquiv_symm_apply_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `Pseudofunctor.DescentData.ofObj_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app`, `Pseudofunctor.CoGrothendieck.ext_iff`, `Pseudofunctor.DescentData.hom_comp_assoc`, `Pseudofunctor.Grothendieck.map_obj_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_fiber`, `Pseudofunctor.isStackFor_iff`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `Pseudofunctor.bijective_toDescentData_map_iff`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `Pseudofunctor.CoGrothendieck.ι_map_fiber`, `Functor.toOplaxFunctor'_map`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `LocallyDiscrete.mkPseudofunctor_map`, `Pseudofunctor.DescentData.pullFunctorObj_obj`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `Functor.toOplaxFunctor_mapComp`, `LocallyDiscrete.mkPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `Pseudofunctor.IsStack.essSurj_of_sieve`, `FreeBicategory.normalize_naturality`, `LocallyDiscrete.mkPseudofunctor_mapComp`, `Pseudofunctor.toDescentData_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app`, `LocallyDiscrete.eqToHom_toLoc`, `Functor.toOplaxFunctor_map`, `Pseudofunctor.presheafHomObjHomEquiv_apply`, `Pseudofunctor.Grothendieck.Hom.ext_iff`, `LocallyDiscrete.locallyDiscreteEquiv_apply`, `Functor.toPseudoFunctor_mapId`, `Pseudofunctor.isPrestackFor_iff`, `Pseudofunctor.IsStackFor.isEquivalence`, `Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `Pseudofunctor.Grothendieck.Hom.congr`, `Pseudofunctor.Grothendieck.map_comp_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map`, `Pseudofunctor.Grothendieck.map_map_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_base`, `Pseudofunctor.toDescentData_map_hom`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `locallyDiscreteBicategory.strict`, `Pseudofunctor.IsStackFor.essSurj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `Functor.toPseudoFunctor'_mapId`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `Functor.toPseudoFunctor'_mapComp`, `Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq`, `LocallyDiscrete.mkPseudofunctor_obj`, `Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom`, `Quiver.Hom.id_toLoc`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq`, `Pseudofunctor.CoGrothendieck.comp_const`, `Pseudofunctor.CoGrothendieck.map_id_eq`, `Pseudofunctor.CoGrothendieck.compIso_inv_app`, `Functor.toOplaxFunctor_mapId`, `Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom`, `GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `Pseudofunctor.DescentData.id_hom`, `Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `Pseudofunctor.DescentData.isoMk_hom_hom`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `Pseudofunctor.DescentData.hom_self`, `Pseudofunctor.DescentData.comp_hom_assoc`, `Functor.toOplaxFunctor'_mapComp`, `Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `FreeBicategory.preinclusion_obj`, `Pseudofunctor.CoGrothendieck.map_id_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app`, `GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app`, `Functor.toPseudoFunctor_obj`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.CoGrothendieck.compIso_hom_app`, `Pseudofunctor.DescentData.hom_comp`, `Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `Pseudofunctor.Grothendieck.map_map_base`, `Functor.toOplaxFunctor'_mapId`, `Pseudofunctor.DescentData.Hom.comm`
`locallyDiscreteBicategory` 📖	CompOp	139 math math: `Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le`, `Pseudofunctor.DescentData.ofObj_hom`, `Pseudofunctor.DescentData.subtypeCompatibleHomEquiv_toCompatible_presheafHomObjHomEquiv`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `Pseudofunctor.isEquivalence_toDescentData`, `Pseudofunctor.CoGrothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.map_comp_eq`, `Pseudofunctor.DescentData.pullFunctor_map_hom`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Functor.toPseudoFunctor'_obj`, `Pseudofunctor.CoGrothendieck.instIsEquivalenceαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `Pseudofunctor.DescentData.isoMk_inv_hom`, `Pseudofunctor.CoGrothendieck.map_map_base`, `Pseudofunctor.CoGrothendieck.map_map_fiber`, `Pseudofunctor.Grothendieck.map_id_eq`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `Pseudofunctor.DescentData.comp_hom`, `Pseudofunctor.Grothendieck.ext_iff`, `Functor.toOplaxFunctor'_obj`, `Pseudofunctor.isStackFor_ofArrows_iff`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app`, `GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app`, `Pseudofunctor.DescentData.iso_hom`, `Bicategory.instIsLocallyDiscreteLocallyDiscrete`, `Functor.toPseudoFunctor'_map`, `Pseudofunctor.presheafHom_obj`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `Pseudofunctor.DescentData.iso_inv`, `Pseudofunctor.CoGrothendieck.instFullαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `CommSq.toLoc`, `Pseudofunctor.DescentData.nonempty_fullyFaithful_toDescentData_iff_of_sieve_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj`, `Pseudofunctor.Grothendieck.map_id_map`, `Functor.toOplaxFunctor_obj`, `Functor.toPseudoFunctor_mapComp`, `Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `Pseudofunctor.CoGrothendieck.ι_map_base`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `Pseudofunctor.isPrestackFor_ofArrows_iff`, `Pseudofunctor.CoGrothendieck.map_obj_fiber`, `Pseudofunctor.DescentData.Hom.comm_assoc`, `Functor.toPseudoFunctor_map`, `Pseudofunctor.Grothendieck.categoryStruct_id_fiber`, `Pseudofunctor.CoGrothendieck.Hom.congr`, `FreeBicategory.preinclusion_map₂`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `Pseudofunctor.DescentData.ofObj_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app`, `Pseudofunctor.CoGrothendieck.ext_iff`, `Pseudofunctor.DescentData.hom_comp_assoc`, `Pseudofunctor.Grothendieck.map_obj_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_fiber`, `Pseudofunctor.isStackFor_iff`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `Pseudofunctor.bijective_toDescentData_map_iff`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `Pseudofunctor.CoGrothendieck.ι_map_fiber`, `Functor.toOplaxFunctor'_map`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `LocallyDiscrete.mkPseudofunctor_map`, `Pseudofunctor.DescentData.pullFunctorObj_obj`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `Functor.toOplaxFunctor_mapComp`, `LocallyDiscrete.mkPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `Pseudofunctor.IsStack.essSurj_of_sieve`, `FreeBicategory.normalize_naturality`, `LocallyDiscrete.mkPseudofunctor_mapComp`, `Pseudofunctor.toDescentData_obj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app`, `Functor.toOplaxFunctor_map`, `Pseudofunctor.presheafHomObjHomEquiv_apply`, `Pseudofunctor.Grothendieck.Hom.ext_iff`, `Functor.toPseudoFunctor_mapId`, `Pseudofunctor.isPrestackFor_iff`, `Pseudofunctor.IsStackFor.isEquivalence`, `Pseudofunctor.CoGrothendieck.instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `Pseudofunctor.Grothendieck.Hom.congr`, `Pseudofunctor.Grothendieck.map_comp_eq`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map`, `Pseudofunctor.Grothendieck.map_map_fiber`, `Pseudofunctor.CoGrothendieck.ι_obj_base`, `Pseudofunctor.toDescentData_map_hom`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `locallyDiscreteBicategory.strict`, `Pseudofunctor.IsStackFor.essSurj`, `GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `Functor.toPseudoFunctor'_mapId`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `Functor.toPseudoFunctor'_mapComp`, `Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq`, `LocallyDiscrete.mkPseudofunctor_obj`, `Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `Pseudofunctor.DescentData.isEquivalence_toDescentData_iff_of_sieve_eq`, `Pseudofunctor.CoGrothendieck.comp_const`, `Pseudofunctor.CoGrothendieck.map_id_eq`, `Pseudofunctor.CoGrothendieck.compIso_inv_app`, `Functor.toOplaxFunctor_mapId`, `Pseudofunctor.DescentData.pullFunctorIdIso_hom_app_hom`, `GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `Pseudofunctor.DescentData.id_hom`, `Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `Pseudofunctor.DescentData.isoMk_hom_hom`, `Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `Pseudofunctor.DescentData.hom_self`, `Pseudofunctor.DescentData.comp_hom_assoc`, `Functor.toOplaxFunctor'_mapComp`, `Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `Pseudofunctor.CoGrothendieck.instFaithfulαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor`, `FreeBicategory.preinclusion_obj`, `Pseudofunctor.CoGrothendieck.map_id_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app`, `GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app`, `Functor.toPseudoFunctor_obj`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `Pseudofunctor.CoGrothendieck.compIso_hom_app`, `Pseudofunctor.DescentData.hom_comp`, `Pseudofunctor.IsPrestackFor.nonempty_fullyFaithful`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `Pseudofunctor.Grothendieck.map_map_base`, `Functor.toOplaxFunctor'_mapId`, `Pseudofunctor.DescentData.Hom.comm`

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`IsLocallyDiscrete` 📖	MathDef	1 math math: `instIsLocallyDiscreteLocallyDiscrete`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocallyDiscreteLocallyDiscrete` 📖	mathematical	—	`IsLocallyDiscrete` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory`	—	`CategoryTheory.Discrete.isDiscrete`
`instStrictOfIsLocallyDiscrete` 📖	mathematical	`IsLocallyDiscrete`	`Strict`	—	`CategoryTheory.obj_ext_of_isDiscrete` `CategoryTheory.Iso.ext` `CategoryTheory.IsDiscrete.subsingleton`

CategoryTheory.CommSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLoc` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.LocallyDiscrete` `CategoryTheory.StrictBicategory.category` `CategoryTheory.locallyDiscreteBicategory` `CategoryTheory.locallyDiscreteBicategory.strict` `Quiver.Hom.toLoc` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.locallyDiscreteBicategory.strict` `w`

CategoryTheory.LocallyDiscrete

Definitions

Name	Category	Theorems
`as` 📖	CompOp	63 math math: `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂`, `mk_as`, `id_as`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `CategoryTheory.Functor.toPseudoFunctor'_obj`, `comp_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l`, `CategoryTheory.Functor.toOplaxFunctor'_obj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp_val_app`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_inv_toNatTrans_app_val_app`, `CategoryTheory.Functor.toPseudoFunctor'_map`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_obj`, `CategoryTheory.Functor.toOplaxFunctor_obj`, `CategoryTheory.Functor.toPseudoFunctor_mapComp`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_map`, `CategoryTheory.Functor.toPseudoFunctor_map`, `locallyDiscreteEquiv_symm_apply_as`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_id_val_app`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr`, `CategoryTheory.Functor.toOplaxFunctor'_map`, `ext_iff`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapId`, `mkPseudofunctor_map`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_obj`, `CategoryTheory.Functor.toOplaxFunctor_mapComp`, `mkPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr`, `RingCat.moduleCatRestrictScalarsPseudofunctor_map`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj`, `CategoryTheory.FreeBicategory.normalize_naturality`, `mkPseudofunctor_mapComp`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map_val_app`, `CategoryTheory.Functor.toOplaxFunctor_map`, `locallyDiscreteEquiv_apply`, `CategoryTheory.Functor.toPseudoFunctor_mapId`, `RingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj_val_map`, `RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α`, `CategoryTheory.Functor.toPseudoFunctor'_mapId`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl`, `CategoryTheory.Functor.toPseudoFunctor'_mapComp`, `mkPseudofunctor_obj`, `CategoryTheory.Functor.toOplaxFunctor_mapId`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_val_app`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl`, `CategoryTheory.Functor.toOplaxFunctor'_mapComp`, `CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr`, `Quiver.Hom.toLoc_as`, `CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_inv_toNatTrans_app_val_app`, `CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapId_hom_toNatTrans_app_val_app`, `CategoryTheory.Functor.toPseudoFunctor_obj`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl`, `AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr`, `CategoryTheory.Functor.toOplaxFunctor'_mapId`
`categoryStruct` 📖	CompOp	10 math math: `id_as`, `comp_as`, `subsingleton2Hom`, `Quiver.Hom.comp_toLoc`, `eqToHom_toLoc`, `CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_apply`, `Quiver.Hom.id_toLoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`
`homSmallCategory` 📖	CompOp	1 math math: `subsingleton2Hom`
`instDecidableEq` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`locallyDiscreteEquiv` 📖	CompOp	2 math math: `locallyDiscreteEquiv_symm_apply_as`, `locallyDiscreteEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `as` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`eqToHom_toLoc` 📖	mathematical	—	`Quiver.Hom.toLoc` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`eq_of_hom` 📖	—	—	—	—	`CategoryTheory.Discrete.ext`
`ext` 📖	—	`as`	—	—	—
`ext_iff` 📖	mathematical	—	`as`	—	`ext`
`id_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `as` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocallyDiscrete` `categoryStruct`	—	—
`locallyDiscreteEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.LocallyDiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `locallyDiscreteEquiv` `as`	—	—
`locallyDiscreteEquiv_symm_apply_as` 📖	mathematical	—	`as` `DFunLike.coe` `Equiv` `CategoryTheory.LocallyDiscrete` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `locallyDiscreteEquiv`	—	—
`mk_as` 📖	mathematical	—	`as`	—	—
`subsingleton2Hom` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.LocallyDiscrete` `CategoryTheory.CategoryStruct.toQuiver` `categoryStruct` `CategoryTheory.Category.toCategoryStruct` `homSmallCategory`	—	`CategoryTheory.Discrete.instSubsingletonDiscreteHom`

CategoryTheory.locallyDiscreteBicategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strict` 📖	mathematical	—	`CategoryTheory.Bicategory.Strict` `CategoryTheory.LocallyDiscrete` `CategoryTheory.locallyDiscreteBicategory`	—	`CategoryTheory.Discrete.ext` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`

Quiver.Hom

Definitions

Name	Category	Theorems
`toLoc` 📖	CompOp	40 math math: `CategoryTheory.Pseudofunctor.DescentData.ofObj_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_inv_app_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctor_map_hom`, `CategoryTheory.Pseudofunctor.CoGrothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.DescentData.iso_hom`, `CategoryTheory.Pseudofunctor.presheafHom_obj`, `CategoryTheory.Pseudofunctor.DescentData.iso_inv`, `CategoryTheory.CommSq.toLoc`, `CategoryTheory.Functor.toPseudoFunctor_mapComp`, `CategoryTheory.Pseudofunctor.DescentData.instIsIsoαCategoryObjLocallyDiscreteOppositeCatMkOpHom`, `CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc`, `CategoryTheory.Functor.toPseudoFunctor_map`, `CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.congr`, `comp_toLoc`, `CategoryTheory.Pseudofunctor.DescentData.ofObj_obj`, `CategoryTheory.Pseudofunctor.DescentData.hom_comp_assoc`, `CategoryTheory.Pseudofunctor.CoGrothendieck.ι_map_fiber`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj`, `CategoryTheory.Functor.toOplaxFunctor_mapComp`, `CategoryTheory.LocallyDiscrete.eqToHom_toLoc`, `CategoryTheory.Functor.toOplaxFunctor_map`, `CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff`, `CategoryTheory.Functor.toPseudoFunctor_mapId`, `CategoryTheory.Pseudofunctor.Grothendieck.Hom.congr`, `CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber`, `CategoryTheory.Pseudofunctor.toDescentData_map_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc`, `id_toLoc`, `CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom_assoc`, `CategoryTheory.Functor.toOplaxFunctor_mapId`, `CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.map_eq_pullHom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorCompIso_hom_app_hom`, `CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq`, `CategoryTheory.Pseudofunctor.DescentData.hom_self`, `CategoryTheory.Pseudofunctor.CoGrothendieck.categoryStruct_comp_fiber`, `toLoc_as`, `CategoryTheory.Pseudofunctor.Grothendieck.categoryStruct_comp_fiber`, `CategoryTheory.Pseudofunctor.DescentData.hom_comp`, `CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.ext_iff`, `CategoryTheory.Pseudofunctor.DescentData.Hom.comm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toLoc` 📖	mathematical	—	`toLoc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.LocallyDiscrete` `CategoryTheory.LocallyDiscrete.categoryStruct`	—	—
`id_toLoc` 📖	mathematical	—	`toLoc` `CategoryTheory.CategoryStruct.id` `CategoryTheory.LocallyDiscrete` `CategoryTheory.LocallyDiscrete.categoryStruct`	—	—
`toLoc_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.LocallyDiscrete.as` `toLoc`	—	—

---

← Back to Index