imageForgetAdj — Mathlib

Lean4
/-- `MonoOver.image : Over X ⥤ MonoOver X` is left adjoint to
`MonoOver.forget : MonoOver X ⥤ Over X`
-/
def imageForgetAdj : image ⊣ forget X :=
  Adjunction.mkOfHomEquiv
    {
      homEquiv := fun f g =>
        { toFun := fun k => by
            apply Over.homMk (factorThruImage f.hom ≫ k.left) _
            change (factorThruImage f.hom ≫ k.left) ≫ _ = f.hom
            rw [assoc, Over.w k]
            apply image.fac
          invFun := fun k => by
            refine Over.homMk ?_ ?_
            ·
              exact
                image.lift
                  { I := g.obj.left
                    m := g.arrow
                    e := k.left
                    fac := Over.w k }
            · apply image.lift_fac
          left_inv := fun _ => Subsingleton.elim _ _
          right_inv := fun k => by simp } }
Похожие утверждения