π_comp_hom — Mathlib

English

For any morphism f: s ⟶ t of Coforks, one has s.π ≫ f.hom = t.π; the leg coequalizes through the morphism.

Русский

Для морфизма f: s ⟶ t между кофорами выполняется s.π ≫ f.hom = t.π; нога кофорка сохраняется под морфизм.

LaTeX

$$$\forall f:\, s\to t,\ s.\pi \circ f.hom = t.\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_hom {s t : Cofork f g} (f : s ⟶ t) : s.π ≫ f.hom = t.π := by cases s; cases t; cases f; aesop

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