map_epi_on_summand_id — Mathlib

English

A specialization of the map_epi_on_summand_id result for the Γ₀ construction: the induced map on summands via a mono epi factorization equals the map induced by the mono epi itself.

Русский

Уточнение результата map_epi_on_summand_id для Γ₀: индуцированное отображение на сумманд через факторизацию через эпиморфизм и мономорфизм равно отображению самим эпиморфизмом.

LaTeX

$$map_epi_on_summand_id(K,e) = map(K,e)$$

Lean4

@[reassoc]
theorem map_epi_on_summand_id {Δ Δ' : SimplexCategory} (e : Δ' ⟶ Δ) [Epi e] :
    ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op Δ)) ≫ (Γ₀.obj K).map e.op =
      ((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.mk e) :=
  by
  simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
    Γ₀.Obj.Termwise.mapMono_id] using id_comp _

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