English
Let L: C → D be a localization for W. For any functors F1, F2: D → E and natural transformations τ, τ′: F1 ⇒ F2, if τ and τ′ agree on the image of L, i.e. τ_{L(X)} = τ′_{L(X)} for every X in C, then τ = τ′.
Русский
Пусть L: C → D локализация для W. Для любых функционоров F1, F2: D → E и натуральных трансформаций τ, τ′: F1 ⇒ F2, если они согласованы на образе L, т.е. для каждого X ∈ C выполняется τ_{L(X)} = τ′_{L(X)}, тогда τ = τ′.
LaTeX
$$$\\forall F_1,F_2:D\\to E\\;\\forall \\tau,\\tau':F_1\\Rightarrow F_2\\;\\Big(\\forall X\\in C:\\;\\tau_{L X}=\\tau'_{L X}\\Big) \\Rightarrow \\tau=\\tau'.$$
Lean4
theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} {τ τ' : F₁ ⟶ F₂}
(h : ∀ X : C, τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ' :=
by
haveI := essSurj L W
ext Y
rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]
