[Agda] Re: Formalization of Linear Algebra in agda

[Guillermo Calderon]

Dear Sergei,

Thanks for your answer.
I will take a look to Docon.
Thanks
Guillermo

On 30/06/16 08:06, Sergei Meshveliani wrote:
> 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
>
>
>