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
Note: even if is not, strictly speaking, built on an underlying (sub)set of functions into we will stick to the exponential notation for definiteness.
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
is generated by elements of
(the inc) constructor, the
operations of an Abelian group (which we write with
_+_), together with a scalar
multiplication operation
The equations imposed are precisely those necessary to make _+_ into an abelian group,
and the scalar multiplication into an action by
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 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
structures on
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
Each operation is mapped to the corresponding operation on
so the path constructors are also handled by the witnesses that
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 then 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↩︎