ι_comp_coequalizerComparison — Mathlib

English

For HasCoequalizer f g and HasCoequalizer (G.map f) (G.map g), the projection composed with coequalizerComparison and then coequalizer.desc equals G.map (coequalizer.π f g).

Русский

Пусть существуют коэквалайзер f g и коэквалайзер (G.map f) (G.map g). Тогда π (G.map f) (G.map g) ≫ coequalizerComparison f g G = G.map (coequalizer.π f g).

LaTeX

$$$ coequalizer.\\pi (G.map f) (G.map g) \\; \\circ \\; coequalizerComparison f g G = G.map (coequalizer.\\pi f g) $$$

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_coequalizerComparison [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] :
    coequalizer.π _ _ ≫ coequalizerComparison f g G = G.map (coequalizer.π _ _) :=
  coequalizer.π_desc _ _

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