factorThru_comp — Mathlib

English

For a projective object P and morphisms f: P → X, e: E → X with e epi, the factorThrough of f through e composed with e equals f: factorThru f e ≫ e = f.

Русский

Для проективного объекта P и морфизмов f: P → X, e: E → X с e ― эпиморфизм, композиция factorThru f e с e даёт f: factorThru f e ≫ e = f.

LaTeX

$$$ \\text{factorThru}(f,e) \\; \\; e = f $$$

Lean4

@[reassoc (attr := simp)]
theorem factorThru_comp {P X E : C} [Projective P] (f : P ⟶ X) (e : E ⟶ X) [Epi e] : factorThru f e ≫ e = f :=
  (Projective.factors f e).choose_spec

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