mathlib documentation

data.qpf.multivariate.constructions.quot

The quotient of QPF is itself a QPF

The quotients are here defined using a surjective function and its right inverse. They are very similar to the abs and repr functions found in the definition of mvqpf

def mvqpf.quotient_qpf {n : } {F : typevec nType u} [mvfunctor F] [q : mvqpf F] {G : typevec nType u} [mvfunctor G] {FG_abs : Π {α : typevec n}, F αG α} {FG_repr : Π {α : typevec n}, G αF α} :
(∀ {α : typevec n} (x : G α), FG_abs (FG_repr x) = x)(∀ {α β : typevec n} (f : α β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x)mvqpf G

If F is a QPF then G is a QPF as well. Can be used to construct mvqpf instances by transporting them across surjective functions

Equations
def mvqpf.quot1 {n : } {F : typevec nType u} :
(Π ⦃α : typevec n⦄, F αF α → Prop)typevec nType u

Functorial quotient type

Equations
@[instance]
def mvqpf.quot1.inhabited {n : } {F : typevec nType u} (R : Π ⦃α : typevec n⦄, F αF α → Prop) {α : typevec n} [inhabited (F α)] :

Equations
def mvqpf.quot1.map {n : } {F : typevec nType u} (R : Π ⦃α : typevec n⦄, F αF α → Prop) [mvfunctor F] (Hfunc : ∀ ⦃α β : typevec n⦄ (a b : F α) (f : α β), R a bR (f <$$> a) (f <$$> b)) ⦃α β : typevec n⦄ :
α βmvqpf.quot1 R αmvqpf.quot1 R β

map of the quot1 functor

Equations
def mvqpf.quot1.mvfunctor {n : } {F : typevec nType u} (R : Π ⦃α : typevec n⦄, F αF α → Prop) [mvfunctor F] :
(∀ ⦃α β : typevec n⦄ (a b : F α) (f : α β), R a bR (f <$$> a) (f <$$> b))mvfunctor (mvqpf.quot1 R)

mvfunctor instance for quot1 with well-behaved R

Equations
def mvqpf.rel_quot {n : } {F : typevec nType u} (R : Π ⦃α : typevec n⦄, F αF α → Prop) [mvfunctor F] [q : mvqpf F] (Hfunc : ∀ ⦃α β : typevec n⦄ (a b : F α) (f : α β), R a bR (f <$$> a) (f <$$> b)) :

quot1 is a qpf

Equations