hasWideCoequalizers_of_hasColimit_parallelFamily

English

For nonempty J and k : Y → W with a coherence h, the composite f j with wideCoequalizer.π f equals the same result as k after π_desc.

Русский

Для непустого J и k : Y → W с когерентностью h, композиция f j через wideCoequalizer.π f эквивалентна desc(k,h).

LaTeX

$$$\forall j_1,j_2,\ f j_1 ≫ k = f j_2 ≫ k \Rightarrow wideCoequalizer.π f ≫ wideCoequalizer.desc k h = k$$$

Lean4

/-- If `C` has all colimits of diagrams `parallelFamily f`, then it has all wide coequalizers -/
theorem hasWideCoequalizers_of_hasColimit_parallelFamily
    [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, HasColimit (parallelFamily f)] : HasWideCoequalizers.{w} C := fun _ =>
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoParallelFamily F) }

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