mathlib documentation

data.​qpf.​multivariate.​basic

data.​qpf.​multivariate.​basic

Multivariate quotients of polynomial functors.

Basic definition of multivariate QPF. QPFs form a compositional framework for defining inductive and coinductive types, their quotients and nesting.

The idea is based on building ever larger functors. For instance, we can define a list using a shape functor:

inductive list_shape (a b : Type)
| nil : list_shape
| cons : a -> b -> list_shape

This shape can itself be decomposed as a sum of product which are themselves QPFs. It follows that the shape is a QPF and we can take its fixed point and create the list itself:

def list (a : Type) := fix list_shape a -- not the actual notation

We can continue and define the quotient on permutation of lists and create the multiset type:

def multiset (a : Type) := qpf.quot list.perm list a -- not the actual notion

And multiset is also a QPF. We can then create a novel data type (for Lean):

inductive tree (a : Type)
| node : a -> multiset tree -> tree

An unordered tree. This is currently not supported by Lean because it nests an inductive type inside of a quotient. We can go further and define unordered, possibly infinite trees:

coinductive tree' (a : Type)
| node : a -> multiset tree' -> tree'

by using the cofix construct. Those options can all be mixed and matched because they preserve the properties of QPF. The latter example, tree', combines fixed point, co-fixed point and quotients.

Related modules

each proves that some operations on functors preserves the QPF structure

reference

@[class]
structure mvqpf {n : } (F : typevec nType u_1) [mvfunctor F] :
Type (max (u+1) u_1)

Multivariate quotients of polynomial functors.

Instances

Show that every mvqpf is a lawful mvfunctor.

theorem mvqpf.​id_map {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) :

@[simp]
theorem mvqpf.​comp_map {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α β γ : typevec n} (f : α.arrow β) (g : β.arrow γ) (x : F α) :

@[instance]
def mvqpf.​is_lawful_mvfunctor {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] :

Equations
theorem mvqpf.​liftp_iff {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (p : Π ⦃i : fin2 n⦄, α i → Prop) (x : F α) :
mvfunctor.liftp p x ∃ (a : (mvqpf.P F).A) (f : ((mvqpf.P F).B a).arrow α), x = mvqpf.abs a, f⟩ ∀ (i : fin2 n) (j : (mvqpf.P F).B a i), p (f i j)

theorem mvqpf.​liftr_iff {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : Π ⦃i : fin2 n⦄, α iα i → Prop) (x y : F α) :
mvfunctor.liftr r x y ∃ (a : (mvqpf.P F).A) (f₀ f₁ : ((mvqpf.P F).B a).arrow α), x = mvqpf.abs a, f₀⟩ y = mvqpf.abs a, f₁⟩ ∀ (i : fin2 n) (j : (mvqpf.P F).B a i), r (f₀ i j) (f₁ i j)

theorem mvqpf.​mem_supp {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) (i : fin2 n) (u : α i) :
u mvfunctor.supp x i ∀ (a : (mvqpf.P F).A) (f : ((mvqpf.P F).B a).arrow α), mvqpf.abs a, f⟩ = xu f i '' set.univ

theorem mvqpf.​supp_eq {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} {i : fin2 n} (x : F α) :
mvfunctor.supp x i = {u : α i | ∀ (a : (mvqpf.P F).A) (f : ((mvqpf.P F).B a).arrow α), mvqpf.abs a, f⟩ = xu f i '' set.univ}

theorem mvqpf.​has_good_supp_iff {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F α) :
(∀ (p : Π (i : fin2 n), α i → Prop), mvfunctor.liftp p x ∀ (i : fin2 n) (u : α i), u mvfunctor.supp x ip i u) ∃ (a : (mvqpf.P F).A) (f : ((mvqpf.P F).B a).arrow α), mvqpf.abs a, f⟩ = x ∀ (i : fin2 n) (a' : (mvqpf.P F).A) (f' : ((mvqpf.P F).B a').arrow α), mvqpf.abs a', f'⟩ = xf i '' set.univ f' i '' set.univ

def mvqpf.​is_uniform {n : } {F : typevec nType u_1} [mvfunctor F] :
mvqpf F → Prop

A qpf is said to be uniform if every polynomial functor representing a single value all have the same range.

Equations
def mvqpf.​liftp_preservation {n : } {F : typevec nType u_1} [mvfunctor F] :
mvqpf F → Prop

does abs preserve liftp?

Equations
def mvqpf.​supp_preservation {n : } {F : typevec nType u_1} [mvfunctor F] :
mvqpf F → Prop

does abs preserve supp?

Equations
theorem mvqpf.​supp_eq_of_is_uniform {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α : typevec n} (a : (mvqpf.P F).A) (f : ((mvqpf.P F).B a).arrow α) (i : fin2 n) :

theorem mvqpf.​liftp_iff_of_is_uniform {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α : typevec n} (x : F α) (p : Π (i : fin2 n), α i → Prop) :
mvfunctor.liftp p x ∀ (i : fin2 n) (u : α i), u mvfunctor.supp x ip i u

theorem mvqpf.​supp_map {n : } {F : typevec nType u_1} [mvfunctor F] [q : mvqpf F] (h : q.is_uniform) {α β : typevec n} (g : α.arrow β) (x : F α) (i : fin2 n) :