# Documentation

## Mathlib.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 : ) :

The projection i functor

Equations
• = v i
Instances For
instance MvQPF.Prj.inhabited {n : } (i : Fin2 n) {v : } [Inhabited (v i)] :
Equations
• = { default := default }
def MvQPF.Prj.map {n : } (i : Fin2 n) ⦃α : ⦃β : (f : ) :

map on functor Prj i

Equations
• = f i
Instances For
instance MvQPF.Prj.mvfunctor {n : } (i : Fin2 n) :
Equations
• = { map := }
def MvQPF.Prj.P {n : } (i : Fin2 n) :

Polynomial representation of the projection functor

Equations
Instances For
def MvQPF.Prj.abs {n : } (i : Fin2 n) ⦃α : :
() α

Abstraction function of the QPF instance

Equations
• = match x with | { fst := _x, snd := f } => f i { down := { down := } }
Instances For
def MvQPF.Prj.repr {n : } (i : Fin2 n) ⦃α : :
() α

Representation function of the QPF instance

Equations
• = { fst := PUnit.unit, snd := fun (j : Fin2 n) (x_1 : ().B PUnit.unit j) => match x_1 with | { down := { down := h } } => hx }
Instances For
instance MvQPF.Prj.mvqpf {n : } (i : Fin2 n) :
Equations
• = { P := , abs := , repr := , abs_repr := , abs_map := }