<!--
```agda
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
```
-->

```agda
module Algebra.Ring.Module.Free {ℓ} (R : Ring ℓ) where
```

# Free modules {defines="free-module"}

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.

[vectors]: Algebra.Ring.Module.Vec.html
[finite set]: Data.Fin.Finite.html
[modules]: Algebra.Ring.Module.html

<!--
```agda
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^[truncated, higher] inductive types.

```agda
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`{.Agda}) constructor, the operations of an [[Abelian group]] (which
we write with `_+_`{.Agda}), together with a scalar multiplication
operation $R \to R^A \to R^A$. The equations imposed are precisely those
necessary to make `_+_`{.Agda} into an abelian group, and the scalar
multiplication into an action by $R$. We also add a `squash`{.Agda}
constructor, since modules must have an underlying set.

[Abelian group]: Algebra.Group.Ab.html

```agda
  +-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.

```agda
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
```

<!--
```agda
  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
```
-->

<details>
<summary>I'll leave the definition of the group, Abelian group, and
$R$-module structures on $R^A$ in this `<details>`{.html} tag, since
they're not particularly interesting. For every operation _and_ law, we
simply use the corresponding constructors.</summary>

```agda
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
```

</details>

```agda
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`{.Agda} 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.

```agda
  -- 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 #-}
```

<!--
```agda
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\rm{inc}$, then $\rm{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:

```agda
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`{.Agda} has the right universal property: that is, we can
rearrange the proof above into the form of a functor and an adjunction.

```agda
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 {ℓ' = ℓ'})
```

<!--
```agda
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)
```
-->
