open import Algebra.Ring.Module
open import Algebra.Group.NAry
open import Algebra.Group.Ab
open import Algebra.Group
open import Algebra.Ring

open import Cat.Diagram.Coproduct.Indexed
open import Cat.Displayed.Univalence.Thin
open import Cat.Diagram.Product.Indexed
open import Cat.Functor.FullSubcategory
open import Cat.Prelude

open import Data.Dec
open import Data.Fin

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-group : βˆ€ n β†’ AbGroup β„“
Fin-vec-group n = to-abelian-group mg Ξ» x y β†’ funext Ξ» _ β†’ R.+-commutes where
  mg : make-group (Fin n β†’ ⌞ R ⌟)
  mg .group-is-set = hlevel!
  mg .unit _ = R.0r
  mg .mul f g i = f i R.+ g i
  mg .inv f i = R.- (f i)
  mg .assoc x y z = funext Ξ» _ β†’ sym R.+-associative
  mg .invl x = funext Ξ» _ β†’ R.+-invl
  mg .invr x = funext Ξ» _ β†’ R.+-invr
  mg .idl x = funext Ξ» _ β†’ R.+-idl

Fin-vec-module : βˆ€ n β†’ Module-on R (Fin-vec-group n)
Fin-vec-module n .Module-on._⋆_ r f i = r R.* f i
Fin-vec-module n .Module-on.⋆-id x = funext Ξ» i β†’ R.*-idl
Fin-vec-module n .Module-on.⋆-add-r r x y = funext Ξ» i β†’ R.*-distribl
Fin-vec-module n .Module-on.⋆-add-l r s x = funext Ξ» i β†’ R.*-distribr
Fin-vec-module n .Module-on.⋆-assoc r s x = funext Ξ» i β†’ R.*-associative

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.Gβ‚€)
                   β†’ Linear-map (_ , Fin-vec-module n) S Rings.id
  linear-extension fun .map x = βˆ‘ Gβ€² Ξ» i β†’ x i S.⋆ fun i
  linear-extension fun .linear r m s n =
    βˆ‘ Gβ€² (Ξ» i β†’ (r R.* m i R.+ s R.* n i) S.⋆ fun i)                          β‰‘βŸ¨ ap (βˆ‘ Gβ€²) (funext Ξ» i β†’ S.⋆-add-l (r R.* m i) (s R.* n i) (fun i)) βŸ©β‰‘
    βˆ‘ Gβ€² (Ξ» i β†’ ((r R.* m i) S.⋆ fun i) S.+ ((s R.* n i) S.⋆ fun i))          β‰‘βŸ¨ βˆ‘-split Gβ€² (S .fst .witness) (Ξ» i β†’ (r R.* m i) S.⋆ fun i) (Ξ» i β†’ (s R.* n i) S.⋆ fun i) βŸ©β‰‘
    (βˆ‘ Gβ€² Ξ» i β†’ (r R.* m i) S.⋆ fun i) S.+ (βˆ‘ Gβ€² Ξ» i β†’ (s R.* n i) S.⋆ fun i) β‰‘Λ˜βŸ¨ apβ‚‚ S._+_ (ap (βˆ‘ Gβ€²) (funext Ξ» i β†’ S.⋆-assoc r (m i) (fun i))) (ap (βˆ‘ Gβ€²) (funext Ξ» i β†’ S.⋆-assoc s (n i) (fun i))) βŸ©β‰‘Λ˜
    (βˆ‘ Gβ€² Ξ» i β†’ r S.⋆ (m i S.⋆ fun i)) S.+ (βˆ‘ Gβ€² Ξ» i β†’ s S.⋆ (n i S.⋆ fun i)) β‰‘Λ˜βŸ¨ apβ‚‚ S._+_ (βˆ‘-distr r Ξ» i β†’ m i S.⋆ fun i) (βˆ‘-distr s Ξ» i β†’ n i S.⋆ fun i) βŸ©β‰‘Λ˜
    (r S.⋆ βˆ‘ Gβ€² (Ξ» i β†’ m i S.⋆ fun i)) S.+ (s 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 .map k = k i
Fin-vec-is-product .Ο€ i .linear r m s n = refl
Fin-vec-is-product {n} .has-is-ip .tuple {Y} f = assemble where
  assemble : Linear-map Y (_ , Fin-vec-module n) Rings.id
  assemble .map yob ix = f ix .map yob
  assemble .linear r m s n = funext Ξ» i β†’ f i .linear _ _ _ _
Fin-vec-is-product .has-is-ip .commute = Linear-map-path (refl)
Fin-vec-is-product .has-is-ip .unique {h = h} f ps =
  Linear-map-path $ funext Ξ» i β†’ funext Ξ» ix β†’ ap map (ps ix) $β‚š i