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β†’RBB \to R^B.

Note: even if RBR^B is not, strictly speaking, built on an underlying (sub)set of functions into RR, 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 AA is generated by elements of AA (the inc) constructor, the operations of an Abelian group (which we write with _+_), together with a scalar multiplication operation R→RA→RAR \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 RR. 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 RAR^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 RR-module structures on RAR^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 RR-module NN. Each operation is mapped to the corresponding operation on NN, so the path constructors are also handled by the witnesses that NN 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∘incf = g\circ\mathrm{inc}, then fold(f)=g\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β†©οΈŽ