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 n Type u} [mvfunctor F] [q : mvqpf F] {G : typevec n 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 (mvfunctor.map f x) = mvfunctor.map 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 : typevec n Type u} (R : Π ⦃α : typevec n⦄, F α F α Prop) (α : typevec n) :

Functorial quotient type

Equations
Instances for mvqpf.quot1
@[protected, instance]
def mvqpf.quot1.inhabited {n : } {F : typevec n Type u} (R : Π ⦃α : typevec n⦄, F α F α Prop) {α : typevec n} [inhabited (F α)] :
Equations
def mvqpf.quot1.map {n : } {F : typevec n Type u} (R : Π ⦃α : typevec n⦄, F α F α Prop) [mvfunctor F] (Hfunc : ⦃α β : typevec n⦄ (a b : F α) (f : α.arrow β), R a b R (mvfunctor.map f a) (mvfunctor.map f b)) ⦃α β : typevec n⦄ (f : α.arrow β) :

map of the quot1 functor

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

mvfunctor instance for quot1 with well-behaved R

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

quot1 is a qpf

Equations