open import Algebra.Ring.Commutative
open import Algebra.Ring.Module
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring

open import Data.Fin.Product
open import Data.Fin.Base

import Algebra.Ring.Module.Multilinear

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.

private module R = Ring-on (R .snd)

infixr 30 _·_
infixl 25 _+_


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
·-distribl : ∀ x y z → x · (y + z)   ≡ x · y + x · z
·-distribr : ∀ 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

  elim (inc x) = P-inc x
elim (x · y) = P-· x y (elim y)
elim (x + y) = P-+ x y (elim x) (elim y)
elim (neg x) = P-neg x (elim x)
elim 0m = P-0m
elim (+-comm x y i) =
is-prop→pathp (λ j → has-is-prop (+-comm x y j))
(P-+ x y (elim x) (elim y)) (P-+ y x (elim y) (elim x)) i
elim (+-assoc x y z i) =
is-prop→pathp (λ j → has-is-prop (+-assoc x y z j))
(P-+ _ _ (elim x) (P-+ _ _ (elim y) (elim z)))
(P-+ _ _ (P-+ _ _ (elim x) (elim y)) (elim z)) i
elim (+-invl x i) =
is-prop→pathp (λ j → has-is-prop (+-invl x j))
(P-+ _ _ (P-neg _ (elim x)) (elim x)) P-0m i
elim (+-idl x i) =
is-prop→pathp (λ j → has-is-prop (+-idl x j))
(P-+ _ _ P-0m (elim x)) (elim x) i
elim (·-id x i)  =
is-prop→pathp (λ j → has-is-prop (·-id x j))
(P-· R.1r _ (elim x)) (elim x) i
elim (·-distribl x y z i) =
is-prop→pathp (λ j → has-is-prop (·-distribl x y z j))
(P-· x _ (P-+ _ _ (elim y) (elim z)))
(P-+ _ _ (P-· x _ (elim y)) (P-· x _ (elim z))) i
elim (·-distribr x y z i) =
is-prop→pathp (λ j → has-is-prop (·-distribr x y z j ))
(P-· (x R.+ y) _ (elim z))
(P-+ _ _ (P-· x _ (elim z)) (P-· y _ (elim z))) i
elim (·-assoc x y z i) =
is-prop→pathp (λ j → has-is-prop (·-assoc x y z j))
(P-· x (y · z) (P-· y _ (elim z)))
(P-· (x R.* y) z (elim z)) i
elim (squash x y p q i j) =
is-prop→squarep (λ i j → has-is-prop (squash x y p q i j))
(λ _ → elim x) (λ j → elim (p j)) (λ j → elim (q j)) (λ _ → elim y) i j

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 hiding (_+_)
open make-module hiding (_+_)

Module-on-free-mod
: ∀ {ℓ′} (A : Type ℓ′)
→ Module-on R (Free-mod A)
Module-on-free-mod A = to-module-on mk module Module-on-free-mod where
mk : make-module R (Free-mod A)
mk .has-is-set = squash
mk .make-module._+_ = _+_
mk .inv = neg
mk .0g = 0m
mk .make-module.+-assoc = Free-mod.+-assoc
mk .make-module.+-invl = Free-mod.+-invl
mk .make-module.+-idl = Free-mod.+-idl
mk .make-module.+-comm = Free-mod.+-comm
mk ._⋆_ = _·_
mk .⋆-distribl = Free-mod.·-distribl
mk .⋆-distribr = Free-mod.·-distribr
mk .⋆-assoc x y z = Free-mod.·-assoc x y z
mk .⋆-id = Free-mod.·-id

Free-Mod : ∀ {ℓ′} → Type ℓ′ → Module R (ℓ ⊔ ℓ′)
Free-Mod T = to-module (Module-on-free-mod.mk T)

open Functor

fold-free-mod
: ∀ {ℓ ℓ′} {A : Type ℓ} (N : Module R ℓ′)
→ (A → ⌞ N ⌟)
→ Linear-map (Free-Mod A) N
fold-free-mod {A = A} N f = go-linear module fold-free-mod where
private module N = Module-on (N .snd)


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 ⌟
go (inc x) = f x
go (x · y) = x N.⋆ go y
go (x + y) = go x N.+ go y
go (neg x) = N.- (go x)
go 0m      = N.0g
go (+-comm x y i)       = N.+-comm {go x} {go y} i
go (+-assoc x y z i)    = N.+-assoc {go x} {go y} {go z} i
go (+-invl x i)         = N.+-invl {go x} i
go (+-idl x i)          = N.+-idl {go x} i
go (·-id x i)           = N.⋆-id (go x) i
go (·-distribl x y z i) = N.⋆-distribl x (go y) (go z) i
go (·-distribr x y z i) = N.⋆-distribr 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.has-is-set (go a) (go b) (λ i → go (p i)) (λ i → go (q i)) i j

go-linear : Linear-map (Free-Mod A) N
go-linear .map = go
go-linear .lin .linear r s t = refl

{-# DISPLAY fold-free-mod.go = fold-free-mod #-}
{-# DISPLAY fold-free-mod.go-linear = 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 : make-left-adjoint (Forget-structure (R-Mod-structure R))
go .free x = Free-Mod ∣ x ∣
go .unit x = Free-mod.inc
go .universal {y = y} f = linear-map→hom (fold-free-mod {ℓ = ℓ ⊔ ℓ′} y f)
go .commutes f = refl
go .unique {y = y} {f = f} {g = g} p = Homomorphism-path {ℓ ⊔ ℓ′} (Free-elim-prop.elim m) where
open Free-elim-prop
module g = Linear-map (hom→linear-map g)
module y = Module-on (y .snd)
fold = fold-free-mod y f .map
m : Free-elim-prop (λ a → fold-free-mod y 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.pres-⋆ _ _ ⟩≡˘
g.map (x · y)  ∎
m .P-0m = sym g.pres-0
m .P-+ x y p q =
fold x y.+ fold y   ≡⟨ ap₂ y._+_ p q ⟩≡
g.map x y.+ g.map y ≡˘⟨ g.pres-+ _ _ ⟩≡˘
g.map (x + y)       ∎
m .P-neg x p =
y.- (fold x)  ≡⟨ ap y.-_ p ⟩≡
y.- (g.map x) ≡˘⟨ g.pres-neg ⟩≡˘
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 {ℓ′ = ℓ′})  open Free-elim-prop equal-on-basis : ∀ {ℓb ℓg} {T : Type ℓb} (M : Module R ℓg) → {f g : Linear-map (Free-Mod T) M} → ((x : T) → f .map (inc x) ≡ g .map (inc x)) → f ≡ g equal-on-basis M {f} {g} p = Linear-map-path$ Free-elim-prop.elim λ where
.has-is-prop x → M .fst .is-tr _ _
.P-0m        → f.pres-0 ∙ sym g.pres-0
.P-neg x α   → f.pres-neg ·· ap M.-_ α ·· sym g.pres-neg
.P-inc       → p
.P-· x y α   → f.pres-⋆ _ _ ·· ap (x M.⋆_) α ·· sym (g.pres-⋆ _ _)
.P-+ x y α β → f.pres-+ _ _ ·· ap₂ M._+_ α β ·· sym (g.pres-+ _ _)
where
module f = Linear-map f
module g = Linear-map g
module M = Module-on (M .snd)

equal-on-basis′
: ∀ {ℓb ℓg} {T : Type ℓb} {G : Type ℓg} (M : Module-on R G)
→ (let module M = Module-on M)
→ {f : Free-mod T → G}
→ (∀ r x y → f (r · x + y) ≡ r M.⋆ f x M.+ f y)
→ {g : Free-mod T → G}
→ (∀ r x y → g (r · x + y) ≡ r M.⋆ g x M.+ g y)
→ ((x : T) → f (inc x) ≡ g (inc x))
→ f ≡ g
equal-on-basis′ M l1 l2 p = ap map $equal-on-basis (el _ (Module-on.has-is-set M) , M) {f = record { lin = record { linear = l1 } }} {g = record { lin = record { linear = l2 } }} p module _ (cring : is-commutative-ring R) where open Algebra.Ring.Module.Multilinear R cring multilinear-extension : ∀ {n} {ℓₙ} {ℓₘ : Fin (suc n) → Level} {Ms : (i : Fin (suc n)) → Type (ℓₘ i)} {N : Module R ℓₙ} → (f : Arrᶠ Ms ⌞ N ⌟) → Multilinear-map (suc n) (λ i → Free-Mod (Ms i)) N multilinear-extension {zero} {N = N} f = 1-linear-map (fold-free-mod N f) multilinear-extension {suc n} f = Uncurry.from$
fold-free-mod _ λ x → multilinear-extension (f x)

multi-equal-on-bases
: ∀ {n} {ℓₙ} {ℓₘ : Fin n → Level} {Ms : (i : Fin n) → Type (ℓₘ i)} {N : Module R ℓₙ}
→ {f g : Multilinear-map n (λ i → Free-Mod (Ms i)) N}
→ (∀ (as : Πᶠ Ms) → applyᶠ (f .map) (mapₚ (λ _ → inc) as) ≡ applyᶠ (g .map) (mapₚ (λ _ → inc) as))
→ f ≡ g
multi-equal-on-bases {n = zero} p = Multilinear-map-path (p tt)
multi-equal-on-bases {n = suc n} {f = f} {g} p =
Uncurry.injective \$ equal-on-basis _ λ x →
multi-equal-on-bases λ as →
p (x , as)


1. truncated, higher↩︎