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 : } (i : fin2 n) (v : typevec n) :

The projection i functor

Equations
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
@[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⦄ :

Abstraction function of the qpf instance

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

Representation function of the qpf instance

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