Theory Module_Exact_Sequence

section β€ΉExact sequences of modulesβ€Ί

theory Module_Exact_Sequence
  imports Module_Complements
begin

locale composable_module_homomorphisms =
  first: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    M "(βŠ•)" "𝟬M" "(βŠ™)" M' "(βŠ•2)" "𝟬2" "(βŠ™2)" Ξ· +
  second: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    M' "(βŠ•2)" "𝟬2" "(βŠ™2)" M'' "(βŠ•3)" "𝟬3" "(βŠ™3)" ΞΈ
  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 M'' and madd'' (infixl β€ΉβŠ•3β€Ί 65) and mzero'' (β€ΉπŸ¬3β€Ί)
      and scale'' (infixr β€ΉβŠ™3β€Ί 75)
    and Ξ· and ΞΈ
begin

definition exact :: bool
  where "exact ⟷ η ` M = second.Ker"

definition short_exact :: bool
  where "short_exact ⟷ inj_on η M ∧ exact ∧ θ ` M' = M''"

definition right_split :: bool
  where "right_split ⟷
    (βˆƒΟƒ. module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ ∧
      (βˆ€x∈M''. ΞΈ (Οƒ x) = x))"

definition left_split :: bool
  where "left_split ⟷
    (βˆƒΟ. module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M' (βŠ•2) 𝟬2 (βŠ™2) M (βŠ•) 𝟬M (βŠ™) ρ ∧
      (βˆ€x∈M. ρ (Ξ· x) = x))"

lemma exact_iff: "exact ⟷ η ` M = second.Ker"
  by (rule exact_def)

lemma short_exact_iff:
  "short_exact ⟷ inj_on η M ∧ η ` M = second.Ker ∧ θ ` M' = M''"
  by (simp add: short_exact_def exact_def)

lemma exact_imp_composition_zero:
  assumes ex: exact and x: "x ∈ M"
  shows "θ (η x) = 𝟬3"
proof -
  have "η x ∈ η ` M" using x by (rule imageI)
  then have "η x ∈ second.Ker" using ex by (simp add: exact_def)
  then show ?thesis by (rule second.Ker_image)
qed

lemma right_split_imp_surjective:
  assumes split: right_split
  shows "ΞΈ ` M' = M''"
proof
  show "ΞΈ ` M' βŠ† M''" using second.hom_closed by blast
  show "M'' βŠ† ΞΈ ` M'"
  proof
    fix x assume x: "x ∈ M''"
    obtain Οƒ where hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
      and sec: "βˆ€x∈M''. ΞΈ (Οƒ x) = x"
      using split unfolding right_split_def by blast
    interpret S: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M'' "(βŠ•3)" "𝟬3" "(βŠ™3)" M' "(βŠ•2)" "𝟬2" "(βŠ™2)" Οƒ
      by (rule hom)
    have sx: "Οƒ x ∈ M'" by (rule S.hom_closed[OF x])
    have eq: "ΞΈ (Οƒ x) = x" using sec x by blast
    have "ΞΈ (Οƒ x) ∈ ΞΈ ` M'" by (rule imageI[OF sx])
    then show "x ∈ θ ` M'" using eq by simp
  qed
qed

text β€ΉThe image of an explicit right section is complementary to the
  kernel of the split map.  The composite β€ΉΟƒ ∘ ΞΈβ€Ί is the
  corresponding idempotent projection on the middle module.β€Ί
theorem right_section_image_kernel_complementary:
  assumes section_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    and sec_eq: "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x"
  shows "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
    and "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
proof -
  interpret S: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    M'' "(βŠ•3)" "𝟬3" "(βŠ™3)"
    M' "(βŠ•2)" "𝟬2" "(βŠ™2)" Οƒ
    by (rule section_hom)
  define p where "p = compose M' Οƒ ΞΈ"
  have p_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M' (βŠ•2) 𝟬2 (βŠ™2) M' (βŠ•2) 𝟬2 (βŠ™2) p"
    unfolding p_def by (rule second.compose_module_homomorphism[OF section_hom])
  interpret P: idempotent_module_endomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    M' "(βŠ•2)" "𝟬2" "(βŠ™2)" p
  proof (rule idempotent_module_endomorphism.intro[OF p_hom])
    show "idempotent_module_endomorphism_axioms M' p"
    proof
      fix x assume x: "x ∈ M'"
      have tx: "θ x ∈ M''" by (rule second.hom_closed[OF x])
      have stx: "Οƒ (ΞΈ x) ∈ M'" by (rule S.hom_closed[OF tx])
      show "p (p x) = p x"
        unfolding p_def compose_def
        using x tx stx sec_eq[OF tx] by simp
    qed
  qed
  have image_p: "p ` M' = Οƒ ` M''"
  proof (rule set_eqI, rule iffI)
    fix y assume y: "y ∈ p ` M'"
    then obtain x where x: "x ∈ M'" "y = p x" by blast
    have tx: "θ x ∈ M''" by (rule second.hom_closed[OF x(1)])
    have value_eq: "y = Οƒ (ΞΈ x)" using x unfolding p_def compose_def by simp
    have "Οƒ (ΞΈ x) ∈ Οƒ ` M''" by (rule imageI[OF tx])
    then show "y ∈ Οƒ ` M''" using value_eq by simp
  next
    fix y assume y: "y ∈ Οƒ ` M''"
    then obtain z where z: "z ∈ M''" "y = Οƒ z" by blast
    have sz: "Οƒ z ∈ M'" by (rule S.hom_closed[OF z(1)])
    have value_eq: "p (Οƒ z) = Οƒ z"
      unfolding p_def compose_def using z sz sec_eq[OF z(1)] by simp
    have "p (Οƒ z) ∈ p ` M'" by (rule imageI[OF sz])
    then show "y ∈ p ` M'" using z value_eq by simp
  qed
  have kernel_p: "P.Ker = second.Ker"
  proof (rule set_eqI, rule iffI)
    fix x assume x: "x ∈ P.Ker"
    have xM: "x ∈ M'" by (rule P.Ker_mem[OF x])
    have tx: "θ x ∈ M''" by (rule second.hom_closed[OF xM])
    have theta_p: "ΞΈ (p x) = ΞΈ x"
      unfolding p_def compose_def using xM tx sec_eq[OF tx] by simp
    have "θ (p x) = 𝟬3"
      using P.Ker_image[OF x] second.hom_zero by simp
    then have "θ x = 𝟬3" using theta_p by simp
    then show "x ∈ second.Ker" by (rule second.Ker_memI[OF _ xM])
  next
    fix x assume x: "x ∈ second.Ker"
    have xM: "x ∈ M'" by (rule second.Ker_mem[OF x])
    have "p x = 𝟬2"
      unfolding p_def compose_def
      using xM second.Ker_image[OF x] S.hom_zero by simp
    then show "x ∈ P.Ker" by (rule P.Ker_memI[OF _ xM])
  qed
  show "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
    using P.image_kernel_complementary(1) image_p kernel_p by simp
  show "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
    using P.image_kernel_complementary(2) image_p kernel_p by simp
qed

theorem right_split_obtains_image_kernel_complement:
  assumes split: right_split
  obtains Οƒ where
    "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x"
    "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
    "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
proof -
  obtain Οƒ where hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    and sec: "βˆ€x∈M''. ΞΈ (Οƒ x) = x"
    using split unfolding right_split_def by blast
  have sec_eq: "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x" using sec by blast
  have complementary:
      "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
      "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
  proof -
    show "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
      by (rule right_section_image_kernel_complementary(1)[OF hom sec_eq])
    show "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
      by (rule right_section_image_kernel_complementary(2)[OF hom sec_eq])
  qed
  show thesis by (rule that[OF hom sec_eq complementary])
qed

theorem short_exact_right_split_obtains_decomposition:
  assumes short: short_exact and split: right_split
  obtains Οƒ where
    "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x"
    "Οƒ ` M'' ∩ Ξ· ` M = {𝟬2}"
    "Module.submodule_sum (βŠ•2) (Οƒ ` M'') (Ξ· ` M) = M'"
proof -
  obtain Οƒ where hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    and sec_eq: "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x"
    and disjoint: "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
    and full: "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
    using right_split_obtains_image_kernel_complement[OF split] by blast
  have exact: "Ξ· ` M = second.Ker" using short by (simp add: short_exact_iff)
  show thesis
    by (rule that[OF hom sec_eq]) (use disjoint full exact in simp_all)
qed

text β€ΉA right section yields a retraction of the injection.  The projection onto the image of
  @{term Ξ·} along the section image is followed by the inverse of @{term Ξ·} onto its image.β€Ί
theorem short_exact_right_split_imp_left_split:
  assumes short: short_exact and split: right_split
  shows left_split
proof -
  obtain Οƒ where section_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M'' (βŠ•3) 𝟬3 (βŠ™3) M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    and sec_eq: "β‹€x. x ∈ M'' ⟹ ΞΈ (Οƒ x) = x"
    and disjoint: "Οƒ ` M'' ∩ second.Ker = {𝟬2}"
    and full: "Module.submodule_sum (βŠ•2) (Οƒ ` M'') second.Ker = M'"
    using right_split_obtains_image_kernel_complement[OF split] by blast
  have exact: "Ξ· ` M = second.Ker" using short by (simp add: short_exact_iff)
  have eta_sub: "first.target.submodule (Ξ· ` M)" using first.image_submodule .
  interpret S: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M'' "(βŠ•3)" "𝟬3" "(βŠ™3)"
      M' "(βŠ•2)" "𝟬2" "(βŠ™2)" Οƒ
    by (rule section_hom)
  have sigma_sub: "first.target.submodule (Οƒ ` M'')" using S.image_submodule .
  have eta_sub': "Module.submodule R (βŠ•2) 𝟬2 M' (βŠ™2) (Ξ· ` M)"
    using eta_sub .
  have sigma_sub': "Module.submodule R (βŠ•2) 𝟬2 M' (βŠ™2) (Οƒ ` M'')"
    using sigma_sub .
  have disjoint': "Ξ· ` M ∩ Οƒ ` M'' = {𝟬2}"
    using disjoint exact by (simp add: Int_commute)
  have full': "Module.submodule_sum (βŠ•2) (Ξ· ` M) (Οƒ ` M'') = M'"
    using full exact first.target.submodule_sum_commute[OF eta_sub sigma_sub] by simp
  interpret Kq: submodule_in_module R "(+)" "(β‹…)" 𝟬 𝟭
      "(βŠ•2)" "𝟬2" M' "(βŠ™2)" "(Οƒ ` M'')"
    using sigma_sub' by unfold_locales
  interpret Q: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      "(Ξ· ` M)" "(βŠ•2)" "𝟬2" "(βŠ™2)"
      Kq.Qcarrier Kq.qadd "Kq.Qclass 𝟬2" Kq.qscale
      "first.target.proj_res (Ξ· ` M) (Οƒ ` M'')"
    by (rule first.target.proj_res_hom[OF eta_sub' sigma_sub'])
  have projection_bij:
      "bij_betw (first.target.proj_res (Ξ· ` M) (Οƒ ` M''))
        (Ξ· ` M) Kq.Qcarrier"
    using first.target.complement_quotient_isomorphism
      [OF eta_sub' sigma_sub' disjoint' full'] by blast
  have inverse_projection:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        Kq.Qcarrier Kq.qadd (Kq.Qclass 𝟬2) Kq.qscale
        (Ξ· ` M) (βŠ•2) 𝟬2 (βŠ™2)
        (restrict (inv_into (Ξ· ` M) (first.target.proj_res (Ξ· ` M) (Οƒ ` M''))) Kq.Qcarrier)"
    by (rule Q.inverse_module_homomorphism[OF projection_bij])
  interpret P: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M' "(βŠ•2)" "𝟬2" "(βŠ™2)"
      "(Ξ· ` M)" "(βŠ•2)" "𝟬2" "(βŠ™2)"
      "first.target.complement_projection (Ξ· ` M) (Οƒ ` M'')"
    by (rule first.target.complement_projection_hom
      [OF eta_sub' sigma_sub' disjoint' full'])
  have eta_image_hom:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M (βŠ•) 𝟬M (βŠ™)
        (Ξ· ` M) (βŠ•2) 𝟬2 (βŠ™2) Ξ·"
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (β‹…) 𝟬 𝟭 (βŠ•) 𝟬M M (βŠ™)"
      by (rule first.source.Module_axioms)
    show "Module R (+) (β‹…) 𝟬 𝟭
        (βŠ•2) 𝟬2 (Ξ· ` M) (βŠ™2)"
      by (rule first.image_is_module)
    show "Ξ· ∈ M β†’E (Ξ· ` M)"
      using first.hom_closed by (auto simp: PiE_iff extensional_def)
  next
    fix u v assume uv: "u ∈ M" "v ∈ M"
    then show "Ξ· (u βŠ• v) = Ξ· u βŠ•2 Ξ· v"
      by (rule first.hom_add)
  next
    fix a v assume av: "a ∈ R" "v ∈ M"
    then show "Ξ· (a βŠ™ v) = a βŠ™2 Ξ· v"
      by (rule first.hom_scale)
  qed
  interpret I: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M "(βŠ•)" "𝟬M" "(βŠ™)"
      "(Ξ· ` M)" "(βŠ•2)" "𝟬2" "(βŠ™2)" Ξ·
    by (rule eta_image_hom)
  have inj_eta: "inj_on Ξ· M" using short by (simp add: short_exact_def)
  have eta_bij: "bij_betw Ξ· M (Ξ· ` M)"
    using inj_eta by (simp add: bij_betw_def)
  have J_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      (Ξ· ` M) (βŠ•2) 𝟬2 (βŠ™2)
      M (βŠ•) 𝟬M (βŠ™)
      (restrict (inv_into M Ξ·) (Ξ· ` M))"
    by (rule I.inverse_module_homomorphism[OF eta_bij])
  define ρ where
    "ρ = compose M' (restrict (inv_into M η) (η ` M))
      (first.target.complement_projection (Ξ· ` M) (Οƒ ` M''))"
  have rho_hom:
    "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M' (βŠ•2) 𝟬2 (βŠ™2)
        M (βŠ•) 𝟬M (βŠ™) ρ"
    unfolding ρ_def
    by (rule P.compose_module_homomorphism[OF J_hom])
  have retract: "β‹€x. x ∈ M ⟹ ρ (Ξ· x) = x"
  proof -
    fix x assume x: "x ∈ M"
    have eta_x: "η x ∈ η ` M" by (rule imageI[OF x])
    have eta_xM': "η x ∈ M'" by (rule first.hom_closed[OF x])
    have projection: "first.target.complement_projection (Ξ· ` M) (Οƒ ` M'') (Ξ· x) = Ξ· x"
      by (rule first.target.complement_projection_apply_left
          [OF eta_sub sigma_sub disjoint' full' eta_x])
    have inverse: "restrict (inv_into M Ξ·) (Ξ· ` M) (Ξ· x) = x"
      by (rule I.inverse_module_homomorphism_left[OF eta_bij x])
    show "ρ (η x) = x"
      unfolding ρ_def compose_def
      using projection inverse eta_x eta_xM' by (simp add: restrict_apply')
  qed
  show ?thesis unfolding left_split_def using rho_hom retract by blast
qed

text β€ΉA retraction of the injection makes its image a direct summand.  Exactness then
  identifies the complementary summand with the quotient, so the second map has a
  carrier-restricted inverse that supplies a right section.β€Ί
theorem short_exact_left_split_imp_right_split:
  assumes short: short_exact and split: left_split
  shows right_split
proof -
  obtain ρ where rho_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M' (βŠ•2) 𝟬2 (βŠ™2) M (βŠ•) 𝟬M (βŠ™) ρ"
    and retract: "β‹€x. x ∈ M ⟹ ρ (Ξ· x) = x"
    using split unfolding left_split_def by blast
  interpret Rho: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M' "(βŠ•2)" "𝟬2" "(βŠ™2)"
      M "(βŠ•)" "𝟬M" "(βŠ™)" ρ
    by (rule rho_hom)
  have eta_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M (βŠ•) 𝟬M (βŠ™)
      M' (βŠ•2) 𝟬2 (βŠ™2) Ξ·"
    by unfold_locales
  define p where "p = compose M' η ρ"
  have p_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      M' (βŠ•2) 𝟬2 (βŠ™2)
      M' (βŠ•2) 𝟬2 (βŠ™2) p"
    unfolding p_def
    by (rule Rho.compose_module_homomorphism[OF eta_hom])
  interpret P: idempotent_module_endomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M' "(βŠ•2)" "𝟬2" "(βŠ™2)" p
  proof (rule idempotent_module_endomorphism.intro[OF p_hom])
    show "idempotent_module_endomorphism_axioms M' p"
    proof
      fix x assume xM': "x ∈ M'"
      have rx: "ρ x ∈ M" by (rule Rho.hom_closed[OF xM'])
      have etarx: "η (ρ x) ∈ M'" by (rule first.hom_closed[OF rx])
      show "p (p x) = p x"
        unfolding p_def compose_def
        using xM' rx etarx retract[OF rx] by simp
    qed
  qed
  have inj_eta: "inj_on Ξ· M" using short by (simp add: short_exact_def)
  have image_p: "p ` M' = Ξ· ` M"
  proof (rule set_eqI, rule iffI)
    fix y assume y: "y ∈ p ` M'"
    then obtain x where x: "x ∈ M'" "y = p x" by blast
    have rx: "ρ x ∈ M" by (rule Rho.hom_closed[OF x(1)])
    have value_eq: "y = η (ρ x)"
      using x unfolding p_def compose_def by simp
    then show "y ∈ η ` M" using rx by blast
  next
    fix y assume y: "y ∈ η ` M"
    then obtain x where x: "x ∈ M" "y = η x" by blast
    have etax: "η x ∈ M'" by (rule first.hom_closed[OF x(1)])
    have value_eq: "p (Ξ· x) = Ξ· x"
      unfolding p_def compose_def using x retract[OF x(1)] by simp
    have image_value: "p (η x) ∈ p ` M'" by (rule imageI[OF etax])
    then show "y ∈ p ` M'" using value_eq x(2) by simp
  qed
  have Pker_sub: "first.target.submodule P.Ker" using P.Ker_submodule .
  have eta_sub: "first.target.submodule (Ξ· ` M)" using first.image_submodule .
  have disjoint_P: "P.Ker ∩ (η ` M) = {𝟬2}"
    using P.image_kernel_complementary(1) image_p by (simp add: Int_commute)
  have full_eta_P: "Module.submodule_sum (βŠ•2) (Ξ· ` M) P.Ker = M'"
    using P.image_kernel_complementary(2) image_p by simp
  have full_P_eta: "Module.submodule_sum (βŠ•2) P.Ker (Ξ· ` M) = M'"
    using full_eta_P first.target.submodule_sum_commute[OF Pker_sub eta_sub] by simp
  have exact: "Ξ· ` M = second.Ker" using short by (simp add: short_exact_iff)
  have theta_restrict_hom:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        P.Ker (βŠ•2) 𝟬2 (βŠ™2)
        M'' (βŠ•3) 𝟬3 (βŠ™3)
        (restrict ΞΈ P.Ker)"
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (β‹…) 𝟬 𝟭
        (βŠ•2) 𝟬2 P.Ker (βŠ™2)"
      by (rule first.target.submodule_is_module[OF Pker_sub])
    show "Module R (+) (β‹…) 𝟬 𝟭
        (βŠ•3) 𝟬3 M'' (βŠ™3)"
      by (rule second.target.Module_axioms)
    show "restrict ΞΈ P.Ker ∈ P.Ker β†’E M''"
      using first.target.submodule_subset[OF Pker_sub] second.hom_closed
      by (auto simp: PiE_iff extensional_def)
  next
    fix u v assume uv: "u ∈ P.Ker" "v ∈ P.Ker"
    have uM': "u ∈ M'" and vM': "v ∈ M'"
      using uv first.target.submodule_subset[OF Pker_sub] by auto
    have uvP: "u βŠ•2 v ∈ P.Ker"
      by (rule first.target.submodule_add[OF Pker_sub uv(1) uv(2)])
    show "restrict ΞΈ P.Ker (u βŠ•2 v) =
        restrict ΞΈ P.Ker u βŠ•3 restrict ΞΈ P.Ker v"
      using uv uvP uM' vM' by (simp add: restrict_apply' second.hom_add)
  next
    fix a v assume av: "a ∈ R" "v ∈ P.Ker"
    have vM': "v ∈ M'" using av(2) first.target.submodule_subset[OF Pker_sub] by blast
    have avP: "a βŠ™2 v ∈ P.Ker"
      by (rule first.target.submodule_scale[OF Pker_sub av(1) av(2)])
    show "restrict ΞΈ P.Ker (a βŠ™2 v) =
        a βŠ™3 restrict ΞΈ P.Ker v"
      using av avP vM' by (simp add: restrict_apply' second.hom_scale)
  qed
  interpret T: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      P.Ker "(βŠ•2)" "𝟬2" "(βŠ™2)"
      M'' "(βŠ•3)" "𝟬3" "(βŠ™3)" "restrict ΞΈ P.Ker"
    by (rule theta_restrict_hom)
  have T_kernel: "T.Ker = {𝟬2}"
  proof (rule set_eqI, rule iffI)
    fix x assume x: "x ∈ T.Ker"
    have xP: "x ∈ P.Ker" by (rule T.Ker_mem[OF x])
    have xM': "x ∈ M'" using xP first.target.submodule_subset[OF Pker_sub] by blast
    have theta_x: "θ x = 𝟬3"
      using T.Ker_image[OF x] xP by (simp add: restrict_apply')
    have xeta: "x ∈ η ` M"
    proof -
      have xsecond: "x ∈ second.Ker" by (rule second.Ker_memI[OF theta_x xM'])
      then show ?thesis using exact by simp
    qed
    have "x ∈ P.Ker ∩ (η ` M)" by (rule IntI[OF xP xeta])
    then show "x ∈ {𝟬2}" using disjoint_P by simp
  next
    fix x assume x: "x ∈ {𝟬2}"
    have zeroP: "𝟬2 ∈ P.Ker" by (rule first.target.submodule_zero[OF Pker_sub])
    have zeroT: "restrict θ P.Ker 𝟬2 = 𝟬3" by (rule T.hom_zero)
    show "x ∈ T.Ker" using x zeroP zeroT by (simp add: T.Ker_def)
  qed
  have T_inj: "inj_on (restrict ΞΈ P.Ker) P.Ker"
    using T.injective_iff_kernel_trivial T_kernel by blast
  have T_image: "(restrict ΞΈ P.Ker) ` P.Ker = M''"
  proof (rule set_eqI, rule iffI)
    fix z assume z: "z ∈ (restrict θ P.Ker) ` P.Ker"
    then obtain u where u: "u ∈ P.Ker" "z = restrict θ P.Ker u" by blast
    have uM': "u ∈ M'" using u(1) first.target.submodule_subset[OF Pker_sub] by blast
    show "z ∈ M''" using u(1) u(2) second.hom_closed[OF uM'] by (simp add: restrict_apply')
  next
    fix z assume z: "z ∈ M''"
    have theta_surj: "ΞΈ ` M' = M''" using short by (simp add: short_exact_iff)
    have zimage: "z ∈ θ ` M'" using z theta_surj by simp
    then obtain y where y: "y ∈ M'" "z = θ y" by blast
    have ysum: "y ∈ Module.submodule_sum (βŠ•2) P.Ker (Ξ· ` M)"
      using y(1) full_P_eta by simp
    then obtain u v where uv: "u ∈ P.Ker" "v ∈ Ξ· ` M" "y = u βŠ•2 v"
      by (rule first.target.submodule_sum_memE)
    have uM': "u ∈ M'" using uv(1) first.target.submodule_subset[OF Pker_sub] by blast
    have vM': "v ∈ M'" using uv(2) first.target.submodule_subset[OF eta_sub] by blast
    have theta_v: "θ v = 𝟬3"
    proof -
      have vker: "v ∈ second.Ker" using uv(2) exact by simp
      then show ?thesis by (rule second.Ker_image)
    qed
    have theta_u: "ΞΈ u = z"
      using y uv(3) uM' vM' theta_v by (simp add: second.hom_add)
    have image_u: "(restrict θ P.Ker) u ∈
        (restrict ΞΈ P.Ker) ` P.Ker" by (rule imageI[OF uv(1)])
    show "z ∈ (restrict θ P.Ker) ` P.Ker"
      using image_u theta_u uv(1) by (simp add: restrict_apply')
  qed
  have T_bij: "bij_betw (restrict ΞΈ P.Ker) P.Ker M''"
    using T_inj T_image by (simp add: bij_betw_def)
  have inverse_hom:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M'' (βŠ•3) 𝟬3 (βŠ™3)
        P.Ker (βŠ•2) 𝟬2 (βŠ™2)
        (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'')"
    by (rule T.inverse_module_homomorphism[OF T_bij])
  interpret U: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
      M'' "(βŠ•3)" "𝟬3" "(βŠ™3)"
      P.Ker "(βŠ•2)" "𝟬2" "(βŠ™2)"
      "restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M''"
    by (rule inverse_hom)
  have inclusion_hom:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        P.Ker (βŠ•2) 𝟬2 (βŠ™2)
        M' (βŠ•2) 𝟬2 (βŠ™2) (identity P.Ker)"
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (β‹…) 𝟬 𝟭
        (βŠ•2) 𝟬2 P.Ker (βŠ™2)"
      by (rule first.target.submodule_is_module[OF Pker_sub])
    show "Module R (+) (β‹…) 𝟬 𝟭
        (βŠ•2) 𝟬2 M' (βŠ™2)"
      by (rule first.target.Module_axioms)
    show "identity P.Ker ∈ P.Ker β†’E M'"
      using first.target.submodule_subset[OF Pker_sub] by (auto simp: PiE_iff)
  next
    fix u v assume u: "u ∈ P.Ker" and v: "v ∈ P.Ker"
    have uv: "u βŠ•2 v ∈ P.Ker"
      by (rule first.target.submodule_add[OF Pker_sub u v])
    then show "identity P.Ker (u βŠ•2 v) =
        identity P.Ker u βŠ•2 identity P.Ker v"
      using u v by simp
  next
    fix a v assume a: "a ∈ R" and v: "v ∈ P.Ker"
    have av: "a βŠ™2 v ∈ P.Ker"
      by (rule first.target.submodule_scale[OF Pker_sub a v])
    then show "identity P.Ker (a βŠ™2 v) =
        a βŠ™2 identity P.Ker v"
      using v by simp
  qed
  define Οƒ where
    "Οƒ = compose M'' (identity P.Ker)
      (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'')"
  have section_hom:
      "module_homomorphism R (+) (β‹…) 𝟬 𝟭
        M'' (βŠ•3) 𝟬3 (βŠ™3)
        M' (βŠ•2) 𝟬2 (βŠ™2) Οƒ"
    unfolding Οƒ_def
    by (rule U.compose_module_homomorphism[OF inclusion_hom])
  have section_eq: "β‹€z. z ∈ M'' ⟹ ΞΈ (Οƒ z) = z"
  proof -
    fix z assume z: "z ∈ M''"
    have uz: "restrict (inv_into P.Ker (restrict θ P.Ker)) M'' z ∈ P.Ker"
      by (rule U.hom_closed[OF z])
    have inverse: "restrict ΞΈ P.Ker
        (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z) = z"
      by (rule T.inverse_module_homomorphism_right[OF T_bij z])
    have sigma_apply: "Οƒ z =
        restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z"
      unfolding Οƒ_def compose_def
      using uz z by (simp add: restrict_apply')
    have inverse_value: "ΞΈ
        (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z) =
        restrict ΞΈ P.Ker
          (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z)"
      by (rule sym, rule restrict_apply'[OF uz])
    have theta_sigma: "ΞΈ (Οƒ z) = ΞΈ
        (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z)"
      by (simp only: sigma_apply)
    have theta_restrict: "ΞΈ
        (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z) =
        restrict ΞΈ P.Ker
          (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z)"
      by (rule inverse_value)
    have theta_intermediate: "ΞΈ (Οƒ z) =
        restrict ΞΈ P.Ker
          (restrict (inv_into P.Ker (restrict ΞΈ P.Ker)) M'' z)"
      by (rule trans[OF theta_sigma theta_restrict])
    show "ΞΈ (Οƒ z) = z"
      by (rule trans[OF theta_intermediate inverse])
  qed
  show ?thesis unfolding right_split_def using section_hom section_eq by blast
qed

theorem short_exact_right_split_iff_left_split:
  assumes short: short_exact
  shows "right_split ⟷ left_split"
  using short_exact_right_split_imp_left_split[OF short]
    short_exact_left_split_imp_right_split[OF short] by blast

end

context Module
begin

text β€ΉThe carrier-restricted identity on a submodule is its inclusion into the
  ambient module.β€Ί
theorem submodule_inclusion_hom:
  assumes N: "submodule N"
  shows "module_homomorphism R (+) (β‹…) 𝟬 𝟭
    N (βŠ•) 𝟬M (βŠ™) M (βŠ•) 𝟬M (βŠ™) (identity N)"
proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
  show "Module R (+) (β‹…) 𝟬 𝟭 (βŠ•) 𝟬M N (βŠ™)"
    by (rule submodule_is_module[OF N])
  show "Module R (+) (β‹…) 𝟬 𝟭 (βŠ•) 𝟬M M (βŠ™)"
    by (rule Module_axioms)
  show "identity N ∈ N β†’E M"
    using submodule_subset[OF N] by (auto simp: PiE_iff)
next
  fix u v assume u: "u ∈ N" and v: "v ∈ N"
  have uv: "u βŠ• v ∈ N" using N u v by (rule submodule_add)
  then show "identity N (u βŠ• v) = identity N u βŠ• identity N v"
    using u v by simp
next
  fix a v assume a: "a ∈ R" and v: "v ∈ N"
  have av: "a βŠ™ v ∈ N" using N a v by (rule submodule_scale)
  then show "identity N (a βŠ™ v) = a βŠ™ identity N v"
    using v by simp
qed

text β€ΉComplementary submodules give the canonical split short exact sequence
  β€Ή0 ⟢ K ⟢ M ⟢ N ⟢ 0β€Ί.  The inclusion of β€ΉNβ€Ί
  is a section of the complementary projection.β€Ί
theorem complementary_submodules_split_short_exact:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬M}"
    and full: "N βŠ•S K = M"
  shows "composable_module_homomorphisms.short_exact
      K M N 𝟬M (identity K) (complement_projection N K)
    ∧ composable_module_homomorphisms.right_split
      R (+) (β‹…) 𝟬 𝟭
      M (βŠ•) 𝟬M (βŠ™) N (βŠ•) 𝟬M (βŠ™)
      (complement_projection N K)"
proof -
  interpret I: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    K "(βŠ•)" "𝟬M" "(βŠ™)" M "(βŠ•)" "𝟬M" "(βŠ™)" "identity K"
    by (rule submodule_inclusion_hom[OF K])
  interpret P: module_homomorphism R "(+)" "(β‹…)" 𝟬 𝟭
    M "(βŠ•)" "𝟬M" "(βŠ™)" N "(βŠ•)" "𝟬M" "(βŠ™)" "complement_projection N K"
    by (rule complement_projection_hom[OF N K disjoint full])
  interpret E: composable_module_homomorphisms R "(+)" "(β‹…)" 𝟬 𝟭
    K "(βŠ•)" "𝟬M" "(βŠ™)" M "(βŠ•)" "𝟬M" "(βŠ™)"
    N "(βŠ•)" "𝟬M" "(βŠ™)" "identity K" "complement_projection N K"
    by unfold_locales
  have image_I: "identity K ` K = K" by auto
  have ker_P: "P.Ker = K"
    using complement_projection_Ker[OF N K disjoint full]
    by (simp add: P.Ker_def)
  have image_P: "complement_projection N K ` M = N"
    by (rule complement_projection_image[OF N K disjoint full])
  have short: "E.short_exact"
    by (simp add: E.short_exact_def E.exact_def image_I ker_P image_P)
  have section_hom: "module_homomorphism R (+) (β‹…) 𝟬 𝟭
      N (βŠ•) 𝟬M (βŠ™) M (βŠ•) 𝟬M (βŠ™) (identity N)"
    by (rule submodule_inclusion_hom[OF N])
  have sec: "βˆ€x∈N. complement_projection N K (identity N x) = x"
    using complement_projection_apply_left[OF N K disjoint full] by simp
  have split: "E.right_split"
    unfolding E.right_split_def using section_hom sec by blast
  show ?thesis using short split by simp
qed

end

end