GroupoidModel.Pointed.Basic

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

source

class CategoryTheory.PointedCategory (C : Type u) extends CategoryTheory.Category.{v, u} C :

Type (max u (v + 1))

A typeclass for pointed categories.

Hom : C → C → Type v
id (X : C) : X ⟶ X
comp {X Y Z : C} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
id_comp {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (CategoryStruct.id X) f = f
comp_id {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (CategoryStruct.id Y) = f
assoc {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)
pt : C

Instances

source

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

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

Instances For

source

structure CategoryTheory.PointedFunctor (C : Type u_1) (D : Type u_2) [cp : PointedCategory C] [dp : PointedCategory D] extends CategoryTheory.Functor C D :

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.

obj : C → D
map {X Y : C} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map_id (X : C) : self.map (CategoryStruct.id X) = CategoryStruct.id (self.obj X)
map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryStruct.comp f g) = CategoryStruct.comp (self.map f) (self.map g)
point : self.obj PointedCategory.pt ⟶ PointedCategory.pt

Instances For

source

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

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 }

Instances For

source

@[simp]

theorem CategoryTheory.PointedFunctor.id_map (C : Type u_1) [PointedCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :

(id C).map f = f

source

@[simp]

theorem CategoryTheory.PointedFunctor.id_point (C : Type u_1) [PointedCategory C] :

(id C).point = CategoryStruct.id PointedCategory.pt

source

@[simp]

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

(id C).obj X = X

source

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

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 }

Instances For

source

@[simp]

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

(F.comp G).obj X = G.obj (F.obj X)

source

@[simp]

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

(F.comp G).map f = G.map (F.map f)

source

@[simp]

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

(F.comp G).point = CategoryStruct.comp (G.map F.point) G.point

source

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

F.toFunctor = G.toFunctor

source

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

F.point = CategoryStruct.comp (eqToHom ⋯) G.point

source

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

F = G

The extensionality principle for pointed functors

source

def CategoryTheory.PCat :

Type (max (u + 1) u (v + 1))

The category of pointed categorys and pointed functors

Equations

CategoryTheory.PCat = CategoryTheory.Bundled CategoryTheory.PointedCategory

Instances For

source

instance CategoryTheory.PCat.instCoeSortType :

CoeSort PCat (Type u)

Equations

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

source

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

PointedCategory ↑C

Equations

C.str = C.str

source

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

PCat

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

Equations

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

Instances For

source

instance CategoryTheory.PCat.category :

LargeCategory PCat

Equations

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

source

def CategoryTheory.PCat.forgetToCat :

Functor PCat 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.

Instances For

source

@[simp]

theorem CategoryTheory.PCat.forgetToCat_obj (x : PCat) :

forgetToCat.obj x = Cat.of ↑x

source

@[simp]

theorem CategoryTheory.PCat.forgetToCat_map {X✝ Y✝ : PCat} (f : X✝ ⟶ Y✝) :

forgetToCat.map f = f.toFunctor

source

@[simp]

theorem CategoryTheory.PCat.id_obj {C : PCat} (X : ↑C) :

(CategoryStruct.id C).obj X = X

source

@[simp]

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

(CategoryStruct.id C).map f = f

source

@[simp]

theorem CategoryTheory.PCat.id_toFunctor {C : PCat} :

(CategoryStruct.id C).toFunctor = Functor.id ↑C

source

@[simp]

theorem CategoryTheory.PCat.id_point {C : PCat} :

(CategoryStruct.id C).point = CategoryStruct.id PointedCategory.pt

source

@[simp]

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

(CategoryStruct.comp F G).obj X = G.obj (F.obj X)

source

@[simp]

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

(CategoryStruct.comp F G).map f = G.map (F.map f)

source

@[simp]

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

(CategoryStruct.comp F G).toFunctor = F.comp G.toFunctor

source

@[simp]

theorem CategoryTheory.PCat.comp_point {C D E : PCat} (F : C ⟶ D) (G : D ⟶ E) :

(CategoryStruct.comp F G).point = CategoryStruct.comp (G.map F.point) G.point

source

theorem CategoryTheory.PCat.eqToHom_hom_aux {C1 C2 : PCat} (x y : ↑C1) (eq : C1 = C2) :

(x ⟶ y) = ((eqToHom eq).obj x ⟶ (eqToHom eq).obj y)

This is the proof of equality used in the eqToHom in PCat.eqToHom_hom

source

theorem CategoryTheory.PCat.eqToHom_hom {C1 C2 : PCat} {x y : ↑C1} (f : x ⟶ y) (eq : C1 = C2) :

(eqToHom eq).map f = cast ⋯ f

This is the turns the hom part of eqToHom functors into a cast

source

theorem CategoryTheory.PCat.map_id_point {C : Type u} [Category.{v, u} C] {F : Functor C PCat} {x : C} :

(F.map (CategoryStruct.id x)).point = eqToHom ⋯

source

theorem CategoryTheory.PCat.eqToHom_toFunctor {P1 P2 : PCat} (eq : P1 = P2) :

(eqToHom eq).toFunctor = eqToHom ⋯

source

theorem CategoryTheory.PCat.eqToHom_point_aux {P1 P2 : PCat} (eq : P1 = P2) :

(eqToHom eq).obj PointedCategory.pt = PointedCategory.pt

This is the proof of equality used in the eqToHom in PointedFunctor.eqToHom_point

source

theorem CategoryTheory.PCat.eqToHom_point {P1 P2 : PCat} (eq : P1 = P2) :

(eqToHom eq).point = eqToHom ⋯

This shows that the point of an eqToHom in PCat is an eqToHom

source

theorem CategoryTheory.PCat.hext {C D : PCat} (hα : ↑C = ↑D) (hstr : HEq C.str D.str) :

C = D

source

theorem CategoryTheory.PCat.hext_iff {C D : PCat} :

↑C = ↑D ∧ HEq C.str D.str ↔ C = D

source

class CategoryTheory.PointedGroupoid (C : Type u) extends CategoryTheory.Groupoid C, CategoryTheory.PointedCategory C :

Type (max u (v + 1))

The class of pointed groupoids.

Hom : C → C → Type v
id (X : C) : X ⟶ X
comp {X Y Z : C} : (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
id_comp {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (CategoryStruct.id X) f = f
comp_id {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (CategoryStruct.id Y) = f
assoc {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)
inv {X Y : C} : (X ⟶ Y) → (Y ⟶ X)
inv_comp {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (inv f) f = CategoryStruct.id Y
comp_inv {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (inv f) = CategoryStruct.id X
pt : C

Instances

source

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

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

Instances For

source

def CategoryTheory.PGrpd :

Type (max (u + 1) u (v + 1))

The category of pointed groupoids and pointed functors

Equations

CategoryTheory.PGrpd = CategoryTheory.Bundled CategoryTheory.PointedGroupoid

Instances For

source

instance CategoryTheory.PGrpd.instCoeSortType :

CoeSort PGrpd (Type u)

Equations

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

source

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

PointedGroupoid ↑C

Equations

C.str = C.str

source

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

PGrpd

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

Equations

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

Instances For

source

def CategoryTheory.PGrpd.ofGrpd (G : Grpd) (pt : ↑G) :

PGrpd

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

Equations

CategoryTheory.PGrpd.ofGrpd G pt = { α := ↑G, str := CategoryTheory.PointedGroupoid.of (↑G) pt }

Instances For

source

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

PGrpd

Construct a bundled PGrpd from a Grpd and a point

Equations

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

Instances For

source

instance CategoryTheory.PGrpd.category :

LargeCategory PGrpd

Equations

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

source

def CategoryTheory.PGrpd.homOf {C D : PGrpd} (F : PointedFunctor ↑C ↑D) :

C ⟶ D

Construct a morphism in PGrpd from the underlying functor

Equations

CategoryTheory.PGrpd.homOf F = F

Instances For

source

def CategoryTheory.PGrpd.forgetToGrpd :

Functor PGrpd 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.

Instances For

source

@[simp]

theorem CategoryTheory.PGrpd.forgetToGrpd_obj (x : PGrpd) :

forgetToGrpd.obj x = Grpd.of ↑x

source

@[simp]

theorem CategoryTheory.PGrpd.forgetToGrpd_map {X✝ Y✝ : PGrpd} (f : X✝ ⟶ Y✝) :

forgetToGrpd.map f = f.toFunctor

source

def CategoryTheory.PGrpd.forgetToPCat :

Functor PGrpd PCat

This takes PGrpd to PCat

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PGrpd.forgetToPCat_obj (x : PGrpd) :

forgetToPCat.obj x = PCat.of ↑x

source

@[simp]

theorem CategoryTheory.PGrpd.forgetToPCat_map {X✝ Y✝ : PGrpd} (f : X✝ ⟶ Y✝) :

forgetToPCat.map f = f

source

@[simp]

theorem CategoryTheory.PGrpd.id_obj {C : PGrpd} (X : ↑C) :

(CategoryStruct.id C).obj X = X

source

@[simp]

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

(CategoryStruct.id C).map f = f

source

@[simp]

theorem CategoryTheory.PGrpd.id_toFunctor {C : PGrpd} :

(CategoryStruct.id C).toFunctor = Functor.id ↑C

source

@[simp]

theorem CategoryTheory.PGrpd.id_point {C : PGrpd} :

(CategoryStruct.id C).point = CategoryStruct.id PointedCategory.pt

source

@[simp]

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

(CategoryStruct.comp F G).obj X = G.obj (F.obj X)

source

@[simp]

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

(CategoryStruct.comp F G).map f = G.map (F.map f)

source

@[simp]

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

(CategoryStruct.comp F G).toFunctor = F.comp G.toFunctor

source

@[simp]

theorem CategoryTheory.PGrpd.comp_point {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) :

(CategoryStruct.comp F G).point = CategoryStruct.comp (G.map F.point) G.point

source

theorem CategoryTheory.PGrpd.map_id_point {C : Type u} [Category.{v, u} C] {F : Functor C PGrpd} {x : C} :

(F.map (CategoryStruct.id x)).point = eqToHom ⋯

source

theorem CategoryTheory.PGrpd.eqToHom_point_aux {P1 P2 : PGrpd} (eq : P1 = P2) :

(eqToHom eq).obj PointedCategory.pt = PointedCategory.pt

This is the proof of equality used in the eqToHom in PGrpd.eqToHom_point

source

theorem CategoryTheory.PGrpd.eqToHom_point {P1 P2 : PGrpd} (eq : P1 = P2) :

(eqToHom eq).point = eqToHom ⋯

This shows that the point of an eqToHom in PGrpd is an eqToHom

source

theorem CategoryTheory.PGrpd.hext {C D : PGrpd} (hα : ↑C = ↑D) (hstr : HEq C.str D.str) :

C = D

source

theorem CategoryTheory.PGrpd.hext_iff {C D : PGrpd} :

↑C = ↑D ∧ HEq C.str D.str ↔ C = D

source

instance CategoryTheory.PGrpd.asSmall (Γ : Type u) [PointedGroupoid Γ] :

PointedGroupoid (AsSmall Γ)

Equations

CategoryTheory.PGrpd.asSmall Γ = CategoryTheory.PointedGroupoid.mk (CategoryTheory.AsSmall.up.obj CategoryTheory.PointedGroupoid.pt)

source

def CategoryTheory.PGrpd.asSmallFunctor :

Functor PGrpd PGrpd

Equations

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

Instances For

source

instance CategoryTheory.PGrpd.instReflectsIsomorphismsGrpdForgetToGrpd :

forgetToGrpd.ReflectsIsomorphisms