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

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

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

    Constructor for functor composition

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

      Destructor for functor composition

      Instances For
        @[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 fun i => G i α) :
        def MvQPF.Comp.map' {n : } {m : } {G : Fin2 nTypeVec mType u} [fG : (i : Fin2 n) → MvFunctor (G i)] {α : TypeVec m} {β : TypeVec m} (f : TypeVec.Arrow α β) :
        TypeVec.Arrow (fun i => G i α) fun i => G i β

        map operation defined on a vector of functors

        Instances For
          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} {β : TypeVec m} (f : TypeVec.Arrow α β) :
          MvQPF.Comp F G αMvQPF.Comp F G β

          The composition of functors is itself functorial

          Instances For
            instance MvQPF.Comp.instMvFunctorComp {n : } {m : } {F : TypeVec nType u_1} [fF : MvFunctor F] {G : Fin2 nTypeVec mType u} [fG : (i : Fin2 n) → MvFunctor (G i)] :
            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} {β : TypeVec m} (f : TypeVec.Arrow α β) (x : F fun i => G i α) :
            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} {β : TypeVec m} (f : TypeVec.Arrow α β) (x : MvQPF.Comp F G α) :
            instance MvQPF.Comp.instMvQPFCompInstMvFunctorCompFin2 {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)] :