mapPushoutAdj — Mathlib

Lean4
/-- `Under.pushout f` is left adjoint to `Under.map f`. -/
@[simps! unit_app counit_app]
def mapPushoutAdj {X Y : C} (f : X ⟶ Y) [HasPushoutsAlong f] : pushout f ⊣ map f :=
  Adjunction.mkOfHomEquiv
    {
      homEquiv := fun x y =>
        { toFun := fun u =>
            Under.homMk (pushout.inl _ _ ≫ u.right) <|
              by
              simp only [map_obj_hom]
              rw [← Under.w u]
              simp only [Functor.const_obj_obj, map_obj_right, Functor.id_obj, pushout_obj, mk_right, mk_hom]
              rw [← assoc, ← assoc, pushout.condition]
          invFun := fun v => Under.homMk (pushout.desc v.right y.hom <| by simp)
          left_inv := fun u => by
            ext
            dsimp
            ext
            · simp
            · simpa using (Under.w u).symm
          right_inv := by cat_disch } }
Похожие утверждения