mathlib3 documentation

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 #

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

The category of pointed types.

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

Turns a point into a pointed type.

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

Alias of Pointed.of.

source
@[protected, instance]
def Pointed.inhabited  :
inhabited Pointed
Equations
source
@[ext]
structure Pointed.hom (X Y : Pointed) :
Type u

Morphisms in Pointed.

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

The identity morphism of X : Pointed.

Equations
source
@[simp]
theorem Pointed.hom.id_to_fun (X : Pointed) (a : ↥X) :
(Pointed.hom.id X).to_fun a = id a
source
@[protected, instance]
def Pointed.hom.inhabited (X : Pointed) :
inhabited (X.hom X)
Equations
source
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
source
@[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) ᾰ
source
@[protected, instance]
def Pointed.large_category  :
category_theory.large_category Pointed
Equations
source
@[protected, instance]
def Pointed.concrete_category  :
category_theory.concrete_category Pointed
Equations
source
@[simp]
theorem Pointed.iso.mk_inv_to_fun {α β : Pointed} (e : ↥α ≃ ↥β) (he : ⇑e α.point = β.point) (ᾰ : ↥β) :
(Pointed.iso.mk e he).inv.to_fun ᾰ = ⇑(e.symm) ᾰ
source
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
source
@[simp]
theorem Pointed.iso.mk_hom_to_fun {α β : Pointed} (e : ↥α ≃ ↥β) (he : ⇑e α.point = β.point) (ᾰ : ↥α) :
(Pointed.iso.mk e he).hom.to_fun ᾰ = ⇑e ᾰ
source
@[simp]
theorem Type_to_Pointed_obj_point (X : Type u) :
(Type_to_Pointed.obj X).point = option.none
source
def Type_to_Pointed  :
Type u ⥤ Pointed

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

Equations
source
@[simp]
theorem Type_to_Pointed_map_to_fun (X Y : Type u) (f : X ⟶ Y) (o : option X) :
(Type_to_Pointed.map f).to_fun o = option.map f o
source
@[simp]
theorem Type_to_Pointed_obj_X (X : Type u) :
↥(Type_to_Pointed.obj X) = option X
source
def Type_to_Pointed_forget_adjunction  :
Type_to_Pointed ⊣ category_theory.forget Pointed

Type_to_Pointed is the free functor.

Equations