Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Prj

Projection functors are QPFs. The n-ary projection functors on i is an n-ary functor F such that F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ

def MvQPF.Prj {n : } (i : Fin2 n) (v : TypeVec.{u} n) :

The projection i functor

Equations
Instances For
    instance MvQPF.Prj.inhabited {n : } (i : Fin2 n) {v : TypeVec.{u} n} [Inhabited (v i)] :
    Equations
    def MvQPF.Prj.map {n : } (i : Fin2 n) ⦃α : TypeVec.{u_1} n ⦃β : TypeVec.{u_2} n (f : α.Arrow β) :
    MvQPF.Prj i αMvQPF.Prj i β

    map on functor Prj i

    Equations
    Instances For
      instance MvQPF.Prj.mvfunctor {n : } (i : Fin2 n) :
      Equations
      def MvQPF.Prj.P {n : } (i : Fin2 n) :

      Polynomial representation of the projection functor

      Equations
      Instances For
        def MvQPF.Prj.abs {n : } (i : Fin2 n) ⦃α : TypeVec.{u_1} n :
        (MvQPF.Prj.P i) αMvQPF.Prj i α

        Abstraction function of the QPF instance

        Equations
        • MvQPF.Prj.abs i x = match x with | _x, f => f i { down := { down := } }
        Instances For
          def MvQPF.Prj.repr {n : } (i : Fin2 n) ⦃α : TypeVec.{u_1} n :
          MvQPF.Prj i α(MvQPF.Prj.P i) α

          Representation function of the QPF instance

          Equations
          Instances For