mathlib3 documentation

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

source
def mvqpf.comp {n m : ℕ} (F : typevec n → Type u_1) (G : fin2 n → typevec m → 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
Instances for mvqpf.comp
source
@[protected, instance]
def mvqpf.comp.inhabited {n m : ℕ} {F : typevec n → Type u_1} {G : fin2 n → typevec m → Type u} {α : typevec m} [I : inhabited (F (λ (i : fin2 n), G i α))] :
inhabited (mvqpf.comp F G α)
Equations
source
@[protected]
def mvqpf.comp.mk {n m : ℕ} {F : typevec n → Type u_1} {G : fin2 n → typevec m → Type u} {α : typevec m} (x : F (λ (i : fin2 n), G i α)) :
mvqpf.comp F G α

Constructor for functor composition

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

Destructor for functor composition

Equations
source
@[protected, simp]
theorem mvqpf.comp.mk_get {n m : ℕ} {F : typevec n → Type u_1} {G : fin2 n → typevec m → Type u} {α : typevec m} (x : mvqpf.comp F G α) :
mvqpf.comp.mk x.get = x
source
@[protected, simp]
theorem mvqpf.comp.get_mk {n m : ℕ} {F : typevec n → Type u_1} {G : fin2 n → typevec m → Type u} {α : typevec m} (x : F (λ (i : fin2 n), G i α)) :
(mvqpf.comp.mk x).get = x
source
@[protected]
def mvqpf.comp.map' {n m : ℕ} {G : fin2 n → typevec m → 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
source
@[protected]
def mvqpf.comp.map {n m : ℕ} {F : typevec n → Type u_1} [fF : mvfunctor F] {G : fin2 n → typevec m → Type u} [fG : Π (i : fin2 n), mvfunctor (G i)] {α β : typevec m} (f : α.arrow β) :
mvqpf.comp F G α → mvqpf.comp F G β

The composition of functors is itself functorial

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