Theory Module_Complements

section ‹Complementary submodules and projections›

theory Module_Complements
  imports Module_Iso_Theorems
begin

text ‹An idempotent module endomorphism is a projection onto its image.  The
  image and kernel therefore recover the two internal summands without any
  finite-dimensional assumption or choice of bases.›
locale idempotent_module_endomorphism =
  module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
    M "(⊕)" "𝟬⇩M" "(⊙)"
    M "(⊕)" "𝟬⇩M" "(⊙)" p
  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 p +
  assumes idempotent: "⋀x. x ∈ M ⟹ p (p x) = p x"
begin

theorem image_kernel_complementary:
  "p ` M ∩ Ker = {𝟬⇩M}"
  "p ` M ⊕⇩S Ker = M"
proof -
  have image_sub: "source.submodule (p ` M)"
    using image_submodule .
  show disjoint: "p ` M ∩ Ker = {𝟬⇩M}"
  proof (rule set_eqI, rule iffI)
    fix x assume x: "x ∈ p ` M ∩ Ker"
    then obtain y where y: "y ∈ M" "x = p y" by auto
    have "x = p x" using y idempotent[OF y(1)] by simp
    also have "... = 𝟬⇩M" using x by (simp add: Ker_image)
    finally show "x ∈ {𝟬⇩M}" by simp
  next
    fix x assume x: "x ∈ {𝟬⇩M}"
    have xeq: "x = 𝟬⇩M" using x by simp
    have zero_image: "𝟬⇩M ∈ p ` M"
    proof -
      have "p 𝟬⇩M ∈ p ` M"
        by (rule imageI[OF source.mzero_closed])
      then show ?thesis using hom_zero by simp
    qed
    have zero_kernel: "𝟬⇩M ∈ Ker"
      by (rule source.submodule_zero[OF Ker_submodule])
    have image_x: "x ∈ p ` M" using xeq zero_image by simp
    have kernel_x: "x ∈ Ker" using xeq zero_kernel by simp
    show "x ∈ p ` M ∩ Ker" by (rule IntI[OF image_x kernel_x])
  qed
  show "p ` M ⊕⇩S Ker = M"
  proof
    have sum_sub: "source.submodule (p ` M ⊕⇩S Ker)"
      by (rule source.submodule_sum_submodule[OF image_sub Ker_submodule])
    show "p ` M ⊕⇩S Ker ⊆ M"
      by (rule source.submodule_subset[OF sum_sub])
    show "M ⊆ p ` M ⊕⇩S Ker"
    proof
      fix x assume x: "x ∈ M"
      have px: "p x ∈ M" by (rule hom_closed[OF x])
      have remainder: "x ⊕ source.madd.inverse (p x) ∈ Ker"
      proof (rule Ker_memI)
        show "p (x ⊕ source.madd.inverse (p x)) = 𝟬⇩M"
          using x px idempotent[OF x]
          by (simp add: hom_add hom_neg)
        show "x ⊕ source.madd.inverse (p x) ∈ M" using x px by simp
      qed
      have image: "p x ∈ p ` M" by (rule imageI[OF x])
      have decomposition:
        "x = p x ⊕ (x ⊕ source.madd.inverse (p x))"
        using x px by (simp add: source.madd.ac)
      have "p x ⊕ (x ⊕ source.madd.inverse (p x))
          ∈ p ` M ⊕⇩S Ker"
        by (rule source.submodule_sum_memI[OF image remainder])
      show "x ∈ p ` M ⊕⇩S Ker"
        using decomposition ‹p x ⊕ (x ⊕ source.madd.inverse (p x))
          ∈ p ` M ⊕⇩S Ker› by simp
    qed
  qed
qed

end

context Module
begin

text ‹The projection onto @{term N} along @{term K} is obtained canonically from the quotient:
  first map an element of @{term M} to its class in @{text "M/K"}, then use the inverse of the
  restricted quotient isomorphism from @{term N}.  Both maps are restricted to their carriers, so
  the resulting projection follows the extensional-map convention of the module hierarchy.›
definition complement_projection :: "'b set ⇒ 'b set ⇒ 'b ⇒ 'b"
  where "complement_projection N K =
    compose M
      (restrict (inv_into N (proj_res N K))
        (submodule_in_module.Qcarrier (⊕) 𝟬⇩M M K))
      (submodule_in_module.nat_proj (⊕) 𝟬⇩M M K)"

text ‹The construction is a module homomorphism whenever the two submodules are complementary.
  This packages the quotient projection, the complement--quotient isomorphism, and its
  carrier-restricted inverse.›
theorem complement_projection_hom:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
    M (⊕) 𝟬⇩M (⊙) N (⊕) 𝟬⇩M (⊙)
    (complement_projection N 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 bij: "bij_betw (proj_res N K) N K.Qcarrier"
    using complement_quotient_isomorphism[OF N K disjoint full] by blast
  have inverse_hom: "module_homomorphism R (+) (⋅) 𝟬 𝟭
      K.Qcarrier K.qadd (K.Qclass 𝟬⇩M) K.qscale
      N (⊕) 𝟬⇩M (⊙)
      (restrict (inv_into N (proj_res N K)) K.Qcarrier)"
    by (rule P.inverse_module_homomorphism[OF bij])
  show ?thesis
    unfolding complement_projection_def
    by (rule K.nat_proj.compose_module_homomorphism[OF inverse_hom])
qed

text ‹The projection fixes the chosen summand.›
lemma complement_projection_apply_left:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and x: "x ∈ N"
  shows "complement_projection N K x = x"
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 bij: "bij_betw (proj_res N K) N K.Qcarrier"
    using complement_quotient_isomorphism[OF N K disjoint full] by blast
  have xM: "x ∈ M" using x submodule_subset[OF N] by blast
  show ?thesis
    unfolding complement_projection_def compose_def
    using P.inverse_module_homomorphism_left[OF bij x] x xM by simp
qed

text ‹The complementary summand is annihilated.›
lemma complement_projection_apply_right:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and x: "x ∈ K"
  shows "complement_projection N K x = 𝟬⇩M"
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 bij: "bij_betw (proj_res N K) N K.Qcarrier"
    using complement_quotient_isomorphism[OF N K disjoint full] by blast
  interpret I: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      K.Qcarrier K.qadd "K.Qclass 𝟬⇩M" K.qscale
      N "(⊕)" "𝟬⇩M" "(⊙)"
      "restrict (inv_into N (proj_res N K)) K.Qcarrier"
    by (rule P.inverse_module_homomorphism[OF bij])
  have xM: "x ∈ M" using x submodule_subset[OF K] by blast
  have xKer: "x ∈ K.nat_proj.Ker" using x K.nat_proj_Ker by simp
  have quotient_zero: "K.nat_proj x = K.Qclass 𝟬⇩M"
    by (rule K.nat_proj.Ker_image[OF xKer])
  show ?thesis
    unfolding complement_projection_def compose_def
    using xM quotient_zero I.hom_zero by simp
qed

text ‹On an explicitly decomposed element, the projection selects its left component.›
lemma complement_projection_apply_sum:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and u: "u ∈ N" and v: "v ∈ K"
  shows "complement_projection N K (u ⊕ v) = u"
proof -
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      M "(⊕)" "𝟬⇩M" "(⊙)"
      N "(⊕)" "𝟬⇩M" "(⊙)" "complement_projection N K"
    by (rule complement_projection_hom[OF N K disjoint full])
  have uM: "u ∈ M" using u submodule_subset[OF N] by blast
  have vM: "v ∈ M" using v submodule_subset[OF K] by blast
  have "complement_projection N K (u ⊕ v) =
      complement_projection N K u ⊕ complement_projection N K v"
    by (rule P.hom_add[OF uM vM])
  also have "... = u ⊕ 𝟬⇩M"
    using complement_projection_apply_left[OF N K disjoint full u]
      complement_projection_apply_right[OF N K disjoint full v]
    by simp
  also have "... = u" using uM by simp
  finally show ?thesis .
qed

text ‹Every element of a full, disjoint submodule sum has exactly one ordered pair of
  components.  Pairing the witnesses makes the uniqueness quantifier directly usable by clients.›
theorem complementary_decomposition_exists_unique:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and x: "x ∈ M"
  shows "∃!uv. fst uv ∈ N ∧ snd uv ∈ K ∧ x = fst uv ⊕ snd uv"
proof -
  have xsum: "x ∈ N ⊕⇩S K" using x full by simp
  then obtain u v where u: "u ∈ N" and v: "v ∈ K" and xeq: "x = u ⊕ v"
    by (rule submodule_sum_memE)
  show ?thesis
  proof (rule ex1I[of _ "(u, v)"])
    show "fst (u, v) ∈ N ∧ snd (u, v) ∈ K ∧ x = fst (u, v) ⊕ snd (u, v)"
      using u v xeq by simp
  next
    fix uv assume uv: "fst uv ∈ N ∧ snd uv ∈ K ∧
      x = fst uv ⊕ snd uv"
    have components: "u = fst uv ∧ v = snd uv"
      by (rule submodule_sum_decomposition_unique[OF N K disjoint u v])
        (use uv xeq in auto)
    then show "uv = (u, v)" by (cases uv) auto
  qed
qed

text ‹The image is precisely the summand onto which the map projects.›
theorem complement_projection_image:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
  shows "complement_projection N K ` M = N"
proof -
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      M "(⊕)" "𝟬⇩M" "(⊙)"
      N "(⊕)" "𝟬⇩M" "(⊙)" "complement_projection N K"
    by (rule complement_projection_hom[OF N K disjoint full])
  show ?thesis
  proof
    show "complement_projection N K ` M ⊆ N" using P.hom_closed by blast
    show "N ⊆ complement_projection N K ` M"
    proof
      fix x assume x: "x ∈ N"
      have xM: "x ∈ M" using x submodule_subset[OF N] by blast
      have "complement_projection N K x = x"
        by (rule complement_projection_apply_left[OF N K disjoint full x])
      moreover have "complement_projection N K x ∈ complement_projection N K ` M"
        by (rule imageI[OF xM])
      ultimately show "x ∈ complement_projection N K ` M" by simp
    qed
  qed
qed

text ‹The kernel is precisely the complementary summand.›
theorem complement_projection_Ker:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
  shows "{x ∈ M. complement_projection N K x = 𝟬⇩M} = K"
proof -
  have decompose: "⋀x. x ∈ M ⟹
      ∃u ∈ N. ∃v ∈ K. x = u ⊕ v"
  proof -
    fix x assume x: "x ∈ M"
    have "x ∈ N ⊕⇩S K" using x full by simp
    then show "∃u ∈ N. ∃v ∈ K. x = u ⊕ v"
      by (rule submodule_sum_memE) blast
  qed
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      M "(⊕)" "𝟬⇩M" "(⊙)"
      N "(⊕)" "𝟬⇩M" "(⊙)" "complement_projection N K"
    by (rule complement_projection_hom[OF N K disjoint full])
  have kernel: "P.Ker = K"
  proof
    show "P.Ker ⊆ K"
    proof
      fix x assume xKer: "x ∈ P.Ker"
      then have xM: "x ∈ M" and px: "complement_projection N K x = 𝟬⇩M"
        using P.Ker_mem P.Ker_image by auto
      obtain u v where u: "u ∈ N" and v: "v ∈ K" and xeq: "x = u ⊕ v"
        using decompose[OF xM] by blast
      have "complement_projection N K x = u"
        using xeq complement_projection_apply_sum[OF N K disjoint full u v] by simp
      then have "u = 𝟬⇩M" using px by simp
      moreover have vM: "v ∈ M" using v submodule_subset[OF K] by blast
      ultimately have "x = v" using xeq by (simp add: madd.left_unit)
      then show "x ∈ K" using v by simp
    qed
    show "K ⊆ P.Ker"
    proof
      fix x assume x: "x ∈ K"
      have xM: "x ∈ M" using x submodule_subset[OF K] by blast
      have "complement_projection N K x = 𝟬⇩M"
        by (rule complement_projection_apply_right[OF N K disjoint full x])
      then show "x ∈ P.Ker" by (rule P.Ker_memI[OF _ xM])
    qed
  qed
  show ?thesis using kernel by (simp add: P.Ker_def)
qed

text ‹Applying a complementary projection twice has no further effect.›
lemma complement_projection_idempotent:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and x: "x ∈ M"
  shows "complement_projection N K (complement_projection N K x) =
    complement_projection N K x"
proof -
  interpret P: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
      M "(⊕)" "𝟬⇩M" "(⊙)"
      N "(⊕)" "𝟬⇩M" "(⊙)" "complement_projection N K"
    by (rule complement_projection_hom[OF N K disjoint full])
  have "complement_projection N K x ∈ N" by (rule P.hom_closed[OF x])
  then show ?thesis by (rule complement_projection_apply_left[OF N K disjoint full])
qed

text ‹The two complementary projections recover the original element.  This also cross-checks
  the orientation of the construction: the first map selects the @{term N}-component and the
  swapped map selects the @{term K}-component.›
theorem complement_projections_sum:
  assumes N: "submodule N" and K: "submodule K"
    and disjoint: "N ∩ K = {𝟬⇩M}"
    and full: "N ⊕⇩S K = M"
    and x: "x ∈ M"
  shows "complement_projection N K x ⊕ complement_projection K N x = x"
proof -
  have disjoint': "K ∩ N = {𝟬⇩M}" using disjoint by (simp add: Int_commute)
  have full': "K ⊕⇩S N = M"
    using full submodule_sum_commute[OF K N] by simp
  have xsum: "x ∈ N ⊕⇩S K" using x full by simp
  then obtain u v where u: "u ∈ N" and v: "v ∈ K" and xeq: "x = u ⊕ v"
    by (rule submodule_sum_memE)
  have first: "complement_projection N K x = u"
    using xeq complement_projection_apply_sum[OF N K disjoint full u v] by simp
  have uM: "u ∈ M" using u submodule_subset[OF N] by blast
  have vM: "v ∈ M" using v submodule_subset[OF K] by blast
  have xeq': "x = v ⊕ u" using xeq uM vM by (simp add: madd.commutative)
  have second: "complement_projection K N x = v"
    using xeq' complement_projection_apply_sum[OF K N disjoint' full' v u] by simp
  show ?thesis using first second xeq by simp
qed

end


end