# 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 α} (FG_abs_repr : ∀ {α : typevec n} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : typevec n} (f : α.arrow β) (x : F α), FG_abs x) = (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} (R : Π ⦃α : ⦄, F αF α → Prop) (α : typevec n) :
Type u

Functorial quotient type

Equations
• α = quot R
Instances for mvqpf.quot1
@[protected, 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 : α.arrow β), R a bR a) b)) ⦃α β : typevec n⦄ (f : α.arrow β) :
α β

map of the quot1 functor

Equations
• Hfunc f = quot.lift (λ (x : F α), quot.mk R x)) _
def mvqpf.quot1.mvfunctor {n : } {F : Type u} (R : Π ⦃α : ⦄, F αF α → Prop) [mvfunctor F] (Hfunc : ∀ ⦃α β : ⦄ (a b : F α) (f : α.arrow β), R a bR a) b)) :

mvfunctor instance for quot1 with well-behaved R

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

quot1 is a qpf

Equations
• Hfunc =