mathlib documentation

data.​pfunctor.​multivariate.​basic

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  :
Type (u+1)

multivariate polynomial functors

def mvpfunctor.​obj {n : } :
mvpfunctor ntypevec nType u

Applying P to an object of Type

Equations
def mvpfunctor.​map {n : } (P : mvpfunctor n) {α β : typevec n} :
α.arrow βP.obj αP.obj β

Applying P to a morphism of Type

Equations
@[instance]

Equations
@[instance]
def mvpfunctor.​obj.​inhabited {n : } (P : mvpfunctor n) {α : typevec n} [inhabited P.A] [Π (i : fin2 n), inhabited (α i)] :
inhabited (P.obj α)

Equations
@[instance]

Equations
theorem mvpfunctor.​map_eq {n : } (P : mvpfunctor n) {α β : typevec 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 n) {α : typevec n} (x : P.obj α) :

theorem mvpfunctor.​comp_map {n : } (P : mvpfunctor n) {α β γ : typevec n} (f : α.arrow β) (g : β.arrow γ) (x : P.obj α) :

@[instance]

Equations
  • _ = _
def mvpfunctor.​const (n : ) :
Type umvpfunctor n

Constant functor where the input object does not affect the output

Equations
def mvpfunctor.​const.​mk (n : ) {A : Type u} (x : A) {α : typevec n} :

Constructor for the constant functor

Equations
def mvpfunctor.​const.​get {n : } {A : Type u} {α : typevec n} :
(mvpfunctor.const n A).obj α → A

Destructor for the constant functor

Equations
@[simp]
theorem mvpfunctor.​const.​get_map {n : } {A : Type u} {α β : typevec n} (f : α.arrow β) (x : (mvpfunctor.const n A).obj α) :

@[simp]
theorem mvpfunctor.​const.​get_mk {n : } {A : Type u} {α : typevec n} (x : A) :

@[simp]
theorem mvpfunctor.​const.​mk_get {n : } {A : Type u} {α : typevec n} (x : (mvpfunctor.const n A).obj α) :

def mvpfunctor.​comp {n m : } :
mvpfunctor n(fin2 nmvpfunctor m)mvpfunctor m

Functor composition on polynomial functors

Equations
  • P.comp Q = {A := Σ (a₂ : P.A), Π (i : fin2 n), P.B a₂ i(Q i).A, B := λ (a : Σ (a₂ : P.A), Π (i : fin2 n), P.B a₂ i(Q i).A) (i : fin2 m), Σ (j : fin2 n) (b : P.B a.fst j), (Q j).B (a.snd j b) i}
def mvpfunctor.​comp.​mk {n m : } {P : mvpfunctor n} {Q : fin2 nmvpfunctor m} {α : typevec m} :
P.obj (λ (i : fin2 n), (Q i).obj α)(P.comp Q).obj α

Constructor for functor composition

Equations
def mvpfunctor.​comp.​get {n m : } {P : mvpfunctor n} {Q : fin2 nmvpfunctor m} {α : typevec m} :
(P.comp Q).obj αP.obj (λ (i : fin2 n), (Q i).obj α)

Destructor for functor composition

Equations
theorem mvpfunctor.​comp.​get_map {n m : } {P : mvpfunctor n} {Q : fin2 nmvpfunctor m} {α β : typevec m} (f : α.arrow β) (x : (P.comp Q).obj α) :

@[simp]
theorem mvpfunctor.​comp.​get_mk {n m : } {P : mvpfunctor n} {Q : fin2 nmvpfunctor m} {α : typevec m} (x : P.obj (λ (i : fin2 n), (Q i).obj α)) :

@[simp]
theorem mvpfunctor.​comp.​mk_get {n m : } {P : mvpfunctor n} {Q : fin2 nmvpfunctor m} {α : typevec m} (x : (P.comp Q).obj α) :

theorem mvpfunctor.​liftp_iff {n : } {P : mvpfunctor n} {α : typevec n} (p : Π ⦃i : fin2 n⦄, α i → Prop) (x : P.obj α) :
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 n} {α : typevec n} (p : Π ⦃i : fin2 n⦄, α i → Prop) (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 n} {α : typevec n} (r : Π ⦃i : fin2 n⦄, α iα i → Prop) (x y : P.obj α) :
mvfunctor.liftr r x y ∃ (a : P.A) (f₀ 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 n} {α : typevec n} (a : P.A) (f : (P.B a).arrow α) (i : fin2 n) :

def mvpfunctor.​drop {n : } :
mvpfunctor (n + 1)mvpfunctor n

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

Equations
def mvpfunctor.​last {n : } :

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

Equations
def mvpfunctor.​append_contents {n : } (P : mvpfunctor (n + 1)) {α : typevec n} {β : Type u_1} {a : P.A} :
(P.drop.B a).arrow α(P.last.B a → β)(P.B a).arrow ::: β)

append arrows of a polynomial functor application

Equations