Documentation

Mathlib.CategoryTheory.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, 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 #

def PartialFun :
Type (u_3 + 1)

The category of types equipped with partial functions.

Instances For

    Turns a type into a PartialFun.

    Instances For
      @[simp]
      theorem PartialFun.Iso.mk_hom {α : PartialFun} {β : PartialFun} (e : α β) (x : α) :
      (PartialFun.Iso.mk e).hom x = ↑(some (e x))
      @[simp]
      theorem PartialFun.Iso.mk_inv {α : PartialFun} {β : PartialFun} (e : α β) (x : β) :
      (PartialFun.Iso.mk e).inv x = ↑(some (e.symm x))
      def PartialFun.Iso.mk {α : PartialFun} {β : PartialFun} (e : α β) :
      α β

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

      Instances For

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

        Instances For
          @[simp]
          theorem pointedToPartialFun_map :
          ∀ {X Y : Pointed} (f : X Y) (a : { x // x X.point }), pointedToPartialFun.map f a = (PFun.toSubtype (fun x => x Y.point) f.toFun Subtype.val) a

          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.

          Instances For
            @[simp]
            theorem partialFunToPointed_map :
            ∀ {X Y : PartialFun} (f : X Y), partialFunToPointed.map f = { toFun := Option.elim' none fun a => Part.toOption (f a), map_point := (_ : Option.elim' none (fun a => Part.toOption (f a)) ((fun X => { X := Option X, point := none }) X).point = Option.elim' none (fun a => Part.toOption (f a)) ((fun X => { X := Option X, point := none }) X).point) }

            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.

            Instances For
              @[simp]
              theorem partialFunEquivPointed_unitIso_hom_app (X : PartialFun) :
              partialFunEquivPointed.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).hom (CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map (Pointed.Iso.mk { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } (_ : { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).point = { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).point)).inv) (pointedToPartialFun.map { toFun := Option.elim' none fun a => Part.toOption (Part.some (Option.get a (_ : Option.isSome a = true))), map_point := (_ : Option.elim' none (fun a => Part.toOption ((PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).inv a)) ((fun X => { X := Option X, point := none }) (pointedToPartialFun.obj (partialFunToPointed.obj X))).point = Option.elim' none (fun a => Part.toOption ((PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).inv a)) ((fun X => { X := Option X, point := none }) (pointedToPartialFun.obj (partialFunToPointed.obj X))).point) }))
              @[simp]
              theorem partialFunEquivPointed_unitIso_inv_app (X : PartialFun) :
              partialFunEquivPointed.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map { toFun := Option.elim' none fun a => Part.toOption (Part.some { val := some a, property := (_ : some a none) }), map_point := (_ : Option.elim' none (fun a => Part.toOption ((PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).hom a)) ((fun X => { X := Option X, point := none }) X).point = Option.elim' none (fun a => Part.toOption ((PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).hom a)) ((fun X => { X := Option X, point := none }) X).point) }) (CategoryTheory.CategoryStruct.comp (pointedToPartialFun.map (Pointed.Iso.mk { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } (_ : { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).point = { toFun := Option.elim' (partialFunToPointed.obj X).point Subtype.val, invFun := fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }, left_inv := (_ : ∀ (a : ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).X), (fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) (Option.elim' (partialFunToPointed.obj X).point Subtype.val a) = a), right_inv := (_ : ∀ (a : ((CategoryTheory.Functor.id Pointed).obj (partialFunToPointed.obj X)).X), Option.elim' (partialFunToPointed.obj X).point Subtype.val ((fun a => if h : a = (partialFunToPointed.obj X).point then none else some { val := a, property := h }) a) = a) } ((CategoryTheory.Functor.comp pointedToPartialFun partialFunToPointed).obj (partialFunToPointed.obj X)).point)).hom) (PartialFun.Iso.mk { toFun := fun a => { val := some a, property := (_ : some a none) }, invFun := fun a => Option.get a (_ : Option.isSome a = true), left_inv := (_ : ∀ (a : (CategoryTheory.Functor.id PartialFun).obj X), Option.get (some a) (_ : Option.isSome ↑((fun a => { val := some a, property := (_ : some a none) }) a) = true) = a), right_inv := (_ : ∀ (a : (CategoryTheory.Functor.comp partialFunToPointed pointedToPartialFun).obj X), { val := some ((fun a => Option.get a (_ : Option.isSome a = true)) a), property := (_ : some ((fun a => Option.get a (_ : Option.isSome a = true)) a) none) } = a) }).inv)
              @[simp]
              theorem partialFunEquivPointed_functor_map_toFun :
              ∀ {X Y : PartialFun} (f : X Y) (a : Option X), Pointed.Hom.toFun (partialFunEquivPointed.functor.map f) a = Option.elim' none (fun a => Part.toOption (f a)) a
              @[simp]
              theorem partialFunEquivPointed_inverse_map_get_coe :
              ∀ {X Y : Pointed} (f : X Y) (a : { x // x X.point }) (property : Pointed.Hom.toFun f a Y.point), ↑(Part.get (partialFunEquivPointed.inverse.map f a) property) = Pointed.Hom.toFun f a
              @[simp]
              theorem partialFunEquivPointed_inverse_obj (X : Pointed) :
              partialFunEquivPointed.inverse.obj X = { x // ¬x = X.point }
              @[simp]
              theorem partialFunEquivPointed_inverse_map_Dom :
              ∀ {X Y : Pointed} (f : X Y) (a : { x // x X.point }), (partialFunEquivPointed.inverse.map f a).Dom = ¬Pointed.Hom.toFun f a = Y.point
              @[simp]
              @[simp]
              theorem partialFunEquivPointed_counitIso_inv_app_toFun (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X) :
              Pointed.Hom.toFun (partialFunEquivPointed.counitIso.inv.app X) a = if h : a = X.point then none else some { val := a, property := h }

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

              Instances For

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

                Instances For