# 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 : A → TypeVec 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

• B : s.A

The child family of types

multivariate polynomial functors

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

Applying P to an object of Type

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

Applying P to a morphism of Type

Instances For
instance MvPFunctor.Obj.inhabited {n : } (P : ) {α : } [Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
instance MvPFunctor.instMvFunctorObj {n : } (P : ) :
theorem MvPFunctor.map_eq {n : } (P : ) {α : } {β : } (g : ) (a : P.A) (f : TypeVec.Arrow () α) :
MvFunctor.map g { fst := a, snd := f } = { fst := a, snd := }
theorem MvPFunctor.id_map {n : } (P : ) {α : } (x : ) :
MvFunctor.map TypeVec.id x = x
theorem MvPFunctor.comp_map {n : } (P : ) {α : } {β : } {γ : } (f : ) (g : ) (x : ) :
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) {α : } :

Constructor for the constant functor

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

Destructor for the constant functor

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

Functor composition on polynomial functors

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

Constructor for functor composition

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

Destructor for functor composition

Instances For
theorem MvPFunctor.comp.get_map {n : } {m : } {P : } {Q : Fin2 n} {α : } {β : } (f : ) (x : ) :
= MvFunctor.map (fun i x => ) ()
@[simp]
theorem MvPFunctor.comp.get_mk {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : MvPFunctor.Obj P fun i => MvPFunctor.Obj (Q i) α) :
@[simp]
theorem MvPFunctor.comp.mk_get {n : } {m : } {P : } {Q : Fin2 n} {α : } (x : ) :
theorem MvPFunctor.liftP_iff {n : } {P : } {α : } (p : i : Fin2 n⦄ → α iProp) (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 : } {α : } (p : i : Fin2 n⦄ → α iProp) (a : P.A) (f : TypeVec.Arrow () α) :
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 : } {α : } (r : i : Fin2 n⦄ → α iα iProp) (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 : } {α : } (a : P.A) (f : TypeVec.Arrow () α) (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)) {α : } {β : Type u_1} {a : P.A} (f' : TypeVec.Arrow () α) (f : β) :
TypeVec.Arrow () (α ::: β)

append arrows of a polynomial functor application

Instances For