essSurj_mapArrow_of_hasRightCalculusOfFractions

English

If L has a localization with W and has right calculus of fractions, then L.mapArrow is essentially surjective.

Русский

Если у L есть локализация с W и правый расчет дробей, тогда L.mapArrow является по сути сюръективным.

LaTeX

$$$L.mapArrow\;\text{EssSurj}$$$

Lean4

theorem essSurj_mapArrow_of_hasRightCalculusOfFractions : L.mapArrow.EssSurj where
  mem_essImage
    f := by
    have := Localization.essSurj_mapArrow L.op W.op
    obtain ⟨g, ⟨e⟩⟩ : ∃ (g : _), Nonempty (L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op) :=
      ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
    exact
      ⟨Arrow.mk g.hom.unop,
        ⟨Arrow.isoMk (Arrow.rightFunc.mapIso e.symm).unop (Arrow.leftFunc.mapIso e.symm).unop
            (Quiver.Hom.op_inj e.inv.w.symm)⟩⟩

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