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)

multivariate polynomial functors

  • A : Type u

    The head type

  • B : self.ATypeVec.{u} n

    The child family of types

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

    Applying P to an object of Type

    Equations
    Instances For
      Equations
      • MvPFunctor.instCoeFunMvPFunctorForAllTypeVecType = { coe := MvPFunctor.Obj }
      def MvPFunctor.map {n : } (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : TypeVec.Arrow α β) :
      P αP β

      Applying P to a morphism of Type

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

        Constant functor where the input object does not affect the output

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

          Constructor for the constant functor

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

            Destructor for the constant functor

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

              Functor composition on polynomial functors

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def MvPFunctor.comp.mk {n : } {m : } {P : MvPFunctor.{u} n} {Q : Fin2 nMvPFunctor.{u} m} {α : TypeVec.{u} m} (x : P fun (i : Fin2 n) => (Q i) α) :
                (MvPFunctor.comp P Q) α

                Constructor for functor composition

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def MvPFunctor.comp.get {n : } {m : } {P : MvPFunctor.{u} n} {Q : Fin2 nMvPFunctor.{u} m} {α : TypeVec.{u} m} (x : (MvPFunctor.comp P Q) α) :
                  P fun (i : Fin2 n) => (Q i) α

                  Destructor for functor composition

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem MvPFunctor.comp.get_map {n : } {m : } {P : MvPFunctor.{u} n} {Q : Fin2 nMvPFunctor.{u} m} {α : TypeVec.{u} m} {β : TypeVec.{u} m} (f : TypeVec.Arrow α β) (x : (MvPFunctor.comp P Q) α) :
                    MvPFunctor.comp.get (MvFunctor.map f x) = MvFunctor.map (fun (i : Fin2 n) (x : (Q i) α) => MvFunctor.map f x) (MvPFunctor.comp.get x)
                    @[simp]
                    theorem MvPFunctor.comp.get_mk {n : } {m : } {P : MvPFunctor.{u} n} {Q : Fin2 nMvPFunctor.{u} m} {α : TypeVec.{u} m} (x : P fun (i : Fin2 n) => (Q i) α) :
                    @[simp]
                    theorem MvPFunctor.comp.mk_get {n : } {m : } {P : MvPFunctor.{u} n} {Q : Fin2 nMvPFunctor.{u} m} {α : TypeVec.{u} m} (x : (MvPFunctor.comp P Q) α) :
                    theorem MvPFunctor.liftP_iff {n : } {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (p : i : Fin2 n⦄ → α iProp) (x : P α) :
                    MvFunctor.LiftP p x ∃ (a : P.A) (f : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := f } ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
                    theorem MvPFunctor.liftP_iff' {n : } {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (p : i : Fin2 n⦄ → α iProp) (a : P.A) (f : TypeVec.Arrow (P.B a) α) :
                    MvFunctor.LiftP p { fst := a, snd := f } ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
                    theorem MvPFunctor.liftR_iff {n : } {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (r : i : Fin2 n⦄ → α iα iProp) (x : P α) (y : P α) :
                    MvFunctor.LiftR r x y ∃ (a : P.A) (f₀ : TypeVec.Arrow (P.B a) α) (f₁ : TypeVec.Arrow (P.B a) α), x = { fst := a, snd := f₀ } y = { fst := a, snd := f₁ } ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
                    theorem MvPFunctor.supp_eq {n : } {P : MvPFunctor.{u} n} {α : TypeVec.{u} n} (a : P.A) (f : TypeVec.Arrow (P.B a) α) (i : Fin2 n) :
                    MvFunctor.supp { fst := a, snd := f } i = f i '' Set.univ

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

                    Equations
                    Instances For

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

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

                        append arrows of a polynomial functor application

                        Equations
                        Instances For