mathlib documentation

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 : } :
fin2 ntypevec nType u

The projection i functor

Equations
@[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⦄ :
α βmvqpf.prj i αmvqpf.prj i β

map on functor prj i

Equations
@[instance]
def mvqpf.prj.mvfunctor {n : } (i : fin2 n) :

Equations
def mvqpf.prj.P {n : } :

Polynomial representation of the projection functor

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

Abstraction function of the qpf instance

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

Representation function of the qpf instance

Equations
@[instance]
def mvqpf.prj.mvqpf {n : } (i : fin2 n) :

Equations