The category of types with partial functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)
The category of types equipped with partial functions.
Equations
- PartialFun = Type u_1
Instances for PartialFun
Equations
Equations
- PartialFun.inhabited = {default := Type u_1}
Equations
- PartialFun.large_category = {to_category_struct := {to_quiver := {hom := pfun}, id := pfun.id, comp := λ (X Y Z : PartialFun) (f : X ⟶ Y) (g : Y ⟶ Z), pfun.comp g f}, id_comp' := pfun.comp_id, comp_id' := pfun.id_comp, assoc' := PartialFun.large_category._proof_1}
Constructs a partial function isomorphism between types from an equivalence between them.
Equations
- PartialFun.iso.mk e = {hom := ↑⇑e, inv := ↑⇑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
The forgetful functor from Type to PartialFun which forgets that the maps are total.
Equations
Instances for Type_to_PartialFun
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.
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
- PartialFun_to_Pointed = {obj := λ (X : PartialFun), {X := option X, point := option.none X}, map := λ (X Y : PartialFun) (f : X ⟶ Y), {to_fun := option.elim option.none (λ (a : X), (f a).to_option), map_point := _}, map_id' := PartialFun_to_Pointed._proof_2, map_comp' := PartialFun_to_Pointed._proof_3}
The equivalence induced by PartialFun_to_Pointed and Pointed_to_PartialFun.
part.equiv_option made functorial.
Equations
- PartialFun_equiv_Pointed = category_theory.equivalence.mk PartialFun_to_Pointed Pointed_to_PartialFun (category_theory.nat_iso.of_components (λ (X : PartialFun), PartialFun.iso.mk {to_fun := λ (a : (𝟭 PartialFun).obj X), ⟨option.some a, _⟩, inv_fun := λ (a : (PartialFun_to_Pointed ⋙ Pointed_to_PartialFun).obj X), option.get _, left_inv := _, right_inv := _}) PartialFun_equiv_Pointed._proof_4) (category_theory.nat_iso.of_components (λ (X : Pointed), Pointed.iso.mk {to_fun := option.elim X.point subtype.val, inv_fun := λ (a : ↥((𝟭 Pointed).obj X)), dite (a = X.point) (λ (h : a = X.point), option.none) (λ (h : ¬a = X.point), option.some ⟨a, h⟩), left_inv := _, right_inv := _} _) PartialFun_equiv_Pointed._proof_8)
Forgetting that maps are total and making them total again by adding a point is the same as just adding a point.
Equations
- Type_to_PartialFun_iso_PartialFun_to_Pointed = category_theory.nat_iso.of_components (λ (X : Type u_1), {hom := {to_fun := id ↥((Type_to_PartialFun ⋙ PartialFun_to_Pointed).obj X), map_point := _}, inv := {to_fun := id ↥(Type_to_Pointed.obj X), map_point := _}, hom_inv_id' := _, inv_hom_id' := _}) Type_to_PartialFun_iso_PartialFun_to_Pointed._proof_5