map — Mathlib

English

A path in X is defined as a 1-truncated path in the 1-truncation of X.

Русский

Путь в X определяется как 1-усечённый путь в 1-усечке X.

LaTeX

$$$\\mathrm{Path}(X,n) = \\mathrm{Path}_1(\\mathrm{trunc}_1(X))(n)$$$

Lean4

/-- Maps of `n + 1`-truncated simplicial sets induce maps of paths. -/
def map (f : Path X m) (σ : X ⟶ Y) : Path Y m
    where
  vertex i := σ.app (op ⦋0⦌ₙ ₊ ₁) (f.vertex i)
  arrow i := σ.app (op ⦋1⦌ₙ ₊ ₁) (f.arrow i)
  arrow_src
    i := by
    simp only [← f.arrow_src i]
    exact congr (σ.naturality (tr (δ 1)).op) rfl |>.symm
  arrow_tgt
    i := by
    simp only [← f.arrow_tgt i]
    exact congr (σ.naturality (tr (δ 0)).op) rfl |>.symm

Похожие утверждения