mapPullbackAdj — Mathlib

Lean4
/-- `Over.map f` is left adjoint to `Over.pullback f`. -/
@[simps! unit_app counit_app]
def mapPullbackAdj {X Y : C} (f : X ⟶ Y) [HasPullbacksAlong f] : Over.map f ⊣ pullback f :=
  Adjunction.mkOfHomEquiv
    {
      homEquiv := fun x y =>
        { toFun := fun u => Over.homMk (pullback.lift u.left x.hom <| by simp)
          invFun := fun v => Over.homMk (v.left ≫ pullback.fst _ _) <| by simp [← Over.w v, pullback.condition]
          left_inv := by cat_disch
          right_inv := fun v => by
            ext
            dsimp
            ext
            · simp
            · simpa using (Over.w v).symm } }
Похожие утверждения