The category of pointed types

This defines Pointed, the category of pointed types.

TODO

• Monoidal structure
• Upgrade typeToPointed to an equivalence

structure Pointed : Type (u + 1)

The category of pointed types.

• X : Type u

  the underlying type

• point : self.X

  the distinguished element

instance Pointed.instCoeSortType : CoeSort Pointed (Type u_1)

Equations

• Pointed.instCoeSortType = { coe := Pointed.X }

def Pointed.of {X : Type u_1} (point : X) : Pointed

Turns a point into a pointed type.

Equations

• Pointed.of point = { X := X, point := point }

@[simp]

theorem Pointed.coe_of {X : Type u_1} (point : X) : (of point).X = X

def Prod.Pointed {X : Type u_1} (point : X) : _root_.Pointed

Alias of Pointed.of.

---

Turns a point into a pointed type.

Equations

• @Prod.Pointed = @Pointed.of

instance Pointed.instInhabited : Inhabited Pointed

Equations

• Pointed.instInhabited = { default := Pointed.of ((), ()) }

structure Pointed.Hom (X Y : Pointed) : Type u

Morphisms in Pointed.

• toFun : X.X → Y.X

  the underlying map

• map_point : self.toFun X.point = Y.point

  compatibility with the distinguished points

theorem Pointed.Hom.ext {X Y : Pointed} {x y : X.Hom Y} (toFun : x.toFun = y.toFun) : x = y

def Pointed.Hom.id (X : Pointed) : X.Hom X

The identity morphism of X : Pointed.

Equations

• Pointed.Hom.id X = { toFun := id, map_point := ⋯ }

@[simp]

theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) : (id X).toFun a = _root_.id a

instance Pointed.Hom.instInhabited (X : Pointed) : Inhabited (X.Hom X)

Equations

• Pointed.Hom.instInhabited X = { default := Pointed.Hom.id X }

def Pointed.Hom.comp {X Y Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms of Pointed.

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, map_point := ⋯ }

@[simp]

theorem Pointed.Hom.comp_toFun {X Y Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) (a✝ : X.X) : (f.comp g).toFun a✝ = (g.toFun ∘ f.toFun) a✝

instance Pointed.largeCategory : CategoryTheory.LargeCategory Pointed

Equations

• Pointed.largeCategory = CategoryTheory.Category.mk @Pointed.largeCategory.proof_1 @Pointed.largeCategory.proof_2 @Pointed.largeCategory.proof_3

@[simp]

theorem Pointed.Hom.id_toFun' (X : Pointed) : (CategoryTheory.CategoryStruct.id X).toFun = _root_.id

@[simp]

theorem Pointed.Hom.comp_toFun' {X Y Z : Pointed} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).toFun = g.toFun ∘ f.toFun

instance Pointed.hasForget : CategoryTheory.HasForget Pointed

Equations

• Pointed.hasForget = CategoryTheory.HasForget.mk { obj := Pointed.X, map := @Pointed.Hom.toFun, map_id := Pointed.hasForget.proof_1, map_comp := @Pointed.hasForget.proof_2 }

def Pointed.Iso.mk {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) : α ≅ β

Constructs an isomorphism between pointed types from an equivalence that preserves the point between them.

Equations

• Pointed.Iso.mk e he = { hom := { toFun := ⇑e, map_point := he }, inv := { toFun := ⇑e.symm, map_point := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Pointed.Iso.mk_hom_toFun {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : α.X) : (mk e he).hom.toFun a = e a

@[simp]

theorem Pointed.Iso.mk_inv_toFun {α β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : β.X) : (mk e he).inv.toFun a = e.symm a

def typeToPointed : CategoryTheory.Functor (Type u) Pointed

Option as a functor from types to pointed types. This is the free functor.

Equations

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

@[simp]

theorem typeToPointed_map_toFun {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) (a✝ : Option X✝) : (typeToPointed.map f).toFun a✝ = Option.map f a✝

@[simp]

theorem typeToPointed_obj_point (X : Type u) : (typeToPointed.obj X).point = none

@[simp]

theorem typeToPointed_obj_X (X : Type u) : (typeToPointed.obj X).X = Option X

def typeToPointedForgetAdjunction : typeToPointed ⊣ CategoryTheory.forget Pointed

typeToPointed is the free functor.

Equations

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