mathlib documentation


Polynomial functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines polynomial functors and the W-type construction as a polynomial functor. (For the M-type construction, see pfunctor/M.lean.)

structure pfunctor  :
Type (u+1)

A polynomial functor P is given by a type A and a family B of types over A. P maps any type α to a new type P.obj α, which is defined as the sigma type Σ x, P.B x → α.

An element of P.obj α is a pair ⟨a, f⟩, where a is an element of a type A and f : B a → α. Think of a as the shape of the object and f as an index to the relevant elements of α.

Instances for pfunctor
def pfunctor.obj (P : pfunctor) (α : Type u_2) :
Type (max u_1 u_2)

Applying P to an object of Type

Instances for pfunctor.obj
def (P : pfunctor) {α : Type u_2} {β : Type u_3} (f : α β) :
P.obj α P.obj β

Applying P to a morphism of Type

  • f = λ (_x : P.obj α), P f _x
  • P f a, g⟩ = a, f g
@[protected, instance]
def pfunctor.obj.inhabited (P : pfunctor) {α : Type u} [inhabited P.A] [inhabited α] :
inhabited (P.obj α)
@[protected, instance]
theorem pfunctor.map_eq (P : pfunctor) {α β : Type u_2} (f : α β) (a : P.A) (g : P.B a α) :
f <$> a, g⟩ = a, f g
theorem pfunctor.id_map (P : pfunctor) {α : Type u_2} (x : P.obj α) :
id <$> x = id x
theorem pfunctor.comp_map (P : pfunctor) {α β γ : Type u_2} (f : α β) (g : β γ) (x : P.obj α) :
(g f) <$> x = g <$> f <$> x
@[protected, instance]
def pfunctor.W (P : pfunctor) :
Type u_1

re-export existing definition of W-types and adapt it to a packaged definition of polynomial functor

def pfunctor.W.head {P : pfunctor} :

root element of a W tree

def pfunctor.W.children {P : pfunctor} (x : P.W) :
P.B x.head P.W

children of the root of a W tree

def pfunctor.W.dest {P : pfunctor} :
P.W P.obj P.W

destructor for W-types

def {P : pfunctor} :
P.obj P.W P.W

constructor for W-types

theorem pfunctor.W.dest_mk {P : pfunctor} (p : P.obj P.W) :
theorem pfunctor.W.mk_dest {P : pfunctor} (p : P.W) :
def pfunctor.Idx (P : pfunctor) :
Type u_1

Idx identifies a location inside the application of a pfunctor. For F : pfunctor, x : F.obj α and i : F.Idx, i can designate one part of x or is invalid, if i.1 ≠ x.1

Instances for pfunctor.Idx
def pfunctor.obj.iget {P : pfunctor} [decidable_eq P.A] {α : Type u_2} [inhabited α] (x : P.obj α) (i : P.Idx) :

x.iget i takes the component of x designated by i if any is or returns a default value

theorem pfunctor.fst_map {P : pfunctor} {α β : Type u} (x : P.obj α) (f : α β) :
(f <$> x).fst = x.fst
theorem pfunctor.iget_map {P : pfunctor} [decidable_eq P.A] {α β : Type u} [inhabited α] [inhabited β] (x : P.obj α) (f : α β) (i : P.Idx) (h : i.fst = x.fst) :
pfunctor.obj.iget (f <$> x) i = f (x.iget i)
def pfunctor.comp (P₂ P₁ : pfunctor) :

functor composition for polynomial functors

  • P₂.comp P₁ = {A := Σ (a₂ : P₂.A), P₂.B a₂ P₁.A, B := λ (a₂a₁ : Σ (a₂ : P₂.A), P₂.B a₂ P₁.A), Σ (u : P₂.B a₂a₁.fst), P₁.B (a₂a₁.snd u)}
def (P₂ P₁ : pfunctor) {α : Type} (x : P₂.obj (P₁.obj α)) :
(P₂.comp P₁).obj α

constructor for composition

def pfunctor.comp.get (P₂ P₁ : pfunctor) {α : Type} (x : (P₂.comp P₁).obj α) :
P₂.obj (P₁.obj α)

destructor for composition

theorem pfunctor.liftp_iff {P : pfunctor} {α : Type u} (p : α Prop) (x : P.obj α) :
functor.liftp p x (a : P.A) (f : P.B a α), x = a, f⟩ (i : P.B a), p (f i)
theorem pfunctor.liftp_iff' {P : pfunctor} {α : Type u} (p : α Prop) (a : P.A) (f : P.B a α) :
functor.liftp p a, f⟩ (i : P.B a), p (f i)
theorem pfunctor.liftr_iff {P : pfunctor} {α : Type u} (r : α α Prop) (x y : P.obj α) :
functor.liftr r x y (a : P.A) (f₀ f₁ : P.B a α), x = a, f₀⟩ y = a, f₁⟩ (i : P.B a), r (f₀ i) (f₁ i)
theorem pfunctor.supp_eq {P : pfunctor} {α : Type u} (a : P.A) (f : P.B a α) :