Documentation

Mathlib.Data.QPF.Univariate.Basic

Quotients of Polynomial Functors #

We assume the following:

We define:

The main goal is to construct:

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) extends Functor :
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.abs_repr {F : Type u → Type u} [self : QPF F] {α : Type u} (x : F α) :
    theorem QPF.abs_map {F : Type u → Type u} [self : QPF F] {α : Type u} {β : Type u} (f : αβ) (p : (QPF.P F) α) :
    QPF.abs ((QPF.P F).map f p) = f <$> QPF.abs p
    theorem QPF.id_map {F : Type u → Type u} [q : QPF F] {α : Type u} (x : F α) :
    id <$> x = x
    theorem QPF.comp_map {F : Type u → Type u} [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} [q : QPF F] (h : ∀ (α β : Type u), Functor.mapConst = Functor.map Function.const β) :
    theorem QPF.liftp_iff {F : Type u → Type u} [q : QPF F] {α : Type u} (p : αProp) (x : F α) :
    Functor.Liftp p x ∃ (a : (QPF.P F).A) (f : (QPF.P F).B aα), x = QPF.abs a, f ∀ (i : (QPF.P F).B a), p (f i)
    theorem QPF.liftp_iff' {F : Type u → Type u} [q : QPF F] {α : Type u} (p : αProp) (x : F α) :
    Functor.Liftp p x ∃ (u : (QPF.P F) α), QPF.abs u = x ∀ (i : (QPF.P F).B u.fst), p (u.snd i)
    theorem QPF.liftr_iff {F : Type u → Type u} [q : QPF F] {α : Type u} (r : ααProp) (x : F α) (y : F α) :
    Functor.Liftr r x y ∃ (a : (QPF.P F).A) (f₀ : (QPF.P F).B aα) (f₁ : (QPF.P F).B aα), x = QPF.abs a, f₀ y = QPF.abs a, f₁ ∀ (i : (QPF.P F).B a), r (f₀ i) (f₁ i)
    def QPF.recF {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F αα) :
    (QPF.P F).Wα

    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} [q : QPF F] {α : Type u} (g : F αα) (x : (QPF.P F).W) :
      QPF.recF g x = g (QPF.abs ((QPF.P F).map (QPF.recF g) x.dest))
      theorem QPF.recF_eq' {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F αα) (a : (QPF.P F).A) (f : (QPF.P F).B a(QPF.P F).W) :
      QPF.recF g (WType.mk a f) = g (QPF.abs ((QPF.P F).map (QPF.recF g) a, f))
      inductive QPF.Wequiv {F : Type u → Type u} [q : QPF F] :
      (QPF.P F).W(QPF.P F).WProp

      two trees are equivalent if their F-abstractions are

      Instances For
        theorem QPF.recF_eq_of_Wequiv {F : Type u → Type u} [q : QPF F] {α : Type u} (u : F αα) (x : (QPF.P F).W) (y : (QPF.P F).W) :
        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} [q : QPF F] (x : (QPF.P F).W) (y : (QPF.P F).W) (h : QPF.abs x.dest = QPF.abs y.dest) :
        theorem QPF.Wequiv.refl {F : Type u → Type u} [q : QPF F] (x : (QPF.P F).W) :
        theorem QPF.Wequiv.symm {F : Type u → Type u} [q : QPF F] (x : (QPF.P F).W) (y : (QPF.P F).W) :
        def QPF.Wrepr {F : Type u → Type u} [q : QPF F] :
        (QPF.P F).W(QPF.P F).W

        maps every element of the W type to a canonical representative

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

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

          Equations
          • QPF.Wsetoid = { r := QPF.Wequiv, iseqv := }
          Instances For
            def QPF.Fix (F : Type u → Type u) [q : QPF F] :

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

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

              recursor of a type defined by a qpf

              Equations
              Instances For
                def QPF.fixToW {F : Type u → Type u} [q : QPF F] :
                QPF.Fix F(QPF.P F).W

                access the underlying W-type of a fixpoint data type

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

                  constructor of a type defined by a qpf

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

                    destructor of a type defined by a qpf

                    Equations
                    Instances For
                      theorem QPF.Fix.rec_eq {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F αα) (x : F (QPF.Fix F)) :
                      theorem QPF.Fix.ind_aux {F : Type u → Type u} [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a(QPF.P F).W) :
                      QPF.Fix.mk (QPF.abs a, fun (x : (QPF.P F).B a) => f x) = WType.mk a f
                      theorem QPF.Fix.ind_rec {F : Type u → Type u} [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} [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} [q : QPF F] (x : QPF.Fix F) :
                      QPF.Fix.mk x.dest = x
                      theorem QPF.Fix.dest_mk {F : Type u → Type u} [q : QPF F] (x : F (QPF.Fix F)) :
                      (QPF.Fix.mk x).dest = x
                      theorem QPF.Fix.ind {F : Type u → Type u} [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} [q : QPF F] {α : Type u} (g : αF α) :
                      α(QPF.P F).M

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

                      Equations
                      Instances For
                        theorem QPF.corecF_eq {F : Type u → Type u} [q : QPF F] {α : Type u} (g : αF α) (x : α) :
                        (QPF.corecF g x).dest = (QPF.P F).map (QPF.corecF g) (QPF.repr (g x))
                        def QPF.IsPrecongr {F : Type u → Type u} [q : QPF F] (r : (QPF.P F).M(QPF.P F).MProp) :

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

                        Equations
                        Instances For
                          def QPF.Mcongr {F : Type u → Type u} [q : QPF F] :
                          (QPF.P F).M(QPF.P F).MProp

                          The maximal congruence on q.P.M.

                          Equations
                          Instances For
                            def QPF.Cofix (F : Type u → Type u) [q : QPF F] :

                            coinductive type defined as the final coalgebra of a qpf

                            Equations
                            Instances For
                              instance QPF.instInhabitedCofixOfAP {F : Type u → Type u} [q : QPF F] [Inhabited (QPF.P F).A] :
                              Equations
                              • QPF.instInhabitedCofixOfAP = { default := Quot.mk QPF.Mcongr default }
                              def QPF.Cofix.corec {F : Type u → Type u} [q : QPF F] {α : Type u} (g : αF α) (x : α) :

                              corecursor for type defined by Cofix

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

                                destructor for type defined by Cofix

                                Equations
                                Instances For
                                  theorem QPF.Cofix.dest_corec {F : Type u → Type u} [q : QPF F] {α : Type u} (g : αF α) (x : α) :
                                  theorem QPF.Cofix.bisim_rel {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix FQPF.Cofix FProp) (h : ∀ (x y : QPF.Cofix F), r x yQuot.mk r <$> x.dest = Quot.mk r <$> y.dest) (x : QPF.Cofix F) (y : QPF.Cofix F) :
                                  r x yx = y
                                  theorem QPF.Cofix.bisim {F : Type u → Type u} [q : QPF F] (r : QPF.Cofix FQPF.Cofix FProp) (h : ∀ (x y : QPF.Cofix F), r x yFunctor.Liftr r x.dest y.dest) (x : QPF.Cofix F) (y : QPF.Cofix F) :
                                  r x yx = y
                                  theorem QPF.Cofix.bisim' {F : Type u → Type u} [q : QPF F] {α : Type u_1} (Q : αProp) (u : αQPF.Cofix F) (v : αQPF.Cofix F) (h : ∀ (x : α), Q x∃ (a : (QPF.P F).A) (f : (QPF.P F).B aQPF.Cofix F) (f' : (QPF.P F).B aQPF.Cofix F), (u x).dest = QPF.abs a, f (v x).dest = QPF.abs a, f' ∀ (i : (QPF.P F).B 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} [q₂ : QPF F₂] {F₁ : Type u → Type u} [q₁ : QPF F₁] :
                                  QPF (Functor.Comp F₂ F₁)

                                  composition of qpfs gives another qpf

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def QPF.quotientQPF {F : Type u → Type u} [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.

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

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

                                      Equations
                                      Instances For
                                        def QPF.LiftpPreservation {F : Type u → Type u} [q : QPF F] :

                                        does abs preserve Liftp?

                                        Equations
                                        Instances For
                                          def QPF.SuppPreservation {F : Type u → Type u} [q : QPF F] :

                                          does abs preserve supp?

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