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

Instances for pfunctor
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 → α
Instances for pfunctor.obj
def pfunctor.map (P : pfunctor) {α : Type u_2} {β : Type u_3} (f : α → β) :
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
@[protected, instance]
def pfunctor.obj.inhabited (P : pfunctor) {α : Type u} [inhabited P.A] [inhabited α] :
inhabited (P.obj α)
Equations
@[protected, instance]
Equations
@[protected]
theorem pfunctor.map_eq (P : pfunctor) {α β : Type u_2} (f : α → β) (a : P.A) (g : P.B a → α) :
f <$> a, g⟩ = a, f g
@[protected]
theorem pfunctor.id_map (P : pfunctor) {α : Type u_2} (x : P.obj α) :
id <$> x = id x
@[protected]
theorem pfunctor.comp_map (P : pfunctor) {α β γ : Type u_2} (f : α → β) (g : β → γ) (x : P.obj α) :
(g f) <$> x = g <$> f <$> x
@[protected, instance]
@[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
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 (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
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

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