# mathlib3documentation

data.qpf.multivariate.constructions.fix

# The initial algebra of a multivariate qpf is again a qpf. #

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

For a (n+1)-ary QPF F (α₀,..,αₙ), we take the least fixed point of F with regards to its last argument αₙ. The result is a n-ary functor: fix F (α₀,..,αₙ₋₁). Making fix F into a functor allows us to take the fixed point, compose with other functors and take a fixed point again.

## Main definitions #

• fix.mk - constructor
• fix.dest - destructor
• fix.rec - recursor: basis for defining functions by structural recursion on fix F α
• fix.drec - dependent recursor: generalization of fix.rec where the result type of the function is allowed to depend on the fix F α value
• fix.rec_eq - defining equation for recursor
• fix.ind - induction principle for fix F α

## Implementation notes #

For F a QPF, we definefix F αin terms of the W-type of the polynomial functorPofF. We define the relationWequivand take its quotient as the definition offix F α.

inductive Wequiv {α : typevec n} : q.P.W α → q.P.W α → Prop
| ind (a : q.P.A) (f' : q.P.drop.B a ⟹ α) (f₀ f₁ : q.P.last.B a → q.P.W α) :
(∀ x, Wequiv (f₀ x) (f₁ x)) → Wequiv (q.P.W_mk a f' f₀) (q.P.W_mk a f' f₁)
| abs (a₀ : q.P.A) (f'₀ : q.P.drop.B a₀ ⟹ α) (f₀ : q.P.last.B a₀ → q.P.W α)
(a₁ : q.P.A) (f'₁ : q.P.drop.B a₁ ⟹ α) (f₁ : q.P.last.B a₁ → q.P.W α) :
abs ⟨a₀, q.P.append_contents f'₀ f₀⟩ = abs ⟨a₁, q.P.append_contents f'₁ f₁⟩ →
Wequiv (q.P.W_mk a₀ f'₀ f₀) (q.P.W_mk a₁ f'₁ f₁)
| trans (u v w : q.P.W α) : Wequiv u v → Wequiv v w → Wequiv u w


See [ACH19] for more details.

## Reference #

def mvqpf.recF {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) :
(mvqpf.P F).W α β

recF is used as a basis for defining the recursor on fix F α. recF traverses recursively the W-type generated by q.P using a function on F as a recursive step

Equations
theorem mvqpf.recF_eq {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f : (mvqpf.P F).last.B a (mvqpf.P F).W α) :
((mvqpf.P F).W_mk a f' f) = g (mvqpf.abs a, f)⟩)
theorem mvqpf.recF_eq' {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) (x : (mvqpf.P F).W α) :
x = g (mvqpf.abs ((mvqpf.P F).W_dest' x)))
inductive mvqpf.Wequiv {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).W α (mvqpf.P F).W α Prop

Equivalence relation on W-types that represent the same fix F value

theorem mvqpf.recF_eq_of_Wequiv {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] (α : typevec n) {β : Type u} (u : F ::: β) β) (x y : (mvqpf.P F).W α) :
y x = y
theorem mvqpf.Wequiv.abs' {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : (mvqpf.P F).W α) (h : mvqpf.abs ((mvqpf.P F).W_dest' x) = mvqpf.abs ((mvqpf.P F).W_dest' y)) :
y
theorem mvqpf.Wequiv.refl {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : (mvqpf.P F).W α) :
x
theorem mvqpf.Wequiv.symm {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : (mvqpf.P F).W α) :
y x
def mvqpf.Wrepr {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).W α (mvqpf.P F).W α

maps every element of the W type to a canonical representative

Equations
theorem mvqpf.Wrepr_W_mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f : (mvqpf.P F).last.B a (mvqpf.P F).W α) :
mvqpf.Wrepr ((mvqpf.P F).W_mk a f' f) = (mvqpf.P F).W_mk' (mvqpf.repr (mvqpf.abs a, f' f⟩)))
theorem mvqpf.Wrepr_equiv {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : (mvqpf.P F).W α) :
x
theorem mvqpf.Wequiv_map {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} (g : α.arrow β) (x y : (mvqpf.P F).W α) :
y y)
def mvqpf.W_setoid {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] (α : typevec n) :
setoid ((mvqpf.P F).W α)

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

Equations
@[nolint]
def mvqpf.fix {n : } (F : typevec (n + 1) Type u_1) [mvfunctor F] [q : mvqpf F] (α : typevec n) :
Type u_1

Least fixed point of functor F. The result is a functor with one fewer parameters than the input. For F a b c a ternary functor, fix F is a binary functor such that

fix F a b = F a b (fix F a b)

Equations
• α =
Instances for mvqpf.fix
def mvqpf.fix.map {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} (g : α.arrow β) :
α β

fix F is a functor

Equations
@[protected, instance]
def mvqpf.fix.mvfunctor {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] :
Equations
def mvqpf.fix.rec {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) :
α β

Recursor for fix F

Equations
def mvqpf.fix_to_W {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
α (mvqpf.P F).W α

Access W-type underlying fix F

Equations
def mvqpf.fix.mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F ::: α)) :
α

Constructor for fix F

Equations
def mvqpf.fix.dest {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
α F ::: α)

Destructor for fix F

Equations
theorem mvqpf.fix.rec_eq {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) (x : F ::: α)) :
= g x)
theorem mvqpf.fix.ind_aux {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f : (mvqpf.P F).last.B a (mvqpf.P F).W α) :
mvqpf.fix.mk (mvqpf.abs a, f' (λ (x : (mvqpf.P F).last.B a), f x)⟩) = (mvqpf.P F).W_mk a f' f
theorem mvqpf.fix.ind_rec {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g₁ g₂ : α β) (h : (x : F ::: α)), x = x g₁ (mvqpf.fix.mk x) = g₂ (mvqpf.fix.mk x)) (x : α) :
g₁ x = g₂ x
theorem mvqpf.fix.rec_unique {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : F ::: β) β) (h : α β) (hyp : (x : F ::: α)), h (mvqpf.fix.mk x) = g x)) :
theorem mvqpf.fix.mk_dest {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : α) :
theorem mvqpf.fix.dest_mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F ::: α)) :
theorem mvqpf.fix.ind {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (p : α Prop) (h : (x : F ::: α)), mvfunctor.liftp (α.pred_last p) x p (mvqpf.fix.mk x)) (x : α) :
p x
@[protected, instance]
def mvqpf.mvqpf_fix {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] :
Equations
def mvqpf.fix.drec {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : α Type u} (g : Π (x : F ::: sigma β)), β ) (x : α) :
β x

Dependent recursor for fix F

Equations