TopAdj

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean

Statistics

Metric	Count
Definitions toSSetObjI, toTopObjIsoI, toTopHomeo, stdSimplexHomeomorphI, toSSetObj₀Equiv, instMonoidalTopCatSSetToSSet, instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat, instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex	8
Theorems toSSetObj_app_const_one, toSSetObj_app_const_zero, δ_one_toSSetObjI, δ_zero_toSSetObjI, ι₀_whiskerLeft_toSSetObjI_μ, ι₀_whiskerLeft_toSSetObjI_μ_assoc, ι₁_whiskerLeft_toSSetObjI_μ, ι₁_whiskerLeft_toSSetObjI_μ_assoc, toTopHomeo_naturality, toTopHomeo_naturality_apply, toTopHomeo_symm_naturality, toTopHomeo_symm_naturality_apply, toSSetObj₀Equiv_apply, toSSetObj₀Equiv_symm_apply, toSSet_map_const, sSetTopAdj_homEquiv_stdSimplex_zero	16
Total	24

SSet.stdSimplex

Definitions

Name	Category	Theorems
toSSetObjI 📖	CompOp	8 math math: ι₁_whiskerLeft_toSSetObjI_μ, δ_zero_toSSetObjI, toSSetObj_app_const_zero, ι₀_whiskerLeft_toSSetObjI_μ_assoc, δ_one_toSSetObjI, toSSetObj_app_const_one, ι₀_whiskerLeft_toSSetObjI_μ, ι₁_whiskerLeft_toSSetObjI_μ_assoc
toTopObjIsoI 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSSetObj_app_const_one 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category SSet.stdSimplex TopCat TopCat.instCategory TopCat.toSSet TopCat.I toSSetObjI Opposite.op const DFunLike.coe Equiv TopCat.carrier EquivLike.toFunLike Equiv.instEquivLike Equiv.symm TopCat.toSSetObj₀Equiv TopCat.I.instOfNatCarrierOfNatNat_1	—	Equiv.injective SSet.yonedaEquiv_symm_zero SSet.const_comp δ_zero_eq_const δ_zero_toSSetObjI
toSSetObj_app_const_zero 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category SSet.stdSimplex TopCat TopCat.instCategory TopCat.toSSet TopCat.I toSSetObjI Opposite.op const DFunLike.coe Equiv TopCat.carrier EquivLike.toFunLike Equiv.instEquivLike Equiv.symm TopCat.toSSetObj₀Equiv TopCat.I.instOfNatCarrierOfNatNat	—	Equiv.injective SSet.yonedaEquiv_symm_zero SSet.const_comp δ_one_eq_const δ_one_toSSetObjI
δ_one_toSSetObjI 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex TopCat TopCat.instCategory TopCat.toSSet TopCat.I CategoryTheory.CosimplicialObject.δ toSSetObjI SSet.const DFunLike.coe Equiv TopCat.carrier Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm TopCat.toSSetObj₀Equiv TopCat.I.instOfNatCarrierOfNatNat	—	CategoryTheory.Adjunction.homEquiv_naturality_left sSetTopAdj_homEquiv_stdSimplex_zero Real.instIsOrderedRing single_mem_stdSimplex Real.instZeroLEOneClass stdSimplexHomeomorphUnitInterval_zero SimplexCategory.toTopHomeo_naturality_apply Unique.instSubsingleton stdSimplex.map_vertex
δ_zero_toSSetObjI 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj SSet.stdSimplex TopCat TopCat.instCategory TopCat.toSSet TopCat.I CategoryTheory.CosimplicialObject.δ toSSetObjI SSet.const DFunLike.coe Equiv TopCat.carrier Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm TopCat.toSSetObj₀Equiv TopCat.I.instOfNatCarrierOfNatNat_1	—	CategoryTheory.Adjunction.homEquiv_naturality_left sSetTopAdj_homEquiv_stdSimplex_zero Real.instIsOrderedRing single_mem_stdSimplex Real.instZeroLEOneClass stdSimplexHomeomorphUnitInterval_one SimplexCategory.toTopHomeo_naturality_apply Unique.instSubsingleton stdSimplex.map_vertex
ι₀_whiskerLeft_toSSetObjI_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj TopCat TopCat.instCategory TopCat.toSSet CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory SSet.stdSimplex CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct TopCat.instCartesianMonoidalCategory TopCat.I SSet.ι₀ CategoryTheory.MonoidalCategoryStruct.whiskerLeft toSSetObjI CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalTopCatSSetToSSet CategoryTheory.Functor.map TopCat.ι₀	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.μIso_inv CategoryTheory.Functor.Monoidal.μ_δ CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst CategoryTheory.Functor.OplaxMonoidal.δ_fst CategoryTheory.Functor.map_id CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd SSet.ι₀_snd_assoc SSet.const_comp toSSetObj_app_const_zero CategoryTheory.Functor.OplaxMonoidal.δ_snd
ι₀_whiskerLeft_toSSetObjI_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj TopCat TopCat.instCategory TopCat.toSSet CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory SSet.stdSimplex SSet.ι₀ TopCat.I CategoryTheory.MonoidalCategoryStruct.whiskerLeft toSSetObjI CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct TopCat.instCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalTopCatSSetToSSet CategoryTheory.Functor.map TopCat.ι₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_whiskerLeft_toSSetObjI_μ
ι₁_whiskerLeft_toSSetObjI_μ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj TopCat TopCat.instCategory TopCat.toSSet CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory SSet.stdSimplex CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct TopCat.instCartesianMonoidalCategory TopCat.I SSet.ι₁ CategoryTheory.MonoidalCategoryStruct.whiskerLeft toSSetObjI CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalTopCatSSetToSSet CategoryTheory.Functor.map TopCat.ι₁	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Functor.Monoidal.μIso_inv CategoryTheory.Functor.Monoidal.μ_δ CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst CategoryTheory.Functor.OplaxMonoidal.δ_fst CategoryTheory.Functor.map_id CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd SSet.ι₁_snd_assoc SSet.const_comp toSSetObj_app_const_one CategoryTheory.Functor.OplaxMonoidal.δ_snd
ι₁_whiskerLeft_toSSetObjI_μ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.Functor.obj TopCat TopCat.instCategory TopCat.toSSet CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory SSet.stdSimplex SSet.ι₁ TopCat.I CategoryTheory.MonoidalCategoryStruct.whiskerLeft toSSetObjI CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct TopCat.instCartesianMonoidalCategory CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalTopCatSSetToSSet CategoryTheory.Functor.map TopCat.ι₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_whiskerLeft_toSSetObjI_μ

SimplexCategory

Definitions

Name	Category	Theorems
toTopHomeo 📖	CompOp	4 math math: toTopHomeo_symm_naturality, toTopHomeo_naturality_apply, toTopHomeo_symm_naturality_apply, toTopHomeo_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toTopHomeo_naturality 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory CategoryTheory.types TopCat TopCat.instCategory SSet.toTop SSet.stdSimplex Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat DFunLike.coe Homeomorph TopCat.str instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike toTopHomeo CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map stdSimplex.map Real.instIsOrderedRing OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat	—	Real.instIsOrderedRing ULift.up_injective CategoryTheory.Functor.congr_map CategoryTheory.NatTrans.naturality
toTopHomeo_naturality_apply 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory CategoryTheory.types TopCat TopCat.instCategory SSet.toTop SSet.stdSimplex Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat TopCat.str instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike toTopHomeo CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map stdSimplex.map Real.instIsOrderedRing OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat	—	Real.instIsOrderedRing toTopHomeo_naturality
toTopHomeo_symm_naturality 📖	mathematical	—	Set.Elem stdSimplex Real Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat len TopCat.carrier CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory CategoryTheory.types TopCat TopCat.instCategory SSet.toTop SSet.stdSimplex DFunLike.coe Homeomorph instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace TopCat.str EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toTopHomeo stdSimplex.map Real.instIsOrderedRing CategoryTheory.ConcreteCategory.hom OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.Functor.map	—	Real.instIsOrderedRing CategoryTheory.Functor.congr_map CategoryTheory.NatTrans.naturality
toTopHomeo_symm_naturality_apply 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem stdSimplex Real len Real.semiring Real.partialOrder instFintypeToTypeOrderHomFinHAddNatLenOfNat TopCat.carrier CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory CategoryTheory.types TopCat TopCat.instCategory SSet.toTop SSet.stdSimplex instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace TopCat.str EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toTopHomeo stdSimplex.map Real.instIsOrderedRing CategoryTheory.ConcreteCategory.hom OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike instConcreteCategoryOrderHomFinHAddNatLenOfNat ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.Functor.map	—	Real.instIsOrderedRing toTopHomeo_symm_naturality

TopCat

Definitions

Name	Category	Theorems
stdSimplexHomeomorphI 📖	CompOp	—
toSSetObj₀Equiv 📖	CompOp	8 math math: sSetTopAdj_homEquiv_stdSimplex_zero, SSet.stdSimplex.δ_zero_toSSetObjI, toSSetObj₀Equiv_symm_apply, SSet.stdSimplex.toSSetObj_app_const_zero, toSSetObj₀Equiv_apply, SSet.stdSimplex.δ_one_toSSetObjI, toSSet_map_const, SSet.stdSimplex.toSSetObj_app_const_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSSetObj₀Equiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types TopCat instCategory SSet CategoryTheory.Functor.category toSSet Opposite.op carrier EquivLike.toFunLike Equiv.instEquivLike toSSetObj₀Equiv ContinuousMap Set.Elem stdSimplex Real Real.semiring Real.partialOrder SimplexCategory.instFintypeToTypeOrderHomFinHAddNatLenOfNat Opposite.unop instTopologicalSpaceSubtype Set Set.instMembership SimplexCategory.len Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace str ContinuousMap.instFunLike Unique.instInhabited instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex toSSetObjEquiv	—	—
toSSetObj₀Equiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv carrier CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types TopCat instCategory SSet CategoryTheory.Functor.category toSSet Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSSetObj₀Equiv ContinuousMap Set.Elem stdSimplex Real Real.semiring Real.partialOrder SimplexCategory.instFintypeToTypeOrderHomFinHAddNatLenOfNat Opposite.unop instTopologicalSpaceSubtype Set Set.instMembership SimplexCategory.len Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace str toSSetObjEquiv ContinuousMap.instFunLike Unique.instInhabited instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex	—	—
toSSet_map_const 📖	mathematical	—	CategoryTheory.Functor.map TopCat instCategory SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types toSSet const SSet.const CategoryTheory.Functor.obj DFunLike.coe Equiv carrier Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSSetObj₀Equiv	—	—

(root)

Definitions

Name	Category	Theorems
instMonoidalTopCatSSetToSSet 📖	CompOp	4 math math: SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc
instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat 📖	CompOp	1 math math: sSetTopAdj_homEquiv_stdSimplex_zero
instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex 📖	CompOp	2 math math: TopCat.toSSetObj₀Equiv_symm_apply, TopCat.toSSetObj₀Equiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sSetTopAdj_homEquiv_stdSimplex_zero 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom TopCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.Functor.obj SSet CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types SSet.toTop SSet.stdSimplex TopCat.toSSet EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv sSetTopAdj SSet.const TopCat.carrier Opposite.op Equiv.symm TopCat.toSSetObj₀Equiv CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier Unique.instInhabited instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat	—	Equiv.injective Unique.instSubsingleton CategoryTheory.Adjunction.homEquiv_unit TopCat.toSSetObj₀Equiv_symm_apply

---

← Back to Index