# mathlib3documentation

data.qpf.multivariate.constructions.sigma

# Dependent product and sum of QPFs are QPFs #

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

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

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

Equations
• v = Σ (α : A), F α v
Instances for mvqpf.sigma
def mvqpf.pi {n : } {A : Type u} (F : A Type u) (v : typevec n) :

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

Equations
• v = Π (α : A), F α v
Instances for mvqpf.pi
@[protected, instance]
def mvqpf.sigma.inhabited {n : } {A : Type u} (F : A Type u) {α : typevec n} [inhabited A] [inhabited α)] :
Equations
@[protected, instance]
def mvqpf.pi.inhabited {n : } {A : Type u} (F : A Type u) {α : typevec n} [Π (a : A), inhabited (F a α)] :
Equations
@[protected, instance]
def mvqpf.sigma.mvfunctor {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] :
Equations
• = {map := λ (α β : typevec n) (f : α.arrow β) (_x : α), mvqpf.sigma.mvfunctor._match_1 F α β f _x}
• mvqpf.sigma.mvfunctor._match_1 F α β f a, x⟩ = a, ⟩
@[protected]
def mvqpf.sigma.P {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent sum

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

abstraction function for dependent sums

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

representation function for dependent sums

Equations
@[protected, instance]
def mvqpf.sigma.mvqpf {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations
• = {P := (λ (α : A), _inst_2 α), abs := (λ (α : A), _inst_2 α), repr := (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}
@[protected, instance]
def mvqpf.pi.mvfunctor {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] :
Equations
@[protected]
def mvqpf.pi.P {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :

polynomial functor representation of a dependent product

Equations
@[protected]
def mvqpf.pi.abs {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
(mvqpf.pi.P F).obj α α

abstraction function for dependent products

Equations
@[protected]
def mvqpf.pi.repr {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] ⦃α : typevec n⦄ :
α (mvqpf.pi.P F).obj α

representation function for dependent products

Equations
@[protected, instance]
def mvqpf.pi.mvqpf {n : } {A : Type u} (F : A Type u) [Π (α : A), mvfunctor (F α)] [Π (α : A), mvqpf (F α)] :
Equations
• = {P := (λ (α : A), _inst_2 α), abs := (λ (α : A), _inst_2 α), repr := (λ (α : A), _inst_2 α), abs_repr := _, abs_map := _}