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  _·_
infixl  _+_

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

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)