comp_factorThru — Mathlib

English

If J is injective and f: X → Y is mono, then the composition X → Y → J equals the original map g: X → J when factoring g through f; i.e., f ≫ factorThru(g,f) = g.

Русский

Пусть J инъективен, а f: X → Y мономорфизм. Тогда композиция X → Y → J через факторизацию g через f совпадает с исходным г: X → J; то есть f ≫ factorThru(g,f) = g.

LaTeX

$$$$ f \;\text{is mono} \Rightarrow f \;\gg\; \text{factorThru}(g,f) = g.$$$$

Lean4

@[reassoc (attr := simp)]
theorem comp_factorThru {J X Y : C} [Injective J] (g : X ⟶ J) (f : X ⟶ Y) [Mono f] : f ≫ factorThru g f = g :=
  (Injective.factors g f).choose_spec

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