Theory Finitely_Generated_Abelian_Groups.Group_Hom

(*
    File:     Group_Hom.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Group Homomorphisms›

theory Group_Hom
  imports Set_Multiplication
begin

text ‹This section extends the already existing library about group homomorphisms in HOL-Algebra by
some useful lemmas. These were mainly inspired by the needs that arised throughout the other proofs.›

lemma (in group_hom) generate_hom:
  assumes "A ⊆ carrier G"
  shows "h ` (generate G A) = generate H (h ` A)"
  using assms group_hom.generate_img group_hom_axioms by blast

text ‹For two elements with the same image we can find an element in the kernel that maps one of the
two elements on the other by multiplication.›

lemma (in group_hom) kernel_assoc_elem:
  assumes "x ∈ carrier G" "y ∈ carrier G" "h x = h y"
  obtains z where "x = y ⊗⇘G⇙ z" "z ∈ kernel G H h"
proof -
  have c: "inv y ⊗⇘G⇙ x ∈ carrier G" using assms by simp
  then have e: "x = y ⊗⇘G⇙ (inv y ⊗⇘G⇙ x)" using assms G.m_assoc
    using G.inv_solve_left by blast
  then have "h x = h (y ⊗⇘G⇙ (inv y ⊗⇘G⇙ x))" by simp
  then have "h x = h y ⊗⇘H⇙ h (inv y ⊗⇘G⇙ x)" using c assms by simp
  then have "𝟭⇘H⇙ = h (inv y ⊗⇘G⇙ x)" using assms by simp
  then have "(inv y ⊗⇘G⇙ x) ∈ kernel G H h" unfolding kernel_def using c by simp
  thus ?thesis using e that by blast
qed

text ‹This can then be used to characterize the pre-image of a set $A$ under homomorphism as a
product of $A$ itself with the kernel of the homomorphism.›

lemma (in group_hom) vimage_eq_set_mult_kern_right:
  assumes "A ⊆ carrier G"
  shows "{x ∈ carrier G. h x ∈ h ` A} = A <#> kernel G H h"
proof(intro equalityI subsetI)
  fix x
  assume assm: "x ∈ A <#> kernel G H h"
  then have xc: "x ∈ carrier G" unfolding kernel_def set_mult_def using assms by blast
  from assm obtain a b where ab: "a ∈ A" "b ∈ kernel G H h" "x = a ⊗⇘G⇙ b"
    unfolding set_mult_def by blast
  then have abc: "a ∈ carrier G" "b ∈ carrier G" unfolding kernel_def using assms by auto
  from ab have "h x = h (a ⊗⇘G⇙ b)" by blast
  also have "… = h a ⊗⇘H⇙ h b" using abc by simp
  also have "… = h a ⊗⇘H⇙ 𝟭⇘H⇙" using ab(2) unfolding kernel_def by simp
  also have "… = h a" using abc by simp
  also have "… ∈ h ` A" using ab by blast 
  finally have "h x ∈ h ` A" .
  thus "x ∈ {x ∈ carrier G. h x ∈ h ` A}" using xc by blast
next
  fix x
  assume "x ∈ {x ∈ carrier G. h x ∈ h ` A}"
  then have x: "x ∈ carrier G" "h x ∈ h ` A" by simp+
  then obtain y where y: "y ∈ A" "h x = h y" "y ∈ carrier G" using assms by auto
  with kernel_assoc_elem obtain z where "x = y ⊗⇘G⇙ z" "z ∈ kernel G H h" using x by metis
  thus "x ∈ A <#> kernel G H h" unfolding set_mult_def using y by blast
qed

lemma (in group_hom) vimage_subset_generate_kern:
  assumes "A ⊆ carrier G"
  shows "{x ∈ carrier G. h x ∈ h ` A} ⊆ generate G (A ∪ kernel G H h)"
  using vimage_eq_set_mult_kern_right[of A] G.set_mult_subset_generate[of "A" "kernel G H h"] assms
  unfolding kernel_def by blast

text ‹The preimage of a subgroup under a homomorphism is also a subgroup.›

lemma (in group_hom) subgroup_vimage_is_subgroup:
  assumes "subgroup I H"
  shows "subgroup {x ∈ carrier G. h x ∈ I} G" (is "subgroup ?J G")
proof
  show "?J ⊆ carrier G" by blast
  show "𝟭 ∈ ?J" using subgroup.one_closed[of I H] assms by simp
  fix x
  assume x: "x ∈ ?J"
  then have hx: "h x ∈ I" by blast
  show "inv x ∈ ?J"
  proof -
    from hx have "inv⇘H⇙ (h x) ∈ I" using subgroup.m_inv_closed assms by fast
    moreover have "inv x ∈ carrier G" using x by simp
    moreover have "inv⇘H⇙ (h x) = h (inv x)" using x by auto
    ultimately show "inv x ∈ ?J" by simp
  qed
  fix y
  assume y: "y ∈ ?J"
  then have hy: "h y ∈ I" by blast
  show "x ⊗ y ∈ {x ∈ carrier G. h x ∈ I}"
  proof -
    have "h (x ⊗ y) = h x ⊗⇘H⇙ h y" using x y by simp
    also have "… ∈ I" using hx hy assms subgroup.m_closed by fast
    finally have "h (x ⊗ y) ∈ I" .
    moreover have "x ⊗ y ∈ carrier G" using x y by simp
    ultimately show ?thesis by blast
  qed
qed

lemma (in group_hom) iso_kernel:
  assumes "h ∈ iso G H"
  shows "kernel G H h = {𝟭⇘G⇙}"
  unfolding kernel_def using assms
  using hom_one iso_iff by blast

✐‹contributor ‹Paulo Emílio de Vilhena›› (* adapted by Joseph Thommes *)
lemma (in group_hom) induced_group_hom_same_group: 
  assumes "subgroup I G"
  shows "group_hom (G ⦇ carrier := I ⦈) H h"
proof -
  have "h ∈ hom (G ⦇ carrier := I ⦈) H"
    using homh subgroup.mem_carrier[OF assms] unfolding hom_def by auto
  thus ?thesis
    unfolding group_hom_def group_hom_axioms_def
    using subgroup.subgroup_is_group[OF assms G.is_group] by simp
qed

text ‹The order of an element under a homomorphism divides the order of the element.›

lemma (in group_hom) hom_ord_dvd_ord:
  assumes "a ∈ carrier G"
  shows "H.ord (h a) dvd G.ord a"
proof -
  have "h a [^]⇘H⇙ (G.ord a) = h (a [^]⇘G⇙ G.ord a)"
    using assms local.hom_nat_pow by presburger
  also have "… = h (𝟭⇘G⇙)" using G.pow_ord_eq_1 assms by simp
  also have "… = 𝟭⇘H⇙" by simp
  finally have "h a [^]⇘H⇙ G.ord a = 𝟭⇘H⇙" .
  then show ?thesis using pow_eq_id assms by simp
qed

text ‹In particular, this implies that the image of an element with a finite order also will have a
finite order.›

lemma (in group_hom) finite_ord_stays_finite:
  assumes "a ∈ carrier G" "G.ord a ≠ 0"
  shows "H.ord (h a) ≠ 0"
  using hom_ord_dvd_ord assms by fastforce

text ‹For injective homomorphisms, the order stays the same.›

lemma (in group_hom) inj_imp_ord_eq:
  assumes "a ∈ carrier G" "inj_on h (carrier G)" "G.ord a ≠ 0"
  shows "H.ord (h a) = G.ord a"
proof (rule antisym)
  show "H.ord (h a) ≤ G.ord a" using hom_ord_dvd_ord assms by force
  show "G.ord a ≤ H.ord (h a)"
  proof -
    have "𝟭⇘H⇙ = h (a [^]⇘G⇙ H.ord(h a))" using H.pow_ord_eq_1 assms
      by (simp add: local.hom_nat_pow)
    then have "a [^]⇘G⇙ H.ord (h a) = 𝟭⇘G⇙" using assms inj_on_one_iff by simp
    then have "G.ord a dvd H.ord (h a)" using G.pow_eq_id assms(1) by blast
    thus ?thesis using assms finite_ord_stays_finite by fastforce
  qed
qed

lemma (in group_hom) one_in_kernel:
  "𝟭 ∈ kernel G H h"
  using subgroup.one_closed subgroup_kernel by blast

lemma hom_in_carr:
  assumes "f ∈ hom G H"
  shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H"
  using assms unfolding hom_def bij_betw_def by blast

lemma iso_in_carr:
  assumes "f ∈ iso G H"
  shows "⋀x. x ∈ carrier G ⟹ f x ∈ carrier H"
  using assms unfolding iso_def bij_betw_def by blast

lemma triv_iso:
  assumes "group G" "group H" "carrier G = {𝟭⇘G⇙}" "carrier H = {𝟭⇘H⇙}"
  shows "G ≅ H"
proof(unfold is_iso_def iso_def)
  interpret G: group G by fact
  interpret H: group H by fact
  let ?f = "λ_. 𝟭⇘H⇙"
  have "?f ∈ hom G H" by (intro homI, auto)
  moreover have "bij_betw ?f (carrier G) (carrier H)" unfolding bij_betw_def
    using assms(3, 4) by auto
  ultimately show "{h ∈ hom G H. bij_betw h (carrier G) (carrier H)} ≠ {}" by blast
qed

text ‹The cardinality of the image of a group homomorphism times the cardinality of its kernel is
equal to the group order. This is basically another form of Lagrange's theorem.›

lemma (in group_hom) image_kernel_product: "card (h ` (carrier G)) * card (kernel G H h) = order G" 
proof -
  interpret G: group G by simp
  interpret H: group H by simp
  interpret ih: subgroup "h ` (carrier G)" H using img_is_subgroup by blast
  interpret ih: group "H⦇carrier := h ` (carrier G)⦈" using subgroup.subgroup_is_group by blast
  interpret h: group_hom G "H⦇carrier := h ` (carrier G)⦈"
    by (unfold_locales, unfold hom_def, auto)
  interpret k: subgroup "kernel G (H⦇carrier := h ` carrier G⦈) h" G using h.subgroup_kernel by blast
  from h.FactGroup_iso
  have "G Mod kernel G (H⦇carrier := h ` carrier G⦈) h ≅ H⦇carrier := h ` carrier G⦈" by auto
  hence "card (h ` (carrier G)) = order (G Mod kernel G (H⦇carrier := h ` carrier G⦈) h)"
    using iso_same_card unfolding order_def by fastforce
  moreover have "order (G Mod kernel G (H⦇carrier := h ` carrier G⦈) h)
                 * card (kernel G (H⦇carrier := h ` carrier G⦈) h) = order G"
    using G.lagrange[OF k.subgroup_axioms] unfolding order_def FactGroup_def by force
  moreover have "kernel G (H⦇carrier := h ` carrier G⦈) h = kernel G H h"
    unfolding kernel_def by auto
  ultimately show ?thesis by argo
qed

end