# mathlibdocumentation

category_theory.category.PartialFun

# The category of types with partial functions #

This defines PartialFun, the category of types equipped with partial functions.

This category is classically equivalent to the category of pointed types. The reason it doesn't hold constructively stems from the difference between part and option. Both can model partial functions, but the latter forces a decidable domain.

Precisely, PartialFun_to_Pointed turns a partial function α →. β into a function option α → option β by sending to none the undefined values (and none to none). But being defined is (generally) undecidable while being sent to none is decidable. So it can't be constructive.

## References #

• [nLab, The category of sets and partial functions] (https://ncatlab.org/nlab/show/partial+function)
def PartialFun  :
Type (u_1+1)

The category of types equipped with partial functions.

Equations
Instances for PartialFun
@[protected, instance]
def PartialFun.has_coe_to_sort  :
(Type u_1)
Equations
@[nolint]
def PartialFun.of  :
Type u_1PartialFun

Turns a type into a PartialFun.

Equations
@[simp]
theorem PartialFun.coe_of (X : Type u_1) :
= X
@[protected, instance]
Equations
@[protected, instance]
Equations
def PartialFun.iso.mk {α β : PartialFun} (e : α β) :
α β

Constructs a partial function isomorphism between types from an equivalence between them.

Equations
@[simp]
theorem PartialFun.iso.mk_inv {α β : PartialFun} (e : α β) :
@[simp]
theorem PartialFun.iso.mk_hom {α β : PartialFun} (e : α β) :

The forgetful functor from Type to PartialFun which forgets that the maps are total.

Equations
Instances for Type_to_PartialFun
@[protected, instance]
@[simp]
theorem Pointed_to_PartialFun_map (X Y : Pointed) (f : X Y) (ᾰ : {x // x X.point}) :
= (pfun.to_subtype (λ (x : Y), x Y.point) f.to_fun subtype.val)

The functor which deletes the point of a pointed type. In return, this makes the maps partial. This the computable part of the equivalence PartialFun_equiv_Pointed.

Equations
noncomputable def PartialFun_to_Pointed  :

The functor which maps undefined values to a new point. This makes the maps total and creates pointed types. This the noncomputable part of the equivalence PartialFun_equiv_Pointed. It can't be computable because = option.none is decidable while the domain of a general part isn't.

Equations
@[simp]
theorem PartialFun_to_Pointed_map (X Y : PartialFun) (f : X Y) :
= {to_fun := (λ (a : X), (f a).to_option), map_point := _}
@[simp]
theorem PartialFun_equiv_Pointed_unit_iso_inv_app (X : PartialFun) :
= Pointed_to_PartialFun.map {to_fun := (λ (a : X), option.some , _⟩), map_point := _} Pointed_to_PartialFun.map (Pointed.iso.mk {to_fun := , inv_fun := λ (a : , dite (a = (λ (h : a = , option.none) (λ (h : ¬a = , option.some a, h⟩), left_inv := _, right_inv := _} _).hom (λ (a : ,
@[simp]
theorem PartialFun_equiv_Pointed_inverse_map_get_coe (X Y : Pointed) (f : X Y) (ᾰ : {x // x X.point}) (property : f.to_fun ᾰ.val Y.point) :
.get property) = f.to_fun
@[simp]
theorem PartialFun_equiv_Pointed_inverse_map_dom (X Y : Pointed) (f : X Y) (ᾰ : {x // x X.point}) :
= ¬f.to_fun = Y.point
@[simp]
theorem PartialFun_equiv_Pointed_counit_iso_inv_app_to_fun (X : Pointed) (ᾰ : ((𝟭 Pointed).obj X)) :
= dite (ᾰ = X.point) (λ (h : = X.point), option.none) (λ (h : ¬= X.point), option.some ᾰ, h⟩)
@[simp]
theorem PartialFun_equiv_Pointed_unit_iso_hom_app (X : PartialFun) :
= (λ (a : X), , _⟩) Pointed_to_PartialFun.map (Pointed.iso.mk {to_fun := , inv_fun := λ (a : , dite (a = (λ (h : a = , option.none) (λ (h : ¬a = , option.some a, h⟩), left_inv := _, right_inv := _} _).inv
noncomputable def PartialFun_equiv_Pointed  :

The equivalence induced by PartialFun_to_Pointed and Pointed_to_PartialFun. part.equiv_option made functorial.

Equations
@[simp]
@[simp]
theorem PartialFun_equiv_Pointed_functor_map_to_fun (X Y : PartialFun) (f : X Y) (ᾰ : option X) :
= (λ (a : X), (f a).to_option)
@[simp]

Forgetting that maps are total and making them total again by adding a point is the same as just adding a point.

Equations