eq_lift_of_comp_eq — Mathlib

English

If a morphism g : X → WidePullback satisfies g ≫ π_j = fs_j for all j and g ≫ base arrows = f, then g is the lift of f with fs and w; i.e., g = lift f fs w.

Русский

Если морфизм g : X → WidePullback удовлетворяет g ≫ π_j = fs_j для всех j и g ≫ base arrows = f, то g есть подъём lift f fs w.

LaTeX

$$$\\big(\\forall j:\\, J,\\; g \\circ \\pi arrows j = fs j\\big) \\land (g \\circ \\text{base arrows} = f) \\Rightarrow g = \\mathrm{lift}(f,fs,w).$$$

Lean4

theorem eq_lift_of_comp_eq (g : X ⟶ widePullback _ _ arrows) :
    (∀ j : J, g ≫ π arrows j = fs j) → g ≫ base arrows = f → g = lift f fs w :=
  by
  intro h1 h2
  apply (limit.isLimit (WidePullbackShape.wideCospan B objs arrows)).uniq (WidePullbackShape.mkCone f fs <| w)
  rintro (_ | _)
  · apply h2
  · apply h1

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