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 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-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 -ary vectors has the following nice property: If is an -ary vector with entries for some other -module , 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.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 with itself, times (indirectly justifying the notation while weβre at it). Note that this is a product in the category -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