Theory Free_Module_Universal
section ‹The universal property of a free module›
theory Free_Module_Universal
imports Free_Module Module_Homomorphism
begin
text ‹As in ‹Module_Homomorphism›: the import of ‹FiniteProduct› (through ‹Module›) re-merges HOL's
@{text "+"}/@{text "-"} concrete syntax alongside the ring locale's. That is harmless in term
positions but ambiguous in the locale-header instantiation arguments below, so we remove the HOL
syntax again.›
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax
text ‹A free module is free in the sense of a universal property: a homomorphism out of it may be
prescribed ∗‹arbitrarily› on a basis, and is then determined. Precisely: if @{term B} is a basis
of the @{term R}-module @{term M} and @{term f} maps @{term B} into an @{term R}-module
@{term M'}, then there is exactly one module homomorphism @{text "M → M'"} extending @{term f}.
This is what the uniqueness-of-coordinates results in ‹Free_Module› were for. Existence needs
coordinates to be ∗‹readable› --- every element has a representation over a finite subset of the
basis --- and well-definedness needs them to be ∗‹unique› in the strong sense of
‹lin_indep_lincomb_unique_gen›, across different index sets, since nothing fixes an index set in
advance.
The locale below fixes the ring once in the ‹for› clause and shares it between the two modules,
exactly as @{locale module_homomorphism} does; writing the two module interpretations with
separate ring parameters would make the ‹+› token ambiguous.›
locale free_module_ext =
source: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" +
target: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕⇩2)" "𝟬⇩2" M' "(⊙⇩2)"
for R and addition (infixl ‹+› 65) and multiplication (infixl ‹⋅› 70) and zero (‹𝟬›) and unit (‹𝟭›)
and M and madd (infixl ‹⊕› 65) and mzero (‹𝟬⇩M›) and scale (infixr ‹⊙› 75)
and M' and madd' (infixl ‹⊕⇩2› 65) and mzero' (‹𝟬⇩2›) and scale' (infixr ‹⊙⇩2› 75)
and B and f +
assumes basis: "source.module_basis B"
and f_closed: "v ∈ B ⟹ f v ∈ M'"
begin
text ‹The basis lies in the source module, and is independent and spanning.›
lemma B_subset: "B ⊆ M"
using basis source.module_basis_spanning unfolding source.spanning_def by blast
lemma B_lin_indep: "source.lin_indep B"
by (rule source.module_basis_lin_indep[OF basis])
subsection ‹The twisted sum›
text ‹The image of a linear combination must be @{text "⨁⇘v∈A⇙ c v ⊙⇩2 f v"} --- a sum in the
∗‹target› indexed by elements of the source. We give this ``twisted'' sum a name and prove for it
the three facts the homomorphism obligations need: it is closed, it is unchanged by padding the
index set with zero coefficients, and it is additive and homogeneous in the coefficients.›
definition tsum :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'c"
where "tsum c A = target.madd.fincomp (λv. c v ⊙⇩2 f v) A"
lemma tsum_Pi:
assumes A: "A ⊆ B" and c: "source.coeffs_on c A"
shows "(λv. c v ⊙⇩2 f v) ∈ A → M'"
using A c f_closed by (auto intro!: target.scale_closed intro: source.coeffs_onD)
lemma tsum_closed [intro, simp]:
assumes A: "A ⊆ B" and c: "source.coeffs_on c A"
shows "tsum c A ∈ M'"
unfolding tsum_def using tsum_Pi[OF A c] by (rule target.madd.fincomp_closed)
lemma tsum_empty [simp]: "tsum c {} = 𝟬⇩2"
by (simp add: tsum_def)
text ‹Only the values on the index set matter.›
lemma tsum_cong:
assumes A: "A ⊆ B" and eq: "⋀v. v ∈ A ⟹ c v = d v" and d: "source.coeffs_on d A"
shows "tsum c A = tsum d A"
unfolding tsum_def
proof (rule target.madd.fincomp_cong')
show "A = A" ..
show "(λv. d v ⊙⇩2 f v) ∈ A → M'" by (rule tsum_Pi[OF A d])
show "⋀v. v ∈ A ⟹ c v ⊙⇩2 f v = d v ⊙⇩2 f v" using eq by simp
qed
text ‹Padding the index set with zero coefficients does not change the sum: the extra terms are
@{term "𝟬 ⊙⇩2 f v = 𝟬⇩2"}.›
lemma tsum_mono_zero:
assumes finA': "finite A'" and AA': "A ⊆ A'" and A'B: "A' ⊆ B"
and zero: "⋀v. v ∈ A' ∖ A ⟹ c v = 𝟬" and c: "source.coeffs_on c A'"
shows "tsum c A = tsum c A'"
unfolding tsum_def
proof (rule target.madd.fincomp_mono_neutral_cong_left)
show "finite A'" and "A ⊆ A'" using finA' AA' by simp_all
show "⋀v. v ∈ A' ∖ A ⟹ c v ⊙⇩2 f v = 𝟬⇩2"
using zero A'B f_closed by (auto simp: target.scale_zero_scalar)
show "⋀v. v ∈ A ⟹ c v ⊙⇩2 f v = c v ⊙⇩2 f v" by simp
show "(λv. c v ⊙⇩2 f v) ∈ A' → M'" by (rule tsum_Pi[OF A'B c])
qed
text ‹Additivity in the coefficients.›
lemma tsum_add_coeffs:
assumes A: "A ⊆ B" and c: "source.coeffs_on c A" and d: "source.coeffs_on d A"
shows "tsum (λv. c v + d v) A = tsum c A ⊕⇩2 tsum d A"
unfolding tsum_def
proof (rule trans)
show "target.madd.fincomp (λv. (c v + d v) ⊙⇩2 f v) A
= target.madd.fincomp (λv. (c v ⊙⇩2 f v) ⊕⇩2 (d v ⊙⇩2 f v)) A"
proof (rule target.madd.fincomp_cong')
show "A = A" ..
show "(λv. (c v ⊙⇩2 f v) ⊕⇩2 (d v ⊙⇩2 f v)) ∈ A → M'"
using tsum_Pi[OF A c] tsum_Pi[OF A d] by auto
fix v assume v: "v ∈ A"
then have "c v ∈ R" and "d v ∈ R" and "f v ∈ M'"
using source.coeffs_onD[OF c] source.coeffs_onD[OF d] A f_closed by auto
then show "(c v + d v) ⊙⇩2 f v = (c v ⊙⇩2 f v) ⊕⇩2 (d v ⊙⇩2 f v)"
by (rule target.scale_distrib_add)
qed
show "target.madd.fincomp (λv. (c v ⊙⇩2 f v) ⊕⇩2 (d v ⊙⇩2 f v)) A
= target.madd.fincomp (λv. c v ⊙⇩2 f v) A ⊕⇩2 target.madd.fincomp (λv. d v ⊙⇩2 f v) A"
using tsum_Pi[OF A c] tsum_Pi[OF A d] by (rule target.madd.fincomp_comp)
qed
text ‹Homogeneity in the coefficients.›
lemma tsum_scale_coeffs:
assumes A: "A ⊆ B" and a: "a ∈ R" and c: "source.coeffs_on c A"
shows "tsum (λv. a ⋅ c v) A = a ⊙⇩2 tsum c A"
unfolding tsum_def
proof (rule trans)
show "target.madd.fincomp (λv. (a ⋅ c v) ⊙⇩2 f v) A
= target.madd.fincomp (λv. a ⊙⇩2 (c v ⊙⇩2 f v)) A"
proof (rule target.madd.fincomp_cong')
show "A = A" ..
show "(λv. a ⊙⇩2 (c v ⊙⇩2 f v)) ∈ A → M'"
using a tsum_Pi[OF A c] by (auto intro: target.scale_closed)
fix v assume v: "v ∈ A"
then have cv: "c v ∈ R" and fv: "f v ∈ M'"
using source.coeffs_onD[OF c] A f_closed by auto
show "(a ⋅ c v) ⊙⇩2 f v = a ⊙⇩2 (c v ⊙⇩2 f v)"
by (rule target.scale_scale[OF a cv fv])
qed
show "target.madd.fincomp (λv. a ⊙⇩2 (c v ⊙⇩2 f v)) A
= a ⊙⇩2 target.madd.fincomp (λv. c v ⊙⇩2 f v) A"
using a tsum_Pi[OF A c] by (rule target.scale_fincomp[symmetric])
qed
subsection ‹The extension is well defined›
text ‹Two representations of the same element give the same twisted sum. This is where
‹lin_indep_lincomb_unique_gen› is used: the coefficient functions, extended by @{term 𝟬}, agree,
and each twisted sum equals the one over the union of the two index sets.›
lemma tsum_well_defined:
assumes A: "finite A" "A ⊆ B" and A': "finite A'" "A' ⊆ B"
and c: "source.coeffs_on c A" and d: "source.coeffs_on d A'"
and eq: "source.lincomb c A = source.lincomb d A'"
shows "tsum c A = tsum d A'"
proof -
define c' where "c' = (λu. if u ∈ A then c u else 𝟬)"
define d' where "d' = (λu. if u ∈ A' then d u else 𝟬)"
have finU: "finite (A ∪ A')" using A(1) A'(1) by simp
have UB: "A ∪ A' ⊆ B" using A(2) A'(2) by blast
have c'R: "source.coeffs_on c' (A ∪ A')"
by (rule source.coeffs_onI) (use source.coeffs_onD[OF c] in ‹simp add: c'_def›)
have d'R: "source.coeffs_on d' (A ∪ A')"
by (rule source.coeffs_onI) (use source.coeffs_onD[OF d] in ‹simp add: d'_def›)
have agree: "⋀v. c' v = d' v"
unfolding c'_def d'_def
by (rule source.lin_indep_lincomb_unique_gen[OF B_lin_indep A A' c d eq])
have "tsum c A = tsum c' A"
by (rule tsum_cong[OF A(2)]) (use c in ‹auto simp: c'_def source.coeffs_on_def›)
also have "… = tsum c' (A ∪ A')"
proof (rule tsum_mono_zero[OF finU Un_upper1 UB])
show "⋀v. v ∈ A ∪ A' ∖ A ⟹ c' v = 𝟬" unfolding c'_def by simp
show "source.coeffs_on c' (A ∪ A')" by (rule c'R)
qed
also have "… = tsum d' (A ∪ A')"
by (rule tsum_cong[OF UB]) (use agree d'R in auto)
also have "… = tsum d' A'"
proof (rule sym, rule tsum_mono_zero[OF finU Un_upper2 UB])
show "⋀v. v ∈ A ∪ A' ∖ A' ⟹ d' v = 𝟬" unfolding d'_def by simp
show "source.coeffs_on d' (A ∪ A')" by (rule d'R)
qed
also have "… = tsum d A'"
by (rule tsum_cong[OF A'(2)]) (use d in ‹auto simp: d'_def source.coeffs_on_def›)
finally show ?thesis .
qed
subsection ‹The extension›
text ‹The extension of @{term f} to all of @{term M}: read off any representation over the basis and
take the twisted sum. Made extensional on @{term M} so that it satisfies the @{term map}
obligation of @{locale module_homomorphism} directly.›
definition free_ext :: "'b ⇒ 'c"
where "free_ext =
(λx ∈ M. THE y. ∃A c. finite A ∧ A ⊆ B ∧ source.coeffs_on c A
∧ x = source.lincomb c A ∧ y = tsum c A)"
text ‹On a representation, the extension is the twisted sum.›
lemma free_ext_repr:
assumes A: "finite A" "A ⊆ B" and c: "source.coeffs_on c A" and x: "x = source.lincomb c A"
shows "free_ext x = tsum c A"
proof -
have xM: "x ∈ M"
using x A c source.lincomb_closed[of A c] B_subset source.coeffs_onD by blast
have "(THE y. ∃A' c'. finite A' ∧ A' ⊆ B ∧ source.coeffs_on c' A'
∧ x = source.lincomb c' A' ∧ y = tsum c' A') = tsum c A"
proof (rule the_equality)
show "∃A' c'. finite A' ∧ A' ⊆ B ∧ source.coeffs_on c' A'
∧ x = source.lincomb c' A' ∧ tsum c A = tsum c' A'"
using A c x by blast
next
fix y assume "∃A' c'. finite A' ∧ A' ⊆ B ∧ source.coeffs_on c' A'
∧ x = source.lincomb c' A' ∧ y = tsum c' A'"
then obtain A' c' where y: "finite A'" "A' ⊆ B" "source.coeffs_on c' A'"
"x = source.lincomb c' A'" "y = tsum c' A'" by blast
have "source.lincomb c A = source.lincomb c' A'" using x y(4) by simp
then have "tsum c A = tsum c' A'"
by (rule tsum_well_defined[OF A y(1,2) c y(3)])
then show "y = tsum c A" using y(5) by simp
qed
then show ?thesis unfolding free_ext_def using xM by simp
qed
text ‹The extension agrees with @{term f} on the basis: a basis element is its own singleton
combination with coefficient @{term 𝟭}.›
theorem free_ext_extends:
assumes v: "v ∈ B" shows "free_ext v = f v"
proof -
have vM: "v ∈ M" using v B_subset by blast
have c1: "source.coeffs_on (λ_. 𝟭) {v}" by (rule source.coeffs_onI) simp
have "source.lincomb (λ_. 𝟭) {v} = v"
using vM by (simp add: source.scale_one)
then have "free_ext v = tsum (λ_. 𝟭) {v}"
using v c1 by (auto intro: free_ext_repr[where A = "{v}"])
also have "… = 𝟭 ⊙⇩2 f v"
unfolding tsum_def using f_closed[OF v]
by (simp add: target.scale_one)
also have "… = f v" using f_closed[OF v] by (rule target.scale_one)
finally show ?thesis .
qed
text ‹∗‹Existence.› The extension is a module homomorphism.›
theorem free_ext_hom:
"module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) free_ext"
proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙)" by (rule source.Module_axioms)
show "Module R (+) (⋅) 𝟬 𝟭 (⊕⇩2) 𝟬⇩2 M' (⊙⇩2)" by (rule target.Module_axioms)
show "free_ext ∈ M →⇩E M'"
proof (rule PiE_I)
fix x assume x: "x ∈ M"
obtain A c where A: "finite A" "A ⊆ B" "source.coeffs_on c A" "x = source.lincomb c A"
by (rule source.module_basis_repr_exists[OF basis x])
then show "free_ext x ∈ M'" using free_ext_repr[OF A] by simp
qed (simp add: free_ext_def)
next
fix x y assume x: "x ∈ M" and y: "y ∈ M"
obtain A c where A: "finite A" "A ⊆ B" "source.coeffs_on c A" "x = source.lincomb c A"
by (rule source.module_basis_repr_exists[OF basis x])
obtain A' d where A': "finite A'" "A' ⊆ B" "source.coeffs_on d A'" "y = source.lincomb d A'"
by (rule source.module_basis_repr_exists[OF basis y])
define c' where "c' = (λu. if u ∈ A then c u else 𝟬)"
define d' where "d' = (λu. if u ∈ A' then d u else 𝟬)"
have finU: "finite (A ∪ A')" using A(1) A'(1) by simp
have UB: "A ∪ A' ⊆ B" using A(2) A'(2) by blast
have UM: "A ∪ A' ⊆ M" using UB B_subset by blast
have c'R: "source.coeffs_on c' (A ∪ A')"
by (rule source.coeffs_onI) (use source.coeffs_onD[OF A(3)] in ‹simp add: c'_def›)
have d'R: "source.coeffs_on d' (A ∪ A')"
by (rule source.coeffs_onI) (use source.coeffs_onD[OF A'(3)] in ‹simp add: d'_def›)
have cU: "source.lincomb c' (A ∪ A') = x"
proof -
have "source.lincomb c' A = source.lincomb c' (A ∪ A')"
by (rule source.lincomb_mono_zero[OF finU Un_upper1 UM])
(use c'R in ‹simp_all add: c'_def›)
moreover have "source.lincomb c' A = source.lincomb c A"
by (rule source.lincomb_cong)
(use A(2) A(3) B_subset in ‹auto simp: c'_def›)
ultimately show ?thesis using A(4) by simp
qed
have dU: "source.lincomb d' (A ∪ A') = y"
proof -
have "source.lincomb d' A' = source.lincomb d' (A ∪ A')"
by (rule source.lincomb_mono_zero[OF finU Un_upper2 UM])
(use d'R in ‹simp_all add: d'_def›)
moreover have "source.lincomb d' A' = source.lincomb d A'"
by (rule source.lincomb_cong)
(use A'(2) A'(3) B_subset in ‹auto simp: d'_def›)
ultimately show ?thesis using A'(4) by simp
qed
have sumR: "source.coeffs_on (λu. c' u + d' u) (A ∪ A')"
by (rule source.coeffs_onI)
(use source.coeffs_onD[OF c'R] source.coeffs_onD[OF d'R] in simp)
have "x ⊕ y = source.lincomb (λu. c' u + d' u) (A ∪ A')"
using source.lincomb_add_coeffs[OF UM c'R d'R] cU dU by simp
then have "free_ext (x ⊕ y) = tsum (λu. c' u + d' u) (A ∪ A')"
by (rule free_ext_repr[OF finU UB sumR])
also have "… = tsum c' (A ∪ A') ⊕⇩2 tsum d' (A ∪ A')"
by (rule tsum_add_coeffs[OF UB c'R d'R])
also have "tsum c' (A ∪ A') = free_ext x"
using free_ext_repr[OF finU UB c'R cU[symmetric]] by simp
also have "tsum d' (A ∪ A') = free_ext y"
using free_ext_repr[OF finU UB d'R dU[symmetric]] by simp
finally show "free_ext (x ⊕ y) = free_ext x ⊕⇩2 free_ext y" .
next
fix a x assume a: "a ∈ R" and x: "x ∈ M"
obtain A c where A: "finite A" "A ⊆ B" "source.coeffs_on c A" "x = source.lincomb c A"
by (rule source.module_basis_repr_exists[OF basis x])
have AM: "A ⊆ M" using A(2) B_subset by blast
have scR: "source.coeffs_on (λu. a ⋅ c u) A"
by (rule source.coeffs_onI) (use a source.coeffs_onD[OF A(3)] in simp)
have "a ⊙ x = source.lincomb (λu. a ⋅ c u) A"
proof -
have pi: "(λv. c v ⊙ v) ∈ A → M"
using AM source.coeffs_onD[OF A(3)] by (auto intro!: source.scale_closed)
have "a ⊙ source.lincomb c A
= source.madd.fincomp (λv. a ⊙ (c v ⊙ v)) A"
unfolding source.lincomb_def using a pi by (rule source.scale_fincomp)
also have "… = source.madd.fincomp (λv. (a ⋅ c v) ⊙ v) A"
proof (rule source.madd.fincomp_cong')
show "A = A" ..
show "(λv. (a ⋅ c v) ⊙ v) ∈ A → M"
using AM a source.coeffs_onD[OF A(3)] by (auto intro!: source.scale_closed)
fix v assume v: "v ∈ A"
then have vM: "v ∈ M" and cv: "c v ∈ R"
using AM source.coeffs_onD[OF A(3)] by auto
show "a ⊙ (c v ⊙ v) = (a ⋅ c v) ⊙ v" by (rule source.scale_scale[OF a cv vM, symmetric])
qed
finally show ?thesis
by (simp add: A(4) source.lincomb_def)
qed
then have "free_ext (a ⊙ x) = tsum (λu. a ⋅ c u) A"
by (rule free_ext_repr[OF A(1,2) scR])
also have "… = a ⊙⇩2 tsum c A" by (rule tsum_scale_coeffs[OF A(2) a A(3)])
also have "tsum c A = free_ext x" using free_ext_repr[OF A] by simp
finally show "free_ext (a ⊙ x) = a ⊙⇩2 free_ext x" .
qed
text ‹∗‹Uniqueness.› Any homomorphism agreeing with @{term f} on the basis equals the extension:
two homomorphisms agreeing on a spanning set agree everywhere, because each element is a finite
combination of basis elements and both maps commute with the combination.›
theorem free_ext_unique:
assumes η: "module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) η"
and agree: "⋀v. v ∈ B ⟹ η v = f v"
and x: "x ∈ M"
shows "η x = free_ext x"
proof -
interpret H: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭 M "(⊕)" "𝟬⇩M" "(⊙)"
M' "(⊕⇩2)" "𝟬⇩2" "(⊙⇩2)" η
by (rule η)
obtain A c where A: "finite A" "A ⊆ B" "source.coeffs_on c A" "x = source.lincomb c A"
by (rule source.module_basis_repr_exists[OF basis x])
have AM: "A ⊆ M" using A(2) B_subset by blast
have "η (source.lincomb c A) = target.madd.fincomp (λv. c v ⊙⇩2 η v) A"
by (rule H.hom_lincomb[OF A(1) AM]) (use A(3) in ‹auto intro: source.coeffs_onD›)
also have "target.madd.fincomp (λv. c v ⊙⇩2 η v) A = tsum c A"
unfolding tsum_def
proof (rule target.madd.fincomp_cong')
show "A = A" ..
show "(λv. c v ⊙⇩2 f v) ∈ A → M'" by (rule tsum_Pi[OF A(2) A(3)])
show "⋀v. v ∈ A ⟹ c v ⊙⇩2 η v = c v ⊙⇩2 f v" using agree A(2) by auto
qed
finally show ?thesis using A(4) free_ext_repr[OF A] by simp
qed
text ‹∗‹The universal property.› There is exactly one homomorphism extending @{term f}.›
theorem free_module_universal:
"∃!η. module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) η
∧ (∀v ∈ B. η v = f v) ∧ η ∈ M →⇩E M'"
proof
show "module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) free_ext
∧ (∀v ∈ B. free_ext v = f v) ∧ free_ext ∈ M →⇩E M'"
proof (intro conjI ballI free_ext_hom)
show "⋀v. v ∈ B ⟹ free_ext v = f v" by (rule free_ext_extends)
show "free_ext ∈ M →⇩E M'"
using module_homomorphism.axioms(3)[OF free_ext_hom] map.graph by blast
qed
next
fix η
assume "module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) η
∧ (∀v ∈ B. η v = f v) ∧ η ∈ M →⇩E M'"
then have H: "module_homomorphism R (+) (⋅) 𝟬 𝟭 M (⊕) 𝟬⇩M (⊙) M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) η"
and ag: "⋀v. v ∈ B ⟹ η v = f v" and ext: "η ∈ M →⇩E M'" by auto
show "η = free_ext"
proof (rule extensionalityI)
show "η ∈ extensional M" using ext by (simp add: PiE_iff)
show "free_ext ∈ extensional M" unfolding free_ext_def by simp
fix x assume "x ∈ M"
then show "η x = free_ext x"
using H ag free_ext_unique by blast
qed
qed
end
end