Theorems · Definition · algebraic topology
TopCat.toSSetObjEquiv
(X : TopCat) → (n : SimplexCategoryᵒᵖ) → (TopCat.toSSet.obj X).obj n ≃ C(↑(stdSimplex ℝ (Fin ((Opposite.unop n).len + 1))), ↑X)
If X : TopCat.{u} and n : SimplexCategoryᵒᵖ,
then (toSSet.obj X).obj n identifies to the type of continuous
maps from the standard simplex stdSimplex ℝ (Fin (n.unop.len + 1)) to X.
- Defined in
- Mathlib.AlgebraicTopology.SingularSet
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement · cited by 25,697
- CategoryTheory.Functor.objstatement · cited by 19,642
- Equivstatement · cited by 8,337
- Oppositestatement and proof · cited by 8,081
- Set.Elemstatement · cited by 7,166
- TopCat.carrierstatement and proof · cited by 3,184
- ContinuousMapstatement · cited by 2,491
- Opposite.unopstatement · cited by 2,231
- SimplexCategorystatement and proof · cited by 2,204
- TopCatstatement and proof · cited by 1,889
- SSetstatement · cited by 1,283
Cited by12
Results whose statement or proof uses this declaration.
- TopCat.toSSetObj₀Equivproof · cited by 18
- TopCat.toSSetObj₁Equivproof · cited by 6
- sSetTopAdj_homEquiv_stdSimplex_zeroproof · cited by 2
- TopCat.toSSetObj₀Equiv_symm_applystatement · cited by 1
- TopCat.toSSetObjEquiv_symm_naturalitystatement · cited by 0
- TopCat.toSSetObjEquiv_δ_applystatement · cited by 0
- TopCat.toSSetObjEquiv_σ_applystatement · cited by 0
- TopCat.toSSetObj₀Equiv_applystatement · cited by 0
- TopCat.toSSetObj₁Equiv_apply_oneproof · cited by 0
- TopCat.toSSetObj₁Equiv_apply_zeroproof · cited by 0
- TopCat.toSSetIsoConstproof · cited by 0
- TopCat.toSSetObjEquiv_naturality_applystatement · cited by 0