mathlib documentation

data.qpf.univariate.basic

Quotients of Polynomial Functors

We assume the following:

P : a polynomial functor W : its W-type M : its M-type F : a functor

We define:

q : qpf data, representing F as a quotient of P

The main goal is to construct:

fix : the initial algebra with structure map F fix → fix. cofix : the final coalgebra with structure map cofix → F cofix

We also show that the composition of qpfs is a qpf, and that the quotient of a qpf is a qpf.

The present theory focuses on the univariate case for qpfs

References

@[class]
structure qpf (F : Type uType u) [functor F] :
Type (u+1)

Quotients of polynomial functors.

Roughly speaking, saying that F is a quotient of a polynomial functor means that for each α, elements of F α are represented by pairs ⟨a, f⟩, where a is the shape of the object and f indexes the relevant elements of α, in a suitably natural manner.

theorem qpf.id_map {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
id <$> x = x

theorem qpf.comp_map {F : Type uType u} [functor F] [q : qpf F] {α β γ : Type u} (f : α → β) (g : β → γ) (x : F α) :
(g f) <$> x = g <$> f <$> x

theorem qpf.is_lawful_functor {F : Type uType u} [functor F] [q : qpf F] :

theorem qpf.liftp_iff {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (p : α → Prop) (x : F α) :
functor.liftp p x ∃ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), x = qpf.abs a, f⟩ ∀ (i : (qpf.P F).B a), p (f i)

theorem qpf.liftp_iff' {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (p : α → Prop) (x : F α) :
functor.liftp p x ∃ (u : (qpf.P F).obj α), qpf.abs u = x ∀ (i : (qpf.P F).B u.fst), p (u.snd i)

theorem qpf.liftr_iff {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (r : α → α → Prop) (x y : F α) :
functor.liftr r x y ∃ (a : (qpf.P F).A) (f₀ f₁ : (qpf.P F).B a → α), x = qpf.abs a, f₀⟩ y = qpf.abs a, f₁⟩ ∀ (i : (qpf.P F).B a), r (f₀ i) (f₁ i)

def qpf.recF {F : Type uType u} [functor F] [q : qpf F] {α : Type u} :
(F α → α)(qpf.P F).W → α

does recursion on q.P.W using g : F α → α rather than g : P α → α

Equations
theorem qpf.recF_eq {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (x : (qpf.P F).W) :

theorem qpf.recF_eq' {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (a : (qpf.P F).A) (f : (qpf.P F).B a(qpf.P F).W) :
qpf.recF g (W.mk a f) = g (qpf.abs (qpf.recF g <$> a, f⟩))

inductive qpf.Wequiv {F : Type uType u} [functor F] [q : qpf F] :
(qpf.P F).W(qpf.P F).W → Prop

two trees are equivalent if their F-abstractions are

theorem qpf.recF_eq_of_Wequiv {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (u : F α → α) (x y : (qpf.P F).W) :
qpf.Wequiv x yqpf.recF u x = qpf.recF u y

recF is insensitive to the representation

theorem qpf.Wequiv.abs' {F : Type uType u} [functor F] [q : qpf F] (x y : (qpf.P F).W) :

theorem qpf.Wequiv.refl {F : Type uType u} [functor F] [q : qpf F] (x : (qpf.P F).W) :

theorem qpf.Wequiv.symm {F : Type uType u} [functor F] [q : qpf F] (x y : (qpf.P F).W) :

def qpf.Wrepr {F : Type uType u} [functor F] [q : qpf F] :
(qpf.P F).W(qpf.P F).W

maps every element of the W type to a canonical representative

Equations
theorem qpf.Wrepr_equiv {F : Type uType u} [functor F] [q : qpf F] (x : (qpf.P F).W) :

def qpf.W_setoid {F : Type uType u} [functor F] [q : qpf F] :

Define the fixed point as the quotient of trees under the equivalence relation Wequiv.

Equations
@[nolint]
def qpf.fix (F : Type uType u) [functor F] [q : qpf F] :
Type u

inductive type defined as initial algebra of a Quotient of Polynomial Functor

Equations
def qpf.fix.rec {F : Type uType u} [functor F] [q : qpf F] {α : Type u} :
(F α → α)qpf.fix F → α

recursor of a type defined by a qpf

Equations
def qpf.fix_to_W {F : Type uType u} [functor F] [q : qpf F] :
qpf.fix F(qpf.P F).W

access the underlying W-type of a fixpoint data type

Equations
def qpf.fix.mk {F : Type uType u} [functor F] [q : qpf F] :
F (qpf.fix F)qpf.fix F

constructor of a type defined by a qpf

Equations
def qpf.fix.dest {F : Type uType u} [functor F] [q : qpf F] :
qpf.fix FF (qpf.fix F)

destructor of a type defined by a qpf

Equations
theorem qpf.fix.rec_eq {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (x : F (qpf.fix F)) :

theorem qpf.fix.ind_aux {F : Type uType u} [functor F] [q : qpf F] (a : (qpf.P F).A) (f : (qpf.P F).B a(qpf.P F).W) :
qpf.fix.mk (qpf.abs a, λ (x : (qpf.P F).B a), f x⟩) = W.mk a f

theorem qpf.fix.ind_rec {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g₁ g₂ : qpf.fix F → α) (h : ∀ (x : F (qpf.fix F)), g₁ <$> x = g₂ <$> xg₁ (qpf.fix.mk x) = g₂ (qpf.fix.mk x)) (x : qpf.fix F) :
g₁ x = g₂ x

theorem qpf.fix.rec_unique {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : F α → α) (h : qpf.fix F → α) :
(∀ (x : F (qpf.fix F)), h (qpf.fix.mk x) = g (h <$> x))qpf.fix.rec g = h

theorem qpf.fix.mk_dest {F : Type uType u} [functor F] [q : qpf F] (x : qpf.fix F) :

theorem qpf.fix.dest_mk {F : Type uType u} [functor F] [q : qpf F] (x : F (qpf.fix F)) :

theorem qpf.fix.ind {F : Type uType u} [functor F] [q : qpf F] (p : qpf.fix F → Prop) (h : ∀ (x : F (qpf.fix F)), functor.liftp p xp (qpf.fix.mk x)) (x : qpf.fix F) :
p x

def qpf.corecF {F : Type uType u} [functor F] [q : qpf F] {α : Type u} :
(α → F α)α → (qpf.P F).M

does recursion on q.P.M using g : α → F α rather than g : α → P α

Equations
theorem qpf.corecF_eq {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (x : α) :

def qpf.is_precongr {F : Type uType u} [functor F] [q : qpf F] :
((qpf.P F).M(qpf.P F).M → Prop) → Prop

A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric.

Equations
def qpf.Mcongr {F : Type uType u} [functor F] [q : qpf F] :
(qpf.P F).M(qpf.P F).M → Prop

The maximal congruence on q.P.M

Equations
def qpf.cofix (F : Type uType u) [functor F] [q : qpf F] :
Type u

coinductive type defined as the final coalgebra of a qpf

Equations
@[instance]
def qpf.inhabited {F : Type uType u} [functor F] [q : qpf F] [inhabited (qpf.P F).A] :

Equations
def qpf.cofix.corec {F : Type uType u} [functor F] [q : qpf F] {α : Type u} :
(α → F α)α → qpf.cofix F

corecursor for type defined by cofix

Equations
def qpf.cofix.dest {F : Type uType u} [functor F] [q : qpf F] :
qpf.cofix FF (qpf.cofix F)

destructor for type defined by cofix

Equations
theorem qpf.cofix.dest_corec {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : α → F α) (x : α) :

theorem qpf.cofix.bisim_rel {F : Type uType u} [functor F] [q : qpf F] (r : qpf.cofix Fqpf.cofix F → Prop) (h : ∀ (x y : qpf.cofix F), r x yquot.mk r <$> x.dest = quot.mk r <$> y.dest) (x y : qpf.cofix F) :
r x yx = y

theorem qpf.cofix.bisim {F : Type uType u} [functor F] [q : qpf F] (r : qpf.cofix Fqpf.cofix F → Prop) (h : ∀ (x y : qpf.cofix F), r x yfunctor.liftr r x.dest y.dest) (x y : qpf.cofix F) :
r x yx = y

theorem qpf.cofix.bisim' {F : Type uType u} [functor F] [q : qpf F] {α : Type u_1} (Q : α → Prop) (u v : α → qpf.cofix F) (h : ∀ (x : α), Q x(∃ (a : (qpf.P F).A) (f f' : (qpf.P F).B aqpf.cofix F), (u x).dest = qpf.abs a, f⟩ (v x).dest = qpf.abs a, f'⟩ ∀ (i : (qpf.P F).B a), ∃ (x' : α), Q x' f i = u x' f' i = v x')) (x : α) :
Q xu x = v x

def qpf.comp {F₂ : Type uType u} [functor F₂] [q₂ : qpf F₂] {F₁ : Type uType u} [functor F₁] [q₁ : qpf F₁] :
qpf (functor.comp F₂ F₁)

composition of qpfs gives another qpf

Equations
def qpf.quotient_qpf {F : Type uType u} [functor F] [q : qpf F] {G : Type uType u} [functor G] {FG_abs : Π {α : Type u}, F αG α} {FG_repr : Π {α : Type u}, G αF α} :
(∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x)(∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x)qpf G

Given a qpf F and a well-behaved surjection FG_abs from F α to functor G α, G is a qpf. We can consider G a quotient on F where elements x y : F α are in the same equivalence class if FG_abs x = FG_abs y

Equations
theorem qpf.mem_supp {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) (u : α) :
u functor.supp x ∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs a, f⟩ = xu f '' set.univ

theorem qpf.supp_eq {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
functor.supp x = {u : α | ∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs a, f⟩ = xu f '' set.univ}

theorem qpf.has_good_supp_iff {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
(∀ (p : α → Prop), functor.liftp p x ∀ (u : α), u functor.supp xp u) ∃ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs a, f⟩ = x ∀ (a' : (qpf.P F).A) (f' : (qpf.P F).B a' → α), qpf.abs a', f'⟩ = xf '' set.univ f' '' set.univ

def qpf.is_uniform {F : Type uType u} [functor F] :
qpf F → Prop

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

Equations
def qpf.liftp_preservation {F : Type uType u} [functor F] :
qpf F → Prop

does abs preserve liftp?

Equations
def qpf.supp_preservation {F : Type uType u} [functor F] :
qpf F → Prop

does abs preserve supp?

Equations
theorem qpf.supp_eq_of_is_uniform {F : Type uType u} [functor F] [q : qpf F] (h : q.is_uniform) {α : Type u} (a : (qpf.P F).A) (f : (qpf.P F).B a → α) :

theorem qpf.liftp_iff_of_is_uniform {F : Type uType u} [functor F] [q : qpf F] (h : q.is_uniform) {α : Type u} (x : F α) (p : α → Prop) :
functor.liftp p x ∀ (u : α), u functor.supp xp u

theorem qpf.supp_map {F : Type uType u} [functor F] [q : qpf F] (h : q.is_uniform) {α β : Type u} (g : α → β) (x : F α) :

theorem qpf.supp_preservation_iff_uniform {F : Type uType u} [functor F] [q : qpf F] :

theorem qpf.liftp_preservation_iff_uniform {F : Type uType u} [functor F] [q : qpf F] :