Documentation

Mathlib.CategoryTheory.WithTerminal

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.

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

Formally adjoin a terminal object to a category.

source
instance CategoryTheory.instInhabitedWithTerminal {a✝ : Type u_1} :
Inhabited (CategoryTheory.WithTerminal a✝)
Equations
  • CategoryTheory.instInhabitedWithTerminal = { default := CategoryTheory.WithTerminal.star }
source
inductive CategoryTheory.WithInitial (C : Type u) :
Type u

Formally adjoin an initial object to a category.

source
instance CategoryTheory.instInhabitedWithInitial {a✝ : Type u_1} :
Inhabited (CategoryTheory.WithInitial a✝)
Equations
  • CategoryTheory.instInhabitedWithInitial = { default := CategoryTheory.WithInitial.star }
source
def CategoryTheory.WithTerminal.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Type v

Morphisms for WithTerminal C.

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

Identity morphisms for WithTerminal C.

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

Composition of morphisms for WithTerminal C.

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

Helper function for typechecking.

Equations
source
@[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
source
@[simp]
theorem CategoryTheory.WithTerminal.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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)
source
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
source
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.

Equations
  • CategoryTheory.WithTerminal.incl = { obj := CategoryTheory.WithTerminal.of, map := fun {X Y : C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }
source
instance CategoryTheory.WithTerminal.instFullIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithTerminal.incl.Full
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.WithTerminal.instFaithfulIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithTerminal.incl.Faithful
Equations
  • ⋯ = ⋯
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.map_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) {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) :
(CategoryTheory.WithTerminal.map F).map f = match X, Y, f with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => PUnit.unit | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => PUnit.unit
source
@[simp]
theorem CategoryTheory.WithTerminal.map_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.map F).obj X = match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.WithTerminal.of (F.obj x) | CategoryTheory.WithTerminal.star => CategoryTheory.WithTerminal.star
source
def CategoryTheory.WithTerminal.mapId (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
CategoryTheory.WithTerminal.map (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.WithTerminal C)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.mapId_inv_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.mapId C).inv.app X = (match X with | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of a) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
source
@[simp]
theorem CategoryTheory.WithTerminal.mapId_hom_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.mapId C).hom.app X = (match X with | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of a) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
source
def CategoryTheory.WithTerminal.mapComp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) :
CategoryTheory.WithTerminal.map (F.comp G) ≅ (CategoryTheory.WithTerminal.map F).comp (CategoryTheory.WithTerminal.map G)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.mapComp_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.mapComp F G).inv.app X = (match X with | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj a))) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
source
@[simp]
theorem CategoryTheory.WithTerminal.mapComp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.mapComp F G).hom.app X = (match X with | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj a))) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
source
def CategoryTheory.WithTerminal.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) :
CategoryTheory.WithTerminal.map F ⟶ CategoryTheory.WithTerminal.map G

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.map₂_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) (X : CategoryTheory.WithTerminal C) :
(CategoryTheory.WithTerminal.map₂ η).app X = match X with | CategoryTheory.WithTerminal.of x => η.app x | CategoryTheory.WithTerminal.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star
source
def CategoryTheory.WithTerminal.prelaxfunctor :
CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat

The prelax functor from Cat to Cat defined with WithTerminal.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂ {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) :
CategoryTheory.WithTerminal.prelaxfunctor.map₂ η = CategoryTheory.WithTerminal.map₂ η
source
@[simp]
theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj (C : CategoryTheory.Cat) :
CategoryTheory.WithTerminal.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithTerminal ↑C)
source
@[simp]
theorem CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map {X✝ Y✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑X✝ ↑Y✝) :
CategoryTheory.WithTerminal.prelaxfunctor.map F = CategoryTheory.WithTerminal.map F
source
def CategoryTheory.WithTerminal.pseudofunctor :
CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat

The pseudofunctor from Cat to Cat defined with WithTerminal.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithTerminal.pseudofunctor_toPrelaxFunctor :
CategoryTheory.WithTerminal.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithTerminal.prelaxfunctor
source
@[simp]
theorem CategoryTheory.WithTerminal.pseudofunctor_mapComp {a✝ b✝ c✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑a✝ ↑b✝) (G : CategoryTheory.Functor ↑b✝ ↑c✝) :
CategoryTheory.WithTerminal.pseudofunctor.mapComp F G = CategoryTheory.WithTerminal.mapComp F G
source
@[simp]
theorem CategoryTheory.WithTerminal.pseudofunctor_mapId (C : CategoryTheory.Cat) :
CategoryTheory.WithTerminal.pseudofunctor.mapId C = CategoryTheory.WithTerminal.mapId ↑C
source
instance CategoryTheory.WithTerminal.instUniqueHomStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} :
Unique (X ⟶ CategoryTheory.WithTerminal.star)
Equations
  • CategoryTheory.WithTerminal.instUniqueHomStar = { default := PUnit.unit, uniq := ⋯ }
  • CategoryTheory.WithTerminal.instUniqueHomStar = { default := PUnit.unit, uniq := ⋯ }
source
def CategoryTheory.WithTerminal.starTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.Limits.IsTerminal CategoryTheory.WithTerminal.star

WithTerminal.star is terminal.

Equations
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[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
source
@[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 Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) :
(CategoryTheory.WithTerminal.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, 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
source
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.WithTerminal.incl.comp (CategoryTheory.WithTerminal.lift F M hM) ≅ F

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[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✝)
source
@[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)
source
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.

Equations
source
@[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
source
@[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
source
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.WithTerminal.starTerminal.from (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)
source
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.WithTerminal.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.WithTerminal.starTerminal.from (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.

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
source
@[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
source
@[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 Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) :
(CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
source
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.WithTerminal.incl.comp (CategoryTheory.WithTerminal.liftToTerminal F hZ) ≅ F

A variant of incl_lift with Z a terminal object.

Equations
source
@[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✝)
source
@[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)
source
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.WithTerminal.incl.comp 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.

Equations
source
@[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.WithTerminal.incl.comp 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
source
@[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.WithTerminal.incl.comp 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
source
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.

Equations
source
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
Equations
  • ⋯ = ⋯
source
def CategoryTheory.WithInitial.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Type v

Morphisms for WithInitial C.

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

Identity morphisms for WithInitial C.

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

Composition of morphisms for WithInitial C.

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

Helper function for typechecking.

Equations
source
@[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
source
@[simp]
theorem CategoryTheory.WithInitial.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y 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)
source
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
source
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.

Equations
  • CategoryTheory.WithInitial.incl = { obj := CategoryTheory.WithInitial.of, map := fun {X Y : C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }
source
instance CategoryTheory.WithInitial.instFullIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithInitial.incl.Full
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.WithInitial.instFaithfulIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.WithInitial.incl.Faithful
Equations
  • ⋯ = ⋯
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.map_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) {X Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) :
(CategoryTheory.WithInitial.map F).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => PUnit.unit | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => PUnit.unit
source
@[simp]
theorem CategoryTheory.WithInitial.map_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.map F).obj X = match X with | CategoryTheory.WithInitial.of x => CategoryTheory.WithInitial.of (F.obj x) | CategoryTheory.WithInitial.star => CategoryTheory.WithInitial.star
source
def CategoryTheory.WithInitial.mapId (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] :
CategoryTheory.WithInitial.map (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.WithInitial C)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.mapId_inv_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.mapId C).inv.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
source
@[simp]
theorem CategoryTheory.WithInitial.mapId_hom_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.mapId C).hom.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of a) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
source
def CategoryTheory.WithInitial.mapComp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) :
CategoryTheory.WithInitial.map (F.comp G) ≅ (CategoryTheory.WithInitial.map F).comp (CategoryTheory.WithInitial.map G)

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.mapComp_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.mapComp F G).inv.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).inv
source
@[simp]
theorem CategoryTheory.WithInitial.mapComp_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.Category.{u_4, u_2} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.mapComp F G).hom.app X = (match X with | CategoryTheory.WithInitial.of a => CategoryTheory.Iso.refl (CategoryTheory.WithInitial.of (G.obj (F.obj a))) | CategoryTheory.WithInitial.star => CategoryTheory.Iso.refl CategoryTheory.WithInitial.star).hom
source
def CategoryTheory.WithInitial.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) :
CategoryTheory.WithInitial.map F ⟶ CategoryTheory.WithInitial.map G

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.map₂_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) (X : CategoryTheory.WithInitial C) :
(CategoryTheory.WithInitial.map₂ η).app X = match X with | CategoryTheory.WithInitial.of x => η.app x | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
source
def CategoryTheory.WithInitial.prelaxfunctor :
CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat

The prelax functor from Cat to Cat defined with WithInitial.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) :
CategoryTheory.WithInitial.prelaxfunctor.map₂ η = CategoryTheory.WithInitial.map₂ η
source
@[simp]
theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map {X✝ Y✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑X✝ ↑Y✝) :
CategoryTheory.WithInitial.prelaxfunctor.map F = CategoryTheory.WithInitial.map F
source
@[simp]
theorem CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj (C : CategoryTheory.Cat) :
CategoryTheory.WithInitial.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithInitial ↑C)
source
def CategoryTheory.WithInitial.pseudofunctor :
CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat

The pseudofunctor from Cat to Cat defined with WithInitial.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.WithInitial.pseudofunctor_mapId (C : CategoryTheory.Cat) :
CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.WithInitial.mapId ↑C
source
@[simp]
theorem CategoryTheory.WithInitial.pseudofunctor_mapComp {a✝ b✝ c✝ : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑a✝ ↑b✝) (G : CategoryTheory.Functor ↑b✝ ↑c✝) :
CategoryTheory.WithInitial.pseudofunctor.mapComp F G = CategoryTheory.WithInitial.mapComp F G
source
@[simp]
theorem CategoryTheory.WithInitial.pseudofunctor_toPrelaxFunctor :
CategoryTheory.WithInitial.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithInitial.prelaxfunctor
source
instance CategoryTheory.WithInitial.instUniqueHomStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} :
Unique (CategoryTheory.WithInitial.star ⟶ X)
Equations
  • CategoryTheory.WithInitial.instUniqueHomStar = { default := PUnit.unit, uniq := ⋯ }
  • CategoryTheory.WithInitial.instUniqueHomStar = { default := PUnit.unit, uniq := ⋯ }
source
def CategoryTheory.WithInitial.starInitial {C : Type u} [CategoryTheory.Category.{v, u} C] :
CategoryTheory.Limits.IsInitial CategoryTheory.WithInitial.star

WithInitial.star is initial.

Equations
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[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
source
@[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 Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) :
(CategoryTheory.WithInitial.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => M a | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.WithInitial C) => match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z) CategoryTheory.WithInitial.star)
source
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.WithInitial.incl.comp (CategoryTheory.WithInitial.lift F M hM) ≅ F

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[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)
source
@[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✝)
source
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.

Equations
source
@[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
source
@[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
source
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.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
source
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.WithInitial.incl.comp G ≅ F) (hG : G.obj CategoryTheory.WithInitial.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp hG.symm.hom (G.map (CategoryTheory.WithInitial.starInitial.to (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.

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
source
@[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 Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) :
(CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => hZ.to (F.obj a) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
source
@[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
source
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.WithInitial.incl.comp (CategoryTheory.WithInitial.liftToInitial F hZ) ≅ F

A variant of incl_lift with Z an initial object.

Equations
source
@[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✝)
source
@[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)
source
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.WithInitial.incl.comp 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.

Equations
source
@[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.WithInitial.incl.comp 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
source
@[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.WithInitial.incl.comp 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
source
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.

Equations
source
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
Equations
  • ⋯ = ⋯