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.Displayed.Univalence.Thin
open import Cat.Diagram.Product.Indexed
open import Cat.Prelude

open import Data.Fin.Base

module Algebra.Ring.Module.Vec {β} (R : Ring β) where

private module R = Ring-on (R .snd)
open make-abelian-group
open Module-on


# The module of finite vectorsπ

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

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 $n$-ary vectors has the following nice property: If $v = (s_0, ... s_n)$ is an $n$-ary vector with entries $s_i : S$ for some other $R$-module $S$, there is a unique linear map $R^n \to S$ which agrees with our original $v$. This map is given by linear extension: The vector $v$ gives rise to the map which sends $f$ to

$\sum_{i < n} f_iv_i\text{.}$

module _ {β'} (S : Module R β') where
private
module S = Module-on (S .snd)
G' = Module-onβGroup-on (S .snd)

β-distr : β {n} r (f : Fin n β β S β)
β r S.β β G' f
β‘ β G' Ξ» i β r S.β f i
β-distr {n = zero} r f = S.β-idr
β-distr {n = suc n} r f =
r S.β (f fzero S.+ β G' (Ξ» e β f (fsuc e)))            β‘β¨ S.β-distribl r (f fzero) _ β©β‘
(r S.β f fzero) S.+ β r S.β β G' (Ξ» e β f (fsuc e)) β  β‘β¨ ap! (β-distr {n} r (Ξ» e β f (fsuc e))) β©β‘
(r S.β f fzero) S.+ β G' (Ξ» i β r S.β f (fsuc i))      β

  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 $R$ with itself, $n$ times (indirectly justifying the notation $R^n$ while weβre at it). Note that this is a product in the category $R$-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