# mathlib3documentation

category_theory.category.Pointed

# The category of pointed types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This defines Pointed, the category of pointed types.

## TODO #

• Monoidal structure
• Upgrade Type_to_Pointed to an equivalence
structure Pointed  :
Type (u+1)
• X : Type ?
• point : self.X

The category of pointed types.

Instances for Pointed
@[protected, instance]
Equations
def Pointed.of {X : Type u_1} (point : X) :

Turns a point into a pointed type.

Equations
@[simp]
theorem Pointed.coe_of {X : Type u_1} (point : X) :
(Pointed.of point) = X
def prod.Pointed {X : Type u_1} (point : X) :

Alias of Pointed.of.

@[protected, instance]
Equations
@[ext]
structure Pointed.hom (X Y : Pointed) :

Morphisms in Pointed.

Instances for Pointed.hom
theorem Pointed.hom.ext {X Y : Pointed} (x y : X.hom Y) (h : x.to_fun = y.to_fun) :
x = y
theorem Pointed.hom.ext_iff {X Y : Pointed} (x y : X.hom Y) :
x = y x.to_fun = y.to_fun
def Pointed.hom.id (X : Pointed) :
X.hom X

The identity morphism of X : Pointed.

Equations
@[simp]
theorem Pointed.hom.id_to_fun (X : Pointed) (a : X) :
.to_fun a = id a
@[protected, instance]
Equations
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
@[simp]
theorem Pointed.hom.comp_to_fun {X Y Z : Pointed} (f : X.hom Y) (g : Y.hom Z) (ᾰ : X) :
(f.comp g).to_fun = (g.to_fun f.to_fun)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem Pointed.iso.mk_inv_to_fun {α β : Pointed} (e : α β) (he : e α.point = β.point) (ᾰ : β) :
he).inv.to_fun = (e.symm) ᾰ
def Pointed.iso.mk {α β : Pointed} (e : α β) (he : e α.point = β.point) :
α β

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

Equations
@[simp]
theorem Pointed.iso.mk_hom_to_fun {α β : Pointed} (e : α β) (he : e α.point = β.point) (ᾰ : α) :
he).hom.to_fun = e ᾰ
@[simp]
theorem Type_to_Pointed_obj_point (X : Type u) :
def Type_to_Pointed  :

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

Equations
@[simp]
theorem Type_to_Pointed_map_to_fun (X Y : Type u) (f : X Y) (o : option X) :
.to_fun o = o
@[simp]
theorem Type_to_Pointed_obj_X (X : Type u) :

Type_to_Pointed is the free functor.

Equations