explicitCokernel_hom_ext — Mathlib

English

extensionality: if explicitCokernelπ f ≫ e1 = explicitCokernelπ f ≫ e2, then e1 = e2.

Русский

расширение: если explicitCokernelπ f ≫ e1 = explicitCokernelπ f ≫ e2, то e1 = e2.

LaTeX

$$$explicitCokernelπ f \\\\circ e_1 = explicitCokernelπ f \\\\circ e_2 \\\\Rightarrow e_1 = e_2.$$$

Lean4

@[ext]
theorem explicitCokernel_hom_ext {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} (e₁ e₂ : explicitCokernel f ⟶ Z)
    (h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂) : e₁ = e₂ :=
  by
  let g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
  have w : f ≫ g = 0 := by simp [g]
  have : e₂ = explicitCokernelDesc w := by apply explicitCokernelDesc_unique; rfl
  rw [this]
  apply explicitCokernelDesc_unique
  exact h

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