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
    • P α = ((a : P.A) × (P.B a).Arrow α)
    Instances For
      Equations
      • MvPFunctor.instCoeFunForallTypeVecType = { coe := MvPFunctor.Obj }
      def MvPFunctor.map {n : } (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) :
      P αP β

      Applying P to a morphism of Type

      Equations
      Instances For
        Equations
        • MvPFunctor.instInhabited = { 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
        Equations
        theorem MvPFunctor.map_eq {n : } (P : MvPFunctor.{u} n) {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f : (P.B a).Arrow α) :
        MvFunctor.map g a, f = a, 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 : α.Arrow β) (g : β.Arrow γ) (x : P α) :
        Equations
        • =

        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]
              theorem MvPFunctor.const.get_map {n : } {A : Type u} {α : TypeVec.{u} n} {β : TypeVec.{u} n} (f : α.Arrow β) (x : (MvPFunctor.const n A) α) :
              @[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) α) :
                (P.comp 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 : (P.comp Q) α) :
                  P fun (i : Fin2 n) => (Q i) α

                  Destructor for functor composition

                  Equations
                  • MvPFunctor.comp.get x = x.fst.fst, fun (i : Fin2 n) (a : P.B x.fst.fst i) => x.fst.snd i a, fun (j : Fin2 m) (b : (Q i).B (x.fst.snd i a) j) => x.snd j i, a, b
                  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 : α.Arrow β) (x : (P.comp 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 : (P.comp 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 : (P.B a).Arrow α), x = a, 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 : (P.B a).Arrow α) :
                    MvFunctor.LiftP p a, 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₀ : (P.B a).Arrow α) (f₁ : (P.B a).Arrow α), x = a, f₀ y = a, 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 : (P.B a).Arrow α) (i : Fin2 n) :
                    MvFunctor.supp a, f i = f i '' Set.univ

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

                    Equations
                    • P.drop = { A := P.A, B := fun (a : P.A) => (P.B a).drop }
                    Instances For

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

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

                        append arrows of a polynomial functor application

                        Equations
                        Instances For