[Agda] Formalization of Linear Algebra in agda

[Sergei Meshveliani]

On Tue, 2016-06-28 at 15:27 -0300, Guillermo Calderon wrote:

> Dear all,
>
> I am looking for a formalization  in Agda of vectorial spaces (over a 
> field).
> My concern is to work in the formalization of some concepts involved 
> with Grassman and Clifford algebras which are defined as extensions of
> vectorial spaces.
>
> I would be very grateful if anyone can give me some references on 
> this topic.
>
> Thanks,


DoCon-A of 0.04  is written in Agda, and it has

(I) definitions and many items for  Semigroup, Group, Ring, ... , Field,

(II) definitions for  LeftModule (over a ring)
     and  VectorSpace (over a field).

But (II) are only bare definitions. Like this:  

-----------------------------------------------------------------------
record LeftModule {α α= β β=} (upR  : UpRing α α=)
                              (upVG : UpCommutativeGroup β β=) :
                                                       Set (β= ⊔ β ⊔ α)
  where
  constructor lModule′

  private C    = UpRing.Carrier upR
          V    = UpCommutativeGroup.Carrier upVG
          upRd = UpRing.upRingoid upR

  field  _∙_            :  C → V → V         -- coefficient * vector  
         leftModuleLaws :  LeftModuleLaws upRd upVG _∙_

------------------------------------------------------------------------ 
ringAsLeftModule :  ∀ {α α=} (upR : UpRing α α=) →
                         let upA = Ring.+upCommGroup $ UpRing.ring upR
                         in  LeftModule upR upA

-- simple lemma about a ring

ringAsLeftModule upR =  lModule′ _*_ mLaws
  where
  open UpRing upR using (_*_; +upCommGroup; upRingoid; lDistrib;
                                                       rDistrib; *assoc)

  mLaws :  LeftModuleLaws upRingoid +upCommGroup _*_
  mLaws =
        record{ additiveByCoef       =  (\a b v → rDistrib v a b)
              ; additiveByVec        =  lDistrib
              ; moduleMulAssociative =  *assoc }

-----------------------------------------------------------------------

I hope to release DoCon-0.04 this summer (it remains to revise the
manual).

To program any real computation with vector spaces, one needs to add
definitions of a finite basis, decomposition by a basis, and so on.
Probably, I shall do this, because one can compute almost nothing in
algebra without using modules and vector spaces.
But may be this will not be this year.

Regards,

------
Sergei