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 n) :

The projection i functor

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

    map on functor Prj i

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

      Polynomial representation of the projection functor

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

        Abstraction function of the QPF instance

        Instances For
          def MvQPF.Prj.repr {n : } (i : Fin2 n) ⦃α : TypeVec n :

          Representation function of the QPF instance

          Instances For
            instance MvQPF.Prj.mvqpf {n : } (i : Fin2 n) :