lift_unique' — Mathlib

English

If two lifts F1 and F2 from Quotient r to D have the same composition with the quotient functor, then F1 = F2.

Русский

Если два подъема F1 и F2 из Quotient r в D имеют одинаковую композицию с функтором-кватом, то F1 = F2.

LaTeX

$$$\forall F_1 F_2 : Quotient(r) \to D,\; (\mathrm{functor}\ r) \circ F_1 = (\mathrm{functor}\ r) \circ F_2 \Rightarrow F_1 = F_2.$$$

Lean4

theorem lift_unique' (F₁ F₂ : Quotient r ⥤ D) (h : functor r ⋙ F₁ = functor r ⋙ F₂) : F₁ = F₂ :=
  by
  rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]; swap
  · rintro X Y f g h
    dsimp
    rw [Quotient.sound r h]
  apply lift_unique
  rw [h]

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