ι_colimitOfIsReflexivePairIsoCoequalizer_hom

English

Same as above for another naming/variant of the isomorphism between reflexive pair and its coequalizer.

Русский

То же самое для другого варианта обозначения изоморфизма между рефлексивной парой и её кофеквалиайзером.

LaTeX

$$$\text{colimit.ι} (\text{ofIsReflexivePair f g})\ 0 = \text{coequalizer.π} f g$$$

Lean4

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

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