Theorems · Definition · algebraic topology
SSet.stdSimplex.toSSetObjI
SSet.stdSimplex.obj { len := 1 } ⟶ TopCat.toSSet.obj TopCat.IThe canonical morphism Δ[1] ⟶ TopCat.toSSet.obj TopCat.I: by adjunction,
it corresponds to the isomorphism toTopObjIsoI : |Δ[1]| ≅ TopCat.I.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Oppositestatement · cited by 8,081
- CategoryTheory.Iso.homproof · cited by 7,684
- SimplexCategorystatement · cited by 2,204
- TopCatstatement · cited by 1,889
- SSetstatement · cited by 1,283
- SSet.stdSimplexstatement and proof · cited by 499
- CategoryTheory.Adjunction.homEquivproof · cited by 202
- TopCat.Istatement and proof · cited by 64
- TopCat.toSSetstatement · cited by 29
Cited by9
Results whose statement or proof uses this declaration.
- SSet.stdSimplex.toSSetObj_app_const_onestatement and proof · cited by 1
- SSet.stdSimplex.toSSetObj_app_const_zerostatement and proof · cited by 1
- SSet.stdSimplex.δ_one_toSSetObjIstatement · cited by 1
- SSet.stdSimplex.δ_zero_toSSetObjIstatement · cited by 1
- SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μstatement and proof · cited by 1
- SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μstatement and proof · cited by 1
- TopCat.Homotopy.toSSetproof · cited by 0
- SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assocstatement and proof · cited by 0
- SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assocstatement and proof · cited by 0