lift_unique — Mathlib

English

If Φ is a functor from Quotient r to D and its composition with the quotient functor equals F, then Φ is uniquely determined as lift r F H.

Русский

Если Φ — функтор из Quotient r в D и его композиция с Quotient functor равна F, то Φ определяется однозначно как lift r F H.

LaTeX

$$$\forall \Φ:\Quant r ⥤ D,\; (\mathrm{functor}\ r) \circ \Φ = F \Rightarrow \ Φ = \mathrm{lift}\ r F H.$$$

Lean4

theorem lift_unique (Φ : Quotient r ⥤ D) (hΦ : functor r ⋙ Φ = F) : Φ = lift r F H :=
  by
  subst_vars
  fapply Functor.hext
  · rintro X
    dsimp [lift, Functor]
    congr
  · rintro _ _ f
    dsimp [lift, Functor]
    refine Quot.inductionOn f fun _ ↦ ?_
    simp only [heq_eq_eq]
    congr

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