data.qpf.multivariate.constructions.sigma

source

def mvqpf.sigma {n : ℕ} {A : Type u} (F : A → typevec n → Type u) (v : typevec n) :

Type u

Dependent sum of of an n-ary functor. The sum can range over data types like ℕ or over Type.{u-1}

Equations

mvqpf.sigma F v = Σ (α : A), F α v

Instances for mvqpf.sigma

source

def mvqpf.pi {n : ℕ} {A : Type u} (F : A → typevec n → Type u) (v : typevec n) :

Type u

Dependent product of of an n-ary functor. The sum can range over data types like ℕ or over Type.{u-1}

Equations

mvqpf.pi F v = Π (α : A), F α v

Instances for mvqpf.pi

source

@[protected, instance]

def mvqpf.sigma.inhabited {n : ℕ} {A : Type u} (F : A → typevec n → Type u) {α : typevec n} [inhabited A] [inhabited (F inhabited.default α)] :

inhabited (mvqpf.sigma F α)

Equations

mvqpf.sigma.inhabited F = {default := ⟨inhabited.default _inst_1, inhabited.default _inst_2⟩}

source

@[protected, instance]

def mvqpf.pi.inhabited {n : ℕ} {A : Type u} (F : A → typevec n → Type u) {α : typevec n} [Π (a : A), inhabited (F a α)] :

inhabited (mvqpf.pi F α)

Equations

mvqpf.pi.inhabited F = {default := λ (a : A), inhabited.default}

source

@[protected, instance]

def mvqpf.sigma.mvfunctor {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] :

mvfunctor (mvqpf.sigma F)

Equations

mvqpf.sigma.mvfunctor F = {map := λ (α β : typevec n) (f : α.arrow β) (_x : mvqpf.sigma F α), mvqpf.sigma.mvfunctor._match_1 F α β f _x}
mvqpf.sigma.mvfunctor._match_1 F α β f ⟨a, x⟩ = ⟨a, mvfunctor.map f x⟩

source

@[protected]

def mvqpf.sigma.P {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

mvpfunctor n

polynomial functor representation of a dependent sum

Equations

mvqpf.sigma.P F = {A := Σ (a : A), (mvqpf.P (F a)).A, B := λ (x : Σ (a : A), (mvqpf.P (F a)).A), (mvqpf.P (F x.fst)).B x.snd}

source

@[protected]

def mvqpf.sigma.abs {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

(mvqpf.sigma.P F).obj α → mvqpf.sigma F α

abstraction function for dependent sums

Equations

mvqpf.sigma.abs F ⟨a, f⟩ = ⟨a.fst, mvqpf.abs ⟨a.snd, f⟩⟩

source

@[protected]

def mvqpf.sigma.repr {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

mvqpf.sigma F α → (mvqpf.sigma.P F).obj α

representation function for dependent sums

Equations

mvqpf.sigma.repr F ⟨a, f⟩ = let x : (mvqpf.P (F a)).obj α := mvqpf.repr f in ⟨⟨a, x.fst⟩, x.snd⟩

source

@[protected, instance]

def mvqpf.sigma.mvqpf {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

mvqpf (mvqpf.sigma F)

Equations

mvqpf.sigma.mvqpf F = {P := mvqpf.sigma.P F (λ (α : A), _inst_2 α), abs := mvqpf.sigma.abs F (λ (α : A), _inst_2 α), repr := mvqpf.sigma.repr F (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}

source

@[protected, instance]

def mvqpf.pi.mvfunctor {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] :

mvfunctor (mvqpf.pi F)

Equations

mvqpf.pi.mvfunctor F = {map := λ (α β : typevec n) (f : α.arrow β) (x : mvqpf.pi F α) (a : A), mvfunctor.map f (x a)}

source

@[protected]

def mvqpf.pi.P {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

mvpfunctor n

polynomial functor representation of a dependent product

Equations

mvqpf.pi.P F = {A := Π (a : A), (mvqpf.P (F a)).A, B := λ (x : Π (a : A), (mvqpf.P (F a)).A) (i : fin2 n), Σ (a : A), (mvqpf.P (F a)).B (x a) i}

source

@[protected]

def mvqpf.pi.abs {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

(mvqpf.pi.P F).obj α → mvqpf.pi F α

abstraction function for dependent products

Equations

mvqpf.pi.abs F ⟨a, f⟩ = λ (x : A), mvqpf.abs ⟨a x, λ (i : fin2 n) (y : (mvqpf.P (F x)).B (a x) i), f i ⟨x, y⟩⟩

source

@[protected]

def mvqpf.pi.repr {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :

mvqpf.pi F α → (mvqpf.pi.P F).obj α

representation function for dependent products

Equations

mvqpf.pi.repr F f = ⟨λ (a : A), (mvqpf.repr (f a)).fst, λ (i : fin2 n) (a : (mvqpf.pi.P F).B (λ (a : A), (mvqpf.repr (f a)).fst) i), (mvqpf.repr (f a.fst)).snd i a.snd⟩

source

@[protected, instance]

def mvqpf.pi.mvqpf {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

mvqpf (mvqpf.pi F)

Equations

mvqpf.pi.mvqpf F = {P := mvqpf.pi.P F (λ (α : A), _inst_2 α), abs := mvqpf.pi.abs F (λ (α : A), _inst_2 α), repr := mvqpf.pi.repr F (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}

mathlib3 documentation

Dependent product and sum of QPFs are QPFs #