Documentation

Mathlib.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.quotientQPF {n : } {F : TypeVec.{u} nType u} [MvFunctor F] [q : MvQPF F] {G : TypeVec.{u} nType u} [MvFunctor G] {FG_abs : {α : TypeVec.{u} n} → F αG α} {FG_repr : {α : TypeVec.{u} n} → G αF α} (FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x) (FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : TypeVec.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
  • One or more equations did not get rendered due to their size.
Instances For
    def MvQPF.Quot1 {n : } {F : TypeVec.{u} nType u} (R : α : TypeVec.{u} n⦄ → F αF αProp) (α : TypeVec.{u} n) :

    Functorial quotient type

    Equations
    Instances For
      instance MvQPF.Quot1.inhabited {n : } {F : TypeVec.{u} nType u} (R : α : TypeVec.{u} n⦄ → F αF αProp) {α : TypeVec.{u} n} [Inhabited (F α)] :
      Equations
      def MvQPF.Quot1.map {n : } {F : TypeVec.{u} nType u} (R : α : TypeVec.{u} n⦄ → F αF αProp) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : TypeVec.Arrow α β), R a bR (MvFunctor.map f a) (MvFunctor.map f b)) ⦃α : TypeVec.{u} n ⦃β : TypeVec.{u} n (f : TypeVec.Arrow α β) :
      MvQPF.Quot1 R αMvQPF.Quot1 R β

      map of the Quot1 functor

      Equations
      Instances For
        def MvQPF.Quot1.mvFunctor {n : } {F : TypeVec.{u} nType u} (R : α : TypeVec.{u} n⦄ → F αF αProp) [MvFunctor F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : TypeVec.Arrow α β), R a bR (MvFunctor.map f a) (MvFunctor.map f b)) :

        mvFunctor instance for Quot1 with well-behaved R

        Equations
        Instances For
          noncomputable def MvQPF.relQuot {n : } {F : TypeVec.{u} nType u} (R : α : TypeVec.{u} n⦄ → F αF αProp) [MvFunctor F] [q : MvQPF F] (Hfunc : ∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : TypeVec.Arrow α β), R a bR (MvFunctor.map f a) (MvFunctor.map f b)) :

          Quot1 is a QPF

          Equations
          Instances For