eq_desc_of_comp_eq — Mathlib

English

Another formulation of the same universal property: if g has equalities with injections and head as described, then g equals the descent map.

Русский

Другая форма универсального свойства: если g имеет заданные равенства с инъекциями и головой, тогда g равен Desc-map.

LaTeX

$$$\\forall j:\\, J, ι arrows j \\circ g = fs j \\land head arrows \\circ g = f \\Rightarrow g = \\mathrm{desc}(f,fs,w).$$$

Lean4

theorem eq_desc_of_comp_eq (g : widePushout _ _ arrows ⟶ X) :
    (∀ j : J, ι arrows j ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w :=
  by
  intro h1 h2
  apply (colimit.isColimit (WidePushoutShape.wideSpan B objs arrows)).uniq (WidePushoutShape.mkCocone f fs <| w)
  rintro (_ | _)
  · apply h2
  · apply h1

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