lift_unique' — Mathlib

English

If F1, F2 : FreeRefl V ⥤ D and their compositions with the quotient functor from V agree, then F1 = F2.

Русский

Если F1, F2: FreeRefl V ⥤ D и их композиции с фактор-функтором от V совпадают, то F1 = F2.

LaTeX

$$$(F1,F2):\ FreeRefl V ⥤ D$,\ h : (quotientFunctor V) ⋙ F1 = (quotientFunctor V) ⋙ F2\quad \Rightarrow\quad F1 = F2$$$

Lean4

/-- This is a specialization of `Quotient.lift_unique'` rather than `Quotient.lift_unique`, hence
the prime in the name. -/
theorem lift_unique' {V} [ReflQuiver V] {D} [Category D] (F₁ F₂ : FreeRefl V ⥤ D)
    (h : quotientFunctor V ⋙ F₁ = quotientFunctor V ⋙ F₂) : F₁ = F₂ :=
  Quotient.lift_unique' (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) _ _ h

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