open import Algebra.Ring.Module open import Algebra.Group.Ab open import Algebra.Prelude open import Algebra.Group open import Algebra.Ring module Algebra.Ring.Module.Free {β} (R : Ring β) where
Free modulesπ
For a finite set of generators, we can define free modules very directly: for example, using vectors. For infinite sets, this definition does not work as well: rings do not admit infinite sums, so we would need a way to βtameβ the vectors so only a finite amount of information needs to be summed at a time. The usual definition, of being zero in all but finitely many indices, is problematic since we can not (unless the indexing set admits decidable equality) define the map .
Note: even if is not, strictly speaking, built on an underlying (sub)set of functions into , we will stick to the exponential notation for definiteness.
Fortunately, free objects have a very straightforward definition in type theory: they are initial objects in certain categories of algebras, so they can be presented as1 inductive types.
data Free-mod {ββ²} (A : Type ββ²) : Type (β β ββ²) where inc : A β Free-mod A _+_ : Free-mod A β Free-mod A β Free-mod A neg : Free-mod A β Free-mod A 0m : Free-mod A _Β·_ : β R β β Free-mod A β Free-mod A
The free module on is generated by elements of (the inc) constructor, the operations of an Abelian group (which we write with _+_), together with a scalar multiplication operation . The equations imposed are precisely those necessary to make _+_ into an abelian group, and the scalar multiplication into an action by . We also add a squash constructor, since modules must have an underlying set.
+-comm : β x y β x + y β‘ y + x +-assoc : β x y z β (x + y) + z β‘ x + (y + z) +-invl : β x β neg x + x β‘ 0m +-idl : β x β 0m + x β‘ x Β·-id : β x β R.1r Β· x β‘ x Β·-add-r : β x y z β x Β· (y + z) β‘ x Β· y + x Β· z Β·-add-l : β x y z β (x R.+ y) Β· z β‘ x Β· z + y Β· z Β·-assoc : β x y z β x Β· y Β· z β‘ (x R.* y) Β· z squash : is-set (Free-mod A)
In passing, we define a record to package together the data of a predicate on free modules: as long as it is prop-valued, we can prove something for all of by treating the group operations, the ring action, and the generators.
record Free-elim-prop {ββ² ββ²β²} {A : Type ββ²} (P : Free-mod A β Type ββ²β²) : Type (β β ββ² β ββ²β²) where no-eta-equality field has-is-prop : β x β is-prop (P x) P-0m : P 0m P-neg : β x β P x β P (neg x) P-inc : β x β P (inc x) P-Β· : β x y β P y β P (x Β· y) P-+ : β x y β P x β P y β P (x + y) elim : β x β P x
Iβll leave the definition of the group, Abelian group, and
-module
structures on
in this <details>
tag, since theyβre not particularly interesting. For every operation
and law, we simply use the corresponding constructors.
open Module-on using (_β_ ; β-id ; β-add-r ; β-add-l ; β-assoc) open make-group Group-on-free-mod : β {ββ²} {A : Type ββ²} β Group-on (Free-mod A) Group-on-free-mod = to-group-on Ξ» where .group-is-set β squash .unit β 0m .mul β _+_ .inv β neg .assoc β +-assoc .invl β +-invl .invr x β +-comm x (neg x) β +-invl _ .idl β +-idl Free-mod-ab-group : β {ββ²} {A : Type ββ²} β AbGroup _ Free-mod-ab-group {A = A} .object = el (Free-mod A) squash , Group-on-free-mod Free-mod-ab-group .witness = +-comm Module-on-free-mod : β {ββ²} {A : Type ββ²} β Module-on R (Free-mod-ab-group {A = A}) Module-on-free-mod ._β_ = _Β·_ Module-on-free-mod .β-id = Β·-id Module-on-free-mod .β-add-r = Β·-add-r Module-on-free-mod .β-add-l = Β·-add-l Module-on-free-mod .β-assoc = Β·-assoc Free-Mod : β {ββ²} β Type ββ² β Module (β β ββ²) R Free-Mod x .fst = Free-mod-ab-group {A = x} Free-Mod x .snd = Module-on-free-mod open Functor
fold-free-mod : β {β ββ²} {A : Type β} {G : AbGroup ββ²} (N : Module-on R G) β (A β AbGrp.β G) β Linear-map (Free-Mod A) (_ , N) Rings.id fold-free-mod {A = A} {G} N f = go-linear module fold-free-mod where private module N = Module (_ , N)
The endless constructors of Free-mod are powerless in the face of a function from the generators into the underlying type of an actual -module . Each operation is mapped to the corresponding operation on , so the path constructors are also handled by the witnesses that is an actual module. This function, annoying though it may be to write, is definitionally a linear map β saving us a bit of effort.
-- Rough: go : Free-mod A β N.Gβ go (inc x) = f x go (x Β· y) = x N.β go y go (x + y) = go x N.+ go y go (neg x) = N.G.inverse (go x) go 0m = N.G.unit go (+-comm x y i) = N.G.commutative {go x} {go y} i go (+-assoc x y z i) = N.G.associative {go x} {go y} {go z} (~ i) go (+-invl x i) = N.G.inversel {go x} i go (+-idl x i) = N.G.idl {go x} i go (Β·-id x i) = N.β-id (go x) i go (Β·-add-r x y z i) = N.β-add-r x (go y) (go z) i go (Β·-add-l x y z i) = N.β-add-l x y (go z) i go (Β·-assoc x y z i) = N.β-assoc x y (go z) i go (squash a b p q i j) = N.G.has-is-set (go a) (go b) (Ξ» i β go (p i)) (Ξ» i β go (q i)) i j go-linear : Linear-map (Free-Mod A) (G , N) Rings.id go-linear .map = go go-linear .linear r m s n = refl {-# DISPLAY fold-free-mod.go = fold-free-mod #-}
To prove that free modules have the expected universal property, it remains to show that if , then . Since weβre eliminating into a proposition, all we have to handle are the operation constructors, which is.. inductive, but manageable. Iβll leave the computation here if youβre interested:
open make-left-adjoint make-free-module : β {ββ²} β make-left-adjoint (Forget-module {β} {β β ββ²} R) make-free-module = go where go : make-left-adjoint (Forget-module R) go .free x = Free-Mod β£ x β£ go .unit x = Free-mod.inc go .universal {y = y} = fold-free-mod (y .snd) go .commutes f = refl go .unique {y = y} {f = f} {g = g} p = Linear-map-path (funext (Free-elim-prop.elim m)) where open Free-elim-prop module g = Linear-map g module y = Module y fold = fold-free-mod (y .snd) f .map m : Free-elim-prop (Ξ» a β fold-free-mod (y .snd) f .map a β‘ g .map a) m .has-is-prop x = hlevel! m .P-Β· x y p = x y.β fold y β‘β¨ ap (x y.β_) p β©β‘ x y.β g .map y β‘β¨ g.linear-simple _ _ β©β‘ g.map (x Β· y) β m .P-0m = sym g.has-group-hom.pres-id m .P-+ x y p q = fold x y.+ fold y β‘β¨ apβ y._+_ p q β©β‘ g.map x y.+ g.map y β‘Λβ¨ g.has-group-hom.pres-β _ _ β©β‘Λ g.map (x + y) β m .P-neg x p = y.G.inverse (fold x) β‘β¨ ap y.G.inverse p β©β‘ y.G.inverse (g.map x) β‘Λβ¨ g.has-group-hom.pres-inv β©β‘Λ g.map (neg x) β m .P-inc x = p $β x
After that calculation, we can β¨ just β¨ conclude that Free-module has the right universal property: that is, we can rearrange the proof above into the form of a functor and an adjunction.
Free-module : β {ββ²} β Functor (Sets (β β ββ²)) (R-Mod (β β ββ²) R) Free-module {ββ² = ββ²} = make-left-adjoint.to-functor (make-free-module {ββ² = ββ²}) Freeβ£Forget : β {ββ²} β Free-module {ββ²} β£ Forget-module R Freeβ£Forget {ββ²} = make-left-adjoint.to-left-adjoint (make-free-module {ββ² = ββ²})
truncated, higherβ©οΈ