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, PartialFunToPointed 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_3 + 1)

The category of types equipped with partial functions.

Equations

• PartialFun = Type u_3

instance PartialFun.instCoeSortType : CoeSort PartialFun (Type u_3)

Equations

• PartialFun.instCoeSortType = { coe := id }

def PartialFun.of : Type u_3 → PartialFun

Turns a type into a PartialFun.

Equations

• PartialFun.of = id

instance PartialFun.instInhabited : Inhabited PartialFun

Equations

• PartialFun.instInhabited = { default := Type u_3 }

instance PartialFun.largeCategory : CategoryTheory.LargeCategory PartialFun

Equations

• PartialFun.largeCategory = CategoryTheory.Category.mk @PFun.comp_id @PFun.id_comp @PartialFun.largeCategory.proof_1

@[simp]

theorem PartialFun.Iso.mk_inv {α : PartialFun} {β : PartialFun} (e : α ≃ β) (x : β) : (PartialFun.Iso.mk e).inv x = ↑(some (e.symm x))

@[simp]

theorem PartialFun.Iso.mk_hom {α : PartialFun} {β : PartialFun} (e : α ≃ β) (x : α) : (PartialFun.Iso.mk e).hom x = ↑(some (e x))

def PartialFun.Iso.mk {α : PartialFun} {β : PartialFun} (e : α ≃ β) : α ≅ β

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

Equations

• PartialFun.Iso.mk e = { hom := fun (x : α) => ↑(some (e x)), inv := fun (x : β) => ↑(some (e.symm x)), hom_inv_id := ⋯, inv_hom_id := ⋯ }

def typeToPartialFun : CategoryTheory.Functor (Type u) PartialFun

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

Equations

• typeToPartialFun = { obj := id, map := @PFun.lift, map_id := typeToPartialFun.proof_1, map_comp := @typeToPartialFun.proof_2 }

instance instFaithfulPartialFunTypeToPartialFun : typeToPartialFun.Faithful

Equations

• instFaithfulPartialFunTypeToPartialFun = ⋯

@[simp]

theorem pointedToPartialFun_map : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x : X.X // x ≠ X.point }), pointedToPartialFun.map f a = (PFun.toSubtype (fun (x : Y.X) => x ≠ Y.point) f.toFun ∘ Subtype.val) a

@[simp]

theorem pointedToPartialFun_obj (X : Pointed) : pointedToPartialFun.obj X = { x : X.X // x ≠ X.point }

def pointedToPartialFun : CategoryTheory.Functor Pointed PartialFun

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem partialFunToPointed_obj (X : PartialFun) : partialFunToPointed.obj X = { X := Option X, point := none }

@[simp]

theorem partialFunToPointed_map : ∀ {X Y : PartialFun} (f : X ⟶ Y), partialFunToPointed.map f = { toFun := Option.elim' none fun (a : X) => (f a).toOption, map_point := ⋯ }

noncomputable def partialFunToPointed : CategoryTheory.Functor PartialFun Pointed

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem partialFunEquivPointed_unitIso_inv_app (X : PartialFun) : partialFunEquivPointed.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map { toFun := Option.elim' none fun (a : X) => some ⟨some a, ⋯⟩, map_point := ⋯ }) (CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯).hom) (PartialFun.Iso.mk { toFun := fun (a : X) => ⟨some a, ⋯⟩, invFun := fun (a : { x : Option X // ¬x = none }) => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).inv)

@[simp]

theorem partialFunEquivPointed_functor_obj_point (X : PartialFun) : (partialFunEquivPointed.functor.obj X).point = none

@[simp]

theorem partialFunEquivPointed_inverse_map_Dom : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x : X.X // x ≠ X.point }), (partialFunEquivPointed.inverse.map f a).Dom = ¬f.toFun ↑a = Y.point

@[simp]

theorem partialFunEquivPointed_counitIso_hom_app_toFun (X : Pointed) (a : ((pointedToPartialFun.comp partialFunToPointed).obj X).X) : (partialFunEquivPointed.counitIso.hom.app X).toFun a = Option.casesOn' a X.point Subtype.val

@[simp]

theorem partialFunEquivPointed_inverse_obj (X : Pointed) : partialFunEquivPointed.inverse.obj X = { x : X.X // ¬x = X.point }

@[simp]

theorem partialFunEquivPointed_unitIso_hom_app (X : PartialFun) : partialFunEquivPointed.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (PartialFun.Iso.mk { toFun := fun (a : X) => ⟨some a, ⋯⟩, invFun := fun (a : { x : Option X // ¬x = none }) => (↑a).get ⋯, left_inv := ⋯, right_inv := ⋯ }).hom (CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯).inv) (pointedToPartialFun.map { toFun := Option.elim' none fun (a : { x : Option X // ¬x = none }) => ↑a, map_point := ⋯ }))

@[simp]

theorem partialFunEquivPointed_inverse_map_get_coe : ∀ {X Y : Pointed} (f : X ⟶ Y) (a : { x : X.X // x ≠ X.point }) (property : f.toFun ↑a ≠ Y.point), ↑((partialFunEquivPointed.inverse.map f a).get property) = f.toFun ↑a

@[simp]

theorem partialFunEquivPointed_functor_obj_X (X : PartialFun) : (partialFunEquivPointed.functor.obj X).X = Option X

@[simp]

theorem partialFunEquivPointed_counitIso_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) : (partialFunEquivPointed.counitIso.inv.app X).toFun a = if h : a = X.point then none else some ⟨a, h⟩

@[simp]

theorem partialFunEquivPointed_functor_map_toFun : ∀ {X Y : PartialFun} (f : X ⟶ Y) (a : Option X), (partialFunEquivPointed.functor.map f).toFun a = Option.elim' none (fun (a : X) => (f a).toOption) a

noncomputable def partialFunEquivPointed : PartialFun ≌ Pointed

The equivalence induced by PartialFunToPointed and PointedToPartialFun. Part.equivOption made functorial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem typeToPartialFunIsoPartialFunToPointed_inv_app_toFun (X : Type u_3) (a : (typeToPointed.obj X).X) : (typeToPartialFunIsoPartialFunToPointed.inv.app X).toFun a = a

@[simp]

theorem typeToPartialFunIsoPartialFunToPointed_hom_app_toFun (X : Type u_3) (a : ((typeToPartialFun.comp partialFunToPointed).obj X).X) : (typeToPartialFunIsoPartialFunToPointed.hom.app X).toFun a = a

noncomputable def typeToPartialFunIsoPartialFunToPointed : typeToPartialFun.comp partialFunToPointed ≅ typeToPointed

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

Equations

• One or more equations did not get rendered due to their size.