Documentation

Mathlib.Data.QPF.Univariate.Basic

Quotients of Polynomial Functors #

We assume the following:

P : a polynomial functor W : its W-type M : its M-type F : a functor

We define:

q : Qpf data, representing F as a quotient of P

The main goal is to construct:

Fix : the initial algebra with structure map F FixFix. Cofix : the final coalgebra with structure map Cofix → F Cofix

We also show that the composition of qpfs is a qpf, and that the quotient of a qpf is a qpf.

The present theory focuses on the univariate case for qpfs

References #

class Qpf (F : Type u → Type u) [Functor F] :
Type (u + 1)

Quotients of polynomial functors.

Roughly speaking, saying that F is a quotient of a polynomial functor means that for each α, elements of F α are represented by pairs ⟨a, f⟩, where a is the shape of the object and f indexes the relevant elements of α, in a suitably natural manner.

Instances
    theorem Qpf.id_map {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) :
    id <$> x = x
    theorem Qpf.comp_map {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} {β : Type u} {γ : Type u} (f : αβ) (g : βγ) (x : F α) :
    (g f) <$> x = g <$> f <$> x
    theorem Qpf.lawfulFunctor {F : Type u → Type u} [Functor F] [q : Qpf F] (h : ∀ (α β : Type u), Functor.mapConst = Functor.map Function.const β) :
    theorem Qpf.liftp_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (p : αProp) (x : F α) :
    Functor.Liftp p x a f, x = Qpf.abs { fst := a, snd := f } ((i : PFunctor.B (Qpf.P F) a) → p (f i))
    theorem Qpf.liftp_iff' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (p : αProp) (x : F α) :
    Functor.Liftp p x u, Qpf.abs u = x ((i : PFunctor.B (Qpf.P F) u.fst) → p (Sigma.snd (Qpf.P F).A (fun x => PFunctor.B (Qpf.P F) xα) u i))
    theorem Qpf.liftr_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (r : ααProp) (x : F α) (y : F α) :
    Functor.Liftr r x y a f₀ f₁, x = Qpf.abs { fst := a, snd := f₀ } y = Qpf.abs { fst := a, snd := f₁ } ((i : PFunctor.B (Qpf.P F) a) → r (f₀ i) (f₁ i))
    def Qpf.recF {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) :
    PFunctor.W (Qpf.P F)α

    does recursion on q.P.W using g : F α → α rather than g : P α → α

    Equations
    Instances For
      theorem Qpf.recF_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) (x : PFunctor.W (Qpf.P F)) :
      theorem Qpf.recF_eq' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) aPFunctor.W (Qpf.P F)) :
      Qpf.recF g (WType.mk a f) = g (Qpf.abs (Qpf.recF g <$> { fst := a, snd := f }))
      inductive Qpf.Wequiv {F : Type u → Type u} [Functor F] [q : Qpf F] :

      two trees are equivalent if their F-abstractions are

      Instances For
        theorem Qpf.recF_eq_of_Wequiv {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (u : F αα) (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) :
        Qpf.Wequiv x yQpf.recF u x = Qpf.recF u y

        recF is insensitive to the representation

        theorem Qpf.Wequiv.abs' {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) (h : Qpf.abs (PFunctor.W.dest x) = Qpf.abs (PFunctor.W.dest y)) :
        theorem Qpf.Wequiv.refl {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) :
        theorem Qpf.Wequiv.symm {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) (y : PFunctor.W (Qpf.P F)) :
        def Qpf.Wrepr {F : Type u → Type u} [Functor F] [q : Qpf F] :

        maps every element of the W type to a canonical representative

        Instances For
          theorem Qpf.Wrepr_equiv {F : Type u → Type u} [Functor F] [q : Qpf F] (x : PFunctor.W (Qpf.P F)) :
          def Qpf.Wsetoid {F : Type u → Type u} [Functor F] [q : Qpf F] :

          Define the fixed point as the quotient of trees under the equivalence relation Wequiv.

          Instances For
            def Qpf.Fix (F : Type u → Type u) [Functor F] [q : Qpf F] :

            inductive type defined as initial algebra of a Quotient of Polynomial Functor

            Instances For
              def Qpf.Fix.rec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) :
              Qpf.Fix Fα

              recursor of a type defined by a qpf

              Instances For
                def Qpf.fixToW {F : Type u → Type u} [Functor F] [q : Qpf F] :

                access the underlying W-type of a fixpoint data type

                Instances For
                  def Qpf.Fix.mk {F : Type u → Type u} [Functor F] [q : Qpf F] (x : F (Qpf.Fix F)) :

                  constructor of a type defined by a qpf

                  Instances For
                    def Qpf.Fix.dest {F : Type u → Type u} [Functor F] [q : Qpf F] :
                    Qpf.Fix FF (Qpf.Fix F)

                    destructor of a type defined by a qpf

                    Instances For
                      theorem Qpf.Fix.rec_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) (x : F (Qpf.Fix F)) :
                      theorem Qpf.Fix.ind_aux {F : Type u → Type u} [Functor F] [q : Qpf F] (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) aPFunctor.W (Qpf.P F)) :
                      Qpf.Fix.mk (Qpf.abs { fst := a, snd := fun x => Quotient.mk Qpf.Wsetoid (f x) }) = Quotient.mk Qpf.Wsetoid (WType.mk a f)
                      theorem Qpf.Fix.ind_rec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g₁ : Qpf.Fix Fα) (g₂ : Qpf.Fix Fα) (h : ∀ (x : F (Qpf.Fix F)), g₁ <$> x = g₂ <$> xg₁ (Qpf.Fix.mk x) = g₂ (Qpf.Fix.mk x)) (x : Qpf.Fix F) :
                      g₁ x = g₂ x
                      theorem Qpf.Fix.rec_unique {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : F αα) (h : Qpf.Fix Fα) (hyp : ∀ (x : F (Qpf.Fix F)), h (Qpf.Fix.mk x) = g (h <$> x)) :
                      theorem Qpf.Fix.mk_dest {F : Type u → Type u} [Functor F] [q : Qpf F] (x : Qpf.Fix F) :
                      theorem Qpf.Fix.dest_mk {F : Type u → Type u} [Functor F] [q : Qpf F] (x : F (Qpf.Fix F)) :
                      theorem Qpf.Fix.ind {F : Type u → Type u} [Functor F] [q : Qpf F] (p : Qpf.Fix FProp) (h : (x : F (Qpf.Fix F)) → Functor.Liftp p xp (Qpf.Fix.mk x)) (x : Qpf.Fix F) :
                      p x
                      def Qpf.corecF {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : αF α) :
                      αPFunctor.M (Qpf.P F)

                      does recursion on q.P.M using g : α → F α rather than g : α → P α

                      Instances For
                        theorem Qpf.corecF_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : αF α) (x : α) :
                        def Qpf.IsPrecongr {F : Type u → Type u} [Functor F] [q : Qpf F] (r : PFunctor.M (Qpf.P F)PFunctor.M (Qpf.P F)Prop) :

                        A pre-congruence on q.P.M viewed as an F-coalgebra. Not necessarily symmetric.

                        Instances For
                          def Qpf.Mcongr {F : Type u → Type u} [Functor F] [q : Qpf F] :

                          The maximal congruence on q.P.M.

                          Instances For
                            def Qpf.Cofix (F : Type u → Type u) [Functor F] [q : Qpf F] :

                            coinductive type defined as the final coalgebra of a qpf

                            Instances For
                              instance Qpf.instInhabitedCofix {F : Type u → Type u} [Functor F] [q : Qpf F] [Inhabited (Qpf.P F).A] :
                              def Qpf.Cofix.corec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : αF α) (x : α) :

                              corecursor for type defined by Cofix

                              Instances For
                                def Qpf.Cofix.dest {F : Type u → Type u} [Functor F] [q : Qpf F] :
                                Qpf.Cofix FF (Qpf.Cofix F)

                                destructor for type defined by Cofix

                                Instances For
                                  theorem Qpf.Cofix.dest_corec {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (g : αF α) (x : α) :
                                  theorem Qpf.Cofix.bisim_rel {F : Type u → Type u} [Functor F] [q : Qpf F] (r : Qpf.Cofix FQpf.Cofix FProp) (h : ∀ (x y : Qpf.Cofix F), r x yQuot.mk r <$> Qpf.Cofix.dest x = Quot.mk r <$> Qpf.Cofix.dest y) (x : Qpf.Cofix F) (y : Qpf.Cofix F) :
                                  r x yx = y
                                  theorem Qpf.Cofix.bisim {F : Type u → Type u} [Functor F] [q : Qpf F] (r : Qpf.Cofix FQpf.Cofix FProp) (h : ∀ (x y : Qpf.Cofix F), r x yFunctor.Liftr r (Qpf.Cofix.dest x) (Qpf.Cofix.dest y)) (x : Qpf.Cofix F) (y : Qpf.Cofix F) :
                                  r x yx = y
                                  theorem Qpf.Cofix.bisim' {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u_1} (Q : αProp) (u : αQpf.Cofix F) (v : αQpf.Cofix F) (h : ∀ (x : α), Q xa f f', Qpf.Cofix.dest (u x) = Qpf.abs { fst := a, snd := f } Qpf.Cofix.dest (v x) = Qpf.abs { fst := a, snd := f' } ∀ (i : PFunctor.B (Qpf.P F) a), x', Q x' f i = u x' f' i = v x') (x : α) :
                                  Q xu x = v x
                                  def Qpf.comp {F₂ : Type u → Type u} [Functor F₂] [q₂ : Qpf F₂] {F₁ : Type u → Type u} [Functor F₁] [q₁ : Qpf F₁] :
                                  Qpf (Functor.Comp F₂ F₁)

                                  composition of qpfs gives another qpf

                                  Instances For
                                    def Qpf.quotientQpf {F : Type u → Type u} [Functor F] [q : Qpf F] {G : Type u → Type u} [Functor G] {FG_abs : {α : Type u} → F αG α} {FG_repr : {α : Type u} → G αF α} (FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs α (FG_repr α x) = x) (FG_abs_map : ∀ {α β : Type u} (f : αβ) (x : F α), FG_abs β (f <$> x) = f <$> FG_abs α x) :
                                    Qpf G

                                    Given a qpf F and a well-behaved surjection FG_abs from F α to functor G α, G is a qpf. We can consider G a quotient on F where elements x y : F α are in the same equivalence class if FG_abs x = FG_abs y.

                                    Instances For
                                      theorem Qpf.mem_supp {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) (u : α) :
                                      u Functor.supp x ∀ (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) aα), Qpf.abs { fst := a, snd := f } = xu f '' Set.univ
                                      theorem Qpf.supp_eq {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) :
                                      Functor.supp x = {u | ∀ (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) aα), Qpf.abs { fst := a, snd := f } = xu f '' Set.univ}
                                      theorem Qpf.has_good_supp_iff {F : Type u → Type u} [Functor F] [q : Qpf F] {α : Type u} (x : F α) :
                                      (∀ (p : αProp), Functor.Liftp p x ∀ (u : α), u Functor.supp xp u) a f, Qpf.abs { fst := a, snd := f } = x ∀ (a' : (Qpf.P F).A) (f' : PFunctor.B (Qpf.P F) a'α), Qpf.abs { fst := a', snd := f' } = xf '' Set.univ f' '' Set.univ
                                      def Qpf.IsUniform {F : Type u → Type u} [Functor F] [q : Qpf F] :

                                      A qpf is said to be uniform if every polynomial functor representing a single value all have the same range.

                                      Instances For
                                        def Qpf.LiftpPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] :

                                        does abs preserve Liftp?

                                        Instances For
                                          def Qpf.SuppPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] :

                                          does abs preserve supp?

                                          Instances For
                                            theorem Qpf.supp_eq_of_isUniform {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} (a : (Qpf.P F).A) (f : PFunctor.B (Qpf.P F) aα) :
                                            Functor.supp (Qpf.abs { fst := a, snd := f }) = f '' Set.univ
                                            theorem Qpf.liftp_iff_of_isUniform {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} (x : F α) (p : αProp) :
                                            Functor.Liftp p x (u : α) → u Functor.supp xp u
                                            theorem Qpf.supp_map {F : Type u → Type u} [Functor F] [q : Qpf F] (h : Qpf.IsUniform) {α : Type u} {β : Type u} (g : αβ) (x : F α) :
                                            theorem Qpf.suppPreservation_iff_uniform {F : Type u → Type u} [Functor F] [q : Qpf F] :
                                            Qpf.SuppPreservation Qpf.IsUniform
                                            theorem Qpf.suppPreservation_iff_liftpPreservation {F : Type u → Type u} [Functor F] [q : Qpf F] :
                                            Qpf.SuppPreservation Qpf.LiftpPreservation
                                            theorem Qpf.liftpPreservation_iff_uniform {F : Type u → Type u} [Functor F] [q : Qpf F] :
                                            Qpf.LiftpPreservation Qpf.IsUniform