uniq — Mathlib

English

If F1 and F2 are functors from Localization W to E and Q W composed with F1 equals Q W composed with F2, then F1 = F2.

Русский

Если F1 и F2 — функторы из Localization W в E и Q W ⋙ F1 = Q W ⋙ F2, то F1 = F2.

LaTeX

$$$\forall {C} [\text{Category } C], [\text{Category } E], F_1,F_2 : Localization W \to E,\; h : Q W \circ F_1 = Q W \circ F_2 \,\to\, F_1 = F_2$$$

Lean4

theorem uniq (F₁ F₂ : Localization W ⥤ E) (h : Q W ⋙ F₁ = Q W ⋙ F₂) : F₁ = F₂ :=
  Functor.ext (fun X => Functor.congr_obj h X)
    (by
      rintro (X Y : C) f
      obtain ⟨f, rfl⟩ := Hom.mk_surjective f
      rw [show Hom.mk f = homMk (mk f.f f.s f.hs) by rfl, ← Q_map_comp_Qinv f.f f.s f.hs, F₁.map_comp, F₂.map_comp,
        assoc]
      erw [Functor.congr_hom h f.f]
      rw [assoc, assoc]
      congr 2
      have := inverts W _ f.hs
      rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc, Qiso_hom_inv_id, Functor.map_id, id_comp]
      erw [Functor.congr_hom h.symm f.s]
      dsimp
      rw [assoc, assoc, eqToHom_trans_assoc, eqToHom_refl, id_comp, ← F₁.map_comp, Qiso_hom_inv_id]
      dsimp
      rw [F₁.map_id, comp_id])

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