English
The map arrow of the localization has essential surjectivity: every arrow in the target category is the image of a left fraction arrow from the source.
Русский
Отображение стрелы локализации имеет существенную сюръективность: каждая стрелка в целевой категории является образом левой дроби из источника.
LaTeX
$$$\operatorname{essSurj}_{L,W}$ where $L$ is a localization functor and $W$ a left calculus of fractions property.$$
Lean4
theorem essSurj_mapArrow : L.mapArrow.EssSurj where
mem_essImage
f := by
have := Localization.essSurj L W
obtain ⟨X, ⟨eX⟩⟩ : ∃ (X : C), Nonempty (L.obj X ≅ f.left) := ⟨_, ⟨L.objObjPreimageIso f.left⟩⟩
obtain ⟨Y, ⟨eY⟩⟩ : ∃ (Y : C), Nonempty (L.obj Y ≅ f.right) := ⟨_, ⟨L.objObjPreimageIso f.right⟩⟩
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L W (eX.hom ≫ f.hom ≫ eY.inv)
refine ⟨Arrow.mk φ.f, ⟨Iso.symm ?_⟩⟩
refine Arrow.isoMk eX.symm (eY.symm ≪≫ Localization.isoOfHom L W φ.s φ.hs) ?_
dsimp
simp only [← cancel_epi eX.hom, Iso.hom_inv_id_assoc, reassoc_of% hφ, MorphismProperty.LeftFraction.map_comp_map_s]
