Theory Quotient_Module
section ‹Quotient modules and the first isomorphism theorem›
theory Quotient_Module
imports Module_Homomorphism
begin
text ‹Given a submodule @{term N} of an @{term R}-module @{term M}, the quotient set
@{text "M/N"} inherits a module structure with scaling
@{text "a ⋅ Class(v) = Class(a ⊙ v)"}. The construction reuses the group-quotient machinery of
‹Group_Theory› for the additive structure (any subgroup of an abelian group
is normal, so cosets already form an abelian group under coset addition) and only requires the
induced scaling to be shown well-defined.
On this base we prove the natural projection to be a module homomorphism with kernel @{term N},
and derive the first isomorphism theorem: for a module homomorphism @{term η}, the induced map on
@{text "M/Ker η"} is an isomorphism onto the image @{term "η ` M"}.›
subsection ‹The quotient module of a submodule›
text ‹Work inside the @{locale Module} locale, with a submodule fixed.›
locale submodule_in_module = Module +
fixes N :: "'b set"
assumes N_submodule: "submodule N"
begin
text ‹The submodule is an additive subgroup of the module. Since the additive group is abelian, it
is automatically normal.›
lemma N_subgroup: "Subgroup N M (⊕) 𝟬⇩M"
proof (rule madd.subgroupI)
show "N ⊆ M" using submodule_subset[OF N_submodule] .
show "𝟬⇩M ∈ N" using submodule_zero[OF N_submodule] .
next
fix g h assume "g ∈ N" and "h ∈ N"
then show "g ⊕ h ∈ N" using submodule_add[OF N_submodule] by blast
next
fix g assume gN: "g ∈ N"
then have "g ∈ M" using submodule_subset[OF N_submodule] by blast
then show "madd.invertible g" by simp
show "madd.inverse g ∈ N" using submodule_neg[OF N_submodule gN] .
qed
sublocale madd_sub: subgroup_of_abelian_group N M "(⊕)" "𝟬⇩M"
proof -
interpret S: Subgroup N M "(⊕)" "𝟬⇩M" by (rule N_subgroup)
show "subgroup_of_abelian_group N M (⊕) 𝟬⇩M" ..
qed
text ‹Notation: the quotient carrier, the coset class, and the induced coset addition.›
abbreviation Qcarrier :: "'b set set" (‹M'/N›)
where "M/N ≡ madd_sub.Factor_Group"
abbreviation Qclass :: "'b ⇒ 'b set"
where "Qclass v ≡ madd_sub.Class v"
notation madd_sub.quotient_composition (infixl ‹[⊕]› 65)
text ‹An explicit constant for the coset addition, so it can be referred to by name from outside
the locale (in @{command sublocale}-free consumers).›
abbreviation qadd :: "'b set ⇒ 'b set ⇒ 'b set"
where "qadd ≡ madd_sub.quotient_composition"
text ‹The additive coset structure is already a (commutative) group, inherited from
@{locale subgroup_of_abelian_group}.›
lemma qmodule_additive: "Abelian_Group (M/N) ([⊕]) (Qclass 𝟬⇩M)"
by (rule madd_sub.quotient_abelian)
subsubsection ‹The induced scaling is well-defined›
text ‹Two module elements lie in the same coset iff their difference lies in @{term N}.›
lemma Class_eq_iff_diff_in_N:
assumes u: "u ∈ M" and v: "v ∈ M"
shows "Qclass u = Qclass v ⟷ u ⊕ madd.inverse v ∈ N"
proof -
have raw: "Qclass u = Qclass v ⟷ madd.inverse u ⊕ v ∈ N"
using u v madd_sub.Congruence_def madd_sub.Class_equivalence by auto
have iff: "madd.inverse u ⊕ v ∈ N ⟷ u ⊕ madd.inverse v ∈ N"
proof
assume "madd.inverse u ⊕ v ∈ N"
then have "madd.inverse (madd.inverse u ⊕ v) ∈ N"
using N_submodule submodule_neg by blast
also have "madd.inverse (madd.inverse u ⊕ v) = madd.inverse v ⊕ u"
using u v by (simp add: madd.inverse_composition_commute)
also have "… = u ⊕ madd.inverse v" using u v by (simp add: madd.commutative)
finally show "u ⊕ madd.inverse v ∈ N" .
next
assume "u ⊕ madd.inverse v ∈ N"
then have "madd.inverse (u ⊕ madd.inverse v) ∈ N"
using N_submodule submodule_neg by blast
also have "madd.inverse (u ⊕ madd.inverse v) = v ⊕ madd.inverse u"
using u v by (simp add: madd.inverse_composition_commute)
also have "… = madd.inverse u ⊕ v" using u v by (simp add: madd.commutative)
finally show "madd.inverse u ⊕ v ∈ N" .
qed
from raw iff show ?thesis by simp
qed
text ‹The scaling is well-defined on cosets: if ‹u - v ∈ N› (in the module additive sense) then
‹a ⊙ u - a ⊙ v ∈ N›, since ‹a ⊙ (u ⊕ madd.inverse v)› equals
‹(a ⊙ u) ⊕ (a ⊙ madd.inverse v) = (a ⊙ u) ⊕ madd.inverse (a ⊙ v)› and lies in
@{term N} by scaling-closedness of the submodule.›
lemma scale_respects_Class:
assumes a: "a ∈ R" and uv: "Qclass u = Qclass v" and u: "u ∈ M" and v: "v ∈ M"
shows "Qclass (a ⊙ u) = Qclass (a ⊙ v)"
proof -
from uv u v have diff: "u ⊕ madd.inverse v ∈ N"
using Class_eq_iff_diff_in_N by blast
have "a ⊙ (u ⊕ madd.inverse v) = (a ⊙ u) ⊕ (a ⊙ madd.inverse v)"
using a u v by (simp add: scale_distrib_madd)
also have "a ⊙ madd.inverse v = madd.inverse (a ⊙ v)"
proof -
have inv_as_scale: "madd.inverse v = (- 𝟭) ⊙ v"
using v by (simp add: scale_neg_scalar scale_one)
have "a ⊙ madd.inverse v = a ⊙ ((- 𝟭) ⊙ v)" by (simp add: inv_as_scale)
also have "… = (a ⋅ (- 𝟭)) ⊙ v" using a v by (simp add: scale_scale)
also have "a ⋅ (- 𝟭) = - a" using a by (simp add: right_minus)
also have "(- a) ⊙ v = madd.inverse (a ⊙ v)" using a v by (rule scale_neg_scalar)
finally show ?thesis .
qed
finally have expand: "a ⊙ (u ⊕ madd.inverse v) = (a ⊙ u) ⊕ madd.inverse (a ⊙ v)" .
have scaled_diff_in_N: "a ⊙ (u ⊕ madd.inverse v) ∈ N"
by (rule submodule_scale[OF N_submodule a diff])
from scaled_diff_in_N have "(a ⊙ u) ⊕ madd.inverse (a ⊙ v) ∈ N" by (simp add: expand)
moreover have "a ⊙ u ∈ M" using a u by (rule scale_closed)
moreover have "a ⊙ v ∈ M" using a v by (rule scale_closed)
ultimately show ?thesis by (simp add: Class_eq_iff_diff_in_N)
qed
subsubsection ‹The quotient scaling operation and the quotient module›
text ‹Choose any representative and scale it; well-definedness (@{thm [source] scale_respects_Class})
makes the choice immaterial.›
definition qscale :: "'a ⇒ 'b set ⇒ 'b set" (infixr ‹[⊙]› 75)
where "a [⊙] X = (THE Y. ∃v ∈ M. X = Qclass v ∧ Y = Qclass (a ⊙ v))"
lemma qscale_Class:
assumes a: "a ∈ R" and v: "v ∈ M"
shows "a [⊙] Qclass v = Qclass (a ⊙ v)"
proof -
have "(THE Y. ∃u ∈ M. Qclass v = Qclass u ∧ Y = Qclass (a ⊙ u)) = Qclass (a ⊙ v)"
proof (rule the_equality)
show "∃u ∈ M. Qclass v = Qclass u ∧ Qclass (a ⊙ v) = Qclass (a ⊙ u)"
using v by blast
next
fix Y assume "∃u ∈ M. Qclass v = Qclass u ∧ Y = Qclass (a ⊙ u)"
then obtain u where u: "u ∈ M" "Qclass v = Qclass u" "Y = Qclass (a ⊙ u)" by blast
have "Qclass (a ⊙ v) = Qclass (a ⊙ u)"
by (rule scale_respects_Class[OF a u(2) v u(1)])
then show "Y = Qclass (a ⊙ v)" using u(3) by simp
qed
then show ?thesis unfolding qscale_def by simp
qed
lemma qscale_closed [intro, simp]:
assumes a: "a ∈ R" and X: "X ∈ M/N" shows "a [⊙] X ∈ M/N"
proof -
from X obtain v where v: "v ∈ M" "X = Qclass v" using madd_sub.representant_exists by auto
have avM: "a ⊙ v ∈ M" using a v(1) by (rule scale_closed)
then have "Qclass (a ⊙ v) ∈ M/N" by (rule madd_sub.Class_in_Partition)
then show ?thesis using a v by (simp add: qscale_Class)
qed
text ‹The six module axioms on the quotient, packaged as a @{const Module_axioms} fact. This is
the pinch point: proving @{const Module_axioms} separately, and then composing with the ambient
@{const Ring_axioms} via @{thm [source] Module.intro}, avoids the fragile mid-interpretation
goal-order handshake we would face by opening a bare @{command sublocale} on @{locale Module}.›
lemma quotient_module_axioms:
"Module_axioms R (+) (⋅) 𝟭 ([⊕]) (Qclass 𝟬⇩M) (M/N) ([⊙])"
proof (rule Module_axioms.intro)
show "Abelian_Group (M/N) ([⊕]) (Qclass 𝟬⇩M)" by (rule qmodule_additive)
next
fix a X assume a: "a ∈ R" and X: "X ∈ M/N" show "a [⊙] X ∈ M/N"
using a X by (rule qscale_closed)
next
fix a X Y assume a: "a ∈ R" and X: "X ∈ M/N" and Y: "Y ∈ M/N"
from X obtain u where u: "u ∈ M" "X = Qclass u" using madd_sub.representant_exists by auto
from Y obtain v where v: "v ∈ M" "Y = Qclass v" using madd_sub.representant_exists by auto
have "a [⊙] (X [⊕] Y) = a [⊙] Qclass (u ⊕ v)"
using u v by (simp add: madd_sub.Class_commutes_with_composition)
also have "… = Qclass (a ⊙ (u ⊕ v))"
using a u v by (simp add: qscale_Class)
also have "… = Qclass ((a ⊙ u) ⊕ (a ⊙ v))"
using a u v by (simp add: scale_distrib_madd)
also have "… = Qclass (a ⊙ u) [⊕] Qclass (a ⊙ v)"
using a u v by (simp add: madd_sub.Class_commutes_with_composition scale_closed)
also have "… = (a [⊙] X) [⊕] (a [⊙] Y)"
using a u v by (simp add: qscale_Class)
finally show "a [⊙] (X [⊕] Y) = (a [⊙] X) [⊕] (a [⊙] Y)" .
next
fix a b X assume a: "a ∈ R" and b: "b ∈ R" and X: "X ∈ M/N"
from X obtain v where v: "v ∈ M" "X = Qclass v" using madd_sub.representant_exists by auto
have "(a + b) [⊙] X = Qclass ((a + b) ⊙ v)" using a b v by (simp add: qscale_Class)
also have "… = Qclass ((a ⊙ v) ⊕ (b ⊙ v))" using a b v by (simp add: scale_distrib_add)
also have "… = Qclass (a ⊙ v) [⊕] Qclass (b ⊙ v)"
using a b v by (simp add: madd_sub.Class_commutes_with_composition scale_closed)
also have "… = (a [⊙] X) [⊕] (b [⊙] X)" using a b v by (simp add: qscale_Class)
finally show "(a + b) [⊙] X = (a [⊙] X) [⊕] (b [⊙] X)" .
next
fix a b X assume a: "a ∈ R" and b: "b ∈ R" and X: "X ∈ M/N"
from X obtain v where v: "v ∈ M" "X = Qclass v" using madd_sub.representant_exists by auto
have "(a ⋅ b) [⊙] X = Qclass ((a ⋅ b) ⊙ v)" using a b v by (simp add: qscale_Class)
also have "… = Qclass (a ⊙ (b ⊙ v))" using a b v by (simp add: scale_scale)
also have "… = a [⊙] Qclass (b ⊙ v)" using a b v by (simp add: qscale_Class scale_closed)
also have "… = a [⊙] (b [⊙] X)" using b v by (simp add: qscale_Class)
finally show "(a ⋅ b) [⊙] X = a [⊙] (b [⊙] X)" .
next
fix X assume X: "X ∈ M/N"
from X obtain v where v: "v ∈ M" "X = Qclass v" using madd_sub.representant_exists by auto
show "𝟭 [⊙] X = X" using v by (simp add: qscale_Class scale_one)
qed
sublocale quotient: Module R "(+)" "(⋅)" "𝟬" "𝟭" "([⊕])" "Qclass 𝟬⇩M" "M/N" "([⊙])"
by (rule Module.intro[OF Ring_axioms quotient_module_axioms])
subsubsection ‹The natural projection›
text ‹The natural projection @{text "v ↦ Qclass v"} extensional on @{term M}.›
definition nat_proj :: "'b ⇒ 'b set"
where "nat_proj = (λv ∈ M. Qclass v)"
lemma nat_proj_apply [simp]: "v ∈ M ⟹ nat_proj v = Qclass v"
unfolding nat_proj_def by simp
lemma nat_proj_undefined: "v ∉ M ⟹ nat_proj v = undefined"
unfolding nat_proj_def by simp
text ‹The natural projection is a module homomorphism with kernel @{term N}.›
sublocale nat_proj: module_homomorphism
R "(+)" "(⋅)" "𝟬" "𝟭"
M "(⊕)" "𝟬⇩M" "(⊙)"
"M/N" "([⊕])" "Qclass 𝟬⇩M" "([⊙])"
nat_proj
proof
show "nat_proj ∈ M →⇩E M/N"
unfolding nat_proj_def by (rule PiE_I) (auto simp: extensional_def)
next
fix u v assume "u ∈ M" "v ∈ M"
then show "nat_proj (u ⊕ v) = nat_proj u [⊕] nat_proj v"
by (simp add: madd_sub.Class_commutes_with_composition)
next
fix a v assume "a ∈ R" "v ∈ M"
then show "nat_proj (a ⊙ v) = a [⊙] nat_proj v"
by (simp add: qscale_Class scale_closed)
qed
text ‹The natural projection maps onto the entire quotient carrier.›
theorem nat_proj_image: "nat_proj ` M = M/N"
proof
show "nat_proj ` M ⊆ M/N" using nat_proj.hom_closed by blast
next
show "M/N ⊆ nat_proj ` M"
proof
fix X assume X: "X ∈ M/N"
then obtain v where v: "v ∈ M" "X = Qclass v"
using madd_sub.representant_exists by blast
then have "X = nat_proj v" by simp
then show "X ∈ nat_proj ` M" using v(1) by blast
qed
qed
text ‹The kernel of the natural projection is exactly @{term N}.›
theorem nat_proj_Ker: "nat_proj.Ker = N"
proof
show "nat_proj.Ker ⊆ N"
proof
fix v assume vK: "v ∈ nat_proj.Ker"
then have vM: "v ∈ M" using nat_proj.Ker_mem by simp
from vK have "nat_proj v = Qclass 𝟬⇩M" using nat_proj.Ker_image by simp
with vM have Q: "Qclass v = Qclass 𝟬⇩M" by simp
from Q vM have "v ⊕ madd.inverse 𝟬⇩M ∈ N"
using Class_eq_iff_diff_in_N by simp
then show "v ∈ N" using vM by (simp add: madd.inverse_unit)
qed
next
show "N ⊆ nat_proj.Ker"
proof
fix v assume vN: "v ∈ N"
then have vM: "v ∈ M" using N_submodule submodule_subset by blast
have "v ⊕ madd.inverse 𝟬⇩M ∈ N" using vN vM by (simp add: madd.inverse_unit)
then have "Qclass v = Qclass 𝟬⇩M" using vM by (simp add: Class_eq_iff_diff_in_N)
then have "nat_proj v = Qclass 𝟬⇩M" using vM by simp
then show "v ∈ nat_proj.Ker" using vM nat_proj.Ker_memI by simp
qed
qed
end
end