piEquivalenceFunctorDiscrete — Mathlib

Lean4

/-- The equivalence of categories `(J → C) ≌ (Discrete J ⥤ C)`. -/
@[simps]
def piEquivalenceFunctorDiscrete (J : Type u₂) (C : Type u₁) [Category.{v₁} C] : (J → C) ≌ (Discrete J ⥤ C)
    where
  functor :=
    { obj := fun F => Discrete.functor F
      map := fun f => Discrete.natTrans (fun j => f j.as) }
  inverse :=
    { obj := fun F j => F.obj ⟨j⟩
      map := fun f j => f.app ⟨j⟩ }
  unitIso := Iso.refl _
  counitIso :=
    NatIso.ofComponents
      (fun F =>
        (NatIso.ofComponents (fun _ => Iso.refl _)
          (by
            rintro ⟨x⟩ ⟨y⟩ f
            obtain rfl : x = y := Discrete.eq_of_hom f
            obtain rfl : f = 𝟙 _ := rfl
            simp)))
      (by cat_disch)

Похожие утверждения