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 : TypeVec.{u} n) :

The projection i functor

Equations
instance MvQPF.Prj.inhabited {n : } (i : Fin2 n) {v : TypeVec.{u} n} [Inhabited (v i)] :
Equations
def MvQPF.Prj.map {n : } (i : Fin2 n) ⦃α : TypeVec.{u_1} n ⦃β : TypeVec.{u_2} n (f : α.Arrow β) :
Prj i αPrj i β

map on functor Prj i

Equations
instance 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.{u_1} n :
(P i) αPrj i α

Abstraction function of the QPF instance

Equations
def MvQPF.Prj.repr {n : } (i : Fin2 n) ⦃α : TypeVec.{u_1} n :
Prj i α(P i) α

Representation function of the QPF instance

Equations
instance MvQPF.Prj.mvqpf {n : } (i : Fin2 n) :
Equations