π_colimitOfIsReflexivePairIsoCoequalizer_inv

English

Inverse direction preserves π component in the functor-object under reflexive cofork equivalence.

Русский

Обратное направление сохраняет π-компонент в объекте функторa при эквивалентности рефлексивного кофокора.

LaTeX

$$((\mathrm{reflexiveCoforkEquivCofork} F).inverse.obj G).\pi = G.\pi$$

Lean4

@[reassoc (attr := simp)]
theorem π_colimitOfIsReflexivePairIsoCoequalizer_inv :
    coequalizer.π f g ≫ colimitOfIsReflexivePairIsoCoequalizer.inv = colimit.ι (ofIsReflexivePair f g) zero :=
  @π_reflexiveCoequalizerIsoCoequalizer_inv _ _ (ofIsReflexivePair f g) h

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