hom_comp_ι — Mathlib

English

For any morphism f: s ⟶ t of forks of f,g, the relation f.hom ≫ t.ι = s.ι holds; i.e., the fork maps respect the fork legs.

Русский

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

LaTeX

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

Lean4

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

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