Theory Module_First_Iso

section ‹The first isomorphism theorem for modules›

theory Module_First_Iso
  imports Quotient_Module
begin

text ‹Given a module homomorphism @{term "η: M → M'"}, its kernel is a submodule of @{term M}, and
  the induced map on the quotient @{text "M/Ker η"} onto @{term "η ` M"} is a module isomorphism.

  The natural way to organise this development inside @{locale module_homomorphism} is to prove
  once and for all that the kernel gives rise to a @{locale submodule_in_module} instance, and
  then use the operations ‹K.Qcarrier›, ‹K.Qclass›, ‹K.qadd›, ‹K.qscale› supplied by that
  instance in the theorems below.  We do this via
  @{command interpretation}@{text " K: submodule_in_module ... Ker"} at the head of the
  @{command context} block, discharged by the lemma ‹Ker_submodule_in_module› below.›

context module_homomorphism
begin

subsection ‹The kernel-quotient and the induced map›

text ‹The kernel is a submodule (@{thm [source] Ker_submodule}), so the
  @{locale submodule_in_module} locale holds on it.  This lemma is the witness fed to the
  @{command interpretation} below.›
lemma Ker_submodule_in_module:
  "submodule_in_module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙) Ker"
proof
  show "source.submodule Ker" by (rule Ker_submodule)
qed

text ‹Install @{locale submodule_in_module} on the kernel with prefix @{text K}.  The theorems
  below then use @{text K.Qcarrier}, @{text K.Qclass}, @{text K.qadd}, @{text K.qscale}, and other
  facts derived from the locale (@{text K.Class_eq_iff_diff_in_N}, @{text K.qscale_Class},
  @{text K.quotient.Module_axioms}, @{text K.madd_sub.representant_exists},
  @{text K.madd_sub.Class_commutes_with_composition}).›
interpretation K: submodule_in_module
  R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" Ker
  by (rule Ker_submodule_in_module)

text ‹The induced map on cosets.  Made extensional on ‹K.Qcarrier› so that it fits the
  @{locale map} locale in the @{const module_homomorphism} obligation.›
definition ind :: "'b set ⇒ 'c"
  where "ind = (λX ∈ K.Qcarrier. THE y. ∃v ∈ M. X = K.Qclass v ∧ y = η v)"

lemma ind_Class:
  assumes v: "v ∈ M" shows "ind (K.Qclass v) = η v"
proof -
  have "(THE y. ∃u ∈ M. K.Qclass v = K.Qclass u ∧ y = η u) = η v"
  proof (rule the_equality)
    show "∃u ∈ M. K.Qclass v = K.Qclass u ∧ η v = η u" using v by blast
  next
    fix y assume "∃u ∈ M. K.Qclass v = K.Qclass u ∧ y = η u"
    then obtain u where u: "u ∈ M" "K.Qclass v = K.Qclass u" "y = η u" by blast
    have "v ⊕ source.madd.inverse u ∈ Ker"
      using u(2) v u(1) by (subst K.Class_eq_iff_diff_in_N[symmetric]) simp_all
    then have "η (v ⊕ source.madd.inverse u) = 𝟬⇩2"
      using Ker_image by blast
    moreover have iuM: "source.madd.inverse u ∈ M" using u(1) by simp
    ultimately have "η v ⊕⇩2 η (source.madd.inverse u) = 𝟬⇩2"
      using v u(1) by (simp add: hom_add)
    then have eq: "η v ⊕⇩2 target.madd.inverse (η u) = 𝟬⇩2"
      using u(1) by (simp add: hom_neg)
    have "η u ⊕⇩2 target.madd.inverse (η u) = 𝟬⇩2"
      using hom_closed[OF u(1)] by (simp add: target.madd.invertible_right_inverse)
    with eq have "η v ⊕⇩2 target.madd.inverse (η u) = η u ⊕⇩2 target.madd.inverse (η u)"
      by simp
    then have "η v = η u"
      using hom_closed[OF v] hom_closed[OF u(1)] target.madd.invertible_right_cancel
      by (metis target.madd.invertible target.madd.invertible_inverse_closed)
    then show "y = η v" using u(3) by simp
  qed
  moreover have "K.Qclass v ∈ K.Qcarrier" using v by simp
  ultimately show ?thesis unfolding ind_def by simp
qed

lemma ind_closed:
  assumes "X ∈ K.Qcarrier" shows "ind X ∈ η ` M"
proof -
  from assms obtain v where "v ∈ M" "X = K.Qclass v"
    using K.madd_sub.representant_exists by auto
  then show ?thesis by (simp add: ind_Class)
qed


subsection ‹The image ‹η ` M› is a submodule of the target›

lemma image_abelian_group: "Abelian_Group (η ` M) (⊕⇩2) 𝟬⇩2"
proof -
  have sub: "Subgroup (η ` M) M' (⊕⇩2) 𝟬⇩2"
  proof (rule target.madd.subgroupI)
    show "η ` M ⊆ M'" using hom_closed by auto
    show "𝟬⇩2 ∈ η ` M" using hom_zero source.mzero_closed by (metis image_eqI)
  next
    fix u v assume "u ∈ η ` M" "v ∈ η ` M"
    then obtain a b where ab: "a ∈ M" "b ∈ M" "u = η a" "v = η b" by auto
    then have "u ⊕⇩2 v = η (a ⊕ b)" by (simp add: hom_add)
    then show "u ⊕⇩2 v ∈ η ` M" using ab by auto
  next
    fix u assume "u ∈ η ` M" then obtain a where a: "a ∈ M" "u = η a" by auto
    then have "u ∈ M'" using hom_closed by auto
    then show "target.madd.invertible u" by simp
    have "target.madd.inverse u = η (source.madd.inverse a)"
      using a by (simp add: hom_neg source.madd.invertible)
    then show "target.madd.inverse u ∈ η ` M" using a by auto
  qed
  interpret Sub: Subgroup "η ` M" M' "(⊕⇩2)" "𝟬⇩2" by (rule sub)
  show ?thesis
  proof (rule Abelian_Group.intro)
    show "Group (η ` M) (⊕⇩2) 𝟬⇩2" by (rule Sub.sub.Group_axioms)
    show "commutative_monoid (η ` M) (⊕⇩2) 𝟬⇩2"
      by unfold_locales (auto simp: target.madd.commutative)
  qed
qed

lemma image_module_axioms:
  "Module_axioms R (+) (⋅) 𝟭 (⊕⇩2) 𝟬⇩2 (η ` M) (⊙⇩2)"
proof (rule Module_axioms.intro)
  show "Abelian_Group (η ` M) (⊕⇩2) 𝟬⇩2" by (rule image_abelian_group)
next
  fix a v assume a: "a ∈ R" and v: "v ∈ η ` M"
  then obtain x where x: "x ∈ M" "v = η x" by auto
  have "a ⊙⇩2 v = η (a ⊙ x)" using a x by (simp add: hom_scale)
  then show "a ⊙⇩2 v ∈ η ` M" using a x by (auto intro: source.scale_closed)
next
  fix a u v assume a: "a ∈ R" and "u ∈ η ` M" and "v ∈ η ` M"
  then obtain x y where "x ∈ M" "y ∈ M" "u = η x" "v = η y" by auto
  with a show "a ⊙⇩2 (u ⊕⇩2 v) = (a ⊙⇩2 u) ⊕⇩2 (a ⊙⇩2 v)"
    by (simp add: target.scale_distrib_madd hom_closed)
next
  fix a b v assume a: "a ∈ R" and b: "b ∈ R" and v: "v ∈ η ` M"
  then obtain x where "x ∈ M" "v = η x" by auto
  with a b show "(a + b) ⊙⇩2 v = (a ⊙⇩2 v) ⊕⇩2 (b ⊙⇩2 v)"
    by (simp add: target.scale_distrib_add hom_closed)
next
  fix a b v assume a: "a ∈ R" and b: "b ∈ R" and v: "v ∈ η ` M"
  then obtain x where "x ∈ M" "v = η x" by auto
  with a b show "(a ⋅ b) ⊙⇩2 v = a ⊙⇩2 b ⊙⇩2 v"
    by (simp add: target.scale_scale hom_closed)
next
  fix v assume "v ∈ η ` M"
  then obtain x where "x ∈ M" "v = η x" by auto
  then show "𝟭 ⊙⇩2 v = v" by (simp add: target.scale_one hom_closed)
qed

lemma image_is_module: "Module R (+) (⋅) 𝟬 𝟭 (⊕⇩2) 𝟬⇩2 (η ` M) (⊙⇩2)"
  by (rule Module.intro[OF source.Ring_axioms image_module_axioms])


subsection ‹The induced map is a module homomorphism, injective, surjective›

text ‹The quotient module on the kernel is a module (specialisation of the quotient's own
  ‹Module_axioms› to the kernel-as-submodule).›
lemma quotient_is_module:
  "Module R (+) (⋅) 𝟬 𝟭 K.qadd (K.Qclass 𝟬⇩M) K.Qcarrier K.qscale"
  by (rule K.quotient.Module_axioms)

theorem ind_module_homomorphism:
  "module_homomorphism R (+) (⋅) 𝟬 𝟭
     K.Qcarrier K.qadd (K.Qclass 𝟬⇩M) K.qscale
     (η ` M) (⊕⇩2) 𝟬⇩2 (⊙⇩2) ind"
proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
  show "Module R (+) (⋅) 𝟬 𝟭 K.qadd (K.Qclass 𝟬⇩M) K.Qcarrier K.qscale"
    by (rule quotient_is_module)
  show "Module R (+) (⋅) 𝟬 𝟭 (⊕⇩2) 𝟬⇩2 (η ` M) (⊙⇩2)"
    by (rule image_is_module)
  show "ind ∈ K.Qcarrier →⇩E η ` M"
    using ind_closed by (auto simp: ind_def PiE_iff extensional_def)
next
  fix U V assume "U ∈ K.Qcarrier" and "V ∈ K.Qcarrier"
  then obtain u v where uv: "u ∈ M" "v ∈ M"
    "U = K.Qclass u" "V = K.Qclass v"
    using K.madd_sub.representant_exists by (metis (mono_tags, lifting))
  have "ind (K.qadd U V) = ind (K.Qclass (u ⊕ v))"
    using uv by (simp add: K.madd_sub.Class_commutes_with_composition)
  also have "… = η (u ⊕ v)" using uv by (simp add: ind_Class)
  also have "… = η u ⊕⇩2 η v" using uv by (simp add: hom_add)
  also have "… = (ind U) ⊕⇩2 (ind V)" using uv by (simp add: ind_Class)
  finally show "ind (K.qadd U V) = (ind U) ⊕⇩2 (ind V)" .
next
  fix a V assume a: "a ∈ R" and "V ∈ K.Qcarrier"
  then obtain v where v: "v ∈ M" "V = K.Qclass v"
    using K.madd_sub.representant_exists by (metis (mono_tags, lifting))
  have "ind (K.qscale a V) = ind (K.Qclass (a ⊙ v))"
    using a v by (simp add: K.qscale_Class)
  also have "… = η (a ⊙ v)" using a v by (simp add: ind_Class source.scale_closed)
  also have "… = a ⊙⇩2 η v" using a v by (simp add: hom_scale)
  also have "… = a ⊙⇩2 ind V" using v by (simp add: ind_Class)
  finally show "ind (K.qscale a V) = a ⊙⇩2 ind V" .
qed


theorem ind_inj: "inj_on ind K.Qcarrier"
proof (rule inj_onI)
  fix U V assume U: "U ∈ K.Qcarrier" and V: "V ∈ K.Qcarrier" and eq: "ind U = ind V"
  from U obtain u where u: "u ∈ M" "U = K.Qclass u"
    using K.madd_sub.representant_exists by (metis (mono_tags, lifting))
  from V obtain v where v: "v ∈ M" "V = K.Qclass v"
    using K.madd_sub.representant_exists by (metis (mono_tags, lifting))
  from eq u v have h: "η u = η v" by (simp add: ind_Class)
  have "η (u ⊕ source.madd.inverse v) = η u ⊕⇩2 η (source.madd.inverse v)"
    using u v by (simp add: hom_add)
  also have "… = η v ⊕⇩2 target.madd.inverse (η v)" using u v h by (simp add: hom_neg)
  also have "… = 𝟬⇩2"
    using hom_closed[OF v(1)] by (simp add: target.madd.invertible_right_inverse)
  finally have "η (u ⊕ source.madd.inverse v) = 𝟬⇩2" .
  moreover have "u ⊕ source.madd.inverse v ∈ M" using u v by simp
  ultimately have "u ⊕ source.madd.inverse v ∈ Ker" by (rule Ker_memI)
  then have "K.Qclass u = K.Qclass v"
    using u v by (simp add: K.Class_eq_iff_diff_in_N)
  then show "U = V" using u v by simp
qed


theorem ind_surj: "ind ` K.Qcarrier = η ` M"
proof
  show "ind ` K.Qcarrier ⊆ η ` M" using ind_closed by auto
  show "η ` M ⊆ ind ` K.Qcarrier"
  proof
    fix y assume "y ∈ η ` M"
    then obtain v where v: "v ∈ M" "y = η v" by auto
    then have "y = ind (K.Qclass v)" by (simp add: ind_Class)
    moreover have "K.Qclass v ∈ K.Qcarrier" using v by simp
    ultimately show "y ∈ ind ` K.Qcarrier" by auto
  qed
qed

text ‹∗‹The first isomorphism theorem›: the induced map @{term ind} is a bijective module
  homomorphism from @{text "M/Ker η"} onto @{term "η ` M"}.›
theorem first_isomorphism:
  "module_homomorphism R (+) (⋅) 𝟬 𝟭
     K.Qcarrier K.qadd (K.Qclass 𝟬⇩M) K.qscale
     (η ` M) (⊕⇩2) 𝟬⇩2 (⊙⇩2) ind
   ∧ bij_betw ind K.Qcarrier (η ` M)"
  using ind_module_homomorphism ind_inj ind_surj by (auto simp: bij_betw_def)

end (* module_homomorphism *)

end