# mathlibdocumentation

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.

Instances for qpf
• qpf.has_sizeof_inst
theorem qpf.id_map {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
= 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] (h : ∀ (α β : Type u), ) : theorem qpf.liftp_iff {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (p : α → Prop) (x : F α) : ∃ (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 α) : ∃ (u : (qpf.P F).obj α), = 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 α) : 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} (g : 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) : x = g (qpf.abs (qpf.recF g <$> x.dest))
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) :
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) : y x = 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) (h : = ) : y theorem qpf.Wequiv.refl {F : Type uType u} [functor F] [q : qpf F] (x : (qpf.P F).W) : x theorem qpf.Wequiv.symm {F : Type uType u} [functor F] [q : qpf F] (x y : (qpf.P F).W) : y x 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) : x 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} (g : 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.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] (x : 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] : F (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)) : (qpf.fix.mk x) = g <$> x)
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⟩) = f
theorem qpf.fix.ind_rec {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g₁ g₂ : → α) (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 : → α) (hyp : ∀ (x : F (qpf.fix F)), h (qpf.fix.mk x) = g (h <$> x)) : = h theorem qpf.fix.mk_dest {F : Type uType u} [functor F] [q : qpf F] (x : qpf.fix F) : = x 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 : → Prop) (h : ∀ (x : F (qpf.fix F)), p (qpf.fix.mk x)) (x : qpf.fix F) : p x def qpf.corecF {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (g : α → 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 : α) : x).dest = <$> qpf.repr (g x)
def qpf.is_precongr {F : Type uType u} [functor F] [q : qpf F] (r : (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
Instances for qpf.cofix
@[protected, instance]
def qpf.cofix.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} (g : α → F α) (x : α) :

corecursor for type defined by cofix

Equations
def qpf.cofix.dest {F : Type uType u} [functor F] [q : qpf F] :
F (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 : α) :
x).dest = <$> g x theorem qpf.cofix.bisim_rel {F : Type uType u} [functor F] [q : qpf F] (r : → Prop) (h : ∀ (x y : , 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 : → Prop) (h : ∀ (x y : , r x y 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 : α → ) (h : ∀ (x : α), Q x(∃ (a : (qpf.P F).A) (f f' : (qpf.P F).B a, (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 α} (FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : 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 : α) :
∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs a, f⟩ = xu
theorem qpf.supp_eq {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
= {u : α | ∀ (a : (qpf.P F).A) (f : (qpf.P F).B a → α), qpf.abs a, f⟩ = xu
theorem qpf.has_good_supp_iff {F : Type uType u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
(∀ (p : α → Prop), ∀ (u : α), p 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'⟩ = x
def qpf.is_uniform {F : Type uType u} [functor F] (q : 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] (q : qpf F) :
Prop

does abs preserve liftp?

Equations
def qpf.supp_preservation {F : Type uType u} [functor F] (q : 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) :
∀ (u : α), p 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.supp_preservation_iff_liftp_preservation {F : Type uType u} [functor F] [q : qpf F] :
theorem qpf.liftp_preservation_iff_uniform {F : Type uType u} [functor F] [q : qpf F] :