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)

• X : Type u

  the underlying type

• point : s.X

  the distinguished element

The category of pointed types.

instance Pointed.instCoeSortPointedType : CoeSort Pointed (Type u_3)

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

Turns a point into a pointed type.

@[simp]

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

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

Alias of Pointed.of.

---

Turns a point into a pointed type.

instance Pointed.instInhabitedPointed : Inhabited Pointed

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

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

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

• toFun : X.X → Y.X

  the underlying map

• map_point : Pointed.Hom.toFun s X.point = Y.point

  compatibility with the distinguished points

Morphisms in Pointed.

@[simp]

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

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

The identity morphism of X : Pointed.

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

@[simp]

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

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

Composition of morphisms of Pointed.

instance Pointed.largeCategory : CategoryTheory.LargeCategory Pointed

instance Pointed.concreteCategory : CategoryTheory.ConcreteCategory Pointed

@[simp]

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

@[simp]

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

def Pointed.Iso.mk {α : Pointed} {β : 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 typeToPointed_map_toFun : ∀ {X Y : Type u} (f : X ⟶ Y) (a : Option X), Pointed.Hom.toFun (typeToPointed.map f) a = Option.map f a

@[simp]

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

@[simp]

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

def typeToPointed : CategoryTheory.Functor (Type u) Pointed

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

def typeToPointedForgetAdjunction : typeToPointed ⊣ CategoryTheory.forget Pointed

typeToPointed is the free functor.