ULift

📁 Source: Mathlib/Topology/Category/TopCat/ULift.lean

Statistics

Metric	Count
Definitions uliftFunctor, uliftFunctorCompForgetIso, uliftFunctorFullyFaithful, uliftFunctorObjHomeo	4
Theorems instFaithfulUliftFunctor, instFullUliftFunctor, instPreservesColimitsOfSizeUliftFunctor, instPreservesLimitsOfSizeUliftFunctor, uliftFunctorCompForgetIso_hom_app, uliftFunctorCompForgetIso_inv_app, uliftFunctorObjHomeo_naturality_apply, uliftFunctorObjHomeo_symm_naturality_apply	8
Total	12

TopCat

Definitions

Name	Category	Theorems
uliftFunctor 📖	CompOp	10 math math: uliftFunctorObjHomeo_symm_naturality_apply, uliftFunctorCompForgetIso_hom_app, instFaithfulUliftFunctor, instPreservesLimitsOfSizeUliftFunctor, SimplexCategory.toTop_obj, SimplexCategory.toTop_map, uliftFunctorObjHomeo_naturality_apply, uliftFunctorCompForgetIso_inv_app, instPreservesColimitsOfSizeUliftFunctor, instFullUliftFunctor
uliftFunctorCompForgetIso 📖	CompOp	2 math math: uliftFunctorCompForgetIso_hom_app, uliftFunctorCompForgetIso_inv_app
uliftFunctorFullyFaithful 📖	CompOp	—
uliftFunctorObjHomeo 📖	CompOp	2 math math: uliftFunctorObjHomeo_symm_naturality_apply, uliftFunctorObjHomeo_naturality_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful TopCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullUliftFunctor 📖	mathematical	—	CategoryTheory.Functor.Full TopCat instCategory uliftFunctor	—	CategoryTheory.Functor.FullyFaithful.full
instPreservesColimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize TopCat instCategory uliftFunctor	—	nonempty_isColimit_iff_eq_coinduced CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint instIsLeftAdjointForgetContinuousMapCarrier CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor TopologicalSpace.ext Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen Homeomorph.isOpenEmbedding EquivLike.range_eq_univ isOpen_iff_of_isColimit isOpen_iSup_iff
instPreservesLimitsOfSizeUliftFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize TopCat instCategory uliftFunctor	—	nonempty_isLimit_iff_eq_induced CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint instIsRightAdjointForgetContinuousMapCarrier CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor le_antisymm le_iInf_iff Continuous.isOpen_preimage Homeomorph.continuous_invFun ContinuousMap.continuous_toFun generateFrom_iUnion_isOpen induced_of_isLimit induced_iInf Set.mem_iUnion Homeomorph.continuous_toFun
uliftFunctorCompForgetIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopCat instCategory CategoryTheory.types CategoryTheory.Functor.comp uliftFunctor CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftFunctor uliftFunctorCompForgetIso	—	—
uliftFunctorCompForgetIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopCat instCategory CategoryTheory.types CategoryTheory.Functor.comp uliftFunctor CategoryTheory.forget ContinuousMap carrier str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.uliftFunctor uliftFunctorCompForgetIso	—	—
uliftFunctorObjHomeo_naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj TopCat instCategory uliftFunctor carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike uliftFunctorObjHomeo	—	—
uliftFunctorObjHomeo_symm_naturality_apply 📖	mathematical	—	DFunLike.coe Homeomorph carrier CategoryTheory.Functor.obj TopCat instCategory uliftFunctor str EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm uliftFunctorObjHomeo CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map	—	—

---

← Back to Index