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

@[implicit_reducible]

instance Pointed.instCoeSortType : CoeSort Pointed (Type u_1)

@[reducible, inline]

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

Turns a point into a pointed type.

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.

@[implicit_reducible]

instance Pointed.instInhabited : Inhabited Pointed

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

theorem Pointed.Hom.ext_iff {X Y : Pointed} {x y : X.Hom Y} : x = y ↔ x.toFun = y.toFun

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

The identity morphism of X : Pointed.

@[simp]

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

@[implicit_reducible]

instance Pointed.Hom.instInhabited (X : Pointed) : Inhabited (X.Hom 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.

@[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✝

@[implicit_reducible]

instance Pointed.largeCategory : CategoryTheory.LargeCategory Pointed

@[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

@[implicit_reducible]

instance Pointed.instFunLikeSubtypeForallXEqPoint (X : Pointed) (Y : Pointed) : FunLike { f : X.X → Y.X // f X.point = Y.point } X.X Y.X

@[implicit_reducible]

instance Pointed.hasForget : CategoryTheory.ConcreteCategory Pointed fun (X Y : Pointed) => { f : X.X → Y.X // f X.point = Y.point }

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.

@[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.

@[simp]

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

@[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_X (X : Type u) : (typeToPointed.obj X).X = Option X

def typeToPointedForgetAdjunction : typeToPointed ⊣ CategoryTheory.forget Pointed

typeToPointed is the free functor.