uniq — Mathlib

English

Uniqueness of a localization functor: if two functors G1,G2 from W.Localization to D give the same composite with W.Q, then G1 = G2.

Русский

Уникальность локализационной фарнкции: если G1 гам G2: W.Localization ⥤ D дают одинаковые композиции с W.Q, то G1 = G2.

LaTeX

$$$W.Q \circ G_1 = W.Q \circ G_2 \Rightarrow G_1 = G_2$$$

Lean4

theorem uniq (G₁ G₂ : W.Localization ⥤ D) (h : W.Q ⋙ G₁ = W.Q ⋙ G₂) : G₁ = G₂ :=
  by
  suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂
    by
    refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'
  refine Paths.ext_functor ?_ ?_
  · ext X
    cases X
    apply Functor.congr_obj h
  · rintro ⟨X⟩ ⟨Y⟩ (f | ⟨w, hw⟩)
    · simpa only using Functor.congr_hom h f
    · have hw : W.Q.map w = (wIso w hw).hom := rfl
      have hw' := Functor.congr_hom h w
      simp only [Functor.comp_map, hw] at hw'
      refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
      all_goals apply Functor.congr_obj h

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