Polynomial Functors

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

structure PFunctor : Type (max (uA + 1) (uB + 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 α, which is defined as the sigma type Σ x, P.B x → α.

An element of P α 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 α.

• A : Type uA

  The head type

• B : self.A → Type uB

  The child family of types

@[instance_reducible]

instance PFunctor.instInhabited : Inhabited PFunctor.{u_2, u_1}

Equations

• PFunctor.instInhabited = { default := { A := default, B := default } }

@[implicit_reducible]

def PFunctor.Obj (P : PFunctor.{uA, uB}) (α : Type v) : Type (max v uA uB)

Applying P to an object of Type

Equations

• ↑P α = ((x : P.A) × (P.B x → α))

@[instance_reducible]

instance PFunctor.instCoeFunForallType : CoeFun PFunctor.{uA, uB} fun (x : PFunctor.{uA, uB}) => Type v → Type (max v uA uB)

Equations

• PFunctor.instCoeFunForallType = { coe := PFunctor.Obj }

@[implicit_reducible, match_pattern]

def PFunctor.Obj.mk {P : PFunctor.{uA, uB}} {α : Type v₁} (a : P.A) (f : P.B a → α) : ↑P α

Make an element of P α from a "shape" a : P.A and a family of elements f : P.B a → α.

Important: You should use PFunctor.Obj.mk instead of the anonymous constructor ⟨_, _⟩ to avoid abuse of the definitional equality between P α and Σ x : P.A, P.B x → α.

Equations

• PFunctor.Obj.mk a f = ⟨a, f⟩

@[implicit_reducible]

def PFunctor.Obj.rec {P : PFunctor.{uA, uB}} {α : Type v₁} {motive : ↑P α → Sort u_1} (mk : (a : P.A) → (f : P.B a → α) → motive (mk a f)) (t : ↑P α) : motive t

To prove a theorem about t : P α it suffices to prove it for P.Obj.mk a f for all possible values of a and f.

Equations

• PFunctor.Obj.rec mk t = mk t.fst t.snd

@[simp]

theorem PFunctor.Obj.rec_mk {P : PFunctor.{uA, uB}} {α : Type v₁} {motive : ↑P α → Sort u_1} {mk : (a : P.A) → (b : P.B a → α) → motive (mk a b)} (a : P.A) (b : P.B a → α) : rec mk (Obj.mk a b) = mk a b

@[implicit_reducible]

def PFunctor.Obj.fst {P : PFunctor.{uA, uB}} {α : Type v₁} (x : ↑P α) : P.A

Extract the "shape" of a x : P α as x.fst : P.A.

Equations

• x.fst = x.fst

@[implicit_reducible]

def PFunctor.Obj.snd {P : PFunctor.{uA, uB}} {α : Type v₁} (x : ↑P α) : P.B x.fst → α

Extract the underlying value of type α associated to an object x : P α at an index i : P.B x.fst.

Equations

• x.snd = x.snd

@[simp]

theorem PFunctor.Obj.fst_mk {P : PFunctor.{uA, uB}} {α : Type v₁} (a : P.A) (f : P.B a → α) : (mk a f).fst = a

@[simp]

theorem PFunctor.Obj.snd_mk {P : PFunctor.{uA, uB}} {α : Type v₁} (a : P.A) (f : P.B a → α) : (mk a f).snd = f

@[simp]

theorem PFunctor.Obj.eta {P : PFunctor.{uA, uB}} {α : Type v₁} (x : ↑P α) : mk x.fst x.snd = x

def PFunctor.map (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} (f : α → β) : ↑P α → ↑P β

Applying P to a morphism of Type

Equations

• P.map f x = PFunctor.Obj.mk x.fst (f ∘ x.snd)

@[instance_reducible]

instance PFunctor.Obj.inhabited (P : PFunctor.{uA, uB}) {α : Type v₁} [Inhabited P.A] [Inhabited α] : Inhabited (↑P α)

Equations

• PFunctor.Obj.inhabited P = { default := ⟨default, default⟩ }

@[instance_reducible]

instance PFunctor.instFunctorObj (P : PFunctor.{uA, uB}) : Functor ↑P

Equations

• P.instFunctorObj = { map := @PFunctor.map P }

@[simp]

theorem PFunctor.map_eq_map (P : PFunctor.{uA, uB}) {α β : Type v} (f : α → β) (x : ↑P α) : f <$> x = P.map f x

We prefer PFunctor.map to Functor.map because it is universe-polymorphic.

@[simp]

theorem PFunctor.map_eq (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} (f : α → β) (a : P.A) (g : P.B a → α) : P.map f (Obj.mk a g) = Obj.mk a (f ∘ g)

@[simp]

theorem PFunctor.id_map (P : PFunctor.{uA, uB}) {α : Type v₁} (x : ↑P α) : P.map id x = x

@[simp]

theorem PFunctor.map_map (P : PFunctor.{uA, uB}) {α : Type v₁} {β : Type v₂} {γ : Type v₃} (f : α → β) (g : β → γ) (x : ↑P α) : P.map g (P.map f x) = P.map (g ∘ f) x

instance PFunctor.instLawfulFunctorObj (P : PFunctor.{uA, uB}) : LawfulFunctor ↑P

def PFunctor.W (P : PFunctor.{uA, uB}) : Type (max uA uB)

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

Equations

• P.W = WType P.B

def PFunctor.W.head {P : PFunctor.{uA, uB}} : P.W → P.A

The root element of a W tree

Equations

• PFunctor.W.head (WType.mk a _f) = a

def PFunctor.W.children {P : PFunctor.{uA, uB}} (x : P.W) : P.B x.head → P.W

The children of the root of a W tree

Equations

• PFunctor.W.children (WType.mk a _f) = _f

def PFunctor.W.dest {P : PFunctor.{uA, uB}} : P.W → ↑P P.W

The destructor for W-types

Equations

• PFunctor.W.dest (WType.mk a _f) = ⟨a, _f⟩

def PFunctor.W.mk {P : PFunctor.{uA, uB}} : ↑P P.W → P.W

The constructor for W-types

Equations

• PFunctor.W.mk ⟨a, f⟩ = WType.mk a f

@[simp]

theorem PFunctor.W.dest_mk {P : PFunctor.{uA, uB}} (p : ↑P P.W) : (mk p).dest = p

@[simp]

theorem PFunctor.W.mk_dest {P : PFunctor.{uA, uB}} (p : P.W) : mk p.dest = p

def PFunctor.Idx (P : PFunctor.{uA, uB}) : Type (max uA uB)

Idx identifies a location inside the application of a polynomial functor. For F : PFunctor, x : F α 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_reducible]

instance PFunctor.Idx.inhabited (P : PFunctor.{uA, uB}) [Inhabited P.A] [Inhabited (P.B default)] : Inhabited P.Idx

Equations

• PFunctor.Idx.inhabited P = { default := ⟨default, default⟩ }

def PFunctor.Obj.iget {P : PFunctor.{uA, uB}} [DecidableEq P.A] {α : Type u_1} [Inhabited α] (x : ↑P α) (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 = if h : i.fst = x.fst then x.snd (cast ⋯ i.snd) else default

@[simp]

theorem PFunctor.fst_map {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} (x : ↑P α) (f : α → β) : (P.map f x).fst = x.fst

@[simp]

theorem PFunctor.iget_map {P : PFunctor.{uA, uB}} {α : Type v₁} {β : Type v₂} [DecidableEq P.A] [Inhabited α] [Inhabited β] (x : ↑P α) (f : α → β) (i : P.Idx) (h : i.fst = x.fst) : (P.map f x).iget i = f (x.iget i)

@[implicit_reducible]

def PFunctor.comp (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) : PFunctor.{max uA₁ uA₂ uB₂, max uB₁ uB₂}

Composition for polynomial functors

Equations

• P₂.comp P₁ = { A := (a₂ : P₂.A) × (P₂.B a₂ → P₁.A), B := fun (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₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : ↑P₂ (↑P₁ α)) : ↑(P₂.comp P₁) α

Constructor for composition

Equations

• PFunctor.comp.mk P₂ P₁ x = PFunctor.Obj.mk ⟨x.fst, PFunctor.Obj.fst ∘ x.snd⟩ fun (a₂a₁ : (P₂.comp P₁).B ⟨x.fst, PFunctor.Obj.fst ∘ x.snd⟩) => (x.snd a₂a₁.fst).snd a₂a₁.snd

def PFunctor.comp.get (P₂ : PFunctor.{uA₂, uB₂}) (P₁ : PFunctor.{uA₁, uB₁}) {α : Type v} (x : ↑(P₂.comp P₁) α) : ↑P₂ (↑P₁ α)

Destructor for composition

Equations

• PFunctor.comp.get P₂ P₁ x = PFunctor.Obj.mk x.fst.fst fun (a₂ : P₂.B x.fst.fst) => PFunctor.Obj.mk (x.fst.snd a₂) fun (a₁ : P₁.B (x.fst.snd a₂)) => x.snd ⟨a₂, a₁⟩

theorem PFunctor.liftp_iff {P : PFunctor.{uA, uB}} {α : Type u} (p : α → Prop) (x : ↑P α) : Functor.Liftp p x ↔ ∃ (a : P.A) (f : P.B a → α), x = Obj.mk a f ∧ ∀ (i : P.B a), p (f i)

theorem PFunctor.liftp_iff' {P : PFunctor.{uA, uB}} {α : Type u} (p : α → Prop) (a : P.A) (f : P.B a → α) : Functor.Liftp p (Obj.mk a f) ↔ ∀ (i : P.B a), p (f i)

theorem PFunctor.liftr_iff {P : PFunctor.{uA, uB}} {α : Type u} (r : α → α → Prop) (x y : ↑P α) : Functor.Liftr r x y ↔ ∃ (a : P.A) (f₀ : P.B a → α) (f₁ : P.B a → α), x = Obj.mk a f₀ ∧ y = Obj.mk a f₁ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

theorem PFunctor.supp_eq {P : PFunctor.{uA, uB}} {α : Type u} (a : P.A) (f : P.B a → α) : Functor.supp (Obj.mk a f) = f '' Set.univ