fac_lift — Mathlib

English

If for every X, HasColimitsOfShape(F.obj X) H and HasColimitsOfShape C H hold, then HasColimitsOfShape(Grothendieck F) H.

Русский

Если для каждого X выполняются HasColimitsOfShape(F.obj X) H и HasColimitsOfShape C H, то HasColimitsOfShape(Grothendieck F) H.

LaTeX

$$$[\forall X, \mathrm{HasColimitsOfShape}(F.obj X) H] \\ [\mathrm{HasColimitsOfShape} C H] \Rightarrow \mathrm{HasColimitsOfShape}(\mathrm{Grothendieck} F) H.$$$

Lean4

@[reassoc (attr := simp)]
theorem fac_lift {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) : F.e ≫ hF.lift F' = F'.e :=
  (cancel_mono F'.m).1 <| by simp

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