TopComparison

📁 Source: Mathlib/Condensed/TopComparison.lean

Statistics

Metric	Count
Definitions toCondensedSet, toSheafCompHausLike, topCatToCondensedSet, topCatToSheafCompHausLike	4
Theorems toSheafCompHausLike_val_map, toSheafCompHausLike_val_obj, equalizerCondition_yonedaPresheaf, factorsThrough_of_pullbackCondition, instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat, topCatToSheafCompHausLike_map_val_app, topCatToSheafCompHausLike_obj	7
Total	11

TopCat

Definitions

Name	Category	Theorems
toCondensedSet 📖	CompOp	4 math math: CondensedSet.topCatAdjunctionCounit_bijective, CondensedSet.topCatAdjunctionCounit_hom_apply, CondensedSet.topCatAdjunctionUnit_val_app_apply, CondensedSet.topCatAdjunctionUnit_val_app
toSheafCompHausLike 📖	CompOp	4 math math: toSheafCompHausLike_val_obj, topCatToSheafCompHausLike_map_val_app, topCatToSheafCompHausLike_obj, toSheafCompHausLike_val_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSheafCompHausLike_val_map 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap carrier CompHausLike.toTop str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular toSheafCompHausLike ContinuousMap.comp CategoryTheory.Functor.obj TopCat instCategory CompHausLike.compHausLikeToTop Opposite.unop Hom.hom CategoryTheory.InducedCategory.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
toSheafCompHausLike_val_obj 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap carrier CompHausLike.toTop str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular toSheafCompHausLike TopCat instCategory CompHausLike.compHausLikeToTop Opposite.unop	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular

(root)

Definitions

Name	Category	Theorems
topCatToCondensedSet 📖	CompOp	2 math math: CondensedSet.instEpiTopCatAppCounitTopCatAdjunction, CondensedSet.instFaithfulTopCatTopCatToCondensedSet
topCatToSheafCompHausLike 📖	CompOp	2 math math: topCatToSheafCompHausLike_map_val_app, topCatToSheafCompHausLike_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equalizerCondition_yonedaPresheaf 📖	mathematical	CategoryTheory.Limits.PreservesLimit TopCat TopCat.instCategory CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan Topology.IsQuotientMap TopCat.carrier CategoryTheory.Functor.obj TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map	CategoryTheory.regularTopology.EqualizerCondition CategoryTheory.types ContinuousMap.yonedaPresheaf	—	CategoryTheory.Limits.pullback.condition ContinuousMap.ext Topology.IsQuotientMap.surjective factorsThrough_of_pullbackCondition DFunLike.ext'_iff Topology.IsQuotientMap.lift_comp
factorsThrough_of_pullbackCondition 📖	mathematical	TopCat.carrier CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Limits.pullback DFunLike.coe ContinuousMap TopCat.str ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	Function.FactorsThrough	—	CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Presieve.instHasPairwisePullbacksOfHasPullbacks CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits TopCat.topCat_hasLimits CategoryTheory.Limits.hasLimitOfHasLimitsOfShape TopCat.pullbackIsoProdSubtype_inv_snd_apply TopCat.pullbackIsoProdSubtype_inv_fst_apply
instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteProducts Opposite CategoryTheory.Category.opposite CategoryTheory.types ContinuousMap.yonedaPresheaf	—	CategoryTheory.Limits.preservesFiniteProducts_op CategoryTheory.Limits.comp_preservesLimitsOfShape CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts Finite.of_fintype ContinuousMap.instPreservesFiniteProductsOppositeTopCatYonedaPresheaf'
topCatToSheafCompHausLike_map_val_app 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Sheaf.val CategoryTheory.coherentTopology TopCat.toSheafCompHausLike CategoryTheory.Sheaf.Hom.val CategoryTheory.Functor.map TopCat TopCat.instCategory CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.Sheaf.instCategorySheaf topCatToSheafCompHausLike ContinuousMap.comp CategoryTheory.Functor.obj CompHausLike.compHausLikeToTop Opposite.unop TopCat.Hom.hom	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
topCatToSheafCompHausLike_obj 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Sheaf CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf topCatToSheafCompHausLike TopCat.toSheafCompHausLike	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular

---

← Back to Index