mathlib3 documentation

data.qpf.multivariate.constructions.prj

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

mvqpf.prj i v = v i

Instances for mvqpf.prj

@[protected, instance]

def mvqpf.prj.inhabited {n : ℕ} (i : fin2 n) {v : typevec n} [inhabited (v i)] :

inhabited (mvqpf.prj i v)

Equations

mvqpf.prj.inhabited i = {default := inhabited.default _inst_1}

def mvqpf.prj.map {n : ℕ} (i : fin2 n) ⦃α : typevec n⦄ ⦃β : typevec n⦄ (f : α.arrow β) :

mvqpf.prj i α → mvqpf.prj i β

map on functor prj i

Equations

mvqpf.prj.map i f = f i

@[protected, instance]

def mvqpf.prj.mvfunctor {n : ℕ} (i : fin2 n) :

mvfunctor (mvqpf.prj i)

Equations

mvqpf.prj.mvfunctor i = {map := mvqpf.prj.map i}

def mvqpf.prj.P {n : ℕ} (i : fin2 n) :

Polynomial representation of the projection functor

Equations

mvqpf.prj.P i = {A := punit, B := λ (_x : punit) (j : fin2 n), ulift (plift (i = j))}

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

mvqpf.prj.abs i ⟨x, f⟩ = f i {down := {down := _}}

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

mvqpf.prj.repr i = λ (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) :

mvqpf (mvqpf.prj i)

Equations

mvqpf.prj.mvqpf i = {P := mvqpf.prj.P i, abs := mvqpf.prj.abs i, repr := mvqpf.prj.repr i, abs_repr := _, abs_map := _}