π_reflexiveCoequalizerIsoCoequalizer_inv

English

The composition coequalizer.π _ _ followed by reflexiveCoequalizerIsoCoequalizer.inv equals colimit.ι F zero.

Русский

Сочетание коэквалиайзера.π и inv изоморфизма равно Iкоlimit.ι F zero.

LaTeX

$$$\\mathrm{coequalizer.\\,\\pi}(F.map left)(F.map right) \\;\\gg\\; (\\mathrm{reflexiveCoequalizerIsoCoequalizer} F).inv = \\mathrm{colimit.\\,ι} F 0$$$

Lean4

@[reassoc (attr := simp)]
theorem π_reflexiveCoequalizerIsoCoequalizer_inv :
    coequalizer.π _ _ ≫ (reflexiveCoequalizerIsoCoequalizer F).inv = colimit.ι F _ :=
  by
  rw [reflexiveCoequalizerIsoCoequalizer]
  simp only [colimit.comp_coconePointUniqueUpToIso_inv, Cofork.ofπ_pt, colimit.cocone_x, Cofork.ofπ_ι_app,
    colimit.cocone_ι]

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