Colimit

📁 Source: Mathlib/Condensed/Discrete/Colimit.lean

Statistics

Metric	Count
Definitions finYoneda, fintypeCatAsCofan, fintypeCatAsCofanIsColimit, isColimitLocallyConstantPresheaf, isColimitLocallyConstantPresheafDiagram, isoFinYoneda, isoFinYonedaComponents, isoLocallyConstantOfIsColimit, lanCondensedSet, lanPresheaf, lanPresheafExt, lanPresheafIso, lanPresheafNatIso, lanSheafProfinite, locallyConstantIsoFinYoneda, locallyConstantPresheaf, finYoneda, fintypeCatAsCofan, fintypeCatAsCofanIsColimit, isColimitLocallyConstantPresheaf, isColimitLocallyConstantPresheafDiagram, isoFinYoneda, isoFinYonedaComponents, isoLocallyConstantOfIsColimit, lanLightCondSet, lanPresheaf, lanPresheafExt, lanPresheafIso, lanPresheafNatIso, locallyConstantIsoFinYoneda, locallyConstantPresheaf	31
Theorems finYoneda_map, finYoneda_obj, instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, isColimitLocallyConstantPresheafDiagram_desc_apply, isColimitLocallyConstantPresheaf_desc_apply, isoFinYonedaComponents_hom_apply, isoFinYonedaComponents_inv_comp, isoFinYoneda_hom_app, isoFinYoneda_inv_app, isoLocallyConstantOfIsColimit_inv, lanPresheafExt_hom, lanPresheafExt_inv, lanPresheafIso_hom, lanPresheafNatIso_hom_app, locallyConstantIsoFinYoneda_hom_app, finYoneda_map, finYoneda_obj, instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, isColimitLocallyConstantPresheafDiagram_desc_apply, isColimitLocallyConstantPresheaf_desc_apply, isoFinYonedaComponents_hom_apply, isoFinYonedaComponents_inv_comp, isoFinYoneda_hom_app, isoFinYoneda_inv_app, isoLocallyConstantOfIsColimit_inv, lanPresheafExt_hom, lanPresheafExt_inv, lanPresheafIso_hom, lanPresheafNatIso_hom_app	32
Total	63

Condensed

Definitions

Name	Category	Theorems
finYoneda 📖	CompOp	5 math math: finYoneda_obj, finYoneda_map, isoFinYoneda_hom_app, isoFinYoneda_inv_app, locallyConstantIsoFinYoneda_hom_app
fintypeCatAsCofan 📖	CompOp	—
fintypeCatAsCofanIsColimit 📖	CompOp	—
isColimitLocallyConstantPresheaf 📖	CompOp	1 math math: isColimitLocallyConstantPresheaf_desc_apply
isColimitLocallyConstantPresheafDiagram 📖	CompOp	1 math math: isColimitLocallyConstantPresheafDiagram_desc_apply
isoFinYoneda 📖	CompOp	2 math math: isoFinYoneda_hom_app, isoFinYoneda_inv_app
isoFinYonedaComponents 📖	CompOp	4 math math: isoFinYonedaComponents_hom_apply, isoFinYonedaComponents_inv_comp, isoFinYoneda_hom_app, isoFinYoneda_inv_app
isoLocallyConstantOfIsColimit 📖	CompOp	1 math math: isoLocallyConstantOfIsColimit_inv
lanCondensedSet 📖	CompOp	—
lanPresheaf 📖	CompOp	4 math math: lanPresheafExt_inv, lanPresheafNatIso_hom_app, lanPresheafExt_hom, lanPresheafIso_hom
lanPresheafExt 📖	CompOp	2 math math: lanPresheafExt_inv, lanPresheafExt_hom
lanPresheafIso 📖	CompOp	1 math math: lanPresheafIso_hom
lanPresheafNatIso 📖	CompOp	1 math math: lanPresheafNatIso_hom_app
lanSheafProfinite 📖	CompOp	—
locallyConstantIsoFinYoneda 📖	CompOp	1 math math: locallyConstantIsoFinYoneda_hom_app
locallyConstantPresheaf 📖	CompOp	4 math math: isColimitLocallyConstantPresheaf_desc_apply, isoLocallyConstantOfIsColimit_inv, isColimitLocallyConstantPresheafDiagram_desc_apply, locallyConstantIsoFinYoneda_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finYoneda_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda FintypeCat.carrier Opposite.unop CategoryTheory.Functor.obj Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.op FintypeCat.toProfinite Opposite.op FintypeCat.of PUnit.fintype DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype Quiver.Hom.unop	—	—
finYoneda_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda	—	—
instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp 📖	mathematical	—	CategoryTheory.Functor.Final Opposite DiscreteQuotient TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder DiscreteQuotient.instPartialOrder CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory Profinite CompHausLike.category CategoryTheory.Functor.op FintypeCat.toProfinite Opposite.op CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp Profinite.fintypeDiagram Profinite.asLimitCone CategoryTheory.instCategoryCostructuredArrow Profinite.Extend.functorOp	—	Profinite.Extend.functorOp_final CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone
instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types CategoryTheory.Discrete CompHausLike.toTop CategoryTheory.discreteCategory	—	Small.equiv_small Countable.toSmall Finite.to_countable Finite.of_equiv CategoryTheory.Limits.preservesLimitsOfShape_of_equiv CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
isColimitLocallyConstantPresheafDiagram_desc_apply 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc Opposite DiscreteQuotient TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder DiscreteQuotient.instPartialOrder CategoryTheory.types CategoryTheory.Functor.comp Profinite CompHausLike.category CategoryTheory.Functor.op Profinite.diagram locallyConstantPresheaf CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cone.op Profinite.asLimitCone isColimitLocallyConstantPresheafDiagram LocallyConstant.comap CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj TopCat.Hom.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι Opposite.op	—	isColimitLocallyConstantPresheaf_desc_apply CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone
isColimitLocallyConstantPresheaf_desc_apply 📖	mathematical	CategoryTheory.Epi Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat FintypeCat.instCategory FintypeCat.toProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Limits.IsColimit.desc Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op locallyConstantPresheaf CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cone.op isColimitLocallyConstantPresheaf LocallyConstant.comap CompHausLike.toTop TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι Opposite.op	—	CategoryTheory.Limits.IsColimit.fac
isoFinYonedaComponents_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str Opposite.op isoFinYonedaComponents CategoryTheory.Functor.map CompHausLike Profinite.of instTopologicalSpacePUnit Finite.compactSpace Finite.of_fintype PUnit.fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace instMetricSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CompHausLike.const	—	Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit
isoFinYonedaComponents_inv_comp 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types CategoryTheory.Functor.obj Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str Opposite.op isoFinYonedaComponents CompHausLike.toTop Profinite.of instTopologicalSpacePUnit Finite.compactSpace Finite.of_fintype PUnit.fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace instMetricSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit CategoryTheory.injective_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.inv_hom_id_apply isoFinYonedaComponents_hom_apply
isoFinYoneda_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types CategoryTheory.Functor.comp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.op FintypeCat.toProfinite finYoneda CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoFinYoneda CategoryTheory.Functor.obj Opposite.op Opposite.unop isoFinYonedaComponents	—	—
isoFinYoneda_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda CategoryTheory.Functor.comp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.op FintypeCat.toProfinite CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category isoFinYoneda CategoryTheory.Functor.obj Opposite.op Opposite.unop isoFinYonedaComponents	—	—
isoLocallyConstantOfIsColimit_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types CategoryTheory.Functor.category locallyConstantPresheaf CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toProfinite Opposite.op FintypeCat.of PUnit.fintype isoLocallyConstantOfIsColimit CompHausLike.LocallyConstant.counitApp Profinite.instHasPropTotallyDisconnectedSpaceCarrier CompHausLike.toTop instTopologicalSpaceSubtype Subtype.totallyDisconnectedSpace Profinite.instTotallyDisconnectedSpaceCarrierToTop instTopologicalSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier	—	Profinite.instHasPropTotallyDisconnectedSpaceCarrier Subtype.totallyDisconnectedSpace Profinite.instTotallyDisconnectedSpaceCarrierToTop TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CategoryTheory.Category.assoc CategoryTheory.Iso.inv_comp_eq CategoryTheory.NatTrans.ext' CategoryTheory.Limits.colimit.hom_ext CategoryTheory.NatTrans.naturality CategoryTheory.types_ext CompHausLike.LocallyConstant.presheaf_ext CompHausLike.LocallyConstant.incl_of_counitAppApp CategoryTheory.injective_of_mono Subtype.val_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom DiscreteTopology.toT2Space CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.FunctorToTypes.map_id_apply isoFinYonedaComponents_inv_comp CategoryTheory.inv_hom_id_apply Function.Fiber.map_eq_image CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimit lanPresheafExt_inv lanPresheafNatIso_hom_app CategoryTheory.Limits.colimit.map_desc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.colimit.ι_desc_assoc
lanPresheafExt_hom 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types lanPresheaf CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafExt CategoryTheory.Limits.colimMap CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap
lanPresheafExt_inv 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types lanPresheaf CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafExt CategoryTheory.Limits.colimMap CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Limits.Types.hasColimit UnivLE.small UnivLE.self CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap
lanPresheafIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str lanPresheaf Opposite.op lanPresheafIso CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj Profinite.Extend.cocone	—	CategoryTheory.Functor.Final.comp_hasColimit instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp CategoryTheory.Functor.Final.colimit_pre_isIso CategoryTheory.Limits.colimit.pre_desc
lanPresheafNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite Profinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.types lanPresheaf CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafNatIso CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toProfinite Opposite.op Opposite.unop CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj Profinite.Extend.cocone	—	lanPresheafIso_hom
locallyConstantIsoFinYoneda_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types CategoryTheory.Functor.comp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.Functor.op FintypeCat.toProfinite locallyConstantPresheaf CategoryTheory.Functor.obj Opposite.op FintypeCat.of PUnit.fintype finYoneda CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category locallyConstantIsoFinYoneda DFunLike.coe LocallyConstant CompHausLike.toTop Opposite.unop LocallyConstant.instFunLike	—	—

LightCondensed

Definitions

Name	Category	Theorems
finYoneda 📖	CompOp	4 math math: finYoneda_obj, isoFinYoneda_inv_app, finYoneda_map, isoFinYoneda_hom_app
fintypeCatAsCofan 📖	CompOp	—
fintypeCatAsCofanIsColimit 📖	CompOp	—
isColimitLocallyConstantPresheaf 📖	CompOp	1 math math: isColimitLocallyConstantPresheaf_desc_apply
isColimitLocallyConstantPresheafDiagram 📖	CompOp	1 math math: isColimitLocallyConstantPresheafDiagram_desc_apply
isoFinYoneda 📖	CompOp	2 math math: isoFinYoneda_inv_app, isoFinYoneda_hom_app
isoFinYonedaComponents 📖	CompOp	4 math math: isoFinYonedaComponents_hom_apply, isoFinYoneda_inv_app, isoFinYonedaComponents_inv_comp, isoFinYoneda_hom_app
isoLocallyConstantOfIsColimit 📖	CompOp	1 math math: isoLocallyConstantOfIsColimit_inv
lanLightCondSet 📖	CompOp	—
lanPresheaf 📖	CompOp	4 math math: lanPresheafIso_hom, lanPresheafNatIso_hom_app, lanPresheafExt_inv, lanPresheafExt_hom
lanPresheafExt 📖	CompOp	2 math math: lanPresheafExt_inv, lanPresheafExt_hom
lanPresheafIso 📖	CompOp	1 math math: lanPresheafIso_hom
lanPresheafNatIso 📖	CompOp	1 math math: lanPresheafNatIso_hom_app
locallyConstantIsoFinYoneda 📖	CompOp	—
locallyConstantPresheaf 📖	CompOp	3 math math: isColimitLocallyConstantPresheafDiagram_desc_apply, isoLocallyConstantOfIsColimit_inv, isColimitLocallyConstantPresheaf_desc_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finYoneda_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda FintypeCat.carrier Opposite.unop CategoryTheory.Functor.obj LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op FintypeCat.of PUnit.fintype DFunLike.coe FintypeCat.instFunLikeHomCarrier CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.concreteCategoryFintype Quiver.Hom.unop	—	—
finYoneda_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda	—	—
instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp 📖	mathematical	—	CategoryTheory.Functor.Final Preorder.smallCategory Nat.instPreorder CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp LightProfinite.fintypeDiagram LightProfinite.asLimitCone CategoryTheory.instCategoryCostructuredArrow LightProfinite.Extend.functorOp	—	LightProfinite.Extend.functorOp_final LightProfinite.instEpiAppOppositeNatπAsLimitCone
instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.CostructuredArrow Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.types	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.CostructuredArrow.isEquivalence_pre CategoryTheory.Functor.instIsEquivalenceOppositeOp FintypeCat.Skeleton.instIsEquivalenceIncl CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self
instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.Discrete FintypeCat.carrier CategoryTheory.discreteCategory	—	Small.equiv_small Countable.toSmall Finite.to_countable Finite.of_fintype CategoryTheory.Limits.preservesLimitsOfShape_of_equiv CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
isColimitLocallyConstantPresheafDiagram_desc_apply 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc Preorder.smallCategory Nat.instPreorder CategoryTheory.types CategoryTheory.Functor.comp Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.rightOp LightProfinite.diagram locallyConstantPresheaf CategoryTheory.Functor.mapCocone CategoryTheory.Limits.coconeRightOpOfCone LightProfinite.asLimitCone isColimitLocallyConstantPresheafDiagram LocallyConstant.comap CompHausLike.toTop CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.obj Opposite.op TopCat.Hom.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.IsColimit.fac
isColimitLocallyConstantPresheaf_desc_apply 📖	mathematical	CategoryTheory.Epi LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp FintypeCat FintypeCat.instCategory FintypeCat.toLightProfinite CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	CategoryTheory.Limits.IsColimit.desc CategoryTheory.types CategoryTheory.Functor.op locallyConstantPresheaf CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cone.op isColimitLocallyConstantPresheaf LocallyConstant.comap CompHausLike.toTop TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom CompHausLike TopCat TopCat.instCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι Opposite.op	—	CategoryTheory.Limits.IsColimit.fac
isoFinYonedaComponents_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology Opposite.op isoFinYonedaComponents CategoryTheory.Functor.map CompHausLike LightProfinite.of instTopologicalSpacePUnit Finite.compactSpace Finite.of_fintype PUnit.fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace instMetricSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace EMetricSpace.toPseudoEMetricSpace Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CompHausLike.const	—	Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace
isoFinYonedaComponents_inv_comp 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types CategoryTheory.Functor.obj Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology Opposite.op isoFinYonedaComponents CompHausLike.toTop LightProfinite.of instTopologicalSpacePUnit Finite.compactSpace Finite.of_fintype PUnit.fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace instMetricSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace EMetricSpace.toPseudoEMetricSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace CategoryTheory.injective_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.inv_hom_id_apply isoFinYonedaComponents_hom_apply
isoFinYoneda_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types CategoryTheory.Functor.comp LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite finYoneda CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category isoFinYoneda CategoryTheory.Functor.obj Opposite.op Opposite.unop isoFinYonedaComponents	—	—
isoFinYoneda_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite FintypeCat CategoryTheory.Category.opposite FintypeCat.instCategory CategoryTheory.types finYoneda CategoryTheory.Functor.comp LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.Functor.op FintypeCat.toLightProfinite CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category isoFinYoneda CategoryTheory.Functor.obj Opposite.op Opposite.unop isoFinYonedaComponents	—	—
isoLocallyConstantOfIsColimit_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.Functor.category locallyConstantPresheaf CategoryTheory.Functor.obj FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op FintypeCat.of PUnit.fintype isoLocallyConstantOfIsColimit CompHausLike.LocallyConstant.counitApp LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instTopologicalSpacePUnit TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace instMetricSpacePUnit LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology	—	LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CategoryTheory.Category.assoc CategoryTheory.Iso.inv_comp_eq CategoryTheory.NatTrans.ext' CategoryTheory.Limits.colimit.hom_ext CategoryTheory.NatTrans.naturality CategoryTheory.types_ext CompHausLike.LocallyConstant.presheaf_ext CompHausLike.LocallyConstant.incl_of_counitAppApp CategoryTheory.injective_of_mono Subtype.val_injective CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom DiscreteTopology.toT2Space CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.FunctorToTypes.map_id_apply isoFinYonedaComponents_inv_comp CategoryTheory.inv_hom_id_apply Function.Fiber.map_eq_image CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType lanPresheafExt_inv lanPresheafNatIso_hom_app CategoryTheory.Limits.colimit.map_desc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.colimit.ι_desc_assoc
lanPresheafExt_hom 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types lanPresheaf CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafExt CategoryTheory.Limits.colimMap CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toLightProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap
lanPresheafExt_inv 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types lanPresheaf CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafExt CategoryTheory.Limits.colimMap CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toLightProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap
lanPresheafIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types CategoryTheory.Functor.obj Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology lanPresheaf Opposite.op lanPresheafIso CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toLightProfinite CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj LightProfinite.Extend.cocone	—	CategoryTheory.Functor.Final.comp_hasColimit instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp CategoryTheory.Functor.Final.colimit_pre_isIso CategoryTheory.Limits.colimit.pre_desc
lanPresheafNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types lanPresheaf CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category lanPresheafNatIso CategoryTheory.Limits.colimit.desc CategoryTheory.CostructuredArrow FintypeCat FintypeCat.instCategory CategoryTheory.Functor.op FintypeCat.toLightProfinite Opposite.op Opposite.unop CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj LightProfinite.Extend.cocone	—	lanPresheafIso_hom

---

← Back to Index