mathlib documentation

data.qpf.multivariate.constructions.comp

The composition of QPFs is itself a QPF

We define composition between one n-ary functor and n m-ary functors and show that it preserves the QPF structure

def mvqpf.comp {n m : } :
(typevec nType u_1)(fin2 ntypevec mType u)typevec mType u_1

Composition of an n-ary functor with n m-ary functors gives us one m-ary functor

Equations
@[instance]
def mvqpf.comp.inhabited {n m : } {F : typevec nType u_1} {G : fin2 ntypevec mType u} {α : typevec m} [I : inhabited (F (λ (i : fin2 n), G i α))] :

Equations
def mvqpf.comp.mk {n m : } {F : typevec nType u_1} {G : fin2 ntypevec mType u} {α : typevec m} :
F (λ (i : fin2 n), G i α)mvqpf.comp F G α

Constructor for functor composition

Equations
def mvqpf.comp.get {n m : } {F : typevec nType u_1} {G : fin2 ntypevec mType u} {α : typevec m} :
mvqpf.comp F G αF (λ (i : fin2 n), G i α)

Destructor for functor composition

Equations
@[simp]
theorem mvqpf.comp.mk_get {n m : } {F : typevec nType u_1} {G : fin2 ntypevec mType u} {α : typevec m} (x : mvqpf.comp F G α) :

@[simp]
theorem mvqpf.comp.get_mk {n m : } {F : typevec nType u_1} {G : fin2 ntypevec mType u} {α : typevec m} (x : F (λ (i : fin2 n), G i α)) :

def mvqpf.comp.map' {n m : } {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} :
α β((λ (i : fin2 n), G i α) λ (i : fin2 n), G i β)

map operation defined on a vector of functors

Equations
def mvqpf.comp.map {n m : } {F : typevec nType u_1} [fF : mvfunctor F] {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} :
α βmvqpf.comp F G αmvqpf.comp F G β

The composition of functors is itself functorial

Equations
@[instance]
def mvqpf.comp.mvfunctor {n m : } {F : typevec nType u_1} [fF : mvfunctor F] {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] :

Equations
theorem mvqpf.comp.map_mk {n m : } {F : typevec nType u_1} [fF : mvfunctor F] {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α β) (x : F (λ (i : fin2 n), G i α)) :
f <$$> mvqpf.comp.mk x = mvqpf.comp.mk ((λ (i : fin2 n) (x : G i α), f <$$> x) <$$> x)

theorem mvqpf.comp.get_map {n m : } {F : typevec nType u_1} [fF : mvfunctor F] {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α β) (x : mvqpf.comp F G α) :
(f <$$> x).get = (λ (i : fin2 n) (x : G i α), f <$$> x) <$$> x.get

@[instance]
def mvqpf.comp.mvqpf {n m : } {F : typevec nType u_1} [fF : mvfunctor F] [q : mvqpf F] {G : fin2 ntypevec mType u} [fG : Π (i : fin2 n), mvfunctor (G i)] [q' : Π (i : fin2 n), mvqpf (G i)] :

Equations