English
Given A, B, C, D and compatible maps, the relation between explicitCokernelDesc condb, g, fbb', fdd' is mediated by explicitCokernel.map h and explicitCokernelDesc condd.
Русский
При заданных A,B,C,D и совместимых отображениях, связь между explicitCokernelDesc condb, g, fbb', fdd' устанавливается через explicitCokernel.map h и explicitCokernelDesc condd.
LaTeX
$$$ explicitCokernelDesc condb \circ g = explicitCokernel.map h \circ explicitCokernelDesc condd $$$
Lean4
/-- A special case of `CategoryTheory.Limits.cokernel.map_desc` adapted to `explicitCokernel`. -/
theorem map_desc {A B C D B' D' : SemiNormedGrp.{u}} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D}
{h : fab ≫ fbd = fac ≫ fcd} {fbb' : B ⟶ B'} {fdd' : D ⟶ D'} {condb : fab ≫ fbb' = 0} {condd : fcd ≫ fdd' = 0}
{g : B' ⟶ D'} (h' : fbb' ≫ g = fbd ≫ fdd') :
explicitCokernelDesc condb ≫ g = explicitCokernel.map h ≫ explicitCokernelDesc condd :=
by
delta explicitCokernel.map
simp only [← Category.assoc, ← cancel_epi (explicitCokernelπ fab)]
simp [Category.assoc, explicitCokernelπ_desc, h']
