mathlib docs: 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

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

source

@[instance]

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

inhabited (mvqpf.sigma F α)

Equations

mvqpf.sigma.inhabited F = {default := ⟨default A _inst_1, default (F (default A) α) _inst_2⟩}

source

@[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), default (F a α)}

source

@[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 : α ⟹ β) (_x : mvqpf.sigma F α), mvqpf.sigma.mvfunctor._match_1 F α β f _x}
mvqpf.sigma.mvfunctor._match_1 F α β f ⟨a, x⟩ = ⟨a, f <$$> x⟩

source

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

def mvqpf.sigma.abs {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ (a : (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

def mvqpf.sigma.repr {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ (a : 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

@[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

@[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 : α ⟹ β) (x : mvqpf.pi F α) (a : A), f <$$> x a}

source

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

def mvqpf.pi.abs {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ (a : (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

def mvqpf.pi.repr {n : ℕ} {A : Type u} (F : A → typevec n → Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ (a : 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

@[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 := _}

mathlib documentation

Dependent product and sum of QPFs are QPFs