Uniqueness of strict localization over the original category

Proved

QAlgorithms.Papers.Independent.Intake100.P59.strictLocalization_unique

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $C,D,D^{\prime}$ be categories in fixed compatible universes, and let $W$ be any class of arrows of $C$ . Suppose $L:C\to D$ and $L^{\prime}:C\to D^{\prime}$ invert $W$ and satisfy strict unique factorization: every functor $\Phi:C\to E$ inverting $W$ factors as $\Phi=\Psi\circ L$ in exactly one way, and likewise through $L^{\prime}$ , for every target category $E$ in those universes. There is a unique functor $T:D\to D^{\prime}$ commuting with localization and admitting a strict inverse $S:D^{\prime}\to D$ over $C$ :

T\circ L=L^{\prime},\quad S\circ L^{\prime}=L,\quad S\circ T=\mathrm{id}_D,\quad T\circ S=\mathrm{id}_{D^{\prime}}.

Thus uniqueness is a unique compatible isomorphism, rather than equality of category types.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P59

Formal statement

namespace QAlgorithms.Papers.Independent.Intake100.P59

open CategoryTheory

universe u v uC vC uD vD uE vE

/-- Lemma 3.12, PDF p.9: strict localizations are uniquely isomorphic over C.
The hypotheses quantify strict unique factorization over every target category
in the fixed compatible universes. The inverse equalities are literal equalities
of functors, not just natural isomorphisms. -/
theorem strictLocalization_unique
    {C D D2 : Type u} [Category.{v} C] [Category.{v} D] [Category.{v} D2]
    (W : MorphismProperty C) (L : C ⥤ D) (L2 : C ⥤ D2)
    (hL : ∀ (E : Type u) [Category.{v} E],
      Nonempty (Localization.StrictUniversalPropertyFixedTarget L W E))
    (hL2 : ∀ (E : Type u) [Category.{v} E],
      Nonempty (Localization.StrictUniversalPropertyFixedTarget L2 W E)) :
    ∃! F : D ⥤ D2, L ⋙ F = L2 ∧
      ∃ G : D2 ⥤ D, L2 ⋙ G = L ∧ F ⋙ G = 𝟭 D ∧ G ⋙ F = 𝟭 D2 := by sorry

end QAlgorithms.Papers.Independent.Intake100.P59

Source

Orbifolds as stacks?, arXiv:0806.4160v2, PDF p. 9, Lemma 3.12

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $C,D,D_2$ be categories whose object types all lie in the same universe $u$ and whose morphisms all lie in the same universe $v$ , let $W$ be an arbitrary property of morphisms of $C$ , and let $L:C\to D$ and $L_2:C\to D_2$ be functors. Suppose that, for every category $E$ with object universe $u$ and morphism universe $v$ , each of $L$ and $L_2$ admits a strict universal property for $W$ with target $E$ : the functor sends every morphism satisfying $W$ to an isomorphism, and every functor $H:C\to E$ sending such morphisms to isomorphisms factors uniquely through it by equality of functors. Then there exists exactly one functor $F:D\to D_2$ satisfying the combined condition that $F\circ L=L_2$ and that there exists a functor $G:D_2\to D$ with $G\circ L_2=L$ , $G\circ F=\operatorname{Id}_D$ , and $F\circ G=\operatorname{Id}_{D_2}$ . All four displayed comparisons are equalities of functors. The explicit uniqueness assertion concerns $F$ satisfying this entire combined condition; $G$ is existentially quantified.

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph