mathlib documentation


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.


structure Pointed  :
Type (u+1)
  • X : Type ?
  • point : self.X

The category of pointed types.

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

Turns a point into a pointed type.

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.

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 (X : Pointed) :
X.hom X

The identity morphism of X : Pointed.

theorem Pointed.hom.id_to_fun (X : Pointed) (a : X) :
@[protected, instance]
def Pointed.hom.comp {X Y Z : Pointed} (f : X.hom Y) (g : Y.hom Z) :
X.hom Z

Composition of morphisms of Pointed.

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]
@[protected, instance]
theorem Pointed.iso.mk_inv_to_fun {α β : Pointed} (e : α β) (he : e α.point = β.point) (ᾰ : β) :
( e he).inv.to_fun = (e.symm) ᾰ
def {α β : Pointed} (e : α β) (he : e α.point = β.point) :
α β

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

theorem Pointed.iso.mk_hom_to_fun {α β : Pointed} (e : α β) (he : e α.point = β.point) (ᾰ : α) :
( e he).hom.to_fun = e ᾰ

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

theorem Type_to_Pointed_map_to_fun (X Y : Type u) (f : X Y) (o : option X) :