mapMono_id — Mathlib

English

If i′: Δ'' → Δ' and i: Δ' → Δ are mono, then the map on summands composes correctly: mapMono i ≫ mapMono i′ = mapMono (i′ ≫ i).

Русский

Если i′: Δ'' → Δ' и i: Δ' → Δ моно, то отображение на сумманду корректно компонуется: mapMono i ≫ mapMono i′ = mapMono (i′ ≫ i).

LaTeX

$$$mapMono(K,i) \circ mapMono(K,i') = mapMono(K,i'\circ i)$$$

Lean4

theorem mapMono_id : mapMono K (𝟙 Δ) = 𝟙 _ := by
  unfold mapMono
  simp only [eqToHom_refl, dite_eq_ite, if_true]

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