connectedComponentsTypeToCatAdj — Mathlib

Lean4
/-- `typeToCat : Type ⥤ Cat` is right adjoint to `connectedComponents : Cat ⥤ Type` -/
def connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat :=
  Adjunction.mk'
    { homEquiv := fun C X ↦ ConnectedComponents.typeToCatHomEquiv C X
      unit := { app := fun C ↦ ConnectedComponents.functorToDiscrete _ (𝟙 (connectedComponents.obj C)) }
      counit :=
        { app := fun X => ConnectedComponents.liftFunctor _ (𝟙 typeToCat.obj X)
          naturality := fun _ _ _ =>
            funext
              (fun xcc => by
                obtain ⟨x, h⟩ := Quotient.exists_rep xcc
                cat_disch) }
      homEquiv_counit := fun {C X G} => by
        funext cc
        obtain ⟨_, _⟩ := Quotient.exists_rep cc
        cat_disch }
Похожие утверждения