toTop₀ — Mathlib

Lean4
/-- The functor `SimplexCategory ⥤ TopCat.{0}`
associating the topological `n`-simplex to `⦋n⦌ : SimplexCategory`. -/
@[simps obj map]
def toTop₀ : SimplexCategory ⥤ TopCat.{0} where
  obj x := TopCat.of x.toTopObj
  map f := TopCat.ofHom ⟨toTopMap f, by fun_prop⟩
  map_id := by
    classical
    intro Δ
    ext f
    simp [Finset.sum_filter]
  map_comp := fun f g => by
    classical
    ext h : 3
    dsimp
    rw [← Finset.sum_biUnion]
    · apply Finset.sum_congr
      · exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)
      · tauto
    · apply Set.pairwiseDisjoint_filter
Похожие утверждения