cokernelCoforkBiproductFromSubtype

English

There is a canonical cokernel isomorphism between biproduct.fromSubtype f p and ⨁ Subtype.restrict pᶜ f.

Русский

Существует каноническое изоморфизм кокон-конечного типа между biproduct.fromSubtype f p и ⨁ Subtype.restrict pᶜ f.

LaTeX

$$$\\cokernel(\\text{biproduct.fromSubtype } f p) \\cong ⨁ \\text{Subtype.restrict } p^c f$$$

Lean4

/-- The colimit cocone exhibiting `⨁ Subtype.restrict pᶜ f` as the cokernel of
`biproduct.fromSubtype f p` -/
@[simps]
def cokernelCoforkBiproductFromSubtype (p : Set K) : ColimitCocone (parallelPair (biproduct.fromSubtype f p) 0)
    where
  cocone :=
    CokernelCofork.ofπ (biproduct.toSubtype f pᶜ)
      (by
        classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2)
  isColimit :=
    CokernelCofork.IsColimit.ofπ _ _ (fun {_} g _ => biproduct.fromSubtype f pᶜ ≫ g)
      (by
        classical
        intro W g' w
        ext j
        simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]
        split_ifs with h
        · simp
        · replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : p) ≫= w
          simpa using w.symm)
      (by cat_disch)

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