# mathlib3documentation

data.qpf.univariate.basic

# Quotients of Polynomial Functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 u Type 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 u Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
= x
theorem qpf.comp_map {F : Type u Type 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 u Type u} [functor F] [q : qpf F] (h : (α β : Type u), ) : theorem qpf.liftp_iff {F : Type u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type u} [functor F] [q : qpf F] (x y : (qpf.P F).W) (h : = ) : y theorem qpf.Wequiv.refl {F : Type u Type u} [functor F] [q : qpf F] (x : (qpf.P F).W) : x theorem qpf.Wequiv.symm {F : Type u Type u} [functor F] [q : qpf F] (x y : (qpf.P F).W) : y x def qpf.Wrepr {F : Type u Type 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 u Type u} [functor F] [q : qpf F] (x : (qpf.P F).W) : x def qpf.W_setoid {F : Type u Type 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 u Type u) [functor F] [q : qpf F] : inductive type defined as initial algebra of a Quotient of Polynomial Functor Equations def qpf.fix.rec {F : Type u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type 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 u Type u} [functor F] [q : qpf F] {α : Type u} (g₁ g₂ : α) (h : (x : F (qpf.fix F)), g₁ <$> x = g₂ <$> x g₁ (qpf.fix.mk x) = g₂ (qpf.fix.mk x)) (x : qpf.fix F) :
g₁ x = g₂ x
theorem qpf.fix.rec_unique {F : Type u Type 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 u Type u} [functor F] [q : qpf F] (x : qpf.fix F) : = x theorem qpf.fix.dest_mk {F : Type u Type u} [functor F] [q : qpf F] (x : F (qpf.fix F)) : theorem qpf.fix.ind {F : Type u Type 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 u Type 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 u Type u} [functor F] [q : qpf F] {α : Type u} (g : α F α) (x : α) : x).dest = <$> qpf.repr (g x)
def qpf.is_precongr {F : Type u Type 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 u Type 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 u Type u) [functor F] [q : qpf F] :

coinductive type defined as the final coalgebra of a qpf

Equations
Instances for qpf.cofix
@[protected, instance]
def qpf.cofix.inhabited {F : Type u Type u} [functor F] [q : qpf F] [inhabited (qpf.P F).A] :
Equations
def qpf.cofix.corec {F : Type u Type u} [functor F] [q : qpf F] {α : Type u} (g : α F α) (x : α) :

corecursor for type defined by cofix

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

destructor for type defined by cofix

Equations
theorem qpf.cofix.dest_corec {F : Type u Type u} [functor F] [q : qpf F] {α : Type u} (g : α F α) (x : α) :
x).dest = <$> g x theorem qpf.cofix.bisim_rel {F : Type u Type u} [functor F] [q : qpf F] (r : Prop) (h : (x y : , r x y quot.mk r <$> x.dest = quot.mk r <$> y.dest) (x y : qpf.cofix F) : r x y x = y theorem qpf.cofix.bisim {F : Type u Type u} [functor F] [q : qpf F] (r : Prop) (h : (x y : , r x y y.dest) (x y : qpf.cofix F) : r x y x = y theorem qpf.cofix.bisim' {F : Type u Type 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 x u x = v x def qpf.comp {F₂ : Type u Type u} [functor F₂] [q₂ : qpf F₂] {F₁ : Type u Type u} [functor F₁] [q₁ : qpf F₁] : qpf (functor.comp F₂ F₁) composition of qpfs gives another qpf Equations def qpf.quotient_qpf {F : Type u Type u} [functor F] [q : qpf F] {G : Type u Type 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 u Type 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⟩ = x u
theorem qpf.supp_eq {F : Type u Type 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⟩ = x u
theorem qpf.has_good_supp_iff {F : Type u Type 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 u Type 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 u Type u} [functor F] (q : qpf F) :
Prop

does abs preserve liftp?

Equations
def qpf.supp_preservation {F : Type u Type u} [functor F] (q : qpf F) :
Prop

does abs preserve supp?

Equations
theorem qpf.supp_eq_of_is_uniform {F : Type u Type 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 u Type 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 u Type u} [functor F] [q : qpf F] (h : q.is_uniform) {α β : Type u} (g : α β) (x : F α) :
theorem qpf.supp_preservation_iff_uniform {F : Type u Type u} [functor F] [q : qpf F] :
theorem qpf.liftp_preservation_iff_uniform {F : Type u Type u} [functor F] [q : qpf F] :