lift — Mathlib

Lean4
/-- The functor `Localization W ⥤ E` that is induced by a functor `C ⥤ E` which inverts `W`,
when `W` has a left calculus of fractions. -/
noncomputable def lift (F : C ⥤ E) (hF : W.IsInvertedBy F) : Localization W ⥤ E
    where
  obj X := F.obj X
  map {_ _ : C} f := f.map F hF
  map_id := by
    intro (X : C)
    change (Hom.mk (ofHom W (𝟙 X))).map F hF = _
    rw [Hom.map_mk, map_ofHom, F.map_id]
  map_comp := by
    rintro (X Y Z : C) f g
    obtain ⟨f, rfl⟩ := Hom.mk_surjective f
    obtain ⟨g, rfl⟩ := Hom.mk_surjective g
    dsimp
    obtain ⟨z, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction (RightFraction.mk f.s f.hs g.f)
    rw [homMk_comp_homMk f g z fac, Hom.map_mk]
    dsimp at fac ⊢
    have := hF _ g.hs
    have := hF _ z.hs
    rw [← cancel_mono (F.map g.s), assoc, map_comp_map_s, ← cancel_mono (F.map z.s), assoc, assoc, ← F.map_comp, ←
      F.map_comp, map_comp_map_s, fac]
    dsimp
    rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]
Похожие утверждения