mathlib3 documentation

data.pfunctor.univariate.basic

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

source
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
source
@[protected, instance]
def pfunctor.inhabited  :
inhabited pfunctor
Equations
source
def pfunctor.obj (P : pfunctor) (α : Type u_2) :
Type (max u_1 u_2)

Applying P to an object of Type

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

root element of a W tree

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

children of the root of a W tree

Equations
source
def pfunctor.W.dest {P : pfunctor} :
P.W → P.obj P.W

destructor for W-types

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

constructor for W-types

Equations
source
@[simp]
theorem pfunctor.W.dest_mk {P : pfunctor} (p : P.obj P.W) :
(pfunctor.W.mk p).dest = p
source
@[simp]
theorem pfunctor.W.mk_dest {P : pfunctor} (p : P.W) :
pfunctor.W.mk p.dest = p
source
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
source
@[protected, instance]
def pfunctor.Idx.inhabited (P : pfunctor) [inhabited P.A] [inhabited (P.B inhabited.default)] :
inhabited P.Idx
Equations
source
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
source
@[simp]
theorem pfunctor.fst_map {P : pfunctor} {α β : Type u} (x : P.obj α) (f : α → β) :
(f <$> x).fst = x.fst
source
@[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)
source
def pfunctor.comp (P₂ P₁ : pfunctor) :
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)}
source
def pfunctor.comp.mk (P₂ P₁ : pfunctor) {α : Type} (x : P₂.obj (P₁.obj α)) :
(P₂.comp P₁).obj α

constructor for composition

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

destructor for composition

Equations
source
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)
source
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)
source
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)
source
theorem pfunctor.supp_eq {P : pfunctor} {α : Type u} (a : P.A) (f : P.B a → α) :
functor.supp ⟨a, f⟩ = f '' set.univ