Theory Module_Basics

section ‹Modules over a ring›

theory Module_Basics
  imports Ring_Theory Finite_Composite
begin

text ‹A (left) ∗‹module› over the ring @{term R}: an abelian group of elements @{term M} under
  @{text "⊕"} with zero @{text "𝟬⇩M"}, together with a scalar multiplication @{text "⊙"} by ring
  elements satisfying the module axioms.  This is the exact generalisation of
  theory ‹Vector_Space› from a field of scalars to a ring; a vector space is a module
  whose scalar ring is a field.  We develop the elementary arithmetic (scaling by zero, by the ring
  negation, additivity of finite sums) and the notions of submodule and of a linear combination.›

locale Module = Ring +
  fixes madd :: "'b ⇒ 'b ⇒ 'b" (infixl ‹⊕› 65)
    and mzero :: "'b" (‹𝟬⇩M›)
    and mcarrier :: "'b set" (‹M›)
    and scale :: "'a ⇒ 'b ⇒ 'b" (infixr ‹⊙› 75)
  assumes madd_group: "Abelian_Group M (⊕) 𝟬⇩M"
    and scale_closed: "⟦ a ∈ R; v ∈ M ⟧ ⟹ a ⊙ v ∈ M"
    and scale_distrib_madd: "⟦ a ∈ R; u ∈ M; v ∈ M ⟧ ⟹ a ⊙ (u ⊕ v) = (a ⊙ u) ⊕ (a ⊙ v)"
    and scale_distrib_add: "⟦ a ∈ R; b ∈ R; v ∈ M ⟧ ⟹ (a + b) ⊙ v = (a ⊙ v) ⊕ (b ⊙ v)"
    and scale_scale: "⟦ a ∈ R; b ∈ R; v ∈ M ⟧ ⟹ (a ⋅ b) ⊙ v = a ⊙ (b ⊙ v)"
    and scale_one: "v ∈ M ⟹ 𝟭 ⊙ v = v"
begin

text ‹The additive group of the module, available through the @{text madd} prefix.›
sublocale madd: Abelian_Group M "(⊕)" "𝟬⇩M"
  by (rule madd_group)

subsection ‹Elementary closure and arithmetic›

lemma mzero_closed [simp, intro]: "𝟬⇩M ∈ M" by simp

lemma madd_closed [simp, intro]: "⟦ u ∈ M; v ∈ M ⟧ ⟹ u ⊕ v ∈ M" by simp

text ‹Scaling the zero element gives the zero element.›
lemma scale_zero_elem:
  assumes a: "a ∈ R"
  shows "a ⊙ 𝟬⇩M = 𝟬⇩M"
proof -
  have w: "a ⊙ 𝟬⇩M ∈ M" using a by (simp add: scale_closed)
  then have eq: "a ⊙ 𝟬⇩M = (a ⊙ 𝟬⇩M) ⊕ (a ⊙ 𝟬⇩M)"
    by (metis assms madd.left_unit mzero_closed scale_distrib_madd) 
  then show ?thesis
    using madd.invertible_left_inverse2 w by fastforce
qed

text ‹Scaling by the ring zero gives the zero element.›
lemma scale_zero_scalar:
  assumes v: "v ∈ M"
  shows "𝟬 ⊙ v = 𝟬⇩M"
proof -
  have w: "𝟬 ⊙ v ∈ M" using v by (simp add: scale_closed)
  have eq: "𝟬 ⊙ v = (𝟬 ⊙ v) ⊕ (𝟬 ⊙ v)"
    using scale_distrib_add v by force 
  then show ?thesis
    using madd.commute_iff_inverse w by fastforce
qed

text ‹Scaling by the ring negation is the additive inverse of the scaling.›
lemma scale_neg_scalar:
  assumes a: "a ∈ R" and v: "v ∈ M"
  shows "(- a) ⊙ v = madd.inverse (a ⊙ v)"
proof -
  have "(a ⊙ v) ⊕ ((- a) ⊙ v) = 𝟬⇩M" using a v 
    by (simp add: scale_zero_scalar flip: scale_distrib_add)
  then show ?thesis 
    using a v by (simp add: scale_closed madd.inverse_equality madd.commutative)
qed

subsection ‹Submodules›

text ‹A ∗‹submodule› is a subset containing the zero element and closed under addition and under
  scaling by arbitrary ring elements.›
definition submodule :: "'b set ⇒ bool"
  where "submodule N ≡ N ⊆ M ∧ 𝟬⇩M ∈ N ∧ (∀u∈N. ∀v∈N. u ⊕ v ∈ N) ∧ (∀a∈R. ∀v∈N. a ⊙ v ∈ N)"

lemma submoduleI:
  assumes "N ⊆ M" and "𝟬⇩M ∈ N"
    and "⋀u v. ⟦ u ∈ N; v ∈ N ⟧ ⟹ u ⊕ v ∈ N"
    and "⋀a v. ⟦ a ∈ R; v ∈ N ⟧ ⟹ a ⊙ v ∈ N"
  shows "submodule N"
  using assms unfolding submodule_def by blast

lemma submodule_subset: "submodule N ⟹ N ⊆ M" 
  by (simp add: submodule_def)

lemma submodule_zero: "submodule N ⟹ 𝟬⇩M ∈ N"
  by (simp add: submodule_def)

lemma submodule_add: "⟦ submodule N; u ∈ N; v ∈ N ⟧ ⟹ u ⊕ v ∈ N"
  by (simp add: submodule_def)

lemma submodule_scale: "⟦ submodule N; a ∈ R; v ∈ N ⟧ ⟹ a ⊙ v ∈ N"
  by (simp add: submodule_def)

text ‹A submodule is closed under the module negation (scale by @{term "- 𝟭"}).›
lemma submodule_neg:
  assumes N: "submodule N" and v: "v ∈ N" shows "madd.inverse v ∈ N"
proof -
  have vM: "v ∈ M" using N v submodule_subset by blast
  have "madd.inverse v = (- 𝟭) ⊙ v" using vM by (simp add: scale_neg_scalar scale_one)
  moreover have "(- 𝟭) ⊙ v ∈ N" using N v by (auto intro: submodule_scale)
  ultimately show ?thesis by simp
qed

text ‹The whole module and the trivial submodule are submodules.›
lemma submodule_whole: "submodule M"
  by (rule submoduleI) (auto simp: scale_closed)

lemma submodule_trivial: "submodule {𝟬⇩M}"
  by (rule submoduleI) (auto simp: scale_zero_elem)

text ‹The intersection of two submodules is a submodule.›
lemma submodule_inter:
  assumes N: "submodule N" and K: "submodule K" shows "submodule (N ∩ K)"
proof (rule submoduleI)
  show "N ∩ K ⊆ M" using submodule_subset[OF N] by blast
  show "𝟬⇩M ∈ N ∩ K" using submodule_zero[OF N] submodule_zero[OF K] by blast
  show "⋀u v. ⟦ u ∈ N ∩ K; v ∈ N ∩ K ⟧ ⟹ u ⊕ v ∈ N ∩ K"
    using submodule_add[OF N] submodule_add[OF K] by blast
  show "⋀a v. ⟦ a ∈ R; v ∈ N ∩ K ⟧ ⟹ a ⊙ v ∈ N ∩ K"
    using submodule_scale[OF N] submodule_scale[OF K] by blast
qed


subsection ‹The sum of two submodules›

text ‹The ∗‹sum› of two subsets of the module: all sums of an element of each.  This is the module
  analogue of ‹ideal_sum› in ‹Chinese_Remainder›, and is the smallest submodule containing both
  summands when they are themselves submodules.›
definition submodule_sum :: "'b set ⇒ 'b set ⇒ 'b set"  (infixl ‹⊕⇩S› 65)
  where "N ⊕⇩S K = {u ⊕ v | u v. u ∈ N ∧ v ∈ K}"

lemma submodule_sum_memI: "⟦ u ∈ N; v ∈ K ⟧ ⟹ u ⊕ v ∈ N ⊕⇩S K"
  unfolding submodule_sum_def by blast

lemma submodule_sum_memE:
  assumes "x ∈ N ⊕⇩S K"
  obtains u v where "u ∈ N" "v ∈ K" "x = u ⊕ v"
  using assms unfolding submodule_sum_def by blast

text ‹The sum contains both summands, since each submodule contains @{term "𝟬⇩M"}.›
lemma submodule_sum_incl_left:
  assumes N: "submodule N" and K: "submodule K" shows "N ⊆ N ⊕⇩S K"
proof
  fix x assume x: "x ∈ N"
  then have xM: "x ∈ M" using submodule_subset[OF N] by blast
  have "x ⊕ 𝟬⇩M ∈ N ⊕⇩S K" using x submodule_zero[OF K] by (rule submodule_sum_memI)
  then show "x ∈ N ⊕⇩S K" using xM by simp
qed

lemma submodule_sum_incl_right:
  assumes N: "submodule N" and K: "submodule K" shows "K ⊆ N ⊕⇩S K"
proof
  fix x assume x: "x ∈ K"
  then have xM: "x ∈ M" using submodule_subset[OF K] by blast
  have "𝟬⇩M ⊕ x ∈ N ⊕⇩S K" using submodule_zero[OF N] x by (rule submodule_sum_memI)
  then show "x ∈ N ⊕⇩S K" using xM by simp
qed

text ‹The sum of two submodules is a submodule.  Closure under addition needs commutativity of the
  module addition to re-pair the four summands; closure under scaling distributes.›
theorem submodule_sum_submodule:
  assumes N: "submodule N" and K: "submodule K" shows "submodule (N ⊕⇩S K)"
proof (rule submoduleI)
  show sub: "N ⊕⇩S K ⊆ M"
  proof
    fix x assume "x ∈ N ⊕⇩S K"
    then obtain u v where uv: "u ∈ N" "v ∈ K" "x = u ⊕ v" by (rule submodule_sum_memE)
    then show "x ∈ M" using submodule_subset[OF N] submodule_subset[OF K] by auto
  qed
  show "𝟬⇩M ∈ N ⊕⇩S K"
    using submodule_zero[OF N] submodule_zero[OF K]
    by (metis madd.left_unit mzero_closed submodule_sum_memI)
next
  fix x y assume "x ∈ N ⊕⇩S K" and "y ∈ N ⊕⇩S K"
  then obtain u v u' v' where
    a: "u ∈ N" "v ∈ K" "x = u ⊕ v" and b: "u' ∈ N" "v' ∈ K" "y = u' ⊕ v'"
    by (meson submodule_sum_memE)
  have uM: "u ∈ M" and u'M: "u' ∈ M" using a(1) b(1) submodule_subset[OF N] by auto
  have vM: "v ∈ M" and v'M: "v' ∈ M" using a(2) b(2) submodule_subset[OF K] by auto
  ― ‹Re-pair ‹(u ⊕ v) ⊕ (u' ⊕ v')› as ‹(u ⊕ u') ⊕ (v ⊕ v')›, using the confluent
    associative-commutative bundle of the additive group (bare ‹associative›/‹commutative› do not
    reassociate reliably here).›
  have "x ⊕ y = (u ⊕ v) ⊕ (u' ⊕ v')" using a(3) b(3) by simp
  also have "… = (u ⊕ u') ⊕ (v ⊕ v')"
    using uM vM u'M v'M by (simp add: madd.ac)
  finally have "x ⊕ y = (u ⊕ u') ⊕ (v ⊕ v')" .
  moreover have "u ⊕ u' ∈ N" using submodule_add[OF N a(1) b(1)] .
  moreover have "v ⊕ v' ∈ K" using submodule_add[OF K a(2) b(2)] .
  ultimately show "x ⊕ y ∈ N ⊕⇩S K" by (simp add: submodule_sum_memI)
next
  fix a x assume aR: "a ∈ R" and xNK: "x ∈ N ⊕⇩S K"
  ― ‹@{term xNK} named explicitly: a bare ‹then› would feed both assumptions to the rule.›
  from xNK obtain u v where uv: "u ∈ N" "v ∈ K" "x = u ⊕ v" by (rule submodule_sum_memE)
  have uM: "u ∈ M" using uv(1) submodule_subset[OF N] by blast
  have vM: "v ∈ M" using uv(2) submodule_subset[OF K] by blast
  have "a ⊙ x = (a ⊙ u) ⊕ (a ⊙ v)"
    using uv(3) aR uM vM by (simp add: scale_distrib_madd)
  moreover have "a ⊙ u ∈ N" using submodule_scale[OF N aR uv(1)] .
  moreover have "a ⊙ v ∈ K" using submodule_scale[OF K aR uv(2)] .
  ultimately show "a ⊙ x ∈ N ⊕⇩S K" by (simp add: submodule_sum_memI)
qed

text ‹The sum is commutative, as a set.›
lemma submodule_sum_commute:
  assumes N: "submodule N" and K: "submodule K" shows "N ⊕⇩S K = K ⊕⇩S N"
proof
  show "N ⊕⇩S K ⊆ K ⊕⇩S N"
  proof
    fix x assume "x ∈ N ⊕⇩S K"
    then obtain u v where uv: "u ∈ N" "v ∈ K" "x = u ⊕ v" by (rule submodule_sum_memE)
    have uM: "u ∈ M" using uv(1) submodule_subset[OF N] by blast
    have vM: "v ∈ M" using uv(2) submodule_subset[OF K] by blast
    have "x = v ⊕ u" using uv(3) uM vM by (simp add: madd.commutative)
    then show "x ∈ K ⊕⇩S N" using uv(1,2) by (simp add: submodule_sum_memI)
  qed
next
  show "K ⊕⇩S N ⊆ N ⊕⇩S K"
  proof
    fix x assume "x ∈ K ⊕⇩S N"
    then obtain u v where uv: "u ∈ K" "v ∈ N" "x = u ⊕ v" by (rule submodule_sum_memE)
    have uM: "u ∈ M" using uv(1) submodule_subset[OF K] by blast
    have vM: "v ∈ M" using uv(2) submodule_subset[OF N] by blast
    have "x = v ⊕ u" using uv(3) uM vM by (simp add: madd.commutative)
    then show "x ∈ N ⊕⇩S K" using uv(1,2) by (simp add: submodule_sum_memI)
  qed
qed

text ‹A trivial intersection makes representations in the submodule sum unique.  The
  existence of such a representation is already exactly @{thm [source] submodule_sum_memE}; this
  cancellation lemma records the additional content supplied by disjointness.›
lemma submodule_sum_decomposition_unique:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and u: "u ∈ N" and v: "v ∈ K"
    and u': "u' ∈ N" and v': "v' ∈ K"
    and eq: "u ⊕ v = u' ⊕ v'"
  shows "u = u' ∧ v = v'"
proof -
  have uM: "u ∈ M" and u'M: "u' ∈ M"
    using u u' submodule_subset[OF N] by auto
  have vM: "v ∈ M" and v'M: "v' ∈ M"
    using v v' submodule_subset[OF K] by auto
  have invu'M: "madd.inverse u' ∈ M" using u'M by simp
  have invvM: "madd.inverse v ∈ M" using vM by simp
  have differenceM: "u ⊕ madd.inverse u' ∈ M" using uM invu'M by simp
  have difference_eq: "u ⊕ madd.inverse u' = v' ⊕ madd.inverse v"
  proof -
    have "(u ⊕ madd.inverse u') ⊕ v = (u ⊕ v) ⊕ madd.inverse u'"
      using uM u'M vM by (simp add: madd.ac)
    also have "... = (u' ⊕ v') ⊕ madd.inverse u'" using eq by simp
    also have "... = (v' ⊕ u') ⊕ madd.inverse u'"
      using madd.commutative[OF u'M v'M] by simp
    also have "... = v' ⊕ (u' ⊕ madd.inverse u')"
      by (rule madd.associative[OF v'M u'M invu'M])
    also have "... = v'" using u'M v'M by simp
    finally have cancellation: "(u ⊕ madd.inverse u') ⊕ v = v'" .
    have "((u ⊕ madd.inverse u') ⊕ v) ⊕ madd.inverse v =
        (u ⊕ madd.inverse u') ⊕ (v ⊕ madd.inverse v)"
      by (rule madd.associative[OF differenceM vM invvM])
    also have "... = u ⊕ madd.inverse u'" using differenceM vM by simp
    finally have recovered: "((u ⊕ madd.inverse u') ⊕ v) ⊕
      madd.inverse v = u ⊕ madd.inverse u'" .
    have "u ⊕ madd.inverse u' =
        ((u ⊕ madd.inverse u') ⊕ v) ⊕ madd.inverse v"
      using recovered by simp
    also have "... = v' ⊕ madd.inverse v" using cancellation by simp
    finally show ?thesis .
  qed
  have difference_N: "u ⊕ madd.inverse u' ∈ N"
    using submodule_add[OF N u submodule_neg[OF N u']] .
  have difference_K: "u ⊕ madd.inverse u' ∈ K"
    using difference_eq submodule_add[OF K v' submodule_neg[OF K v]] by simp
  have difference_zero: "u ⊕ madd.inverse u' = 𝟬⇩M"
    using difference_N difference_K disjoint by blast
  have uu': "u = u'"
  proof -
    have "madd.inverse u' ⊕ u' = 𝟬⇩M"
      using u'M by (simp add: madd.invertible_left_inverse)
    then show ?thesis
      using madd.inverse_unique uM u'M difference_zero by blast
  qed
  have vv': "v = v'"
    using eq uu' uM vM v'M by simp
  show ?thesis using uu' vv' by blast
qed

subsection ‹Linear combinations›

text ‹A linear combination of a finite set @{term B} of module elements with ring coefficients
  @{term c}: the module sum @{text "⨁⇘v∈B⇙ c v ⊙ v"}.›
definition lincomb :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'b"
  where "lincomb c B = madd.fincomp (λv. c v ⊙ v) B"

lemma lincomb_closed:
  assumes B: "B ⊆ M" and c: "⋀v. v ∈ B ⟹ c v ∈ R"
  shows "lincomb c B ∈ M"
  unfolding lincomb_def using B c by (auto intro!: madd.fincomp_closed scale_closed)

lemma lincomb_empty [simp]: "lincomb c {} = 𝟬⇩M"
  by (simp add: lincomb_def)

text ‹The span of a set of module elements: all linear combinations over its finite subsets.›
definition span :: "'b set ⇒ 'b set"
  where "span S = {lincomb c B | c B. finite B ∧ B ⊆ S ∧ (∀v∈B. c v ∈ R)}"

lemma span_closed:
  assumes "S ⊆ M" and "x ∈ span S" shows "x ∈ M"
  using assms unfolding span_def by (auto intro: lincomb_closed)

lemma span_mono: "S ⊆ T ⟹ span S ⊆ span T"
  unfolding span_def by blast

end

subsection ‹A vector space is a module over a field›

text ‹The module axioms are exactly those of theory ‹Vector_Space›, so any vector space is
  a module.  (We record the relationship at the locale level; the field's ring reduct supplies the
  scalar ring.)  A dedicated theory could re-derive the theory ‹Vector_Space› development
  as the field specialisation of the present one.›

end