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

The module of finite vectorsπŸ”—

Fix a ring RR and choose nn 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 nn a natural number, β€œlists of nn reals” are a vector space over the field of real numbers R\mathbb{R}. Here we prove a generalisation of that fact: lists of nn elements of RR are a module over RR.

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 nn-ary vectors has the following nice property: If v=(s0,...sn)v = (s_0, ... s_n) is an nn-ary vector with entries si:Ss_i : S for some other RR-module SS, there is a unique linear map Rn→SR^n \to S which agrees with our original vv. This map is given by linear extension: The vector vv gives rise to the map which sends ff to

βˆ‘i<nfivi. \sum_{i < n} f_iv_i\text{.} 

  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 RR with itself, nn times (indirectly justifying the notation RnR^n while we’re at it). Note that this is a product in the category RR-Mod, 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