# mathlibdocumentation

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 : Type u} [mvfunctor F] [q : mvqpf F] {G : Type 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)

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 : Type u} :
(Π ⦃α : ⦄, F αF α → Prop)Type u

Functorial quotient type

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

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

map of the quot1 functor

Equations
• Hfunc f = quot.lift (λ (x : F α), quot.mk R (f <$$> x)) _ def mvqpf.quot1.mvfunctor {n : } {F : Type u} (R : Π ⦃α : ⦄, F αF α → Prop) [mvfunctor F] : (∀ ⦃α β : ⦄ (a b : F α) (f : α β), R a bR (f <$$> a) (f <$$> b)) mvfunctor instance for quot1 with well-behaved R Equations def mvqpf.rel_quot {n : } {F : Type u} (R : Π ⦃α : ⦄, F αF α → Prop) [mvfunctor F] [q : mvqpf F] (Hfunc : ∀ ⦃α β : ⦄ (a b : F α) (f : α β), R a bR (f <$$> a) (f <> b)) :

quot1 is a qpf

Equations
• Hfunc =