cofan_inj_id — Mathlib

English

Let X be a simplicial object with a splitting s. For every natural number n, the injection from the nth summand of the splitting into X_n coincides with the nth structural inclusion ι_n.

Русский

Пусть X — симплициальный объект с разложением s. Для каждого натурального числа n инъекция из n-й составной части разложения в X_n совпадает с инклюзией ι_n.

LaTeX

$$$(s.cofan\;\Delta).\mathrm{inj}(\mathrm{IndexSet.id}(\mathrm{op}\;\langle n\rangle)) = s.\iota n$$$

Lean4

theorem cofan_inj_id (n : ℕ) : (s.cofan _).inj (IndexSet.id (op ⦋n⦌)) = s.ι n := by
  simp [IndexSet.id, IndexSet.e, cofan_inj_eq]

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