English
Same as above, expressing compatibility of maps in localization for z1,z2,z3 with h3 under L.
Русский
То же самое, что и выше, про совместимость отображений в локализации для z1,z2,z3 с h3 под L.
LaTeX
$$$\forall {X Y Z : C} (z_1 : W.LeftFraction X Y) (z_2 : W.LeftFraction Y Z) (z_3 : W.LeftFraction z_1.Y' z_2.Y') (h_3 : z_2.f \gg z_3.s = z_1.s \gg z_3.f) (L : C \to D) [L.IsLocalization W],\n z_1.map L (Localization.inverts L W) ≫ z_2.map L (Localization.inverts L W) = (z_1.comp₀ z_2 z_3).map L (Localization.inverts L W)$$$
Lean4
theorem exists_leftFraction {X Y : C} (f : L.obj X ⟶ L.obj Y) :
∃ (φ : W.LeftFraction X Y), f = φ.map L (Localization.inverts L W) :=
by
let E := Localization.uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
let e : _ ⋙ E.functor ≅ L := Localization.compUniqFunctor _ _ _
obtain ⟨f', rfl⟩ : ∃ (f' : E.functor.obj X ⟶ E.functor.obj Y), f = e.inv.app _ ≫ f' ≫ e.hom.app _ :=
⟨e.hom.app _ ≫ f ≫ e.inv.app _, by simp⟩
obtain ⟨g, rfl⟩ := E.functor.map_surjective f'
obtain ⟨g, rfl⟩ := MorphismProperty.LeftFraction.Localization.Hom.mk_surjective g
refine ⟨g, ?_⟩
rw [← MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk,
MorphismProperty.LeftFraction.Localization.homMk_eq g,
g.map_compatibility (MorphismProperty.LeftFraction.Localization.Q W) L, assoc, assoc, Iso.inv_hom_id_app, comp_id,
Iso.inv_hom_id_app_assoc]
