Homotopy

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

Statistics

Metric	Count
Definitions toSimplicialObjectHomotopy, botEquiv	2
Theorems h₀, h₀_assoc, h₁, h₁_assoc, botEquiv_apply, botEquiv_symm_apply_map	6
Total	8

SSet.Homotopy

Definitions

Name	Category	Theorems
toSimplicialObjectHomotopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.obj SSet.stdSimplex SSet.ι₀ SSet.RelativeMorphism.Homotopy.h Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SSet.RelativeMorphism EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.RelativeMorphism.botEquiv	—	SSet.RelativeMorphism.Homotopy.h₀
h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.obj SSet.stdSimplex SSet.ι₀ SSet.RelativeMorphism.Homotopy.h Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SSet.RelativeMorphism EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.RelativeMorphism.botEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₀
h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.obj SSet.stdSimplex SSet.ι₁ SSet.RelativeMorphism.Homotopy.h Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SSet.RelativeMorphism EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.RelativeMorphism.botEquiv	—	SSet.RelativeMorphism.Homotopy.h₁
h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.typesCartesianMonoidalCategory CategoryTheory.Functor.obj SSet.stdSimplex SSet.ι₁ SSet.RelativeMorphism.Homotopy.h Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SSet.RelativeMorphism EquivLike.toFunLike Equiv.instEquivLike Equiv.symm SSet.RelativeMorphism.botEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₁

SSet.RelativeMorphism

Definitions

Name	Category	Theorems
botEquiv 📖	CompOp	6 math math: botEquiv_symm_apply_map, SSet.Homotopy.h₁_assoc, SSet.Homotopy.h₀, botEquiv_apply, SSet.Homotopy.h₀_assoc, SSet.Homotopy.h₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
botEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv SSet.RelativeMorphism Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet CategoryTheory.Functor.category CategoryTheory.types SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct EquivLike.toFunLike Equiv.instEquivLike botEquiv map	—	—
botEquiv_symm_apply_map 📖	mathematical	—	map Bot.bot SSet.Subcomplex OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.instCompleteLatticeSubfunctor Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder CategoryTheory.Limits.IsInitial.to SSet CategoryTheory.Functor.category CategoryTheory.types SSet.Subcomplex.toSSet SSet.Subcomplex.isInitialBot DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SSet.RelativeMorphism EquivLike.toFunLike Equiv.instEquivLike Equiv.symm botEquiv	—	—

---

← Back to Index