def CategoryTheory.Over.equivalenceOfIsTerminal {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : Over X ≌ C

If X : C is initial, then the under category of X is equivalent to C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_map {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (equivalenceOfIsTerminal hX).inverse.map f = homMk f ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_counitIso {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).counitIso = NatIso.ofComponents (fun (x : C) => Iso.refl (({ obj := fun (Y : C) => mk (hX.from Y), map := fun {X_1 Y : C} (f : X_1 ⟶ Y) => homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp (forget X)).obj x)) ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_functor {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).functor = forget X

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_unitIso {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) : (equivalenceOfIsTerminal hX).unitIso = NatIso.ofComponents (fun (Y : Over X) => isoMk (Iso.refl ((Functor.id (Over X)).obj Y).left) ⋯) ⋯

@[simp]

theorem CategoryTheory.Over.equivalenceOfIsTerminal_inverse_obj {C : Type u_1} [Category.{u_2, u_1} C] {X : C} (hX : Limits.IsTerminal X) (Y : C) : (equivalenceOfIsTerminal hX).inverse.obj Y = mk (hX.from Y)