WithInitial and WithTerminal

Given a category C, this file constructs two objects:

1. WithTerminal C, the category built from C by formally adjoining a terminal object.
2. WithInitial C, the category built from C by formally adjoining an initial object.

The terminal resp. initial object is WithTerminal.star resp. WithInitial.star, and the proofs that these are terminal resp. initial are in WithTerminal.star_terminal and WithInitial.star_initial.

The inclusion from C intro WithTerminal C resp. WithInitial C is denoted WithTerminal.incl resp. WithInitial.incl.

The relevant constructions needed for the universal properties of these constructions are:

1. lift, which lifts F : C ⥤ D to a functor from WithTerminal C resp. WithInitial C in the case where an object Z : D is provided satisfying some additional conditions.
2. inclLift shows that the composition of lift with incl is isomorphic to the functor which was lifted.
3. liftUnique provides the uniqueness property of lift.

In addition to this, we provide WithTerminal.map and WithInitial.map providing the functoriality of these constructions with respect to functors on the base categories.

inductive CategoryTheory.WithTerminal (C : Type u) : Type u

• of: {C : Type u} → C → CategoryTheory.WithTerminal C
• star: {C : Type u} → CategoryTheory.WithTerminal C

Formally adjoin a terminal object to a category.

instance CategoryTheory.instInhabitedWithTerminal : {a : Type u_1} → Inhabited (CategoryTheory.WithTerminal a)

inductive CategoryTheory.WithInitial (C : Type u) : Type u

• of: {C : Type u} → C → CategoryTheory.WithInitial C
• star: {C : Type u} → CategoryTheory.WithInitial C

Formally adjoin an initial object to a category.

instance CategoryTheory.instInhabitedWithInitial : {a : Type u_1} → Inhabited (CategoryTheory.WithInitial a)

def CategoryTheory.WithTerminal.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Type v

Morphisms for WithTerminal C.

def CategoryTheory.WithTerminal.id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal C) : CategoryTheory.WithTerminal.Hom X X

Identity morphisms for WithTerminal C.

def CategoryTheory.WithTerminal.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} {Z : CategoryTheory.WithTerminal C} : CategoryTheory.WithTerminal.Hom X Y → CategoryTheory.WithTerminal.Hom Y Z → CategoryTheory.WithTerminal.Hom X Z

Composition of morphisms for WithTerminal C.

instance CategoryTheory.WithTerminal.instCategoryWithTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, u} (CategoryTheory.WithTerminal C)

def CategoryTheory.WithTerminal.down {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y) : X ⟶ Y

Helper function for typechecking.

@[simp]

theorem CategoryTheory.WithTerminal.down_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithTerminal.of X)) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.WithTerminal.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y) (g : CategoryTheory.WithTerminal.of Y ⟶ CategoryTheory.WithTerminal.of Z) : CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithTerminal.down f) (CategoryTheory.WithTerminal.down g)

theorem CategoryTheory.WithTerminal.false_of_from_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.of X) : False

def CategoryTheory.WithTerminal.incl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.WithTerminal C)

The inclusion from C into WithTerminal C.

instance CategoryTheory.WithTerminal.instFullWithTerminalInstCategoryWithTerminalIncl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Full CategoryTheory.WithTerminal.incl

instance CategoryTheory.WithTerminal.instFaithfulWithTerminalInstCategoryWithTerminalIncl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Faithful CategoryTheory.WithTerminal.incl

def CategoryTheory.WithTerminal.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.WithTerminal C) (CategoryTheory.WithTerminal D)

Map WithTerminal with respect to a functor F : C ⥤ D.

instance CategoryTheory.WithTerminal.instUniqueHomWithTerminalToQuiverToCategoryStructInstCategoryWithTerminalStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} : Unique (X ⟶ CategoryTheory.WithTerminal.star)

def CategoryTheory.WithTerminal.starTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.IsTerminal CategoryTheory.WithTerminal.star

WithTerminal.star is terminal.

@[simp]

theorem CategoryTheory.WithTerminal.lift_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.lift F M hM).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z

@[simp]

theorem CategoryTheory.WithTerminal.lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) : (CategoryTheory.WithTerminal.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => M x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z

def CategoryTheory.WithTerminal.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D

Lift a functor F : C ⥤ D to WithTerminal C ⥤ D.

@[simp]

theorem CategoryTheory.WithTerminal.inclLift_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : C) : (CategoryTheory.WithTerminal.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)

@[simp]

theorem CategoryTheory.WithTerminal.inclLift_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : C) : (CategoryTheory.WithTerminal.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.WithTerminal.inclLift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl (CategoryTheory.WithTerminal.lift F M hM) ≅ F

The isomorphism between incl ⋙ lift F _ _ with F.

@[simp]

theorem CategoryTheory.WithTerminal.liftStar_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : (CategoryTheory.WithTerminal.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z

@[simp]

theorem CategoryTheory.WithTerminal.liftStar_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z

def CategoryTheory.WithTerminal.liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) : (CategoryTheory.WithTerminal.lift F M hM).obj CategoryTheory.WithTerminal.star ≅ Z

The isomorphism between (lift F _ _).obj WithTerminal.star with Z.

theorem CategoryTheory.WithTerminal.lift_map_liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.lift F M hM).map (CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal (CategoryTheory.WithTerminal.incl.obj x))) (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)

def CategoryTheory.WithTerminal.liftUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal (CategoryTheory.WithTerminal.incl.obj x))) hG.hom = CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)) : G ≅ CategoryTheory.WithTerminal.lift F M hM

The uniqueness of lift.

@[simp]

theorem CategoryTheory.WithTerminal.liftToTerminal_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminal F hZ).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z

@[simp]

theorem CategoryTheory.WithTerminal.liftToTerminal_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) : (CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => CategoryTheory.Limits.IsTerminal.from hZ (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z

def CategoryTheory.WithTerminal.liftToTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D

A variant of lift with Z a terminal object.

@[simp]

theorem CategoryTheory.WithTerminal.inclLiftToTerminal_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : C) : (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)

def CategoryTheory.WithTerminal.inclLiftToTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl (CategoryTheory.WithTerminal.liftToTerminal F hZ) ≅ F

A variant of incl_lift with Z a terminal object.

@[simp]

theorem CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom

@[simp]

theorem CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C) : (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv

def CategoryTheory.WithTerminal.liftToTerminalUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) : G ≅ CategoryTheory.WithTerminal.liftToTerminal F hZ

A variant of lift_unique with Z a terminal object.

def CategoryTheory.WithTerminal.homFrom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.WithTerminal.incl.obj X ⟶ CategoryTheory.WithTerminal.star

Constructs a morphism to star from of X.

instance CategoryTheory.WithTerminal.isIso_of_from_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} (f : CategoryTheory.WithTerminal.star ⟶ X) : CategoryTheory.IsIso f

def CategoryTheory.WithInitial.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Type v

Morphisms for WithInitial C.

def CategoryTheory.WithInitial.id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial C) : CategoryTheory.WithInitial.Hom X X

Identity morphisms for WithInitial C.

def CategoryTheory.WithInitial.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} {Z : CategoryTheory.WithInitial C} : CategoryTheory.WithInitial.Hom X Y → CategoryTheory.WithInitial.Hom Y Z → CategoryTheory.WithInitial.Hom X Z

Composition of morphisms for WithInitial C.

instance CategoryTheory.WithInitial.instCategoryWithInitial {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, u} (CategoryTheory.WithInitial C)

def CategoryTheory.WithInitial.down {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y) : X ⟶ Y

Helper function for typechecking.

@[simp]

theorem CategoryTheory.WithInitial.down_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithInitial.of X)) = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.WithInitial.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y) (g : CategoryTheory.WithInitial.of Y ⟶ CategoryTheory.WithInitial.of Z) : CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.down f) (CategoryTheory.WithInitial.down g)

theorem CategoryTheory.WithInitial.false_of_to_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.star) : False

def CategoryTheory.WithInitial.incl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.WithInitial C)

The inclusion of C into WithInitial C.

instance CategoryTheory.WithInitial.instFullWithInitialInstCategoryWithInitialIncl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Full CategoryTheory.WithInitial.incl

instance CategoryTheory.WithInitial.instFaithfulWithInitialInstCategoryWithInitialIncl {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Faithful CategoryTheory.WithInitial.incl

def CategoryTheory.WithInitial.map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.WithInitial C) (CategoryTheory.WithInitial D)

Map WithInitial with respect to a functor F : C ⥤ D.

instance CategoryTheory.WithInitial.instUniqueHomWithInitialToQuiverToCategoryStructInstCategoryWithInitialStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} : Unique (CategoryTheory.WithInitial.star ⟶ X)

def CategoryTheory.WithInitial.starInitial {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.IsInitial CategoryTheory.WithInitial.star

WithInitial.star is initial.

@[simp]

theorem CategoryTheory.WithInitial.lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) : (CategoryTheory.WithInitial.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => M x | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id ((fun X => match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z) CategoryTheory.WithInitial.star)

@[simp]

theorem CategoryTheory.WithInitial.lift_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.lift F M hM).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z

def CategoryTheory.WithInitial.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) : CategoryTheory.Functor (CategoryTheory.WithInitial C) D

Lift a functor F : C ⥤ D to WithInitial C ⥤ D.

@[simp]

theorem CategoryTheory.WithInitial.inclLift_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : C) : (CategoryTheory.WithInitial.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.WithInitial.inclLift_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : C) : (CategoryTheory.WithInitial.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)

def CategoryTheory.WithInitial.inclLift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl (CategoryTheory.WithInitial.lift F M hM) ≅ F

The isomorphism between incl ⋙ lift F _ _ with F.

@[simp]

theorem CategoryTheory.WithInitial.liftStar_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) : (CategoryTheory.WithInitial.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z

@[simp]

theorem CategoryTheory.WithInitial.liftStar_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) : (CategoryTheory.WithInitial.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z

def CategoryTheory.WithInitial.liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) : (CategoryTheory.WithInitial.lift F M hM).obj CategoryTheory.WithInitial.star ≅ Z

The isomorphism between (lift F _ _).obj WithInitial.star with Z.

theorem CategoryTheory.WithInitial.liftStar_lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom ((CategoryTheory.WithInitial.lift F M hM).map (CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)

def CategoryTheory.WithInitial.liftUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp hG.symm.hom (G.map (CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)) : G ≅ CategoryTheory.WithInitial.lift F M hM

The uniqueness of lift.

@[simp]

theorem CategoryTheory.WithInitial.liftToInitial_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitial F hZ).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z

@[simp]

theorem CategoryTheory.WithInitial.liftToInitial_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) : (CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => CategoryTheory.Limits.IsInitial.to hZ (F.obj x) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z

def CategoryTheory.WithInitial.liftToInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.Functor (CategoryTheory.WithInitial C) D

A variant of lift with Z an initial object.

@[simp]

theorem CategoryTheory.WithInitial.inclLiftToInitial_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.WithInitial.inclLiftToInitial_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : C) : (CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)

def CategoryTheory.WithInitial.inclLiftToInitial {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl (CategoryTheory.WithInitial.liftToInitial F hZ) ≅ F

A variant of incl_lift with Z an initial object.

@[simp]

theorem CategoryTheory.WithInitial.liftToInitialUnique_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom

@[simp]

theorem CategoryTheory.WithInitial.liftToInitialUnique_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (X : CategoryTheory.WithInitial C) : (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv

def CategoryTheory.WithInitial.liftToInitialUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) : G ≅ CategoryTheory.WithInitial.liftToInitial F hZ

A variant of lift_unique with Z an initial object.

def CategoryTheory.WithInitial.homTo {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.incl.obj X

Constructs a morphism from star to of X.

instance CategoryTheory.WithInitial.isIso_of_to_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} (f : X ⟶ CategoryTheory.WithInitial.star) : CategoryTheory.IsIso f