Here we define pointed categories and pointed groupoids as well as prove some basic lemmas.

class CategoryTheory.PointedCategory (C : Type z) extends CategoryTheory.Category , CategoryTheory.CategoryStruct , Quiver : Type (max (w + 1) z)

A typeclass for pointed categories.

def CategoryTheory.PointedCategory.of (C : Type u_1) (pt : C) [CategoryTheory.Category.{u_2, u_1} C] : CategoryTheory.PointedCategory C

A constructor that makes a pointed category from a category and a point.

Equations

• CategoryTheory.PointedCategory.of C pt = CategoryTheory.PointedCategory.mk pt

structure CategoryTheory.PointedFunctor (C : Type u_1) (D : Type u_2) [cp : CategoryTheory.PointedCategory C] [dp : CategoryTheory.PointedCategory D] extends CategoryTheory.Functor , Prefunctor : Type (max (max (max u_1 u_2) u_3) u_4)

The structure of a functor from C to D along with a morphism from the image of the point of C to the point of D.

def CategoryTheory.PointedFunctor.id (C : Type u_1) [CategoryTheory.PointedCategory C] : CategoryTheory.PointedFunctor C C

The identity PointedFunctor whose underlying functor is the identity functor

Equations

• CategoryTheory.PointedFunctor.id C = { toFunctor := CategoryTheory.Functor.id C, point := CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt }

@[simp]

theorem CategoryTheory.PointedFunctor.id_point (C : Type u_1) [CategoryTheory.PointedCategory C] : (CategoryTheory.PointedFunctor.id C).point = CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt

@[simp]

theorem CategoryTheory.PointedFunctor.id_map (C : Type u_1) [CategoryTheory.PointedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.PointedFunctor.id C).map f = f

@[simp]

theorem CategoryTheory.PointedFunctor.id_obj (C : Type u_1) [CategoryTheory.PointedCategory C] (X : C) : (CategoryTheory.PointedFunctor.id C).obj X = X

def CategoryTheory.PointedFunctor.comp {C : Type u_1} {D : Type u_2} {E : Type u_3} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : CategoryTheory.PointedFunctor C E

Composition of PointedFunctor composes the underlying functors and the point morphisms.

Equations

• F.comp G = { toFunctor := F.comp G.toFunctor, point := CategoryTheory.CategoryStruct.comp (G.map F.point) G.point }

@[simp]

theorem CategoryTheory.PointedFunctor.comp_point {C : Type u_1} {D : Type u_2} {E : Type u_3} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : (F.comp G).point = CategoryTheory.CategoryStruct.comp (G.map F.point) G.point

@[simp]

theorem CategoryTheory.PointedFunctor.comp_map {C : Type u_1} {D : Type u_2} {E : Type u_3} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) : ∀ {X Y : C} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.PointedFunctor.comp_obj {C : Type u_1} {D : Type u_2} {E : Type u_3} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] [CategoryTheory.PointedCategory E] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor D E) (X : C) : (F.comp G).obj X = G.obj (F.obj X)

theorem CategoryTheory.PointedFunctor.congr_func {C : Type u_1} {D : Type u_2} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] {F : CategoryTheory.PointedFunctor C D} {G : CategoryTheory.PointedFunctor C D} (eq : F = G) : F.toFunctor = G.toFunctor

theorem CategoryTheory.PointedFunctor.congr_point {C : Type u_1} {D : Type u_2} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] {F : CategoryTheory.PointedFunctor C D} {G : CategoryTheory.PointedFunctor C D} (eq : F = G) : F.point = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) G.point

theorem CategoryTheory.PointedFunctor.ext {C : Type u_1} {D : Type u_2} [cp : CategoryTheory.PointedCategory C] [CategoryTheory.PointedCategory D] (F : CategoryTheory.PointedFunctor C D) (G : CategoryTheory.PointedFunctor C D) (h_func : F.toFunctor = G.toFunctor) (h_point : F.point = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) G.point) : F = G

The extensionality principle for pointed functors

def CategoryTheory.PCat : Type (max (z + 1) (w + 1) z)

The category of pointed categorys and pointed functors

Equations

• CategoryTheory.PCat = CategoryTheory.Bundled CategoryTheory.PointedCategory

instance CategoryTheory.PCat.instCoeSortType : CoeSort CategoryTheory.PCat (Type u)

Equations

• CategoryTheory.PCat.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.PCat.str (C : CategoryTheory.PCat) : CategoryTheory.PointedCategory ↑C

Equations

• C.str = C.str

def CategoryTheory.PCat.of (C : Type u) [CategoryTheory.PointedCategory C] : CategoryTheory.PCat

Construct a bundled PCat from the underlying type and the typeclass.

Equations

• CategoryTheory.PCat.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.PCat.category : CategoryTheory.LargeCategory CategoryTheory.PCat

Equations

• CategoryTheory.PCat.category = CategoryTheory.Category.mk @CategoryTheory.PCat.category.proof_1 @CategoryTheory.PCat.category.proof_2 @CategoryTheory.PCat.category.proof_3

def CategoryTheory.PCat.forgetPoint : CategoryTheory.Functor CategoryTheory.PCat CategoryTheory.Cat

The functor that takes PCat to Cat by forgetting the points

Equations

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

@[simp]

theorem CategoryTheory.PCat.id_obj {C : CategoryTheory.PCat} (X : ↑C) : (CategoryTheory.CategoryStruct.id C).obj X = X

@[simp]

theorem CategoryTheory.PCat.id_map {C : CategoryTheory.PCat} {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.id C).map f = f

@[simp]

theorem CategoryTheory.PCat.id_toFunctor {C : CategoryTheory.PCat} : (CategoryTheory.CategoryStruct.id C).toFunctor = CategoryTheory.Functor.id ↑C

@[simp]

theorem CategoryTheory.PCat.id_point {C : CategoryTheory.PCat} : (CategoryTheory.CategoryStruct.id C).point = CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt

@[simp]

theorem CategoryTheory.PCat.comp_obj {C : CategoryTheory.PCat} {D : CategoryTheory.PCat} {E : CategoryTheory.PCat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryTheory.CategoryStruct.comp F G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.PCat.comp_map {C : CategoryTheory.PCat} {D : CategoryTheory.PCat} {E : CategoryTheory.PCat} (F : C ⟶ D) (G : D ⟶ E) {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.comp F G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.PCat.comp_toFunctor {C : CategoryTheory.PCat} {D : CategoryTheory.PCat} {E : CategoryTheory.PCat} (F : C ⟶ D) (G : D ⟶ E) : (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.comp G.toFunctor

@[simp]

theorem CategoryTheory.PCat.comp_point {C : CategoryTheory.PCat} {D : CategoryTheory.PCat} {E : CategoryTheory.PCat} (F : C ⟶ D) (G : D ⟶ E) : (CategoryTheory.CategoryStruct.comp F G).point = CategoryTheory.CategoryStruct.comp (G.map F.point) G.point

class CategoryTheory.PointedGroupoid (C : Type z) extends CategoryTheory.Groupoid , CategoryTheory.PointedCategory , CategoryTheory.Category , CategoryTheory.CategoryStruct , Quiver : Type (max (w + 1) z)

The class of pointed groupoids.

def CategoryTheory.PointedGroupoid.of (C : Type u_1) (pt : C) [CategoryTheory.Groupoid C] : CategoryTheory.PointedGroupoid C

A constructor that makes a pointed groupoid from a groupoid and a point.

Equations

• CategoryTheory.PointedGroupoid.of C pt = CategoryTheory.PointedGroupoid.mk pt

def CategoryTheory.PGrpd : Type (max (z + 1) (w + 1) z)

The category of pointed groupoids and pointed functors

Equations

• CategoryTheory.PGrpd = CategoryTheory.Bundled CategoryTheory.PointedGroupoid

instance CategoryTheory.PGrpd.instCoeSortType : CoeSort CategoryTheory.PGrpd (Type u)

Equations

• CategoryTheory.PGrpd.instCoeSortType = { coe := CategoryTheory.Bundled.α }

instance CategoryTheory.PGrpd.str (C : CategoryTheory.PGrpd) : CategoryTheory.PointedGroupoid ↑C

Equations

• C.str = C.str

def CategoryTheory.PGrpd.of (C : Type u) [CategoryTheory.PointedGroupoid C] : CategoryTheory.PGrpd

Construct a bundled PGrpd from the underlying type and the typeclass.

Equations

• CategoryTheory.PGrpd.of C = CategoryTheory.Bundled.of C

def CategoryTheory.PGrpd.fromGrpd (G : CategoryTheory.Grpd) (g : ↑G) : CategoryTheory.PGrpd

Construct a bundled PGrpd from a Grpd and a point

Equations

• CategoryTheory.PGrpd.fromGrpd G g = CategoryTheory.PGrpd.of ↑G

instance CategoryTheory.PGrpd.category : CategoryTheory.LargeCategory CategoryTheory.PGrpd

Equations

• CategoryTheory.PGrpd.category = CategoryTheory.Category.mk @CategoryTheory.PGrpd.category.proof_1 @CategoryTheory.PGrpd.category.proof_2 @CategoryTheory.PGrpd.category.proof_3

def CategoryTheory.PGrpd.forgetPoint : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.Grpd

The functor that takes PGrpd to Grpd by forgetting the points

Equations

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

def CategoryTheory.PGrpd.forgetToCat : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.PCat

This takes PGrpd to PCat

Equations

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

@[simp]

theorem CategoryTheory.PGrpd.id_obj {C : CategoryTheory.PGrpd} (X : ↑C) : (CategoryTheory.CategoryStruct.id C).obj X = X

@[simp]

theorem CategoryTheory.PGrpd.id_map {C : CategoryTheory.PGrpd} {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.id C).map f = f

@[simp]

theorem CategoryTheory.PGrpd.id_toFunctor {C : CategoryTheory.PGrpd} : (CategoryTheory.CategoryStruct.id C).toFunctor = CategoryTheory.Functor.id ↑C

@[simp]

theorem CategoryTheory.PGrpd.id_point {C : CategoryTheory.PGrpd} : (CategoryTheory.CategoryStruct.id C).point = CategoryTheory.CategoryStruct.id CategoryTheory.PointedCategory.pt

@[simp]

theorem CategoryTheory.PGrpd.comp_obj {C : CategoryTheory.PGrpd} {D : CategoryTheory.PGrpd} {E : CategoryTheory.PGrpd} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryTheory.CategoryStruct.comp F G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.PGrpd.comp_map {C : CategoryTheory.PGrpd} {D : CategoryTheory.PGrpd} {E : CategoryTheory.PGrpd} (F : C ⟶ D) (G : D ⟶ E) {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.comp F G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.PGrpd.comp_toFunctor {C : CategoryTheory.PGrpd} {D : CategoryTheory.PGrpd} {E : CategoryTheory.PGrpd} (F : C ⟶ D) (G : D ⟶ E) : (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.comp G.toFunctor

@[simp]

theorem CategoryTheory.PGrpd.comp_point {C : CategoryTheory.PGrpd} {D : CategoryTheory.PGrpd} {E : CategoryTheory.PGrpd} (F : C ⟶ D) (G : D ⟶ E) : (CategoryTheory.CategoryStruct.comp F G).point = CategoryTheory.CategoryStruct.comp (G.map F.point) G.point