Documentation

Mathlib.Data.PFunctor.Multivariate.Basic

Multivariate polynomial functors. #

Multivariate polynomial functors are used for defining M-types and W-types. They map a type vector α to the type Σ a : A, B a ⟹ α, with A : Type and B : ATypeVec n. They interact well with Lean's inductive definitions because they guarantee that occurrences of α are positive.

structure MvPFunctor (n : ) :
Type (u + 1)
  • A : Type u

    The head type

  • B : s.ATypeVec n

    The child family of types

multivariate polynomial functors

Instances For
    def MvPFunctor.Obj {n : } (P : MvPFunctor n) (α : TypeVec n) :

    Applying P to an object of Type

    Instances For
      def MvPFunctor.map {n : } (P : MvPFunctor n) {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) :

      Applying P to a morphism of Type

      Instances For
        instance MvPFunctor.Obj.inhabited {n : } (P : MvPFunctor n) {α : TypeVec n} [Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
        theorem MvPFunctor.map_eq {n : } (P : MvPFunctor n) {α : TypeVec n} {β : TypeVec n} (g : TypeVec.Arrow α β) (a : P.A) (f : TypeVec.Arrow (MvPFunctor.B P a) α) :
        MvFunctor.map g { fst := a, snd := f } = { fst := a, snd := TypeVec.comp g f }
        theorem MvPFunctor.id_map {n : } (P : MvPFunctor n) {α : TypeVec n} (x : MvPFunctor.Obj P α) :
        MvFunctor.map TypeVec.id x = x
        theorem MvPFunctor.comp_map {n : } (P : MvPFunctor n) {α : TypeVec n} {β : TypeVec n} {γ : TypeVec n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow β γ) (x : MvPFunctor.Obj P α) :
        def MvPFunctor.const (n : ) (A : Type u) :

        Constant functor where the input object does not affect the output

        Instances For
          def MvPFunctor.const.mk (n : ) {A : Type u} (x : A) {α : TypeVec n} :

          Constructor for the constant functor

          Instances For
            def MvPFunctor.const.get {n : } {A : Type u} {α : TypeVec n} (x : MvPFunctor.Obj (MvPFunctor.const n A) α) :
            A

            Destructor for the constant functor

            Instances For
              @[simp]
              theorem MvPFunctor.const.get_mk {n : } {A : Type u} {α : TypeVec n} (x : A) :
              def MvPFunctor.comp {n : } {m : } (P : MvPFunctor n) (Q : Fin2 nMvPFunctor m) :

              Functor composition on polynomial functors

              Instances For
                def MvPFunctor.comp.mk {n : } {m : } {P : MvPFunctor n} {Q : Fin2 nMvPFunctor m} {α : TypeVec m} (x : MvPFunctor.Obj P fun i => MvPFunctor.Obj (Q i) α) :

                Constructor for functor composition

                Instances For
                  def MvPFunctor.comp.get {n : } {m : } {P : MvPFunctor n} {Q : Fin2 nMvPFunctor m} {α : TypeVec m} (x : MvPFunctor.Obj (MvPFunctor.comp P Q) α) :
                  MvPFunctor.Obj P fun i => MvPFunctor.Obj (Q i) α

                  Destructor for functor composition

                  Instances For
                    theorem MvPFunctor.comp.get_map {n : } {m : } {P : MvPFunctor n} {Q : Fin2 nMvPFunctor m} {α : TypeVec m} {β : TypeVec m} (f : TypeVec.Arrow α β) (x : MvPFunctor.Obj (MvPFunctor.comp P Q) α) :
                    @[simp]
                    theorem MvPFunctor.comp.get_mk {n : } {m : } {P : MvPFunctor n} {Q : Fin2 nMvPFunctor m} {α : TypeVec m} (x : MvPFunctor.Obj P fun i => MvPFunctor.Obj (Q i) α) :
                    @[simp]
                    theorem MvPFunctor.comp.mk_get {n : } {m : } {P : MvPFunctor n} {Q : Fin2 nMvPFunctor m} {α : TypeVec m} (x : MvPFunctor.Obj (MvPFunctor.comp P Q) α) :
                    theorem MvPFunctor.liftP_iff {n : } {P : MvPFunctor n} {α : TypeVec n} (p : i : Fin2 n⦄ → α iProp) (x : MvPFunctor.Obj P α) :
                    MvFunctor.LiftP p x a f, x = { fst := a, snd := f } ((i : Fin2 n) → (j : MvPFunctor.B P a i) → p i (f i j))
                    theorem MvPFunctor.liftP_iff' {n : } {P : MvPFunctor n} {α : TypeVec n} (p : i : Fin2 n⦄ → α iProp) (a : P.A) (f : TypeVec.Arrow (MvPFunctor.B P a) α) :
                    MvFunctor.LiftP p { fst := a, snd := f } (i : Fin2 n) → (x : MvPFunctor.B P a i) → p i (f i x)
                    theorem MvPFunctor.liftR_iff {n : } {P : MvPFunctor n} {α : TypeVec n} (r : i : Fin2 n⦄ → α iα iProp) (x : MvPFunctor.Obj P α) (y : MvPFunctor.Obj P α) :
                    MvFunctor.LiftR r x y a f₀ f₁, x = { fst := a, snd := f₀ } y = { fst := a, snd := f₁ } ((i : Fin2 n) → (j : MvPFunctor.B P a i) → r i (f₀ i j) (f₁ i j))
                    theorem MvPFunctor.supp_eq {n : } {P : MvPFunctor n} {α : TypeVec n} (a : P.A) (f : TypeVec.Arrow (MvPFunctor.B P a) α) (i : Fin2 n) :
                    MvFunctor.supp { fst := a, snd := f } i = f i '' Set.univ
                    def MvPFunctor.drop {n : } (P : MvPFunctor (n + 1)) :

                    Split polynomial functor, get an n-ary functor from an n+1-ary functor

                    Instances For
                      def MvPFunctor.last {n : } (P : MvPFunctor (n + 1)) :

                      Split polynomial functor, get a univariate functor from an n+1-ary functor

                      Instances For
                        @[reducible]
                        def MvPFunctor.appendContents {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u_1} {a : P.A} (f' : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) a) α) (f : PFunctor.B (MvPFunctor.last P) aβ) :

                        append arrows of a polynomial functor application

                        Instances For