Theory Module_Iso_Theorems

section ‹The second and third isomorphism theorems for modules›

text ‹
  The third isomorphism theorem for modules: for submodules @{text "K ⊆ N ⊆ M"},
  @{text "(M/K)/(N/K) ≅ M/N"}; and the second: for submodules @{term N} and @{term K},
  @{text "(N ⊕⇩S K)/K ≅ N/(N ∩ K)"}, where @{text "⊕⇩S"} is the submodule sum defined in
  ‹Module›.

  ∗‹Performance.›  This theory loads in a fraction of a second.  Earlier drafts of this comment
  claimed that the two proof-local @{command interpret}@{text " ...: submodule_in_module ..."}
  calls per theorem were prohibitively expensive, and that this was why the theory was kept out
  of ‹ROOT›.  That was a misdiagnosis: the long build times seen at the time were machine
  contention, not locale instantiation cost.  There is nothing here to optimise.›

theory Module_Iso_Theorems
  imports Module_First_Iso
begin

text ‹Building on the first isomorphism theorem in ‹Module_First_Iso›, we derive
  the third: given submodules ‹K ⊆ N ⊆ M›, the natural map ‹v + K ↦ v + N› is a surjective
  module homomorphism from @{text "M/K"} onto @{text "M/N"} with kernel @{text "N/K"}; by the first
  iso, @{text "(M/K) / (N/K) ≅ M/N"}.

  ∗‹Note on the two @{command interpret}s.›  Each theorem below interprets
  @{locale submodule_in_module} twice inside its own proof, once for @{term K} and once for
  @{term N}.  This is cheap and needs no refactoring.  A previous version of this note asserted
  that the alternative --- two @{command interpretation}s at the head of the enclosing
  @{command context} @{locale Module} block --- triggers a non-terminating locale roundup.  That
  claim was never soundly established (it shares an origin with the contention misdiagnosis
  above) and should be re-measured before being repeated or acted upon.›

context Module
begin

text ‹The natural map ‹v + K ↦ v + N› from @{text "M/K"} to @{text "M/N"}.  Made extensional on
  ‹M/K› by construction so that the @{term map} obligation of @{locale module_homomorphism} is
  directly discharged.›
definition proj_KN :: "'b set ⇒ 'b set ⇒ 'b set ⇒ 'b set"
  where "proj_KN K N =
    (λA ∈ submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K.
       THE B. ∃v ∈ M. A = submodule_in_module.Qclass (⊕) 𝟬⇩M M K v
                    ∧ B = submodule_in_module.Qclass (⊕) 𝟬⇩M M N v)"

text ‹Well-definedness of the projection: two representatives in the same ‹K›-coset lie in the same
  ‹N›-coset, because @{term "K ⊆ N"}.  This is the workhorse fact for everything below, so we prove
  it once here rather than inside each theorem.›
lemma proj_KN_Class:
  assumes N_sub: "submodule N" and K_sub: "submodule K" and K_in_N: "K ⊆ N" and v: "v ∈ M"
  shows "proj_KN K N (submodule_in_module.Qclass (⊕) 𝟬⇩M M K v)
       = submodule_in_module.Qclass (⊕) 𝟬⇩M M N v"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K_sub by unfold_locales
  interpret N: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" N
    using N_sub by unfold_locales
  have "(THE B. ∃u ∈ M. K.Qclass v = K.Qclass u ∧ B = N.Qclass u) = N.Qclass v"
  proof (rule the_equality)
    show "∃u ∈ M. K.Qclass v = K.Qclass u ∧ N.Qclass v = N.Qclass u" using v by blast
  next
    fix B assume "∃u ∈ M. K.Qclass v = K.Qclass u ∧ B = N.Qclass u"
    then obtain u where u: "u ∈ M" "K.Qclass v = K.Qclass u" "B = N.Qclass u" by blast
    from u(2) v u(1) have "v ⊕ madd.inverse u ∈ K"
      by (simp add: K.Class_eq_iff_diff_in_N)
    with K_in_N have "v ⊕ madd.inverse u ∈ N" by blast
    then have "N.Qclass v = N.Qclass u" using v u(1) by (simp add: N.Class_eq_iff_diff_in_N)
    with u(3) show "B = N.Qclass v" by simp
  qed
  moreover have "K.Qclass v ∈ K.Qcarrier" using v by simp
  ultimately show ?thesis unfolding proj_KN_def by simp
qed

text ‹The main theorem: for submodules @{term K}, @{term N} of @{term M} with @{term "K ⊆ N"},
  the map @{term "proj_KN K N"} is a surjective module homomorphism from @{text "M/K"} onto
  @{text "M/N"} whose kernel is @{text "K.Qclass ` N"} (which is @{text "N/K"} viewed inside
  @{text "M/K"}).›
theorem third_isomorphism_setup:
  assumes N_sub: "submodule N"
    and K_sub: "submodule K"
    and K_in_N: "K ⊆ N"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
          (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
          (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
          (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
          (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K)
          (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N)
          (submodule_in_module.qadd (⊕) 𝟬⇩M M N)
          (submodule_in_module.Qclass (⊕) 𝟬⇩M M N 𝟬⇩M)
          (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) N)
          (proj_KN K N)"
        (is "module_homomorphism _ _ _ _ _ ?QK ?qaddK ?zK ?qscaleK ?QN ?qaddN ?zN ?qscaleN _")
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K_sub by unfold_locales
  interpret N: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" N
    using N_sub by unfold_locales

  note proj_Class = proj_KN_Class[OF N_sub K_sub K_in_N]

  have proj_closed: "proj_KN K N ∈ K.Qcarrier →⇩E N.Qcarrier"
  proof (rule PiE_I)
    fix A assume "A ∈ K.Qcarrier"
    then obtain v where v: "v ∈ M" "A = K.Qclass v" using K.madd_sub.representant_exists by auto
    then have "proj_KN K N A = N.Qclass v" using proj_Class by simp
    moreover have "N.Qclass v ∈ N.Qcarrier" using v by simp
    ultimately show "proj_KN K N A ∈ N.Qcarrier" by simp
  qed (auto simp: proj_KN_def)

  show ?thesis
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (⋅) 𝟬 𝟭 ?qaddK ?zK ?QK ?qscaleK" by (rule K.quotient.Module_axioms)
    show "Module R (+) (⋅) 𝟬 𝟭 ?qaddN ?zN ?QN ?qscaleN" by (rule N.quotient.Module_axioms)
    show "proj_KN K N ∈ ?QK →⇩E ?QN" by (rule proj_closed)
  next
    fix A B assume "A ∈ ?QK" and "B ∈ ?QK"
    then obtain a b where ab: "a ∈ M" "b ∈ M" "A = K.Qclass a" "B = K.Qclass b"
      using K.madd_sub.representant_exists by (metis (mono_tags, lifting))
    have "proj_KN K N (K.qadd A B) = proj_KN K N (K.Qclass (a ⊕ b))"
      using ab by (simp add: K.madd_sub.Class_commutes_with_composition)
    also have "… = N.Qclass (a ⊕ b)" using ab by (simp add: proj_Class)
    also have "… = N.qadd (N.Qclass a) (N.Qclass b)"
      using ab by (simp add: N.madd_sub.Class_commutes_with_composition)
    also have "… = N.qadd (proj_KN K N A) (proj_KN K N B)" using ab by (simp add: proj_Class)
    finally show "proj_KN K N (K.qadd A B) = N.qadd (proj_KN K N A) (proj_KN K N B)" .
  next
    fix a A assume a: "a ∈ R" and "A ∈ ?QK"
    then obtain v where v: "v ∈ M" "A = K.Qclass v" using K.madd_sub.representant_exists
      by (metis (mono_tags, lifting))
    have "proj_KN K N (K.qscale a A) = proj_KN K N (K.Qclass (a ⊙ v))"
      using a v by (simp add: K.qscale_Class)
    also have "… = N.Qclass (a ⊙ v)" using a v by (simp add: proj_Class scale_closed)
    also have "… = N.qscale a (N.Qclass v)" using a v by (simp add: N.qscale_Class)
    also have "… = N.qscale a (proj_KN K N A)" using v by (simp add: proj_Class)
    finally show "proj_KN K N (K.qscale a A) = N.qscale a (proj_KN K N A)" .
  qed
qed

theorem third_isomorphism_surj:
  assumes N_sub: "submodule N"
    and K_sub: "submodule K"
    and K_in_N: "K ⊆ N"
  shows "proj_KN K N ` (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
       = submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K_sub by unfold_locales
  interpret N: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" N
    using N_sub by unfold_locales
  note proj_Class = proj_KN_Class[OF N_sub K_sub K_in_N]
  show ?thesis
  proof
    show "proj_KN K N ` K.Qcarrier ⊆ N.Qcarrier"
    proof
      fix Y assume "Y ∈ proj_KN K N ` K.Qcarrier"
      then obtain A where A: "A ∈ K.Qcarrier" "Y = proj_KN K N A" by auto
      from A(1) obtain v where v: "v ∈ M" "A = K.Qclass v" using K.madd_sub.representant_exists by auto
      with A(2) proj_Class[OF v(1)] have "Y = N.Qclass v" by simp
      then show "Y ∈ N.Qcarrier" using v(1) by simp
    qed
    show "N.Qcarrier ⊆ proj_KN K N ` K.Qcarrier"
    proof
      fix Y assume "Y ∈ N.Qcarrier"
      then obtain v where v: "v ∈ M" "Y = N.Qclass v" using N.madd_sub.representant_exists by auto
      then have "Y = proj_KN K N (K.Qclass v)" using proj_Class by simp
      moreover have "K.Qclass v ∈ K.Qcarrier" using v(1) by simp
      ultimately show "Y ∈ proj_KN K N ` K.Qcarrier" by auto
    qed
  qed
qed


subsection ‹The kernel of the projection is ‹N/K››

text ‹The kernel of @{term "proj_KN K N"} consists of exactly those ‹K›-cosets whose representatives
  lie in @{term N} --- that is, of @{text "N/K"} viewed as a subset of @{text "M/K"}.  Note the
  kernel is computed with respect to the zero of @{text "M/N"}, namely @{text "N.Qclass 𝟬⇩M"}.›
theorem phi_Ker:
  assumes N_sub: "submodule N"
    and K_sub: "submodule K"
    and K_in_N: "K ⊆ N"
  shows "{A ∈ submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K.
            proj_KN K N A = submodule_in_module.Qclass (⊕) 𝟬⇩M M N 𝟬⇩M}
       = submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K_sub by unfold_locales
  interpret N: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" N
    using N_sub by unfold_locales
  note proj_Class = proj_KN_Class[OF N_sub K_sub K_in_N]
  have N_in_M: "N ⊆ M" using submodule_subset[OF N_sub] .
  show ?thesis
  proof
    show "{A ∈ K.Qcarrier. proj_KN K N A = N.Qclass 𝟬⇩M} ⊆ K.Qclass ` N"
    proof
      fix A assume A: "A ∈ {A ∈ K.Qcarrier. proj_KN K N A = N.Qclass 𝟬⇩M}"
      then obtain v where v: "v ∈ M" "A = K.Qclass v"
        using K.madd_sub.representant_exists by auto
      from A have "proj_KN K N A = N.Qclass 𝟬⇩M" by simp
      with v proj_Class have "N.Qclass v = N.Qclass 𝟬⇩M" by simp
      ― ‹A coset equals the zero coset exactly when its representative lies in the submodule ---
        this is @{thm [source] submodule_in_module.Class_eq_iff_diff_in_N} with @{term "𝟬⇩M"},
        whose inverse is itself.›
      then have "v ⊕ madd.inverse 𝟬⇩M ∈ N"
        using v(1) by (simp add: N.Class_eq_iff_diff_in_N)
      then have "v ∈ N" using v(1) by (simp add: madd.inverse_unit)
      with v(2) show "A ∈ K.Qclass ` N" by blast
    qed
    show "K.Qclass ` N ⊆ {A ∈ K.Qcarrier. proj_KN K N A = N.Qclass 𝟬⇩M}"
    proof
      fix A assume "A ∈ K.Qclass ` N"
      then obtain v where v: "v ∈ N" "A = K.Qclass v" by blast
      then have vM: "v ∈ M" using N_in_M by blast
      have "A ∈ K.Qcarrier" using v(2) vM by simp
      moreover have "proj_KN K N A = N.Qclass 𝟬⇩M"
      proof -
        have "v ⊕ madd.inverse 𝟬⇩M ∈ N" using v(1) vM by (simp add: madd.inverse_unit)
        then have "N.Qclass v = N.Qclass 𝟬⇩M" using vM by (simp add: N.Class_eq_iff_diff_in_N)
        with v(2) vM proj_Class show ?thesis by simp
      qed
      ultimately show "A ∈ {A ∈ K.Qcarrier. proj_KN K N A = N.Qclass 𝟬⇩M}" by simp
    qed
  qed
qed


subsection ‹The third isomorphism theorem›

text ‹Assembling the pieces: @{term "proj_KN K N"} is a module homomorphism
  (@{thm [source] third_isomorphism_setup}) from @{text "M/K"} onto @{text "M/N"}
  (@{thm [source] third_isomorphism_surj}) with kernel @{text "N/K"} (@{thm [source] phi_Ker}).
  Applying the first isomorphism theorem to it yields
  @{text "(M/K)/(N/K) ≅ M/N"}.

  We state the conclusion as the ∗‹existence› of an isomorphism rather than by naming the induced
  map explicitly.  Naming it would mean writing out @{const module_homomorphism.ind} applied to the
  iterated-quotient operations, which is a long and fragile parameter list; existence is the
  standard textbook phrasing and is what consumers actually use.›
theorem third_isomorphism:
  assumes N_sub: "submodule N"
    and K_sub: "submodule K"
    and K_in_N: "K ⊆ N"
  shows "∃φ. module_homomorphism R (+) (⋅) 𝟬 𝟭
                (submodule_in_module.Qcarrier
                   (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                   (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N))
                (submodule_in_module.qadd
                   (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                   (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N))
                (submodule_in_module.Qclass
                   (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                   (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M))
                (submodule_in_module.qscale
                   (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                   (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
                   (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N))
                (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N)
                (submodule_in_module.qadd (⊕) 𝟬⇩M M N)
                (submodule_in_module.Qclass (⊕) 𝟬⇩M M N 𝟬⇩M)
                (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) N)
                φ
           ∧ bij_betw φ
                (submodule_in_module.Qcarrier
                   (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                   (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
                   (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N))
                (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N)"
proof -
  ― ‹Interpret the projection as a module homomorphism; its own first isomorphism theorem then
    supplies the induced map, once we rewrite its kernel to ‹N/K› and its image to ‹M/N›.›
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      "submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K"
      "submodule_in_module.qadd (⊕) 𝟬⇩M M K"
      "submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M"
      "submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K"
      "submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N"
      "submodule_in_module.qadd (⊕) 𝟬⇩M M N"
      "submodule_in_module.Qclass (⊕) 𝟬⇩M M N 𝟬⇩M"
      "submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) N"
      "proj_KN K N"
    by (rule third_isomorphism_setup[OF N_sub K_sub K_in_N])
  have Ker_eq: "P.Ker = submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` N"
    unfolding P.Ker_def using phi_Ker[OF N_sub K_sub K_in_N] by simp
  have image_eq: "proj_KN K N ` submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K
                = submodule_in_module.Qcarrier (⊕) 𝟬⇩M M N"
    by (rule third_isomorphism_surj[OF N_sub K_sub K_in_N])
  show ?thesis
    using P.first_isomorphism unfolding Ker_eq image_eq by blast
qed


subsection ‹The second isomorphism theorem›

text ‹For submodules @{term N} and @{term K}, the second isomorphism theorem states
  @{text "(N ⊕⇩S K)/K ≅ N/(N ∩ K)"}.

  The proof restricts the natural projection @{text "M → M/K"} to @{term N}.  A submodule is itself
  a module, so the restriction is a module homomorphism from @{term N} to @{text "M/K"}; its image is
  @{text "(N ⊕⇩S K)/K"} and its kernel is @{term "N ∩ K"}.  The first isomorphism theorem applied to
  it then gives the result.

  As with the third isomorphism theorem, the conclusion is stated as the ∗‹existence› of an
  isomorphism rather than by naming the induced map, whose argument list would otherwise have to be
  written out in full.›

text ‹A submodule, viewed as a module in its own right.›
lemma submodule_is_module:
  assumes N: "submodule N" shows "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M N (⊙)"
proof (rule Module.intro[OF Ring_axioms], rule Module_axioms.intro)
  show "Abelian_Group N (⊕) 𝟬⇩M"
  proof (rule Abelian_Group.intro)
    interpret S: Subgroup N M "(⊕)" "𝟬⇩M"
    proof (rule madd.subgroupI)
      show "N ⊆ M" using submodule_subset[OF N] .
      show "𝟬⇩M ∈ N" using submodule_zero[OF N] .
      show "⋀g h. ⟦ g ∈ N; h ∈ N ⟧ ⟹ g ⊕ h ∈ N" using submodule_add[OF N] by blast
      show "⋀g. g ∈ N ⟹ madd.invertible g"
        using submodule_subset[OF N] by auto
      show "⋀g. g ∈ N ⟹ madd.inverse g ∈ N" using submodule_neg[OF N] by blast
    qed
    show "Group N (⊕) 𝟬⇩M" by (rule S.sub.Group_axioms)
    show "commutative_monoid N (⊕) 𝟬⇩M"
      using submodule_subset[OF N] by unfold_locales (auto simp: madd.commutative)
  qed
next
  show "⋀a v. ⟦ a ∈ R; v ∈ N ⟧ ⟹ a ⊙ v ∈ N" using submodule_scale[OF N] by blast
next
  fix a u v assume "a ∈ R" "u ∈ N" "v ∈ N"
  then show "a ⊙ (u ⊕ v) = (a ⊙ u) ⊕ (a ⊙ v)"
    using submodule_subset[OF N] by (auto intro: scale_distrib_madd)
next
  fix a b v assume "a ∈ R" "b ∈ R" "v ∈ N"
  then show "(a + b) ⊙ v = (a ⊙ v) ⊕ (b ⊙ v)"
    using submodule_subset[OF N] by (auto intro: scale_distrib_add)
next
  fix a b v assume "a ∈ R" "b ∈ R" "v ∈ N"
  then show "(a ⋅ b) ⊙ v = a ⊙ (b ⊙ v)"
    using submodule_subset[OF N] by (auto intro: scale_scale)
next
  fix v assume "v ∈ N"
  then show "𝟭 ⊙ v = v" using submodule_subset[OF N] by (auto intro: scale_one)
qed

text ‹The natural projection @{text "M → M/K"} restricted to @{term N}.›
definition proj_res :: "'b set ⇒ 'b set ⇒ 'b ⇒ 'b set"
  where "proj_res N K = (λv ∈ N. submodule_in_module.Qclass (⊕) 𝟬⇩M M K v)"

lemma proj_res_apply [simp]:
  "v ∈ N ⟹ proj_res N K v = submodule_in_module.Qclass (⊕) 𝟬⇩M M K v"
  unfolding proj_res_def by simp

text ‹The restricted projection is a module homomorphism from @{term N} to @{text "M/K"}.›
lemma proj_res_hom:
  assumes N: "submodule N" and K: "submodule K"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
           N (⊕) 𝟬⇩M (⊙)
           (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
           (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
           (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
           (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K)
           (proj_res N K)"
proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  have NM: "N ⊆ M" using submodule_subset[OF N] .
  show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M N (⊙)" by (rule submodule_is_module[OF N])
  show "Module R (+) (⋅) 𝟬 𝟭 K.qadd (K.Qclass 𝟬⇩M) K.Qcarrier K.qscale"
    by (rule K.quotient.Module_axioms)
  show "proj_res N K ∈ N →⇩E K.Qcarrier"
    unfolding proj_res_def using NM by (rule_tac PiE_I) (auto simp: extensional_def)
next
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  fix u v assume uv: "u ∈ N" "v ∈ N"
  then have uvM: "u ∈ M" "v ∈ M" using submodule_subset[OF N] by auto
  have "u ⊕ v ∈ N" using submodule_add[OF N uv(1) uv(2)] .
  then show "proj_res N K (u ⊕ v) = K.qadd (proj_res N K u) (proj_res N K v)"
    using uv uvM by (simp add: K.madd_sub.Class_commutes_with_composition)
next
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  fix a v assume av: "a ∈ R" "v ∈ N"
  then have vM: "v ∈ M" using submodule_subset[OF N] by blast
  have "a ⊙ v ∈ N" using submodule_scale[OF N av(1) av(2)] .
  then show "proj_res N K (a ⊙ v) = K.qscale a (proj_res N K v)"
    using av vM by (simp add: K.qscale_Class)
qed

text ‹Its kernel is @{term "N ∩ K"}: a coset @{text "v + K"} with @{term "v ∈ N"} is zero exactly
  when @{term "v ∈ K"}.›
lemma proj_res_Ker:
  assumes N: "submodule N" and K: "submodule K"
  shows "{v ∈ N. proj_res N K v = submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M} = N ∩ K"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  have NM: "N ⊆ M" using submodule_subset[OF N] .
  show ?thesis
  proof
    show "{v ∈ N. proj_res N K v = K.Qclass 𝟬⇩M} ⊆ N ∩ K"
    proof
      fix v assume v: "v ∈ {v ∈ N. proj_res N K v = K.Qclass 𝟬⇩M}"
      ― ‹Extract the two conjuncts explicitly; ‹auto› here also unfolds @{const proj_res} and
        times out.›
      from v have vN: "v ∈ N" by blast
      from v have "proj_res N K v = K.Qclass 𝟬⇩M" by blast
      then have eq: "K.Qclass v = K.Qclass 𝟬⇩M" using vN by simp
      from vN have vM: "v ∈ M" using NM by blast
      have "v ⊕ madd.inverse 𝟬⇩M ∈ K"
        by (rule K.Class_eq_iff_diff_in_N[OF vM mzero_closed, THEN iffD1, OF eq])
      then have "v ∈ K" using vM by (simp add: madd.inverse_unit)
      with vN show "v ∈ N ∩ K" by blast
    qed
    show "N ∩ K ⊆ {v ∈ N. proj_res N K v = K.Qclass 𝟬⇩M}"
    proof
      fix v assume v: "v ∈ N ∩ K"
      then have vN: "v ∈ N" and vK: "v ∈ K" by auto
      from vN have vM: "v ∈ M" using NM by blast
      have "v ⊕ madd.inverse 𝟬⇩M ∈ K" using vK vM by (simp add: madd.inverse_unit)
      then have "K.Qclass v = K.Qclass 𝟬⇩M"
        by (rule K.Class_eq_iff_diff_in_N[OF vM mzero_closed, THEN iffD2])
      with vN show "v ∈ {v ∈ N. proj_res N K v = K.Qclass 𝟬⇩M}" by simp
    qed
  qed
qed

text ‹Its image is @{text "(N ⊕⇩S K)/K"}: the ‹K›-cosets of elements of @{term N} are exactly the
  ‹K›-cosets of elements of @{term "N ⊕⇩S K"}, since adding an element of @{term K} to a
  representative does not change its coset.›
lemma proj_res_image:
  assumes N: "submodule N" and K: "submodule K"
  shows "proj_res N K ` N
       = submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` (N ⊕⇩S K)"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  have NM: "N ⊆ M" using submodule_subset[OF N] .
  have KM: "K ⊆ M" using submodule_subset[OF K] .
  show ?thesis
  proof
    show "proj_res N K ` N ⊆ K.Qclass ` (N ⊕⇩S K)"
    proof
      fix X assume "X ∈ proj_res N K ` N"
      then obtain v where v: "v ∈ N" "X = proj_res N K v" by blast
      then have "X = K.Qclass v" by simp
      moreover have "v ∈ N ⊕⇩S K" using submodule_sum_incl_left[OF N K] v(1) by blast
      ultimately show "X ∈ K.Qclass ` (N ⊕⇩S K)" by blast
    qed
    show "K.Qclass ` (N ⊕⇩S K) ⊆ proj_res N K ` N"
    proof
      fix X assume "X ∈ K.Qclass ` (N ⊕⇩S K)"
      then obtain x where x: "x ∈ N ⊕⇩S K" "X = K.Qclass x" by blast
      from x(1) obtain u w where uw: "u ∈ N" "w ∈ K" "x = u ⊕ w"
        by (rule submodule_sum_memE)
      have uM: "u ∈ M" using uw(1) NM by blast
      have wM: "w ∈ M" using uw(2) KM by blast
      ― ‹The representative may be taken in @{term N}: the @{term K}-part is absorbed.›
      have "x ⊕ madd.inverse u = (w ⊕ u) ⊕ madd.inverse u"
        using uw(3) uM wM by (simp add: madd.commutative)
      also have "… = w ⊕ (u ⊕ madd.inverse u)"
        using uM wM by (simp add: madd.associative)
      also have "… = w" using uM wM by simp
      finally have "x ⊕ madd.inverse u = w" .
      then have "x ⊕ madd.inverse u ∈ K" using uw(2) by simp
      moreover have xM: "x ∈ M" using uw(3) uM wM by simp
      ultimately have "K.Qclass x = K.Qclass u"
        using xM uM by (simp add: K.Class_eq_iff_diff_in_N)
      with x(2) have "X = proj_res N K u" using uw(1) by simp
      then show "X ∈ proj_res N K ` N" using uw(1) by blast
    qed
  qed
qed

text ‹If @{term N} complements @{term K}, the restricted natural projection identifies
  @{term N} with the whole quotient @{text "M/K"}.  The two complement conditions have separate
  roles: trivial intersection gives injectivity through the kernel calculation, while the full
  submodule sum gives surjectivity through the image calculation.›
theorem complement_quotient_isomorphism:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
           N (⊕) 𝟬⇩M (⊙)
           (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)
           (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
           (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
           (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K)
           (proj_res N K)
       ∧ bij_betw (proj_res N K) N
           (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K)"
proof -
  interpret K: submodule_in_module R "(+)" "(⋅)" 𝟬 𝟭
      "(⊕)" "𝟬⇩M" M "(⊙)" K
    using K by unfold_locales
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      N "(⊕)" "𝟬⇩M" "(⊙)"
      K.Qcarrier K.qadd "K.Qclass 𝟬⇩M" K.qscale "proj_res N K"
    by (rule proj_res_hom[OF N K])

  have kernel: "P.Ker = N ∩ K"
    unfolding P.Ker_def using proj_res_Ker[OF N K] by simp
  have injective: "inj_on (proj_res N K) N"
    using P.injective_iff_kernel_trivial kernel disjoint by simp

  have class_image: "K.Qclass ` M = K.Qcarrier"
  proof -
    have "K.Qclass ` M = K.nat_proj ` M"
    proof (rule image_cong)
      show "M = M" by simp
    next
      fix x assume x: "x ∈ M"
      show "K.Qclass x = K.nat_proj x"
        by (rule sym, rule K.nat_proj_apply[OF x])
    qed
    also have "... = K.Qcarrier" by (rule K.nat_proj_image)
    finally show ?thesis .
  qed
  have surjective: "proj_res N K ` N = K.Qcarrier"
    using proj_res_image[OF N K] full class_image by simp

  show ?thesis
    using P.module_homomorphism_axioms injective surjective
    by (simp add: bij_betw_def)
qed

text ‹∗‹The second isomorphism theorem.››
theorem second_isomorphism:
  assumes N: "submodule N" and K: "submodule K"
  shows "∃φ. module_homomorphism R (+) (⋅) 𝟬 𝟭
                (submodule_in_module.Qcarrier (⊕) 𝟬⇩M N (N ∩ K))
                (submodule_in_module.qadd (⊕) 𝟬⇩M N (N ∩ K))
                (submodule_in_module.Qclass (⊕) 𝟬⇩M N (N ∩ K) 𝟬⇩M)
                (submodule_in_module.qscale (⊕) 𝟬⇩M N (⊙) (N ∩ K))
                (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` (N ⊕⇩S K))
                (submodule_in_module.qadd (⊕) 𝟬⇩M M K)
                (submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M)
                (submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K)
                φ
           ∧ bij_betw φ
                (submodule_in_module.Qcarrier (⊕) 𝟬⇩M N (N ∩ K))
                (submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` (N ⊕⇩S K))"
proof -
  ― ‹Interpret the restricted projection as a homomorphism out of @{term N}, then quote its own
    first isomorphism theorem, rewriting the kernel to @{term "N ∩ K"} and the image to
    ‹(N ⊕⇩S K)/K›.›
  ― ‹Established BEFORE the interpretation below: once ‹P› is interpreted, its ‹source› module
    supplies a second ‹submodule_sum› and the ‹⊕⇩S› notation becomes ambiguous.›
  have image_eq: "proj_res N K ` N
                = submodule_in_module.Qclass (⊕) 𝟬⇩M M K ` (N ⊕⇩S K)"
    by (rule proj_res_image[OF N K])
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      N "(⊕)" "𝟬⇩M" "(⊙)"
      "submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K"
      "submodule_in_module.qadd (⊕) 𝟬⇩M M K"
      "submodule_in_module.Qclass (⊕) 𝟬⇩M M K 𝟬⇩M"
      "submodule_in_module.qscale (⊕) 𝟬⇩M M (⊙) K"
      "proj_res N K"
    by (rule proj_res_hom[OF N K])
  have Ker_eq: "P.Ker = N ∩ K"
    unfolding P.Ker_def using proj_res_Ker[OF N K] by simp
  show ?thesis
    using P.first_isomorphism unfolding Ker_eq image_eq by blast
qed

end (* context module *)
end