mkOfHomEquiv — Mathlib

Lean4
/-- Construct an adjunction between `F` and `G` out of a natural bijection between each
`F.obj X ⟶ Y` and `X ⟶ G.obj Y`. -/
@[simps!]
def mkOfHomEquiv (adj : CoreHomEquiv F G) : F ⊣ G :=
  mk' {
      unit :=
        { app := fun X => (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X))
          naturality := by
            intros
            simp [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right] }
      counit :=
        { app := fun Y => (adj.homEquiv _ _).invFun (𝟙 (G.obj Y))
          naturality := by
            intros
            simp [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm] }
      homEquiv := adj.homEquiv
      homEquiv_unit := fun {X Y f} => by simp [← adj.homEquiv_naturality_right]
      homEquiv_counit := fun {X Y f} => by simp [← adj.homEquiv_naturality_left_symm] }
Похожие утверждения