essSurj_mapComposableArrows — Mathlib

English

The essSurj property holds for the composable arrows construction under left calculus of fractions.

Русский

Свойство essSurj сохраняется для построения составимых стрелок при левом исчислении дробей.

LaTeX

$$$\\text{essSurj_mapComposableArrows} \\;[W.HasLeftCalculusOfFractions]$$$

Lean4

theorem essSurj_mapComposableArrows [W.HasLeftCalculusOfFractions] (n : ℕ) : (L.mapComposableArrows n).EssSurj :=
  by
  have := essSurj_mapComposableArrows_of_hasRightCalculusOfFractions L.op W.op n
  have := Functor.essSurj_of_iso (L.mapComposableArrowsOpIso n).symm
  exact Functor.essSurj_of_comp_fully_faithful _ (opEquivalence D n).functor.rightOp

Похожие утверждения