fromRightResolution — Mathlib

Lean4
/-- Given `Φ : LocalizerMorphism W₁ W₂`, `L : C₂ ⥤ D` a localization functor for `W₂` and
a morphism `y : L.obj X₂ ⟶ X₃`, this is the functor which sends `R : Φ.RightResolution d` to
`(isoOfHom L W₂ R.w R.hw).inv ≫ y` in the category `w.CostructuredArrowDownwards y`
where `w` is `TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv`. -/
@[simps]
noncomputable def fromRightResolution :
    Φ.RightResolution X₂ ⥤
      (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv).CostructuredArrowDownwards y
    where
  obj R := CostructuredArrow.mk (Y := StructuredArrow.mk R.w) (StructuredArrow.homMk ((isoOfHom L W₂ R.w R.hw).inv ≫ y))
  map {R R'}
    φ :=
    CostructuredArrow.homMk (StructuredArrow.homMk φ.f)
      (by
        ext
        dsimp
        rw [← assoc, ← cancel_epi (isoOfHom L W₂ R.w R.hw).hom, isoOfHom_hom, isoOfHom_hom_inv_id_assoc, assoc, ←
          L.map_comp_assoc, φ.comm, isoOfHom_hom_inv_id_assoc])
Похожие утверждения