English
Assuming a left calculus of fractions, the essSurj property holds for the left map of composable arrows.
Русский
При условии левого исчисления дробей свойство essSurj сохраняется для левой карты составимых стрелок.
LaTeX
$$$[W.HasLeftCalculusOfFractions] (n \\in \\mathbb{N}) \\; \\Rightarrow \\; (L.mapComposableArrows n).EssSurj$$$
Lean4
theorem essSurj_mapComposableArrows_of_hasRightCalculusOfFractions [W.HasRightCalculusOfFractions] (n : ℕ) :
(L.mapComposableArrows n).EssSurj where
mem_essImage
Y := by
have := essSurj L W
induction n with
| zero =>
obtain ⟨Y, rfl⟩ := mk₀_surjective Y
exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩
| succ n hn =>
obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y
obtain ⟨Y', ⟨e⟩⟩ := hn Y
obtain ⟨f', hf'⟩ := exists_rightFraction L W ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)
refine ⟨Y'.precomp f'.f, ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
dsimp at hf' ⊢
simp [← cancel_mono (e.inv.app 0), hf']
