# Documentation

Mathlib.CategoryTheory.Category.Pointed

# 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.

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

Turns a point into a pointed type.

Instances For
@[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) :

Alias of Pointed.of.

Turns a point into a pointed type.

Instances For
theorem Pointed.Hom.ext_iff {X : Pointed} {Y : Pointed} (x : ) (y : ) :
x = y x.toFun = y.toFun
theorem Pointed.Hom.ext {X : Pointed} {Y : Pointed} (x : ) (y : ) (toFun : x.toFun = y.toFun) :
x = y
structure Pointed.Hom (X : Pointed) (Y : Pointed) :
• toFun : X.XY.X

the underlying map

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

compatibility with the distinguished points

Morphisms in Pointed.

Instances For
@[simp]
theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) :
= id a

The identity morphism of X : Pointed.

Instances For
@[simp]
theorem Pointed.Hom.comp_toFun {X : Pointed} {Y : Pointed} {Z : Pointed} (f : ) (g : ) :
∀ (a : X.X), = (g.toFun f.toFun) a
def Pointed.Hom.comp {X : Pointed} {Y : Pointed} {Z : Pointed} (f : ) (g : ) :

Composition of morphisms of Pointed.

Instances For
@[simp]
theorem Pointed.Iso.mk_inv_toFun {α : Pointed} {β : Pointed} (e : α.X β.X) (he : e α.point = β.point) (a : β.X) :
Pointed.Hom.toFun ().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 ().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.

Instances For
@[simp]
theorem typeToPointed_map_toFun :
∀ {X Y : Type u} (f : X Y) (a : ), Pointed.Hom.toFun (typeToPointed.map f) a =
@[simp]
theorem typeToPointed_obj_X (X : Type u) :
(typeToPointed.obj X).X =
@[simp]
theorem typeToPointed_obj_point (X : Type u) :
(typeToPointed.obj X).point = none

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

Instances For

typeToPointed is the free functor.

Instances For