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 $B \to R^B$.

Note: even if $R^B$ is not, strictly speaking, built on an underlying (sub)set of functions into $R$, 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 $A$ is generated by elements of $A$ (the inc) constructor, the operations of an Abelian group (which we write with _+_), together with a scalar multiplication operation $R \to R^A \to R^A$. The equations imposed are precisely those necessary to make _+_ into an abelian group, and the scalar multiplication into an action by $R$. 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 $R^A$ 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 $R$-module structures on $R^A$ 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 .⋆-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 $R$-module $N$. Each operation is mapped to the corresponding operation on $N$, so the path constructors are also handled by the witnesses that $N$ 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 $f = g\circ{\mathrm{inc}}$, then ${\mathrm{fold}}(f) = g$. 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 .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 {ℓ′ = ℓ′} =