Documentation

Mathlib.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 : } (F : TypeVec.{u} nType u_1) (G : Fin2 nTypeVec.{u} mType u) (v : TypeVec.{u} m) :
Type u_1

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

Equations
instance MvQPF.Comp.instInhabited {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} [I : Inhabited (F fun (i : Fin2 n) => G i α)] :
Inhabited (Comp F G α)
Equations
def MvQPF.Comp.mk {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} (x : F fun (i : Fin2 n) => G i α) :
Comp F G α

Constructor for functor composition

Equations
def MvQPF.Comp.get {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} (x : Comp F G α) :
F fun (i : Fin2 n) => G i α

Destructor for functor composition

Equations
@[simp]
theorem MvQPF.Comp.mk_get {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} (x : Comp F G α) :
@[simp]
theorem MvQPF.Comp.get_mk {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} (x : F fun (i : Fin2 n) => G i α) :
(Comp.mk x).get = x
def MvQPF.Comp.map' {n m : } {G : Fin2 nTypeVec.{u} mType u} {α β : TypeVec.{u} m} (f : α.Arrow β) [(i : Fin2 n) → MvFunctor (G i)] :
TypeVec.Arrow (fun (i : Fin2 n) => G i α) fun (i : Fin2 n) => G i β

map operation defined on a vector of functors

Equations
def MvQPF.Comp.map {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] :
Comp F G αComp F G β

The composition of functors is itself functorial

Equations
instance MvQPF.Comp.instMvFunctor {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] :
Equations
theorem MvQPF.Comp.map_mk {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : F fun (i : Fin2 n) => G i α) :
MvFunctor.map f (Comp.mk x) = Comp.mk (MvFunctor.map (fun (i : Fin2 n) (x : G i α) => MvFunctor.map f x) x)
theorem MvQPF.Comp.get_map {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : Comp F G α) :
(MvFunctor.map f x).get = MvFunctor.map (fun (i : Fin2 n) (x : G i α) => MvFunctor.map f x) x.get
instance MvQPF.Comp.inst {n m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} [MvQPF F] [(i : Fin2 n) → MvQPF (G i)] :
MvQPF (Comp F G)
Equations
  • One or more equations did not get rendered due to their size.