map_π_preserves_coequalizer_inv_desc

English

If k: G.obj Y → W is compatible with f and g after mapping, then G.map(coequalizer.π f g) then the inverse of the coequalizer iso followed by coequalizer.desc k wk equals k.

Русский

Если отображение k: G.obj Y → W совместимо с f и g после отображения, то композиция G.map(coequalizer.π f g) с обратной стороной изоморфизма коэквалайзера и с описанием coequalizer(desc) равна k.

LaTeX

$$$ G\\big(\\operatorname{coequalizer.\\,π}(f,g)\\big) \\;\\circ\\; (\\operatorname{PreservesCoequalizer.iso} G f g)^{-1} \\;\\circ\\; \\operatorname{coequalizer.desc} k wk \\\\ = \\\\ k. $$$

Lean4

@[reassoc]
theorem map_π_preserves_coequalizer_inv_desc {W : D} (k : G.obj Y ⟶ W) (wk : G.map f ≫ k = G.map g ≫ k) :
    G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k := by
  rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]

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