# mathlib3documentation

data.qpf.multivariate.constructions.comp

# The composition of QPFs is itself a QPF #

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

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 : } (F : Type u_1) (G : fin2 n Type u) (v : typevec m) :
Type u_1

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

Equations
• G v = F (λ (i : fin2 n), G i v)
Instances for mvqpf.comp
@[protected, instance]
def mvqpf.comp.inhabited {n m : } {F : Type u_1} {G : fin2 n Type u} {α : typevec m} [I : inhabited (F (λ (i : fin2 n), G i α))] :
inhabited G α)
Equations
@[protected]
def mvqpf.comp.mk {n m : } {F : Type u_1} {G : fin2 n Type u} {α : typevec m} (x : F (λ (i : fin2 n), G i α)) :
G α

Constructor for functor composition

Equations
@[protected]
def mvqpf.comp.get {n m : } {F : Type u_1} {G : fin2 n Type u} {α : typevec m} (x : G α) :
F (λ (i : fin2 n), G i α)

Destructor for functor composition

Equations
@[protected, simp]
theorem mvqpf.comp.mk_get {n m : } {F : Type u_1} {G : fin2 n Type u} {α : typevec m} (x : G α) :
@[protected, simp]
theorem mvqpf.comp.get_mk {n m : } {F : Type u_1} {G : fin2 n Type u} {α : typevec m} (x : F (λ (i : fin2 n), G i α)) :
.get = x
@[protected]
def mvqpf.comp.map' {n m : } {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α.arrow β) :
typevec.arrow (λ (i : fin2 n), G i α) (λ (i : fin2 n), G i β)

map operation defined on a vector of functors

Equations
@[protected]
def mvqpf.comp.map {n m : } {F : Type u_1} [fF : mvfunctor F] {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α.arrow β) :
G α G β

The composition of functors is itself functorial

Equations
@[protected, instance]
def mvqpf.comp.mvfunctor {n m : } {F : Type u_1} [fF : mvfunctor F] {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] :
Equations
theorem mvqpf.comp.map_mk {n m : } {F : Type u_1} [fF : mvfunctor F] {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α.arrow β) (x : F (λ (i : fin2 n), G i α)) :
= mvqpf.comp.mk (mvfunctor.map (λ (i : fin2 n) (x : G i α), x) x)
theorem mvqpf.comp.get_map {n m : } {F : Type u_1} [fF : mvfunctor F] {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α.arrow β) (x : G α) :
x).get = mvfunctor.map (λ (i : fin2 n) (x : G i α), x) x.get
@[protected, instance]
def mvqpf.comp.mvqpf {n m : } {F : Type u_1} [fF : mvfunctor F] [q : mvqpf F] {G : fin2 n Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] [q' : Π (i : fin2 n), mvqpf (G i)] :
Equations