Theory Module_Homomorphism

section ‹Module homomorphisms›

theory Module_Homomorphism
  imports Module_Basics
begin

text ‹A ∗‹module homomorphism› (over a fixed ring @{term R}) is a map @{term η} between @{term R}-modules
  that is additive and commutes with scaling.  This mirrors the group and ring homomorphism locales of
  theories ‹Group_Theory› and ‹Ring_Theory›, with the extra axiom linking the two scaling operations.
  We develop the kernel, image, and the injectivity criterion @{text "Ker = {0}"}.›

text ‹The import of ‹FiniteProduct› (through ‹Module›) re-merges HOL's @{text "+"}/@{text "-"} concrete
  syntax alongside the ring locale's, which is harmless in term positions (type inference disambiguates)
  but ambiguous in a locale-header instantiation argument.  We therefore remove the HOL syntax again, as
  ‹Ring_Theory› does, so that within this theory @{text "+"} unambiguously denotes the ring's addition.›
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax

text ‹A module homomorphism fixes a ∗‹single› scalar ring @{term R} and two @{term R}-modules --- the source
  @{term M} and the target @{term M'} --- sharing that ring.  The ring parameters ‹+ ⋅ 𝟬 𝟭› appear once in
  the ‹for› clause and are threaded verbatim into both module interpretations, so no token is bound twice.›
locale module_homomorphism =
  source: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩M" M "(⊙)" +
  target: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕⇩2)" "𝟬⇩2" M' "(⊙⇩2)" +
  map η M M'
  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 η +
  assumes hom_add: "⟦ u ∈ M; v ∈ M ⟧ ⟹ η (u ⊕ v) = η u ⊕⇩2 η v"
    and hom_scale: "⟦ a ∈ R; v ∈ M ⟧ ⟹ η (a ⊙ v) = a ⊙⇩2 η v"
begin

subsection ‹Basic properties›

lemma hom_closed: "v ∈ M ⟹ η v ∈ M'"
  using graph by (auto simp: PiE_iff)

lemma hom_zero: "η 𝟬⇩M = 𝟬⇩2"
proof -
  have "η 𝟬⇩M = η (𝟬 ⊙ 𝟬⇩M)" using source.scale_zero_scalar by simp
  also have "… = 𝟬⇩2"
    by (simp add: hom_scale target.scale_zero_scalar)
  finally show ?thesis .
qed

lemma hom_neg:
  assumes v: "v ∈ M" shows "η (source.madd.inverse v) = target.madd.inverse (η v)"
proof -
  define n where "n = source.additive.inverse 𝟭"
  ― ‹The module negation is scaling by the ring's additive inverse of @{term 𝟭}.›
  have sneg: "source.madd.inverse v = n ⊙ v"
    unfolding n_def using v by (simp add: source.scale_neg_scalar source.scale_one)
  have tneg: "target.madd.inverse (η v) = n ⊙⇩2 η v"
    unfolding n_def using hom_closed[OF v] by (simp add: target.scale_neg_scalar target.scale_one)
  show ?thesis
    by (simp add: hom_scale n_def sneg tneg v)
qed

text ‹A module homomorphism commutes with finite linear combinations.  The target sum remains
  indexed by the source vectors; reindexing it over their images additionally requires injectivity
  on the chosen index set.›

lemma hom_lincomb:
  assumes finA: "finite A" and AM: "A ⊆ M"
    and c: "⋀v. v ∈ A ⟹ c v ∈ R"
  shows "η (source.lincomb c A) =
    target.madd.fincomp (λv. c v ⊙⇩2 η v) A"
  using finA AM c
proof (induction A rule: finite_induct)
  case empty
  then show ?case unfolding source.lincomb_def by (simp add: hom_zero)
next
  case (insert v A)
  have vM: "v ∈ M" and AM: "A ⊆ M" and cv: "c v ∈ R"
    using insert.prems by auto
  have cA: "⋀u. u ∈ A ⟹ c u ∈ R" using insert.prems by auto
  have source_terms: "(λu. c u ⊙ u) ∈ A → M"
    using AM cA by (auto intro!: source.scale_closed)
  have target_terms: "(λu. c u ⊙⇩2 η u) ∈ A → M'"
    using AM cA
    by (auto intro!: target.scale_closed hom_closed)
  have "source.lincomb c (insert v A) = (c v ⊙ v) ⊕ source.lincomb c A"
    unfolding source.lincomb_def
    using insert.hyps source_terms cv vM by (simp add: source.scale_closed)
  then have "η (source.lincomb c (insert v A)) =
      η (c v ⊙ v) ⊕⇩2 η (source.lincomb c A)"
    using cv vM AM cA
    by (simp add: hom_add source.scale_closed source.lincomb_closed)
  also have "η (c v ⊙ v) = c v ⊙⇩2 η v" using cv vM by (rule hom_scale)
  also have "η (source.lincomb c A) =
      target.madd.fincomp (λu. c u ⊙⇩2 η u) A"
    using insert.IH[OF AM cA] .
  also have "(c v ⊙⇩2 η v) ⊕⇩2
      target.madd.fincomp (λu. c u ⊙⇩2 η u) A =
      target.madd.fincomp (λu. c u ⊙⇩2 η u) (insert v A)"
    using insert.hyps target_terms cv vM
    by (auto intro!: target.madd.fincomp_insert[symmetric] target.scale_closed hom_closed)
  finally show ?case .
qed

subsection ‹Composition and inverses›

text ‹Composition is restricted to the source carrier, preserving the extensional-map
  convention used throughout the set-based algebra hierarchy.›
theorem compose_module_homomorphism:
  assumes second_hom: "module_homomorphism R (+) (⋅) 𝟬 𝟭
    M' (⊕⇩2) 𝟬⇩2 (⊙⇩2) N nadd nzero nscale θ"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
    M (⊕) 𝟬⇩M (⊙) N nadd nzero nscale (compose M θ η)"
proof -
  interpret second: module_homomorphism R "(+)" "(⋅)" 𝟬 𝟭
    M' "(⊕⇩2)" "𝟬⇩2" "(⊙⇩2)" N nadd nzero nscale θ
    by (rule second_hom)
  show ?thesis
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙)"
      by (rule source.Module_axioms)
    show "Module R (+) (⋅) 𝟬 𝟭 nadd nzero N nscale"
      by (rule second.target.Module_axioms)
    show "compose M θ η ∈ M →⇩E N"
      using graph second.graph by (auto simp: PiE_iff compose_def)
  next
    fix u v assume uv: "u ∈ M" "v ∈ M"
      then show "compose M θ η (u ⊕ v) =
        nadd (compose M θ η u) (compose M θ η v)"
      by (simp add: compose_def hom_add second.hom_add hom_closed)
  next
    fix a v assume av: "a ∈ R" "v ∈ M"
    then show "compose M θ η (a ⊙ v) =
        nscale a (compose M θ η v)"
      by (simp add: compose_def hom_scale second.hom_scale hom_closed source.scale_closed)
  qed
qed

text ‹The inverse of a bijective homomorphism is again restricted to its source carrier.
  This is essential: a raw ‹inv_into› does not satisfy the repository's extensional-map
  convention away from the carrier.›
theorem inverse_module_homomorphism:
  assumes bij: "bij_betw η M M'"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
    M' (⊕⇩2) 𝟬⇩2 (⊙⇩2)
    M (⊕) 𝟬⇩M (⊙) (restrict (inv_into M η) M')"
proof -
  interpret iso: bijective_map η M M'
    by unfold_locales (rule bij)
  show ?thesis
  proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
    show "Module R (+) (⋅) 𝟬 𝟭 (⊕⇩2) 𝟬⇩2 M' (⊙⇩2)"
      by (rule target.Module_axioms)
    show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙)"
      by (rule source.Module_axioms)
    show "restrict (inv_into M η) M' ∈ M' →⇩E M"
      by (rule iso.inverse.graph)
  next
    fix x y assume xy: "x ∈ M'" "y ∈ M'"
    then obtain u v where uv: "u ∈ M" "v ∈ M" "η u = x" "η v = y"
      using bij_betw_imp_surj_on[OF bij] by blast
    then show "restrict (inv_into M η) M' (x ⊕⇩2 y) =
        restrict (inv_into M η) M' x ⊕ restrict (inv_into M η) M' y"
      using xy bij by (auto simp: inv_into_f_eq hom_add)
  next
    fix a x assume ax: "a ∈ R" "x ∈ M'"
    then obtain v where v: "v ∈ M" "η v = x"
      using bij_betw_imp_surj_on[OF bij] by blast
    have av: "a ⊙ v ∈ M" using ax(1) v(1) by (rule source.scale_closed)
    have image: "η (a ⊙ v) = a ⊙⇩2 x"
      using ax v by (simp add: hom_scale)
    have inverse_image: "inv_into M η (a ⊙⇩2 x) = a ⊙ v"
      using bij av image by (metis bij_betw_inv_into_left)
    have inverse_x: "inv_into M η x = v"
      using bij v by (metis bij_betw_inv_into_left)
    have target_ax: "a ⊙⇩2 x ∈ M'"
      using ax by (rule target.scale_closed)
    show "restrict (inv_into M η) M' (a ⊙⇩2 x) =
        a ⊙ restrict (inv_into M η) M' x"
      using ax inverse_image inverse_x target_ax by simp
  qed
qed

lemma inverse_module_homomorphism_left:
  assumes bij: "bij_betw η M M'" and x: "x ∈ M"
  shows "restrict (inv_into M η) M' (η x) = x"
  using bij x hom_closed by (simp add: bij_betw_inv_into_left)

lemma inverse_module_homomorphism_right:
  assumes bij: "bij_betw η M M'" and y: "y ∈ M'"
  shows "η (restrict (inv_into M η) M' y) = y"
  using bij y by (simp add: bij_betw_inv_into_right)

corollary inverse_module_isomorphism:
  assumes bij: "bij_betw η M M'"
  shows "module_homomorphism R (+) (⋅) 𝟬 𝟭
      M' (⊕⇩2) 𝟬⇩2 (⊙⇩2)
      M (⊕) 𝟬⇩M (⊙) (restrict (inv_into M η) M')
    ∧ bij_betw (restrict (inv_into M η) M') M' M"
  using bij inverse_module_homomorphism by (simp add: bij_betw_inv_into)

subsection ‹The kernel›

definition Ker :: "'b set"
  where "Ker = {v ∈ M. η v = 𝟬⇩2}"

lemma Ker_subset: "Ker ⊆ M"
  by (auto simp: Ker_def)

lemma Ker_mem: "v ∈ Ker ⟹ v ∈ M" 
  by (simp add: Ker_def)

lemma Ker_image: "v ∈ Ker ⟹ η v = 𝟬⇩2" 
  by (simp add: Ker_def)

lemma Ker_memI: "⟦ η v = 𝟬⇩2; v ∈ M ⟧ ⟹ v ∈ Ker" 
  by (simp add: Ker_def)

text ‹The kernel is a submodule of the source.›
theorem Ker_submodule: "source.submodule Ker"
proof (intro source.submoduleI Ker_subset)
  show "𝟬⇩M ∈ Ker" by (simp add: Ker_def hom_zero)
next
  fix u v assume u: "u ∈ Ker" and v: "v ∈ Ker"
  have uM: "u ∈ M" and vM: "v ∈ M" using u v by (auto simp: Ker_def)
  show "u ⊕ v ∈ Ker"
    by (simp add: Ker_image Ker_memI hom_add u uM v vM) 
next
  show "⋀a v. ⟦a ∈ R; v ∈ Ker⟧ ⟹ a ⊙ v ∈ Ker"
    using Ker_def hom_scale source.scale_closed target.scale_zero_elem by auto
qed

subsection ‹The image›

text ‹The image of @{term η} is a submodule of the target.›
theorem image_submodule: "target.submodule (η ` M)"
proof (rule target.submoduleI)
  show "⋀u v. ⟦u ∈ η ` M; v ∈ η ` M⟧ ⟹ u ⊕⇩2 v ∈ η ` M"
    by (smt (verit, ccfv_threshold) hom_add image_iff source.madd_closed)
  show "⋀a v. ⟦a ∈ R; v ∈ η ` M⟧ ⟹ a ⊙⇩2 v ∈ η ` M"
    by (metis hom_scale imageE image_subset_iff source.scale_closed subset_refl) 
qed (use hom_closed hom_zero in blast)+

subsection ‹Injectivity criterion›

text ‹A module homomorphism is injective iff its kernel is trivial.›
theorem injective_iff_kernel_trivial:
  "inj_on η M ⟷ Ker = {𝟬⇩M}"
proof
  assume inj: "inj_on η M"
  show "Ker = {𝟬⇩M}"
    using hom_zero inj inj_on_contraD by (fastforce simp: Ker_def hom_zero)
next
  assume ker: "Ker = {𝟬⇩M}"
  show "inj_on η M"
  proof (rule inj_onI)
    fix x y assume xy: "x ∈ M" "y ∈ M" and eq: "η x = η y"
    have diff: "x ⊕ source.madd.inverse y ∈ M" using xy by auto
    have "η (x ⊕ source.madd.inverse y) = η x ⊕⇩2 η (source.madd.inverse y)"
      using xy by (simp add: hom_add)
    also have "… = 𝟬⇩2"
      using xy eq by (simp add: hom_neg)
    finally have z: "x ⊕ source.madd.inverse y = 𝟬⇩M"
      using Ker_memI diff ker by blast 
    ― ‹Cancel: ‹x ⊕ (- y) = 𝟬⇩M› forces @{term "x = y"}.›
    have "source.madd.inverse y ⊕ y = 𝟬⇩M"
      using xy(2) by (simp add: source.madd.invertible_left_inverse)
    then show "x = y"
      using source.madd.inverse_unique xy z by blast 
  qed
qed

end

context Module
begin

text ‹The carrier-restricted identity is the identity morphism in the extensional-map
  representation.›
theorem identity_module_homomorphism:
  "module_homomorphism R (+) (⋅) 𝟬 𝟭
    M (⊕) 𝟬⇩M (⊙) M (⊕) 𝟬⇩M (⊙) (identity M)"
proof (intro module_homomorphism.intro map.intro module_homomorphism_axioms.intro)
  show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙)"
    by (rule Module_axioms)
  show "Module R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩M M (⊙)"
    by (rule Module_axioms)
  show "identity M ∈ M →⇩E M" by simp
next
  fix u v assume "u ∈ M" "v ∈ M"
  then show "identity M (u ⊕ v) = identity M u ⊕ identity M v"
    by (simp add: madd_closed)
next
  fix a v assume "a ∈ R" "v ∈ M"
  then show "identity M (a ⊙ v) = a ⊙ identity M v"
    by (simp add: scale_closed)
qed

end

end