mapMono — Mathlib

English

For the identity morphism on Δ, the corresponding map on the summand is the identity. This is a consistency check that the construction respects identities.

Русский

Для тождества на Δ соответствующее отображение на сумманду есть тождество. Это проверка согласованности с тождеством.

LaTeX

$$$mapMono(K,\mathrm{id}_{Δ}) = \mathrm{id}$$$

Lean4

/-- A monomorphism `i : Δ' ⟶ Δ` induces a morphism `K.X Δ.len ⟶ K.X Δ'.len` which
is the identity if `Δ = Δ'`, the differential on the complex `K` if `i = δ 0`, and
zero otherwise. -/
def mapMono (K : ChainComplex C ℕ) {Δ' Δ : SimplexCategory} (i : Δ' ⟶ Δ) [Mono i] : K.X Δ.len ⟶ K.X Δ'.len :=
  by
  by_cases Δ = Δ'
  · exact eqToHom (by congr)
  · by_cases Isδ₀ i
    · exact K.d Δ.len Δ'.len
    · exact 0

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