hom_eq_desc — Mathlib

English

If g : X → WidePullback satisfies ∀ j, g ≫ π_j = fs j and g ≫ base arrows = f, then g = lift f fs w.

Русский

Если g : X → WidePullback удовлетворяет g ≫ π_j = fs_j и g ≫ base arrows = f, то g = lift f fs w.

LaTeX

$$$(∀ j:\\, J,\\; g ≫ π arrows j = fs j) \\to (g ≫ base arrows = f) \\to g = \\mathrm{lift}(f,fs,w).$$$

Lean4

theorem hom_eq_desc (g : widePushout _ _ arrows ⟶ X) :
    g =
      desc (head arrows ≫ g) (fun j => ι arrows j ≫ g) fun j =>
        by
        rw [← Category.assoc]
        simp :=
  by cat_disch

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