explicitCokernelIso_hom_π — Mathlib

English

For any X, Y in SemiNormedGrp and a morphism f: X ⟶ Y, the composition of explicitCokernelπ with the hom component of the explicitCokernelIso gives the cokernel projection.

Русский

Для любых X, Y в SemiNormedGrp и морфизма f: X ⟶ Y, композиция explicitCokernelπ с гом-компонентой explicitCokernelIso даёт проекцию кокernel.

LaTeX

$$$ explicitCokernelπ f \;\circ (explicitCokernelIso f).hom = \mathrm{cokernel.π} f $$$

Lean4

@[simp]
theorem explicitCokernelIso_hom_π {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    explicitCokernelπ f ≫ (explicitCokernelIso f).hom = cokernel.π _ := by
  simp [explicitCokernelπ, explicitCokernelIso, IsColimit.coconePointUniqueUpToIso]

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