mathlib documentation

data.​pfunctor.​univariate.​basic

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.AType ?

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

def pfunctor.​obj  :
pfunctorType u_2Type (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} :
(α → β)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
@[instance]

Equations
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]

Equations
  • _ = _
@[nolint]
def pfunctor.​W  :
pfunctorType u_1

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

Equations
def pfunctor.​W.​head {P : pfunctor} :
P.W → P.A

root element of a W tree

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

children of the root of a W tree

Equations
def pfunctor.​W.​dest {P : pfunctor} :
P.WP.obj P.W

destructor for W-types

Equations
def pfunctor.​W.​mk {P : pfunctor} :
P.obj P.W → P.W

constructor for W-types

Equations
@[simp]
theorem pfunctor.​W.​dest_mk {P : pfunctor} (p : P.obj P.W) :

@[simp]
theorem pfunctor.​W.​mk_dest {P : pfunctor} (p : P.W) :

def pfunctor.​Idx  :
pfunctorType 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
def pfunctor.​obj.​iget {P : pfunctor} [decidable_eq P.A] {α : Type u_2} [inhabited α] :
P.obj αP.Idx → α

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

Equations
@[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) :
i.fst = x.fstpfunctor.obj.iget (f <$> x) i = f (x.iget i)

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} :
P₂.obj (P₁.obj α)(P₂.comp P₁).obj α

constructor for composition

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

destructor for composition

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