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
Instances For
    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 α)] :
    Equations
    • MvQPF.Comp.instInhabited = I
    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 α) :
    MvQPF.Comp F G α

    Constructor for functor composition

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

      Destructor for functor composition

      Equations
      • x.get = x
      Instances For
        @[simp]
        theorem MvQPF.Comp.mk_get {n : } {m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} (x : MvQPF.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 α) :
        (MvQPF.Comp.mk x).get = x
        def MvQPF.Comp.map' {n : } {m : } {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} {β : 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
        Instances For
          def MvQPF.Comp.map {n : } {m : } {F : TypeVec.{u} nType u_1} {G : Fin2 nTypeVec.{u} mType u} {α : TypeVec.{u} m} {β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] :
          MvQPF.Comp F G αMvQPF.Comp F G β

          The composition of functors is itself functorial

          Equations
          Instances For
            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} {β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : F fun (i : Fin2 n) => G i α) :
            MvFunctor.map f (MvQPF.Comp.mk x) = MvQPF.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} {β : TypeVec.{u} m} (f : α.Arrow β) [MvFunctor F] [(i : Fin2 n) → MvFunctor (G i)] (x : MvQPF.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)] :
            Equations
            • One or more equations did not get rendered due to their size.