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 into 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.

We define corresponding pseudofunctors WithTerminal.pseudofunctor and WithInitial.pseudofunctor from Cat to Cat.

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

Formally adjoin a terminal object to a category.

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

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

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

Formally adjoin an initial object to a category.

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

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

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

Morphisms for WithTerminal C.

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

Identity morphisms for WithTerminal C.

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

Composition of morphisms for WithTerminal C.

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

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

Helper function for typechecking.

@[simp]

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

@[simp]

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

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

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

The inclusion from C into WithTerminal C.

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

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.WithTerminal.map_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) {X Y : WithTerminal C} (f : X ⟶ Y) : (map F).map f = match X, Y, f with | of a, of a_1, f => F.map (down f) | of a, star, x => PUnit.unit | star, star, x => PUnit.unit

def CategoryTheory.WithTerminal.mapId (C : Type u_1) [Category.{u_2, u_1} C] : map (Functor.id C) ≅ Functor.id (WithTerminal C)

A natural isomorphism between the functor map (𝟭 C) and 𝟭 (WithTerminal C).

@[simp]

theorem CategoryTheory.WithTerminal.mapId_hom_app (C : Type u_1) [Category.{u_2, u_1} C] (X : WithTerminal C) : (mapId C).hom.app X = (match X with | of a => Iso.refl (of a) | star => Iso.refl star).hom

@[simp]

theorem CategoryTheory.WithTerminal.mapId_inv_app (C : Type u_1) [Category.{u_2, u_1} C] (X : WithTerminal C) : (mapId C).inv.app X = (match X with | of a => Iso.refl (of a) | star => Iso.refl star).inv

def CategoryTheory.WithTerminal.mapComp {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) : map (F.comp G) ≅ (map F).comp (map G)

A natural isomorphism between the functor map (F ⋙ G) and map F ⋙ map G .

@[simp]

theorem CategoryTheory.WithTerminal.mapComp_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) (X : WithTerminal C) : (mapComp F G).hom.app X = (match X with | of a => Iso.refl (of (G.obj (F.obj a))) | star => Iso.refl star).hom

@[simp]

theorem CategoryTheory.WithTerminal.mapComp_inv_app {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) (X : WithTerminal C) : (mapComp F G).inv.app X = (match X with | of a => Iso.refl (of (G.obj (F.obj a))) | star => Iso.refl star).inv

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

From a natural transformation of functors C ⥤ D, the induced natural transformation of functors WithTerminal C ⥤ WithTerminal D.

@[simp]

theorem CategoryTheory.WithTerminal.map₂_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C D} (η : F ⟶ G) (X : WithTerminal C) : (map₂ η).app X = match X with | of x => η.app x | star => CategoryStruct.id star

def CategoryTheory.WithTerminal.prelaxfunctor : PrelaxFunctor Cat Cat

The prelax functor from Cat to Cat defined with WithTerminal.

@[simp]

theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂ {a✝ b✝ : Cat} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : prelaxfunctor.map₂ η = map₂ η

@[simp]

theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj (C : Cat) : prelaxfunctor.obj C = Cat.of (WithTerminal ↑C)

@[simp]

theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map {X✝ Y✝ : Cat} (F : Functor ↑X✝ ↑Y✝) : prelaxfunctor.map F = map F

def CategoryTheory.WithTerminal.pseudofunctor : Pseudofunctor Cat Cat

The pseudofunctor from Cat to Cat defined with WithTerminal.

@[simp]

theorem CategoryTheory.WithTerminal.pseudofunctor_toPrelaxFunctor : pseudofunctor.toPrelaxFunctor = prelaxfunctor

@[simp]

theorem CategoryTheory.WithTerminal.pseudofunctor_mapComp {a✝ b✝ c✝ : Cat} (F : Functor ↑a✝ ↑b✝) (G : Functor ↑b✝ ↑c✝) : pseudofunctor.mapComp F G = mapComp F G

@[simp]

theorem CategoryTheory.WithTerminal.pseudofunctor_mapId (C : Cat) : pseudofunctor.mapId C = mapId ↑C

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

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

WithTerminal.star is terminal.

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

noncomputable def CategoryTheory.WithTerminal.starIsoTerminal {C : Type u} [Category.{v, u} C] : star ≅ ⊤_ WithTerminal C

The isomorphism between star and an abstract terminal object of WithTerminal C

@[simp]

theorem CategoryTheory.WithTerminal.starIsoTerminal_inv {C : Type u} [Category.{v, u} C] : starIsoTerminal.inv = starTerminal.from (⊤_ WithTerminal C)

@[simp]

theorem CategoryTheory.WithTerminal.starIsoTerminal_hom {C : Type u} [Category.{v, u} C] : starIsoTerminal.hom = Limits.terminalIsTerminal.from star

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

The uniqueness of lift.

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

A variant of lift with Z a terminal object.

@[simp]

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

@[simp]

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

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

A variant of incl_lift with Z a terminal object.

@[simp]

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

@[simp]

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

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

A variant of lift_unique with Z a terminal object.

@[simp]

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

@[simp]

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

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

Constructs a morphism to star from of X.

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

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

A functor WithTerminal C ⥤ D can be seen as an element of the comma category Comma (𝟭 (C ⥤ D)) (const C).

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaObject_left_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) (X : C) : (mkCommaObject F).left.obj X = F.obj (incl.obj X)

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaObject_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) : (mkCommaObject F).right = F.obj star

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaObject_left_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (mkCommaObject F).left.map f = F.map (incl.map f)

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaObject_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) (x : C) : (mkCommaObject F).hom.app x = F.map (starTerminal.from (of x))

def CategoryTheory.WithTerminal.mkCommaMorphism {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithTerminal C) D} (η : F ⟶ G) : mkCommaObject F ⟶ mkCommaObject G

A morphism of functors WithTerminal C ⥤ D gives a morphism between the associated comma objects.

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaMorphism_left_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithTerminal C) D} (η : F ⟶ G) (X : C) : (mkCommaMorphism η).left.app X = η.app (incl.obj X)

@[simp]

theorem CategoryTheory.WithTerminal.mkCommaMorphism_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithTerminal C) D} (η : F ⟶ G) : (mkCommaMorphism η).right = η.app star

def CategoryTheory.WithTerminal.ofCommaObject {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.id (Functor C D)) (Functor.const C)) : Functor (WithTerminal C) D

An element of the comma category Comma (𝟭 (C ⥤ D)) (Functor.const C) can be seen as a functor WithTerminal C ⥤ D.

@[simp]

theorem CategoryTheory.WithTerminal.ofCommaObject_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.id (Functor C D)) (Functor.const C)) {X Y : WithTerminal C} (f : X ⟶ Y) : (ofCommaObject c).map f = match X, Y, f with | of a, of a_1, f => c.left.map (down f) | of x, star, x_1 => c.hom.app x | star, star, x => CategoryStruct.id c.right

@[simp]

theorem CategoryTheory.WithTerminal.ofCommaObject_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.id (Functor C D)) (Functor.const C)) (X : WithTerminal C) : (ofCommaObject c).obj X = match X with | of x => c.left.obj x | star => c.right

def CategoryTheory.WithTerminal.ofCommaMorphism {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {c c' : Comma (Functor.id (Functor C D)) (Functor.const C)} (φ : c ⟶ c') : ofCommaObject c ⟶ ofCommaObject c'

A morphism in Comma (𝟭 (C ⥤ D)) (Functor.const C) gives a morphism between the associated functors WithTerminal C ⥤ D.

@[simp]

theorem CategoryTheory.WithTerminal.ofCommaMorphism_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {c c' : Comma (Functor.id (Functor C D)) (Functor.const C)} (φ : c ⟶ c') (x : WithTerminal C) : (ofCommaMorphism φ).app x = match x with | of x => φ.left.app x | star => φ.right

def CategoryTheory.WithTerminal.equivComma {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] : Functor (WithTerminal C) D ≌ Comma (Functor.id (Functor C D)) (Functor.const C)

The category of functors WithTerminal C ⥤ D is equivalent to the category Comma (𝟭 (C ⥤ D)) (const C) .

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_inverse_obj_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.id (Functor C D)) (Functor.const C)) {X Y : WithTerminal C} (f : X ⟶ Y) : (equivComma.inverse.obj c).map f = match X, Y, f with | of a, of a_1, f => c.left.map (down f) | of x, star, x_1 => c.hom.app x | star, star, x => CategoryStruct.id c.right

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_left_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.id (Functor C D)) (Functor.const C)) (X✝ : C) : (equivComma.counitIso.hom.app X).left.app X✝ = CategoryStruct.id (match incl.obj X✝ with | of x => X.left.obj x | star => X.right)

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_obj_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) : (equivComma.functor.obj F).right = F.obj star

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_unitIso_hom_app_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Functor (WithTerminal C) D) (X✝ : WithTerminal C) : (equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | of x => (Iso.refl (incl.comp X)).app x | star => Iso.refl (X.obj star)).hom

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_map_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Functor (WithTerminal C) D} (η : X✝ ⟶ Y✝) : (equivComma.functor.map η).right = η.app star

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_obj_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) (x : C) : (equivComma.functor.obj F).hom.app x = F.map (starTerminal.from (of x))

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_inverse_obj_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.id (Functor C D)) (Functor.const C)) (X : WithTerminal C) : (equivComma.inverse.obj c).obj X = match X with | of x => c.left.obj x | star => c.right

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_counitIso_hom_app_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.id (Functor C D)) (Functor.const C)) : (equivComma.counitIso.hom.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_unitIso_inv_app_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Functor (WithTerminal C) D) (X✝ : WithTerminal C) : (equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | of x => (Iso.refl (incl.comp X)).app x | star => Iso.refl (X.obj star)).inv

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_inverse_map_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Comma (Functor.id (Functor C D)) (Functor.const C)} (φ : X✝ ⟶ Y✝) (x : WithTerminal C) : (equivComma.inverse.map φ).app x = match x with | of x => φ.left.app x | star => φ.right

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_left_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.id (Functor C D)) (Functor.const C)) (X✝ : C) : (equivComma.counitIso.inv.app X).left.app X✝ = CategoryStruct.id (match incl.obj X✝ with | of x => X.left.obj x | star => X.right)

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_obj_left_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) (X : C) : (equivComma.functor.obj F).left.obj X = F.obj (incl.obj X)

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_counitIso_inv_app_right {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.id (Functor C D)) (Functor.const C)) : (equivComma.counitIso.inv.app X).right = CategoryStruct.id X.right

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_map_left_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Functor (WithTerminal C) D} (η : X✝ ⟶ Y✝) (X : C) : (equivComma.functor.map η).left.app X = η.app (incl.obj X)

@[simp]

theorem CategoryTheory.WithTerminal.equivComma_functor_obj_left_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithTerminal C) D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (equivComma.functor.obj F).left.map f = F.map (incl.map f)

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

Morphisms for WithInitial C.

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

Identity morphisms for WithInitial C.

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

Composition of morphisms for WithInitial C.

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

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

Helper function for typechecking.

@[simp]

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

@[simp]

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

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

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

The inclusion of C into WithInitial C.

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

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

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

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

@[simp]

theorem CategoryTheory.WithInitial.map_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) {X Y : WithInitial C} (f : X ⟶ Y) : (map F).map f = match X, Y, f with | of a, of a_1, f => F.map (down f) | star, of a, x => PUnit.unit | star, star, x => PUnit.unit

@[simp]

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

def CategoryTheory.WithInitial.mapId (C : Type u_1) [Category.{u_2, u_1} C] : map (Functor.id C) ≅ Functor.id (WithInitial C)

A natural isomorphism between the functor map (𝟭 C) and 𝟭 (WithInitial C).

@[simp]

theorem CategoryTheory.WithInitial.mapId_inv_app (C : Type u_1) [Category.{u_2, u_1} C] (X : WithInitial C) : (mapId C).inv.app X = (match X with | of a => Iso.refl (of a) | star => Iso.refl star).inv

@[simp]

theorem CategoryTheory.WithInitial.mapId_hom_app (C : Type u_1) [Category.{u_2, u_1} C] (X : WithInitial C) : (mapId C).hom.app X = (match X with | of a => Iso.refl (of a) | star => Iso.refl star).hom

def CategoryTheory.WithInitial.mapComp {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) : map (F.comp G) ≅ (map F).comp (map G)

A natural isomorphism between the functor map (F ⋙ G) and map F ⋙ map G .

@[simp]

theorem CategoryTheory.WithInitial.mapComp_inv_app {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) (X : WithInitial C) : (mapComp F G).inv.app X = (match X with | of a => Iso.refl (of (G.obj (F.obj a))) | star => Iso.refl star).inv

@[simp]

theorem CategoryTheory.WithInitial.mapComp_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} {E : Type u_2} [Category.{u_3, u_1} D] [Category.{u_4, u_2} E] (F : Functor C D) (G : Functor D E) (X : WithInitial C) : (mapComp F G).hom.app X = (match X with | of a => Iso.refl (of (G.obj (F.obj a))) | star => Iso.refl star).hom

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

From a natural transformation of functors C ⥤ D, the induced natural transformation of functors WithInitial C ⥤ WithInitial D.

@[simp]

theorem CategoryTheory.WithInitial.map₂_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor C D} (η : F ⟶ G) (X : WithInitial C) : (map₂ η).app X = match X with | of x => η.app x | star => CategoryStruct.id star

def CategoryTheory.WithInitial.prelaxfunctor : PrelaxFunctor Cat Cat

The prelax functor from Cat to Cat defined with WithInitial.

@[simp]

theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ {a✝ b✝ : Cat} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : prelaxfunctor.map₂ η = map₂ η

@[simp]

theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map {X✝ Y✝ : Cat} (F : Functor ↑X✝ ↑Y✝) : prelaxfunctor.map F = map F

@[simp]

theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj (C : Cat) : prelaxfunctor.obj C = Cat.of (WithInitial ↑C)

def CategoryTheory.WithInitial.pseudofunctor : Pseudofunctor Cat Cat

The pseudofunctor from Cat to Cat defined with WithInitial.

@[simp]

theorem CategoryTheory.WithInitial.pseudofunctor_mapId (C : Cat) : pseudofunctor.mapId C = mapId ↑C

@[simp]

theorem CategoryTheory.WithInitial.pseudofunctor_mapComp {a✝ b✝ c✝ : Cat} (F : Functor ↑a✝ ↑b✝) (G : Functor ↑b✝ ↑c✝) : pseudofunctor.mapComp F G = mapComp F G

@[simp]

theorem CategoryTheory.WithInitial.pseudofunctor_toPrelaxFunctor : pseudofunctor.toPrelaxFunctor = prelaxfunctor

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

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

WithInitial.star is initial.

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

noncomputable def CategoryTheory.WithInitial.starIsoInitial {C : Type u} [Category.{v, u} C] : star ≅ ⊥_ WithInitial C

The isomorphism between star and an abstract initial object of WithInitial C

@[simp]

theorem CategoryTheory.WithInitial.starIsoInitial_inv {C : Type u} [Category.{v, u} C] : starIsoInitial.inv = Limits.initialIsInitial.to star

@[simp]

theorem CategoryTheory.WithInitial.starIsoInitial_hom {C : Type u} [Category.{v, u} C] : starIsoInitial.hom = starInitial.to (⊥_ WithInitial C)

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

The uniqueness of lift.

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

A variant of lift with Z an initial object.

@[simp]

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

@[simp]

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

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

A variant of incl_lift with Z an initial object.

@[simp]

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

@[simp]

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

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

A variant of lift_unique with Z an initial object.

@[simp]

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

@[simp]

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

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

Constructs a morphism from star to of X.

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

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

A functor WithInitial C ⥤ D can be seen as an element of the comma category Comma (const C) (𝟭 (C ⥤ D)).

@[simp]

theorem CategoryTheory.WithInitial.mkCommaObject_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) (x : C) : (mkCommaObject F).hom.app x = F.map (starInitial.to (of x))

@[simp]

theorem CategoryTheory.WithInitial.mkCommaObject_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) : (mkCommaObject F).left = F.obj star

@[simp]

theorem CategoryTheory.WithInitial.mkCommaObject_right_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (mkCommaObject F).right.map f = F.map (incl.map f)

@[simp]

theorem CategoryTheory.WithInitial.mkCommaObject_right_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) (X : C) : (mkCommaObject F).right.obj X = F.obj (incl.obj X)

def CategoryTheory.WithInitial.mkCommaMorphism {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithInitial C) D} (η : F ⟶ G) : mkCommaObject F ⟶ mkCommaObject G

A morphism of functors WithInitial C ⥤ D gives a morphism between the associated comma objects.

@[simp]

theorem CategoryTheory.WithInitial.mkCommaMorphism_right_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithInitial C) D} (η : F ⟶ G) (X : C) : (mkCommaMorphism η).right.app X = η.app (incl.obj X)

@[simp]

theorem CategoryTheory.WithInitial.mkCommaMorphism_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F G : Functor (WithInitial C) D} (η : F ⟶ G) : (mkCommaMorphism η).left = η.app star

def CategoryTheory.WithInitial.ofCommaObject {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.const C) (Functor.id (Functor C D))) : Functor (WithInitial C) D

An element of the comma category Comma (Functor.const C) (𝟭 (C ⥤ D)) can be seen as a functor WithInitial C ⥤ D.

@[simp]

theorem CategoryTheory.WithInitial.ofCommaObject_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.const C) (Functor.id (Functor C D))) {X Y : WithInitial C} (f : X ⟶ Y) : (ofCommaObject c).map f = match X, Y, f with | of a, of a_1, f => c.right.map (down f) | star, of a, x => c.hom.app a | star, star, x => CategoryStruct.id c.left

@[simp]

theorem CategoryTheory.WithInitial.ofCommaObject_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.const C) (Functor.id (Functor C D))) (X : WithInitial C) : (ofCommaObject c).obj X = match X with | of x => c.right.obj x | star => c.left

def CategoryTheory.WithInitial.ofCommaMorphism {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {c c' : Comma (Functor.const C) (Functor.id (Functor C D))} (φ : c ⟶ c') : ofCommaObject c ⟶ ofCommaObject c'

A morphism in Comma (Functor.const C) (𝟭 (C ⥤ D)) gives a morphism between the associated functors WithInitial C ⥤ D.

@[simp]

theorem CategoryTheory.WithInitial.ofCommaMorphism_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {c c' : Comma (Functor.const C) (Functor.id (Functor C D))} (φ : c ⟶ c') (x : WithInitial C) : (ofCommaMorphism φ).app x = match x with | of x => φ.right.app x | star => φ.left

def CategoryTheory.WithInitial.equivComma {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] : Functor (WithInitial C) D ≌ Comma (Functor.const C) (Functor.id (Functor C D))

The category of functors WithInitial C ⥤ D is equivalent to the category Comma (const C) (𝟭 (C ⥤ D)).

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_obj_right_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (equivComma.functor.obj F).right.map f = F.map (incl.map f)

@[simp]

theorem CategoryTheory.WithInitial.equivComma_inverse_obj_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.const C) (Functor.id (Functor C D))) (X : WithInitial C) : (equivComma.inverse.obj c).obj X = match X with | of x => c.right.obj x | star => c.left

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_map_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Functor (WithInitial C) D} (η : X✝ ⟶ Y✝) : (equivComma.functor.map η).left = η.app star

@[simp]

theorem CategoryTheory.WithInitial.equivComma_counitIso_hom_app_right_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.const C) (Functor.id (Functor C D))) (X✝ : C) : (equivComma.counitIso.hom.app X).right.app X✝ = CategoryStruct.id (match incl.obj X✝ with | of x => X.right.obj x | star => X.left)

@[simp]

theorem CategoryTheory.WithInitial.equivComma_counitIso_inv_app_right_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.const C) (Functor.id (Functor C D))) (X✝ : C) : (equivComma.counitIso.inv.app X).right.app X✝ = CategoryStruct.id (match incl.obj X✝ with | of x => X.right.obj x | star => X.left)

@[simp]

theorem CategoryTheory.WithInitial.equivComma_unitIso_inv_app_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Functor (WithInitial C) D) (X✝ : WithInitial C) : (equivComma.unitIso.inv.app X).app X✝ = (match X✝ with | of x => (Iso.refl (incl.comp X)).app x | star => Iso.refl (X.obj star)).inv

@[simp]

theorem CategoryTheory.WithInitial.equivComma_unitIso_hom_app_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Functor (WithInitial C) D) (X✝ : WithInitial C) : (equivComma.unitIso.hom.app X).app X✝ = (match X✝ with | of x => (Iso.refl (incl.comp X)).app x | star => Iso.refl (X.obj star)).hom

@[simp]

theorem CategoryTheory.WithInitial.equivComma_inverse_map_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Comma (Functor.const C) (Functor.id (Functor C D))} (φ : X✝ ⟶ Y✝) (x : WithInitial C) : (equivComma.inverse.map φ).app x = match x with | of x => φ.right.app x | star => φ.left

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_obj_hom_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) (x : C) : (equivComma.functor.obj F).hom.app x = F.map (starInitial.to (of x))

@[simp]

theorem CategoryTheory.WithInitial.equivComma_inverse_obj_map {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (c : Comma (Functor.const C) (Functor.id (Functor C D))) {X Y : WithInitial C} (f : X ⟶ Y) : (equivComma.inverse.obj c).map f = match X, Y, f with | of a, of a_1, f => c.right.map (down f) | star, of a, x => c.hom.app a | star, star, x => CategoryStruct.id c.left

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_obj_right_obj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) (X : C) : (equivComma.functor.obj F).right.obj X = F.obj (incl.obj X)

@[simp]

theorem CategoryTheory.WithInitial.equivComma_counitIso_hom_app_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.const C) (Functor.id (Functor C D))) : (equivComma.counitIso.hom.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_obj_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor (WithInitial C) D) : (equivComma.functor.obj F).left = F.obj star

@[simp]

theorem CategoryTheory.WithInitial.equivComma_counitIso_inv_app_left {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (X : Comma (Functor.const C) (Functor.id (Functor C D))) : (equivComma.counitIso.inv.app X).left = CategoryStruct.id X.left

@[simp]

theorem CategoryTheory.WithInitial.equivComma_functor_map_right_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {X✝ Y✝ : Functor (WithInitial C) D} (η : X✝ ⟶ Y✝) (X : C) : (equivComma.functor.map η).right.app X = η.app (incl.obj X)

def CategoryTheory.WithTerminal.opEquiv (C : Type u) [Category.{v, u} C] : (WithTerminal C)ᵒᵖ ≌ WithInitial Cᵒᵖ

The opposite category of WithTerminal C is equivalent to WithInitial Cᵒᵖ.

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_inverse_map (C : Type u) [Category.{v, u} C] {x y : WithInitial Cᵒᵖ} (f : x ⟶ y) : (opEquiv C).inverse.map f = match x, y, f with | WithInitial.of (Opposite.op x), WithInitial.of (Opposite.op y), f => WithInitial.down f | WithInitial.star, WithInitial.of (Opposite.op unop), x => Opposite.op (starTerminal.from (of unop)) | WithInitial.star, WithInitial.star, x => CategoryStruct.id (Opposite.op star)

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_counitIso_inv_app (C : Type u) [Category.{v, u} C] (X : WithInitial Cᵒᵖ) : (opEquiv C).counitIso.inv.app X = (match X with | WithInitial.of x => Iso.refl (WithInitial.of x) | WithInitial.star => Iso.refl WithInitial.star).inv

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_functor_map (C : Type u) [Category.{v, u} C] {x y : (WithTerminal C)ᵒᵖ} (x✝ : x ⟶ y) : (opEquiv C).functor.map x✝ = match x, y, Opposite.unop x✝, x✝ with | Opposite.op (of x), Opposite.op (of y), f, x_1 => (down f).op | Opposite.op star, Opposite.op (of a), x, x_1 => WithInitial.starInitial.to (WithInitial.of (Opposite.op a)) | Opposite.op star, Opposite.op star, x, x_1 => CategoryStruct.id WithInitial.star

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_inverse_obj (C : Type u) [Category.{v, u} C] (x : WithInitial Cᵒᵖ) : (opEquiv C).inverse.obj x = match x with | WithInitial.of x => Opposite.op (of (Opposite.unop x)) | WithInitial.star => Opposite.op star

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_unitIso_hom_app (C : Type u) [Category.{v, u} C] (X : (WithTerminal C)ᵒᵖ) : (opEquiv C).unitIso.hom.app X = (match Opposite.unop X with | of x => Iso.refl (Opposite.op (of x)) | star => Iso.refl (Opposite.op star)).hom

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_functor_obj (C : Type u) [Category.{v, u} C] (x✝ : (WithTerminal C)ᵒᵖ) : (opEquiv C).functor.obj x✝ = match Opposite.unop x✝ with | of x => WithInitial.of (Opposite.op x) | star => WithInitial.star

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_counitIso_hom_app (C : Type u) [Category.{v, u} C] (X : WithInitial Cᵒᵖ) : (opEquiv C).counitIso.hom.app X = (match X with | WithInitial.of x => Iso.refl (WithInitial.of x) | WithInitial.star => Iso.refl WithInitial.star).hom

@[simp]

theorem CategoryTheory.WithTerminal.opEquiv_unitIso_inv_app (C : Type u) [Category.{v, u} C] (X : (WithTerminal C)ᵒᵖ) : (opEquiv C).unitIso.inv.app X = (match Opposite.unop X with | of x => Iso.refl (Opposite.op (of x)) | star => Iso.refl (Opposite.op star)).inv

def CategoryTheory.WithInitial.opEquiv (C : Type u) [Category.{v, u} C] : (WithInitial C)ᵒᵖ ≌ WithTerminal Cᵒᵖ

The opposite category of WithInitial C is equivalent to WithTerminal Cᵒᵖ.

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_functor_map (C : Type u) [Category.{v, u} C] {x y : (WithInitial C)ᵒᵖ} (x✝ : x ⟶ y) : (opEquiv C).functor.map x✝ = match x, y, Opposite.unop x✝, x✝ with | Opposite.op (of x), Opposite.op (of y), f, x_1 => (WithTerminal.down f).op | Opposite.op (of a), Opposite.op star, x, x_1 => WithTerminal.starTerminal.from (WithTerminal.of (Opposite.op a)) | Opposite.op star, Opposite.op star, x, x_1 => CategoryStruct.id WithTerminal.star

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_inverse_obj (C : Type u) [Category.{v, u} C] (x : WithTerminal Cᵒᵖ) : (opEquiv C).inverse.obj x = match x with | WithTerminal.of x => Opposite.op (of (Opposite.unop x)) | WithTerminal.star => Opposite.op star

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_counitIso_hom_app (C : Type u) [Category.{v, u} C] (X : WithTerminal Cᵒᵖ) : (opEquiv C).counitIso.hom.app X = (match X with | WithTerminal.of x => Iso.refl (WithTerminal.of x) | WithTerminal.star => Iso.refl WithTerminal.star).hom

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_unitIso_inv_app (C : Type u) [Category.{v, u} C] (X : (WithInitial C)ᵒᵖ) : (opEquiv C).unitIso.inv.app X = (match Opposite.unop X with | of x => Iso.refl (Opposite.op (of x)) | star => Iso.refl (Opposite.op star)).inv

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_unitIso_hom_app (C : Type u) [Category.{v, u} C] (X : (WithInitial C)ᵒᵖ) : (opEquiv C).unitIso.hom.app X = (match Opposite.unop X with | of x => Iso.refl (Opposite.op (of x)) | star => Iso.refl (Opposite.op star)).hom

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_inverse_map (C : Type u) [Category.{v, u} C] {x y : WithTerminal Cᵒᵖ} (f : x ⟶ y) : (opEquiv C).inverse.map f = match x, y, f with | WithTerminal.of (Opposite.op x), WithTerminal.of (Opposite.op y), f => down f | WithTerminal.of (Opposite.op unop), WithTerminal.star, x => Opposite.op (starInitial.to (of unop)) | WithTerminal.star, WithTerminal.star, x => CategoryStruct.id (Opposite.op star)

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_counitIso_inv_app (C : Type u) [Category.{v, u} C] (X : WithTerminal Cᵒᵖ) : (opEquiv C).counitIso.inv.app X = (match X with | WithTerminal.of x => Iso.refl (WithTerminal.of x) | WithTerminal.star => Iso.refl WithTerminal.star).inv

@[simp]

theorem CategoryTheory.WithInitial.opEquiv_functor_obj (C : Type u) [Category.{v, u} C] (x✝ : (WithInitial C)ᵒᵖ) : (opEquiv C).functor.obj x✝ = match Opposite.unop x✝ with | of x => WithTerminal.of (Opposite.op x) | star => WithTerminal.star