mathlib documentation

data.pfunctor.univariate.basic

Polynomial functors

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 : Type ?
B : c.A → Type ?

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 α.

@[instance]

def pfunctor.inhabited :

inhabited pfunctor

Equations

pfunctor.inhabited = {default := {A := default (Type u_1) sort.inhabited, B := default (default (Type u_1) → Type u_1) (pi.inhabited (default (Type u_1)))}}

def pfunctor.obj (P : pfunctor) (α : Type u_2) :

Type (max u_1 u_2)

Applying P to an object of Type

Equations

P.obj α = Σ (x : P.A), P.B x → α

def pfunctor.map (P : pfunctor) {α : Type u_2} {β : Type u_3} (f : α → β) (a : P.obj α) :

P.obj β

Applying P to a morphism of Type

Equations

P.map f = λ (_x : P.obj α), pfunctor.map._match_1 P f _x
pfunctor.map._match_1 P f ⟨a, g⟩ = ⟨a, f ∘ g⟩

@[instance]

def pfunctor.obj.inhabited (P : pfunctor) {α : Type u} [inhabited P.A] [inhabited α] :

inhabited (P.obj α)

Equations

pfunctor.obj.inhabited P = {default := ⟨default P.A _inst_1, λ (_x : P.B (default P.A)), default α⟩}

@[instance]

def pfunctor.functor (P : pfunctor) :

Equations

P.functor = {map := P.map, map_const := λ (α β : Type u_2), P.map ∘ function.const β}

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

@[instance]

def pfunctor.is_lawful_functor (P : pfunctor) :

is_lawful_functor P.obj

@[nolint]

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

Equations

P.W = W P.B

def pfunctor.W.head {P : pfunctor} (a : P.W) :

P.A

root element of a W tree

Equations

pfunctor.W.head (W.mk a f) = a

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

P.W

children of the root of a W tree

Equations

pfunctor.W.children (W.mk a f) = f

def pfunctor.W.dest {P : pfunctor} (a : P.W) :

P.obj P.W

destructor for W-types

Equations

pfunctor.W.dest (W.mk a f) = ⟨a, f⟩

def pfunctor.W.mk {P : pfunctor} (a : P.obj P.W) :

P.W

constructor for W-types

Equations

pfunctor.W.mk ⟨a, f⟩ = W.mk a f

@[simp]

theorem pfunctor.W.dest_mk {P : pfunctor} (p : P.obj P.W) :

(pfunctor.W.mk p).dest = p

@[simp]

theorem pfunctor.W.mk_dest {P : pfunctor} (p : P.W) :

pfunctor.W.mk p.dest = p

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

Equations

P.Idx = Σ (x : P.A), P.B x

@[instance]

def pfunctor.Idx.inhabited (P : pfunctor) [inhabited P.A] [inhabited (P.B (default P.A))] :

inhabited P.Idx

Equations

pfunctor.Idx.inhabited P = {default := ⟨default P.A _inst_1, default (P.B (default P.A)) _inst_2⟩}

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

Equations

x.iget i = dite (i.fst = x.fst) (λ (h : i.fst = x.fst), x.snd (cast _ i.snd)) (λ (h : ¬i.fst = x.fst), default α)

@[simp]

theorem pfunctor.fst_map {P : pfunctor} {α β : Type u} (x : P.obj α) (f : α → β) :

(f <$> x).fst = x.fst

@[simp]

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

Equations

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 pfunctor.comp.mk (P₂ P₁ : pfunctor) {α : Type} (x : P₂.obj (P₁.obj α)) :

(P₂.comp P₁).obj α

constructor for composition

Equations

pfunctor.comp.mk P₂ P₁ x = ⟨⟨x.fst, sigma.fst ∘ x.snd⟩, λ (a₂a₁ : (P₂.comp P₁).B ⟨x.fst, sigma.fst ∘ x.snd⟩), (x.snd a₂a₁.fst).snd a₂a₁.snd⟩

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

P₂.obj (P₁.obj α)

destructor for composition

Equations

pfunctor.comp.get P₂ P₁ x = ⟨x.fst.fst, λ (a₂ : P₂.B x.fst.fst), ⟨x.fst.snd a₂, λ (a₁ : P₁.B (x.fst.snd a₂)), x.snd ⟨a₂, a₁⟩⟩⟩

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 → α) :

functor.supp ⟨a, f⟩ = f '' set.univ