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 (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ

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

The projection i functor

Instances For
    source
    instance MvQPF.Prj.inhabited {n : ℕ} (i : Fin2 n) {v : TypeVec n} [Inhabited (v i)] :
    Inhabited (MvQPF.Prj i v)
    source
    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
      source
      instance MvQPF.Prj.mvfunctor {n : ℕ} (i : Fin2 n) :
      MvFunctor (MvQPF.Prj i)
      source
      def MvQPF.Prj.P {n : ℕ} (i : Fin2 n) :
      MvPFunctor n

      Polynomial representation of the projection functor

      Instances For
        source
        def MvQPF.Prj.abs {n : ℕ} (i : Fin2 n) ⦃α : TypeVec n⦄ :
        MvPFunctor.Obj (MvQPF.Prj.P i) α → MvQPF.Prj i α

        Abstraction function of the QPF instance

        Instances For
          source
          def MvQPF.Prj.repr {n : ℕ} (i : Fin2 n) ⦃α : TypeVec n⦄ :
          MvQPF.Prj i α → MvPFunctor.Obj (MvQPF.Prj.P i) α

          Representation function of the QPF instance

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