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

open import Cat.Functor.Adjoint
open import Cat.Prelude hiding (_+_ ; _*_)

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 as¹ 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 #-}

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 =
  ext $ 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)

instance
  Extensional-linear-map-free
    : ∀ {ℓb ℓg ℓr} {T : Type ℓb} {M : Module R ℓg}
    → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄
    → Extensional (Linear-map (Free-Mod T) M) ℓr
  Extensional-linear-map-free {M = M} ⦃ ext ⦄ =
    injection→extensional! {f = λ m x → m .map (inc x)} (λ p → equal-on-basis M (happly p)) ext

  {-# OVERLAPS Extensional-linear-map-free #-}

To prove that free modules have the expected universal property, it remains to show that if $f = g \circ inc,$ then $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:

make-free-module : ∀ {ℓ'} (S : Set (ℓ ⊔ ℓ')) → Free-object (R-Mod↪Sets R (ℓ ⊔ ℓ')) S
make-free-module {ℓ' = ℓ'} S = go where
  open Free-object

  go : Free-object (R-Mod↪Sets R (ℓ ⊔ ℓ')) S
  go .free = Free-Mod ⌞ S ⌟
  go .unit = inc
  go .fold {b} f = linear-map→hom (fold-free-mod b f)
  go .commute = refl
  go .unique {M} {f} g p = reext! p

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 {ℓ' = ℓ'} = free-objects→functor (make-free-module {ℓ' = ℓ'})

Free⊣Forget : ∀ {ℓ'} → Free-module {ℓ'} ⊣ R-Mod↪Sets R (ℓ ⊔ ℓ')
Free⊣Forget {ℓ'} = free-objects→left-adjoint (make-free-module {ℓ' = ℓ'})

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)

truncated, higher↩︎