mathlib3 documentation

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 α) :
id <$> x = 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.liftp_iff {F : Type u Type 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 u Type 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 u Type 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 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) :
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) :
qpf.recF g (W_type.mk a 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) :

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 : qpf.abs x.dest = qpf.abs y.dest) :
theorem qpf.Wequiv.refl {F : Type u Type u} [functor F] [q : qpf F] (x : (qpf.P F).W) :
theorem qpf.Wequiv.symm {F : Type u Type u} [functor F] [q : qpf F] (x y : (qpf.P F).W) :
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) :
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] :

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] :

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)) :
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⟩) = W_type.mk a f
theorem qpf.fix.ind_rec {F : Type u Type u} [functor F] [q : qpf F] {α : Type u} (g₁ g₂ : qpf.fix F α) (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 : qpf.fix F α) (hyp : (x : F (qpf.fix F)), h (qpf.fix.mk x) = g (h <$> x)) :
theorem qpf.fix.mk_dest {F : Type u Type u} [functor F] [q : qpf F] (x : qpf.fix F) :
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 : qpf.fix F Prop) (h : (x : F (qpf.fix F)), functor.liftp p x 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 : α) :
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] :

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 : α) :
theorem qpf.cofix.bisim_rel {F : Type u Type u} [functor F] [q : qpf F] (r : qpf.cofix F qpf.cofix F Prop) (h : (x y : qpf.cofix F), 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 : qpf.cofix F qpf.cofix F Prop) (h : (x y : qpf.cofix F), r x y functor.liftr r x.dest 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 : α qpf.cofix F) (h : (x : α), Q x ( (a : (qpf.P F).A) (f f' : (qpf.P F).B a qpf.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 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 : α) :
u functor.supp x (a : (qpf.P F).A) (f : (qpf.P F).B a α), qpf.abs a, f⟩ = x u f '' set.univ
theorem qpf.supp_eq {F : Type u Type 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⟩ = x u f '' set.univ}
theorem qpf.has_good_supp_iff {F : Type u Type u} [functor F] [q : qpf F] {α : Type u} (x : F α) :
( (p : α Prop), functor.liftp p x (u : α), u functor.supp x 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 f '' set.univ f' '' set.univ
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) :
functor.liftp p x (u : α), u functor.supp x 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 α) :