lift_ι' — Mathlib

English

For a limit fork s of f,g and a morphism k: W → X together with h: k ≫ f = k ≫ g, the lift hs.lift k h satisfies hs.lift k h ≫ s.ι = k. This expresses the defining universal property of the mediating morphism.

Русский

Для предел-форка s пары f,g и морфизма k: W → X, если h: k ≫ f = k ≫ g, то медиатор hs.lift k h удовлетворяет равенству hs.lift k h ≫ s.ι = k.

LaTeX

$$$\text{Let } s \text{ be a fork of } f,g,\ hs:\ IsLimit(s),\ W\text{ ambient. Then for any } k: W \to X\text{ with } k \circ f = k \circ g,\ (Fork.IsLimit.lift\, hs\, k\, h) \circ s.ι = k$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_ι' {s : Fork f g} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) :
    Fork.IsLimit.lift hs k h ≫ Fork.ι s = k :=
  hs.fac _ _

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