mathlib3 documentation

data.pfunctor.multivariate.basic

Multivariate polynomial functors. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ?
B : self.A → typevec n

multivariate polynomial functors

Instances for mvpfunctor

mvpfunctor.has_sizeof_inst
mvpfunctor.inhabited

def mvpfunctor.obj {n : ℕ} (P : mvpfunctor n) (α : typevec n) :

Applying P to an object of Type

Equations

P.obj α = Σ (a : P.A), (P.B a).arrow α

Instances for mvpfunctor.obj

def mvpfunctor.map {n : ℕ} (P : mvpfunctor n) {α β : typevec n} (f : α.arrow β) :

P.obj α → P.obj β

Applying P to a morphism of Type

Equations

P.map f = λ (_x : P.obj α), mvpfunctor.map._match_1 P f _x
mvpfunctor.map._match_1 P f ⟨a, g⟩ = ⟨a, typevec.comp f g⟩

@[protected, instance]

def mvpfunctor.inhabited {n : ℕ} :

inhabited (mvpfunctor n)

Equations

mvpfunctor.inhabited = {default := {A := inhabited.default sort.inhabited, B := inhabited.default (pi.inhabited inhabited.default)}}

@[protected, instance]

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

inhabited (P.obj α)

Equations

mvpfunctor.obj.inhabited P = {default := ⟨inhabited.default _inst_1, λ (_x : fin2 n) (_x_1 : P.B inhabited.default _x), inhabited.default⟩}

@[protected, instance]

def mvpfunctor.obj.mvfunctor {n : ℕ} (P : mvpfunctor n) :

mvfunctor P.obj

Equations

mvpfunctor.obj.mvfunctor P = {map := P.map}

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 α) :

mvfunctor.map typevec.id x = x

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

mvfunctor.map (typevec.comp g f) x = mvfunctor.map g (mvfunctor.map f x)

@[protected, instance]

def mvpfunctor.obj.is_lawful_mvfunctor {n : ℕ} (P : mvpfunctor n) :

is_lawful_mvfunctor P.obj

def mvpfunctor.const (n : ℕ) (A : Type u) :

Constant functor where the input object does not affect the output

Equations

mvpfunctor.const n A = {A := A, B := λ (a : A) (i : fin2 n), pempty}

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

(mvpfunctor.const n A).obj α

Constructor for the constant functor

Equations

mvpfunctor.const.mk n x = ⟨x, λ (i : fin2 n) (a : (mvpfunctor.const n A).B x i), pempty.elim a⟩

def mvpfunctor.const.get {n : ℕ} {A : Type u} {α : typevec n} (x : (mvpfunctor.const n A).obj α) :

A

Destructor for the constant functor

Equations

mvpfunctor.const.get x = x.fst

@[simp]

theorem mvpfunctor.const.get_map {n : ℕ} {A : Type u} {α β : typevec n} (f : α.arrow β) (x : (mvpfunctor.const n A).obj α) :

mvpfunctor.const.get (mvfunctor.map f x) = mvpfunctor.const.get x

@[simp]

theorem mvpfunctor.const.get_mk {n : ℕ} {A : Type u} {α : typevec n} (x : A) :

mvpfunctor.const.get (mvpfunctor.const.mk n x) = x

@[simp]

theorem mvpfunctor.const.mk_get {n : ℕ} {A : Type u} {α : typevec n} (x : (mvpfunctor.const n A).obj α) :

mvpfunctor.const.mk n (mvpfunctor.const.get x) = x

def mvpfunctor.comp {n m : ℕ} (P : mvpfunctor n) (Q : fin2 n → 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 n → mvpfunctor m} {α : typevec m} (x : P.obj (λ (i : fin2 n), (Q i).obj α)) :

(P.comp Q).obj α

Constructor for functor composition

Equations

mvpfunctor.comp.mk x = ⟨⟨x.fst, λ (i : fin2 n) (a : P.B x.fst i), (x.snd i a).fst⟩, λ (i : fin2 m) (a : (P.comp Q).B ⟨x.fst, λ (i : fin2 n) (a : P.B x.fst i), (x.snd i a).fst⟩ i), (x.snd a.fst a.snd.fst).snd i a.snd.snd⟩

def mvpfunctor.comp.get {n m : ℕ} {P : mvpfunctor n} {Q : fin2 n → mvpfunctor m} {α : typevec m} (x : (P.comp Q).obj α) :

P.obj (λ (i : fin2 n), (Q i).obj α)

Destructor for functor composition

Equations

mvpfunctor.comp.get x = ⟨x.fst.fst, λ (i : fin2 n) (a : P.B x.fst.fst i), ⟨x.fst.snd i a, λ (j : fin2 m) (b : (Q i).B (x.fst.snd i a) j), x.snd j ⟨i, ⟨a, b⟩⟩⟩⟩

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

mvpfunctor.comp.get (mvfunctor.map f x) = mvfunctor.map (λ (i : fin2 n) (x : (Q i).obj α), mvfunctor.map f x) (mvpfunctor.comp.get x)

@[simp]

theorem mvpfunctor.comp.get_mk {n m : ℕ} {P : mvpfunctor n} {Q : fin2 n → mvpfunctor m} {α : typevec m} (x : P.obj (λ (i : fin2 n), (Q i).obj α)) :

mvpfunctor.comp.get (mvpfunctor.comp.mk x) = x

@[simp]

theorem mvpfunctor.comp.mk_get {n m : ℕ} {P : mvpfunctor n} {Q : fin2 n → mvpfunctor m} {α : typevec m} (x : (P.comp Q).obj α) :

mvpfunctor.comp.mk (mvpfunctor.comp.get x) = x

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) :

mvfunctor.supp ⟨a, f⟩ i = f i '' set.univ

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

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

Equations

P.drop = {A := P.A, B := λ (a : P.A), (P.B a).drop}

def mvpfunctor.last {n : ℕ} (P : mvpfunctor (n + 1)) :

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

Equations

P.last = {A := P.A, B := λ (a : P.A), (P.B a).last}

@[reducible]

def mvpfunctor.append_contents {n : ℕ} (P : mvpfunctor (n + 1)) {α : typevec 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

P.append_contents f' f = typevec.split_fun f' f