# mathlibdocumentation

data.qpf.multivariate.constructions.prj

Projection functors are QPFs. The n-ary projection functors on i is an n-ary functor F such that F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ

def mvqpf.prj {n : } (i : fin2 n) (v : typevec n) :
Type u

The projection i functor

Equations
• v = v i
Instances for mvqpf.prj
@[protected, instance]
def mvqpf.prj.inhabited {n : } (i : fin2 n) {v : typevec n} [inhabited (v i)] :
Equations
def mvqpf.prj.map {n : } (i : fin2 n) ⦃α : typevec n⦄ ⦃β : typevec n⦄ (f : α.arrow β) :
α β

map on functor prj i

Equations
• = f i
@[protected, instance]
def mvqpf.prj.mvfunctor {n : } (i : fin2 n) :
Equations
def mvqpf.prj.P {n : } (i : fin2 n) :

Polynomial representation of the projection functor

Equations
def mvqpf.prj.abs {n : } (i : fin2 n) ⦃α : typevec n⦄ :
(mvqpf.prj.P i).obj α α

Abstraction function of the qpf instance

Equations
def mvqpf.prj.repr {n : } (i : fin2 n) ⦃α : typevec n⦄ :
α(mvqpf.prj.P i).obj α

Representation function of the qpf instance

Equations
• = λ (x : α i), punit.star, λ (j : fin2 n) (_x : (mvqpf.prj.P i).B punit.star j), mvqpf.prj.repr._match_1 i x j _x
• mvqpf.prj.repr._match_1 i x j {down := {down := h}} = eq.rec x h
@[protected, instance]
def mvqpf.prj.mvqpf {n : } (i : fin2 n) :
Equations