English
A morphism f in SimplexCategory induces a map toTopMap between the corresponding topological objects.
Русский
Гомоморфизм f в SimplexCategory индуцирует отображение toTopMap между соответствующими топологическими объектами.
LaTeX
$$$\\text{toTopMap}:\\; x^{\\mathrm{top}} \\to y^{\\mathrm{top}}$ defined by $ (toTopMap f)(g)(i) = \\sum_{j \\in \\mathrm{univ}} \\mathbf{1}_{f(j)=i} \\; g(j) $$$
Lean4
/-- A morphism in `SimplexCategory` induces a map on the associated topological spaces. -/
def toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) : y.toTopObj :=
⟨fun i => ∑ j ∈ Finset.univ.filter (f · = i), g j,
by
simp only [toTopObj, Set.mem_setOf]
rw [← Finset.sum_biUnion]
· have hg : ∑ i : ToType x, g i = 1 := g.2
convert hg
simp [Finset.eq_univ_iff_forall]
· convert Set.pairwiseDisjoint_filter _ _ _⟩
