mathlib3 documentation

data.qpf.multivariate.constructions.quot

The quotient of QPF is itself a QPF #

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

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

source
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)) :
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
source
def mvqpf.quot1 {n : ℕ} {F : typevec n → Type u} (R : Π ⦃α : typevec n⦄, F α → F α → Prop) (α : typevec n) :
Type u

Functorial quotient type

Equations
Instances for mvqpf.quot1
source
@[protected, instance]
def mvqpf.quot1.inhabited {n : ℕ} {F : typevec n → Type u} (R : Π ⦃α : typevec n⦄, F α → F α → Prop) {α : typevec n} [inhabited (F α)] :
inhabited (mvqpf.quot1 R α)
Equations
source
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 β) :
mvqpf.quot1 R α → mvqpf.quot1 R β

map of the quot1 functor

Equations
source
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 (mvqpf.quot1 R)

mvfunctor instance for quot1 with well-behaved R

Equations
source
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)) :
mvqpf (mvqpf.quot1 R)

quot1 is a qpf

Equations