inverse — Mathlib

Lean4
/-- The function `(W.FunctorsInverting D) ⥤ (W.Localization ⥤ D)` induced by
`Construction.lift`. -/
@[simps!]
def inverse : W.FunctorsInverting D ⥤ W.Localization ⥤ D
    where
  obj G := lift G.obj G.property
  map τ := natTransExtension (eqToHom (by rw [fac]) ≫ τ ≫ eqToHom (by rw [fac]))
  map_id
    G :=
    natTrans_hcomp_injective
      (by
        rw [natTransExtension_hcomp]
        ext X
        simp only [NatTrans.comp_app, eqToHom_app, eqToHom_refl, comp_id, id_comp, NatTrans.hcomp_id_app,
          NatTrans.id_app, Functor.map_id]
        rfl)
  map_comp τ₁
    τ₂ :=
    natTrans_hcomp_injective
      (by
        ext X
        simp only [natTransExtension_hcomp, NatTrans.comp_app, eqToHom_app, eqToHom_refl, id_comp, comp_id,
          NatTrans.hcomp_app, NatTrans.id_app, Functor.map_id, natTransExtension_app, NatTransExtension.app_eq]
        rfl)
Похожие утверждения