module Algebra.Ring.Module.Vec {β„“} (R : Ring β„“) where

The module of finite vectorsπŸ”—

Fix a ring and choose to be your favourite natural number β€” or a natural number you totally despise, that’s fine, too. A basic fact from high school linear algebra is that, for a natural number, β€œlists of reals” are a vector space over the field of real numbers Here we prove a generalisation of that fact: lists of elements of are a module over 

Fin-vec-module : βˆ€ n β†’ Module R β„“
Fin-vec-module n = to-module mk where
  mk : make-module R (Fin n β†’ ⌞ R ⌟)
  mk .make-module.has-is-set = hlevel 2
  mk .make-module._+_ f g i = f i R.+ g i
  mk .make-module.inv f i = R.- f i
  mk .make-module.0g i = R.0r
  mk .make-module._⋆_ f g i = f R.* g i

  mk .make-module.+-assoc f g h    = funext Ξ» i β†’ R.+-associative
  mk .make-module.+-invl f         = funext Ξ» i β†’ R.+-invl
  mk .make-module.+-idl f          = funext Ξ» i β†’ R.+-idl
  mk .make-module.+-comm f g       = funext Ξ» i β†’ R.+-commutes
  mk .make-module.⋆-distribl r x y = funext Ξ» i β†’ R.*-distribl
  mk .make-module.⋆-distribr r x y = funext Ξ» i β†’ R.*-distribr
  mk .make-module.⋆-assoc r s x    = funext Ξ» i β†’ R.*-associative
  mk .make-module.⋆-id x           = funext Ξ» i β†’ R.*-idl

Furthermore, the module of vectors has the following nice property: If is an vector with entries for some other there is a unique linear map which agrees with our original This map is given by linear extension: The vector gives rise to the map which sends to

  linear-extension : βˆ€ {n} β†’ (Fin n β†’ ⌞ S ⌟)
                   β†’ Linear-map (Fin-vec-module n) S
  linear-extension fun .map x = βˆ‘ G' Ξ» i β†’ x i S.⋆ fun i
  linear-extension fun .lin .linear r m n =
    βˆ‘ G' (Ξ» i β†’ (r R.* m i R.+ n i) S.⋆ fun i)                            β‰‘βŸ¨ ap (βˆ‘ G') (funext Ξ» i β†’ S.⋆-distribr (r R.* m i) (n i) (fun i)) ⟩
    βˆ‘ G' (Ξ» i β†’ (r R.* m i) S.⋆ fun i S.+ n i S.⋆ fun i)                  β‰‘βŸ¨ βˆ‘-split (Module-onβ†’Abelian-group-on (S .snd)) (Ξ» i β†’ (r R.* m i) S.⋆ fun i) _ ⟩
    ⌜ βˆ‘ G' (Ξ» i β†’ (r R.* m i) S.⋆ fun i) ⌝ S.+ βˆ‘ G' (Ξ» i β†’ n i S.⋆ fun i) β‰‘βŸ¨ ap! (ap (βˆ‘ G') (funext Ξ» i β†’ sym (S.⋆-assoc r (m i) _))) ⟩
    ⌜ βˆ‘ G' (Ξ» i β†’ r S.⋆ m i S.⋆ fun i) ⌝ S.+ βˆ‘ G' (Ξ» i β†’ n i S.⋆ fun i)   β‰‘Λ˜βŸ¨ apΒ‘ (βˆ‘-distr r Ξ» i β†’ m i S.⋆ fun i) ⟩
    (r S.⋆ βˆ‘ G' (Ξ» i β†’ m i S.⋆ fun i) S.+ βˆ‘ G' Ξ» i β†’ n i S.⋆ fun i)       ∎

As productsπŸ”—

To reduce how arbitrary the construction above seems, we show that the module of finite vectors is equivalently the finite product of with itself, times (indirectly justifying the notation while we’re at it). Note that this is a product in the category , not in the category of rings.

open is-indexed-product
open Indexed-product

Fin-vec-is-product
  : βˆ€ {n} β†’ Indexed-product (R-Mod R _) {Idx = Fin n} Ξ» _ β†’ representable-module R
Fin-vec-is-product {n} .Ξ F = Fin-vec-module n
Fin-vec-is-product .Ο€ i .hom k = k i
Fin-vec-is-product .Ο€ i .preserves .linear r m n = refl
Fin-vec-is-product {n} .has-is-ip .tuple {Y} f = assemble where
  assemble : R-Mod.Hom Y (Fin-vec-module n)
  assemble .hom yob ix = f ix # yob
  assemble .preserves .linear r m n = funext Ξ» i β†’ f i .preserves .linear _ _ _
Fin-vec-is-product .has-is-ip .commute = trivial!
Fin-vec-is-product .has-is-ip .unique {h = h} f ps =
  ext Ξ» i ix β†’ ap hom (ps ix) $β‚š i