Theory Group_ZF_5

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2013-2022 Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

section ‹Groups 5›

theory Group_ZF_5 imports Group_ZF_4 Ring_ZF Semigroup_ZF

begin

text‹In this theory we study group homomorphisms.›

subsection‹Homomorphisms›

text‹A homomorphism is a function between groups that preserves the group operations.›

text‹In general we may have a homomorphism not only between groups, but also between various 
  algebraic structures with one operation like magmas, semigroups, quasigroups, loops and monoids. 
  In all cases the homomorphism is defined by using the morphism property. In the 
  multiplicative notation we we will write that $f$ has a morphism property if 
  $f(x\cdot_G y) = f(x)\cdot_H f(y)$ for all $x,y\in G$. Below we write this definition 
  in raw set theory notation and use the expression ‹IsMorphism› instead of the possible, but longer
  ‹HasMorphismProperty›. ›

definition 
  "IsMorphism(G,P,F,f) ≡ ∀g1∈G. ∀g2∈G. f`(P`⟨g1,g2⟩) = F`⟨f`(g1),f`(g2)⟩"

text‹A function $f:G\rightarrow H$ between algebraic structures 
  $(G,\cdot_G)$ and $(H,\cdot_H)$ with one operation (each) is a homomorphism is it has the morphism
  property. › 

definition
  "Homomor(f,G,P,H,F) ≡ f:G→H ∧ IsMorphism(G,P,F,f)"

text‹Now a lemma about the definition:›

lemma homomor_eq:
  assumes "Homomor(f,G,P,H,F)" "g1∈G" "g2∈G"
  shows "f`(P`⟨g1,g2⟩) = F`⟨f`(g1),f`(g2)⟩"
  using assms unfolding Homomor_def IsMorphism_def by auto

text‹An endomorphism is a homomorphism from a group to the same group. In case
the group is abelian, it has a nice structure.›

definition
  "End(G,P) ≡ {f∈G→G. Homomor(f,G,P,G,P)}"

text‹The defining property of an endomorphism written in notation used in ‹group0› context:›

lemma (in group0) endomor_eq: assumes "f ∈ End(G,P)" "g1∈G" "g2∈G"
  shows "f`(g1⋅g2) = f`(g1)⋅f`(g2)"
  using assms homomor_eq unfolding End_def by auto

text‹A function that maps a group $G$ into itself and satisfies 
  $f(g_1\cdot g2) = f(g_1)\cdot f(g_2)$ is an endomorphism.›

lemma (in group0) eq_endomor: 
  assumes "f:G→G" and "∀g1∈G. ∀g2∈G. f`(g1⋅g2)=f`(g1)⋅f`(g2)"
  shows "f ∈ End(G,P)"
  using assms  unfolding End_def Homomor_def IsMorphism_def by simp

text‹The set of endomorphisms forms a submonoid of the monoid of function
from a set to that set under composition.›

lemma (in group0) end_composition:
  assumes "f1∈End(G,P)" "f2∈End(G,P)"
  shows "Composition(G)`⟨f1,f2⟩ ∈ End(G,P)"
proof-
  from assms have fun: "f1:G→G" "f2:G→G" unfolding End_def by auto
  then have "f1 O f2:G→G" using comp_fun by auto
  from assms fun(2) have 
    "∀g1∈G. ∀g2∈G. (f1 O f2)`(g1⋅g2) = ((f1 O f2)`(g1))⋅((f1 O f2)`(g2))"
    using group_op_closed comp_fun_apply endomor_eq apply_type 
    by simp    
  with fun ‹f1 O f2:G→G› show ?thesis using eq_endomor func_ZF_5_L2 
    by simp
qed

text‹We will use some binary operations that are naturally defined on the function space 
   $G\rightarrow G$, but we consider them restricted to the endomorphisms of $G$.
  To shorten the notation in such case we define an abbreviation ‹InEnd(F,G,P)› 
  which restricts a binary operation $F$ to the set of endomorphisms of $G$. ›

abbreviation InEnd("_ {in End} [_,_]")
  where "InEnd(F,G,P) ≡ restrict(F,End(G,P)×End(G,P))"

text‹Endomoprhisms of a group form a monoid with composition as the binary operation,
  with the identity map as the neutral element.›

theorem (in group0) end_comp_monoid:
  shows "IsAmonoid(End(G,P),InEnd(Composition(G),G,P))"
  and "TheNeutralElement(End(G,P),InEnd(Composition(G),G,P)) = id(G)"
proof -
  let ?C0 = "InEnd(Composition(G),G,P)"
  have fun: "id(G):G→G" unfolding id_def by auto
  { fix g h assume "g∈G""h∈G"
    then have "id(G)`(g⋅h)=(id(G)`g)⋅(id(G)`h)"
      using group_op_closed by simp
  } 
  with groupAssum fun have "id(G) ∈ End(G,P)" using eq_endomor by simp 
  moreover  have A0: "id(G)=TheNeutralElement(G → G, Composition(G))" 
    using Group_ZF_2_5_L2(2) by auto 
  ultimately have A1: "TheNeutralElement(G → G, Composition(G)) ∈ End(G,P)" by auto 
  moreover have A2: "End(G,P) ⊆ G→G" unfolding End_def by blast 
  moreover have A3: "End(G,P) {is closed under} Composition(G)" 
    using end_composition unfolding IsOpClosed_def by blast
  ultimately show "IsAmonoid(End(G,P),?C0)" 
    using monoid0.group0_1_T1 Group_ZF_2_5_L2(1) unfolding monoid0_def
    by blast
  have "IsAmonoid(G→G,Composition(G))" using Group_ZF_2_5_L2(1) by auto
  with A0 A1 A2 A3 show "TheNeutralElement(End(G,P),?C0) = id(G)"
    using group0_1_L6 by auto
qed

text‹The set of endomorphisms is closed under pointwise addition (derived from the group operation).
   This is so because the group is abelian.›
  
theorem (in abelian_group) end_pointwise_addition:
  assumes "f∈End(G,P)" "g∈End(G,P)" "F = P {lifted to function space over} G"
  shows "F`⟨f,g⟩ ∈ End(G,P)"
proof-
  from assms(1,2) have fun: "f:G→G" "g∈G→G" unfolding End_def by simp_all
  with assms(3) have fun2: "F`⟨f,g⟩:G→G" 
    using monoid0.Group_ZF_2_1_L0 group0_2_L1 by simp
  { fix g1 g2 assume "g1∈G" "g2∈G"
    with isAbelian assms fun have 
      "(F`⟨f,g⟩)`(g1⋅g2) = (F`⟨f,g⟩)`(g1)⋅(F`⟨f,g⟩)`(g2)"
      using Group_ZF_2_1_L3 group_op_closed endomor_eq
        apply_type group0_4_L8(3) Group_ZF_2_1_L3 by simp
  } with fun2 show ?thesis using eq_endomor by simp
qed

text‹The value of a product of endomorphisms on a group element is the product of values.›

lemma (in abelian_group) end_pointwise_add_val:
  assumes "f∈End(G,P)" "g∈End(G,P)" "x∈G" "F = P {lifted to function space over} G"
  shows "(InEnd(F,G,P)`⟨f,g⟩)`(x) = (f`(x))⋅(g`(x))"
  using assms group_oper_fun monoid.group0_1_L3B func_ZF_1_L4 
  unfolding End_def by simp

text‹The inverse of an abelian group is an endomorphism.›

lemma (in abelian_group) end_inverse_group:
  shows "GroupInv(G,P) ∈ End(G,P)"
  using inverse_in_group group_inv_of_two isAbelian IsCommutative_def 
    group0_2_T2 groupAssum Homomor_def 
  unfolding End_def IsMorphism_def by simp

text‹The set of homomorphisms of an abelian group is an abelian subgroup of
  the group of functions from a set to a group, under pointwise addition.›

theorem (in abelian_group) end_addition_group:
  assumes "F = P {lifted to function space over} G"
  shows "IsAgroup(End(G,P),InEnd(F,G,P))" and
    "InEnd(F,G,P) {is commutative on} End(G,P)"
proof-
  have "End(G,P)≠0" using end_comp_monoid(1) monoid0.group0_1_L3A 
    unfolding monoid0_def by auto
  moreover have "End(G,P) ⊆ G→G" unfolding End_def by auto 
  moreover from isAbelian assms(1) have "End(G,P){is closed under} F" 
    unfolding IsOpClosed_def using end_pointwise_addition by auto 
  moreover from groupAssum assms(1) have 
    "∀f∈End(G,P). GroupInv(G→G,F)`(f) ∈ End(G,P)"
    using monoid0.group0_1_L1 end_composition(1) end_inverse_group 
      func_ZF_5_L2 group0_2_T2 Group_ZF_2_1_L6 
    unfolding monoid0_def End_def by force
  ultimately show "IsAgroup(End(G,P),InEnd(F,G,P))" 
    using assms(1) group0.group0_3_T3 Group_ZF_2_1_T2 
    unfolding IsAsubgroup_def group0_def by blast
  from assms(1) isAbelian show 
    "InEnd(F,G,P) {is commutative on} End(G,P)" 
    using Group_ZF_2_1_L7 unfolding End_def IsCommutative_def by auto
qed

text‹Endomorphisms form a subgroup of the space of functions that map the group to itself.›

lemma (in abelian_group) end_addition_subgroup:
  shows "IsAsubgroup(End(G,P),P {lifted to function space over} G)"
  using end_addition_group unfolding IsAsubgroup_def by simp

text‹The neutral element of the group of endomorphisms of a group is the constant function 
  with value equal to the neutral element of the group.›

lemma (in abelian_group) end_add_neut_elem:
  assumes "F = P {lifted to function space over} G"
  shows "TheNeutralElement(End(G,P),InEnd(F,G,P)) = ConstantFunction(G,𝟭)"
  using assms end_addition_subgroup lift_group_subgr_neut by simp

text‹For the endomorphisms of a group $G$ the group operation lifted to the function space 
  over $G$ is distributive with respect to the composition operation. ›

lemma (in abelian_group) distributive_comp_pointwise:
  assumes "F = P {lifted to function space over} G"
  shows 
    "IsDistributive(End(G,P),InEnd(F,G,P),InEnd(Composition(G),G,P))"
proof -
  let ?CG = "Composition(G)"
  let ?CE = "InEnd(?CG,G,P)"
  let ?FE = "InEnd(F,G,P)"
  { fix b c d assume AS: "b∈End(G,P)" "c∈End(G,P)" "d∈End(G,P)"
    with assms(1) have ig1: "?CG `⟨b, F ` ⟨c, d⟩⟩ = b O (F`⟨c,d⟩)" 
      using monoid.Group_ZF_2_1_L0 func_ZF_5_L2 unfolding End_def 
      by auto
    with AS have ig2: "F`⟨?CG`⟨b,c⟩,?CG `⟨b,d⟩⟩ = F`⟨b O c,b O d⟩" 
      unfolding End_def using func_ZF_5_L2 by auto
    from assms(1) AS have comp1fun: "(b O (F`⟨c,d⟩)):G→G" 
      using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by force
    from assms(1) AS have comp2fun: "(F `⟨b O c,b O d⟩) : G→G" 
      using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by force
    { fix g assume "g∈G"
      with assms(1) AS(2,3) have "(b O (F`⟨c,d⟩))`(g) = b`((F`⟨c,d⟩)`(g))" 
        using comp_fun_apply monoid.Group_ZF_2_1_L0 unfolding End_def 
        by force
      with groupAssum assms(1) AS ‹g∈G› have 
        "(b O (F`⟨c,d⟩))`(g) = (F`⟨b O c,b O d⟩)`(g)"
        using Group_ZF_2_1_L3 apply_type homomor_eq comp_fun 
        unfolding End_def by auto
    } hence "∀g∈G. (b O (F`⟨c,d⟩))`(g) = (F`⟨b O c,b O d⟩)`(g)" by simp
    with comp1fun comp2fun ig1 ig2 have 
      "?CG`⟨b,F`⟨c, d⟩⟩ = F`⟨?CG`⟨b , c⟩,?CG`⟨b,d⟩⟩"
      using func_eq by simp
    moreover from AS(2,3) have "F`⟨c, d⟩ = ?FE`⟨c, d⟩" 
      using restrict by simp
    moreover from AS have "?CG`⟨b,c⟩ = ?CE`⟨b,c⟩" and "?CG`⟨b,d⟩ = ?CE`⟨b,d⟩"
      using restrict by auto 
    moreover from assms AS have "?CG`⟨b,F `⟨c,d⟩⟩ = ?CE`⟨b, F`⟨c, d⟩⟩"
      using end_pointwise_addition by simp
    moreover from AS have "F`⟨?CG`⟨b,c⟩,?CG`⟨b,d⟩⟩ = ?FE`⟨?CG `⟨b,c⟩,?CG `⟨b,d⟩⟩"
      using end_composition by simp
    ultimately have eq1: "?CE`⟨b, ?FE`⟨c,d⟩⟩ = ?FE `⟨?CE`⟨b,c⟩,?CE`⟨b,d⟩⟩"
      by simp
    from assms(1) AS have 
      compfun: "(F`⟨c,d⟩) O b : G→G" "F`⟨c O b,d O b⟩ : G→G" 
      using monoid.Group_ZF_2_1_L0 comp_fun unfolding End_def by auto
    { fix g assume "g∈G"
      with AS(1) have bg: "b`(g) ∈ G" unfolding End_def using apply_type 
        by auto
      from ‹g∈G› AS(1) have "((F`⟨c,d⟩) O b)`g = (F`⟨c,d⟩)`(b`(g))" 
        using comp_fun_apply  unfolding End_def by force
      also from assms(1) AS(2,3) bg have "… = (c`(b`(g)))⋅(d`(b`(g)))" 
        using Group_ZF_2_1_L3 unfolding End_def by auto
      also from ‹g∈G› AS have "… = ((c O b)`(g))⋅((d O b)`(g))" 
        using comp_fun_apply unfolding End_def by auto
      also from assms(1) ‹g∈G› AS have "… = (F`⟨c O b,d O b⟩)`g" 
        using comp_fun Group_ZF_2_1_L3 unfolding End_def by auto
      finally have "((F`⟨c,d⟩) O b)`(g) = (F`⟨c O b,d O b⟩)`(g)" by simp
    } hence "∀g∈G. ((F`⟨c,d⟩) O b)`(g) = (F`⟨c O b,d O b⟩)`(g)" by simp
    with compfun have "(F`⟨c,d⟩) O b = F`⟨c O b,d O b⟩" 
      using func_eq by blast
    with assms(1) AS have "?CG`⟨F`⟨c,d⟩,b⟩ = F`⟨?CG`⟨c,b⟩,?CG`⟨d , b⟩⟩"
      using monoid.Group_ZF_2_1_L0 func_ZF_5_L2 unfolding End_def 
      by simp
    moreover from AS(2,3) have "F`⟨c, d⟩ = ?FE`⟨c, d⟩" 
      using restrict by simp 
    moreover from AS have "?CG`⟨c,b⟩ = ?CE`⟨c , b⟩" "?CG`⟨d,b⟩ = ?CE`⟨d,b⟩"
      using restrict by auto 
    moreover from assms AS have "?CG`⟨F`⟨c,d⟩,b⟩ = ?CE`⟨F`⟨c,d⟩,b⟩" 
      using end_pointwise_addition by auto
    moreover from AS have "F`⟨?CG`⟨c,b⟩,?CG`⟨d,b⟩⟩ = ?FE`⟨?CG`⟨c,b⟩,?CG`⟨d,b⟩⟩"
      using end_composition by auto 
    ultimately have "?CE`⟨?FE`⟨c,d⟩,b⟩ = ?FE`⟨?CE`⟨c,b⟩,?CE`⟨d,b⟩⟩"
      by auto
    with eq1 have "(?CE`⟨b, ?FE`⟨c, d⟩⟩ = ?FE`⟨?CE`⟨b,c⟩,?CE`⟨b,d⟩⟩) ∧
      (?CE`⟨?FE`⟨c,d⟩,b⟩ = ?FE`⟨?CE`⟨c,b⟩,?CE`⟨d,b⟩⟩)"
      by auto
  } then show ?thesis unfolding IsDistributive_def by auto
qed

text‹The endomorphisms of an abelian group is in fact a ring with the previous
  operations.›

theorem (in abelian_group) end_is_ring:
  assumes "F = P {lifted to function space over} G"
  shows 
    "IsAring(End(G,P),InEnd(F,G,P),InEnd(Composition(G),G,P))"
  using assms end_addition_group end_comp_monoid(1) distributive_comp_pointwise
  unfolding IsAring_def by auto

text‹The theorems proven in the ‹ring0› context are valid in the ‹abelian_group› context
   as applied to the endomorphisms of $G$.  ›

sublocale abelian_group < endo_ring: ring0 
  "End(G,P)" 
  "InEnd(P {lifted to function space over} G,G,P)" 
  "InEnd(Composition(G),G,P)"
  "λx b. InEnd(P {lifted to function space over} G,G,P)`⟨x,b⟩" 
  "λx. GroupInv(End(G, P), InEnd(P {lifted to function space over} G,G,P))`(x)" 
  "λx b. InEnd(P {lifted to function space over} G,G,P)`⟨x, GroupInv(End(G, P), InEnd(P {lifted to function space over} G,G,P))`(b)⟩"
  "λx b. InEnd(Composition(G),G,P)`⟨x, b⟩"
  "TheNeutralElement(End(G, P),InEnd(P {lifted to function space over} G,G,P))"
  "TheNeutralElement(End(G, P),InEnd(Composition(G),G,P))"
  "InEnd(P {lifted to function space over} G,G,P)`
     ⟨TheNeutralElement (End(G, P), InEnd(Composition(G),G,P)),
      TheNeutralElement (End(G, P), InEnd(Composition(G),G,P))⟩"
  "λx. InEnd(Composition(G),G,P)`⟨x, x⟩"
  using end_is_ring unfolding ring0_def by blast

subsection‹First isomorphism theorem›

text‹Now we will prove that any homomorphism $f:G\to H$ defines a bijective
  homomorphism between $G/H$ and $f(G)$.›
  
text‹A group homomorphism sends the neutral element to the neutral element.›

lemma image_neutral:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
  shows "f`(TheNeutralElement(G,P)) = TheNeutralElement(H,F)"
proof -
  let ?eG = "TheNeutralElement(G,P)"
  let ?eH = "TheNeutralElement(H,F)"
  from assms(3) have ff: "f:G→H"
    unfolding Homomor_def by simp
  have g: "?eG = P`⟨?eG,?eG⟩" "?eG ∈ G"
    using assms(1) group0.group0_2_L2 unfolding group0_def by simp_all
  with assms have "f`(?eG) = F`⟨f`(?eG),f`(?eG)⟩"
    unfolding Homomor_def IsMorphism_def by force
  moreover
  from ff g(2) have h: "f`(?eG) ∈ H" using apply_type 
    by simp
  with assms(2) have "f`(?eG) = F`⟨f`(?eG),?eH⟩"
    using group0.group0_2_L2 unfolding group0_def by simp 
  ultimately have "F`⟨f`(?eG),?eH⟩ = F`⟨f`(?eG),f`(?eG)⟩" 
    by simp
  with assms(2) h have 
    "LeftTranslation(H,F,f`(?eG))`(?eH) = LeftTranslation(H,F,f`(?eG))`(f`(?eG))"
    using group0.group0_5_L2(2) group0.group0_2_L2 unfolding group0_def 
      by simp
  moreover from assms(2) h have "LeftTranslation(H,F,f`(?eG))∈inj(H,H)"
      using group0.trans_bij(2) unfolding group0_def bij_def
      by simp
  ultimately show ?thesis using h assms(2) group0.group0_2_L2 
    unfolding inj_def group0_def by force
qed

text‹If $f:G\rightarrow H$ is a homomorphism, then it commutes with the inverse ›

lemma image_inv:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" "g∈G"
  shows "f`(GroupInv(G,P)`(g)) = GroupInv(H,F)`(f`(g))"
proof -
  from assms(3) have ff: "f:G→H"
    unfolding Homomor_def by simp
  with assms(4) have im: "f`(g)∈H" using apply_type by simp
  from assms(1,4) have inv: "GroupInv(G,P)`(g)∈G" 
    using group0.inverse_in_group unfolding group0_def by simp
  with ff have inv2: "f`(GroupInv(G,P)`g)∈H" using apply_type by simp
  from assms(1,4) have 
    "f`(TheNeutralElement(G,P)) = f`(P`⟨g,GroupInv(G,P)`(g)⟩)" 
    using group0.group0_2_L6 unfolding group0_def by simp
  also from assms inv have "… = F`⟨f`(g),f`(GroupInv(G,P)`(g))⟩" 
    unfolding Homomor_def IsMorphism_def by simp
  finally have "f`(TheNeutralElement(G,P)) = F`⟨f`(g),f`(GroupInv(G,P)`(g))⟩"
    by simp
  with assms im inv2 show ?thesis 
    using group0.group0_2_L9 image_neutral unfolding group0_def by simp
qed

text‹The preimage of a subgroup is a subgroup›

theorem preimage_sub:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
          "IsAsubgroup(K,F)"
  shows "IsAsubgroup(f-``(K),P)"
proof -
  from assms(3) have ff: "f:G→H"
    unfolding Homomor_def by simp
  from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp
  from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp
  moreover 
  from assms ff Ggr Hgr have "TheNeutralElement(G,P) ∈ f-``(K)"
    using image_neutral group0.group0_3_L5 func1_1_L15 group0.group0_2_L2 
    by simp
  hence "f-``(K)≠0" by blast
  moreover from ff have "f-``(K) ⊆ G" using func1_1_L3 by simp
  moreover from assms ff Ggr Hgr have "f-``(K) {is closed under} P"
    using func1_1_L15 group0.group0_3_L6 group0.group_op_closed func1_1_L15
    unfolding IsOpClosed_def Homomor_def IsMorphism_def by simp
  moreover from assms ff Ggr Hgr have 
    "∀x∈f-``(K). GroupInv(G, P)`(x) ∈ f-``(K)"
    using group0.group0_3_T3A image_inv func1_1_L15 
        group0.inverse_in_group by simp
  ultimately show ?thesis by (rule group0.group0_3_T3)
qed

text‹The preimage of a normal subgroup is normal›

theorem preimage_normal_subgroup:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
          "IsAnormalSubgroup(H,F,K)"
        shows "IsAnormalSubgroup(G,P,f-``(K))"
proof -
  from assms(3) have ff: "f:G→H"
    unfolding Homomor_def by simp
  from assms(2) have Hgr: "group0(H,F)" unfolding group0_def by simp
  with assms(4) have "K⊆H" using group0.group0_3_L2 
    unfolding IsAnormalSubgroup_def by simp
  from assms(1) have Ggr: "group0(G,P)" unfolding group0_def by simp
  moreover from assms have "IsAsubgroup(f-``(K),P)" 
    using preimage_sub unfolding IsAnormalSubgroup_def by simp
  moreover
  { fix g assume gG: "g∈G"
    { fix h assume "h ∈ {P`⟨g,P`⟨h, GroupInv(G, P)`(g)⟩⟩. h ∈ f-``(K)}"
      then obtain k where 
        k: "h = P`⟨g,P`⟨k,GroupInv(G, P)`(g)⟩⟩" "k ∈ f-``(K)" 
        by auto
      from k(1) have "f`(h) = f`(P`⟨g,P`⟨k, GroupInv(G, P)`(g)⟩⟩)" by simp
      moreover from ff k(2) have "k∈G" using vimage_iff 
        unfolding Pi_def by blast
      ultimately have f: "f`(h) = F`⟨f`(g),F`⟨f`(k),GroupInv(H,F)`(f`(g))⟩⟩"
        using assms(1-4) Ggr gG group0.group_op_closed 
          group0.inverse_in_group image_inv homomor_eq by simp
      from assms(1) ff Ggr ‹g∈G› k have "h∈G" using group0.group_op_closed
        group0.inverse_in_group func1_1_L15 by simp
      from assms(4) ff k(2) ‹g∈G› have "f`(k)∈K" "f`(g)∈H" and 
        "F`⟨F`⟨f`(g),f`(k)⟩,GroupInv(H,F)`(f`(g))⟩ ∈ K"
        using func1_1_L15 apply_type unfolding IsAnormalSubgroup_def 
        by auto
      moreover from ‹f`(k)∈K› ‹K⊆H› Hgr f ‹f`(g)∈H› have
        "f`(h) = F`⟨F`⟨f`(g),f`(k)⟩,GroupInv(H,F)`(f`(g))⟩"
        using group0.group_oper_assoc group0.inverse_in_group by auto
      ultimately have "f`(h) ∈ K" by simp
      with ff ‹h∈G› have "h ∈ f-``(K)" using func1_1_L15 by simp
    } hence "{P`⟨g,P`⟨h,GroupInv(G,P)`(g)⟩⟩. h∈f-``(K)} ⊆ f-``(K)" 
      by blast
  } hence "∀g∈G. {P`⟨g, P`⟨h, GroupInv(G, P)`(g)⟩⟩. h∈f-``(K)} ⊆ f-``(K)" 
    by simp
  ultimately show ?thesis using group0.cont_conj_is_normal by simp 
qed        

text‹The kernel of an homomorphism is a normal subgroup.›

corollary kernel_normal_sub:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
  shows "IsAnormalSubgroup(G,P,f-``{TheNeutralElement(H,F)})"
  using assms preimage_normal_subgroup group0.trivial_normal_subgroup 
  unfolding group0_def by auto

text‹The image of a subgroup is a subgroup›

theorem image_subgroup:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" 
    "Homomor(f,G,P,H,F)" "f:G→H" "IsAsubgroup(K,P)"
  shows "IsAsubgroup(f``K,F)"
proof - 
  from assms(1,5) have sub: "K⊆G" using group0.group0_3_L2 
    unfolding group0_def by simp
  from assms(2) have "group0(H,F)" unfolding group0_def by simp
  moreover from assms(4) have "f``(K) ⊆ H" 
    using func_imagedef sub apply_type by auto
  moreover
  from assms(1,4,5) sub have "f`(TheNeutralElement(G,P)) ∈ f``(K)"
    using group0.group0_3_L5 func_imagedef unfolding group0_def 
    by auto
  hence "f``(K) ≠ 0" by blast
  moreover
  { fix x assume "x∈f``(K)"
    with assms(4) sub obtain q where q: "q∈K" "x=f`(q)" 
      using func_imagedef by auto
    with assms(1-4) sub have "GroupInv(H,F)`(x) = f`(GroupInv(G,P)`q)" 
      using image_inv by auto
    with assms(1,4,5) q(1) sub have "GroupInv(H,F)`(x) ∈ f``(K)" 
      using group0.group0_3_T3A func_imagedef unfolding group0_def 
      by auto
  } hence "∀x∈f``(K). GroupInv(H, F)`(x) ∈ f``(K)" by auto
  moreover 
  { fix x y assume "x∈f``(K)" "y∈f``(K)"
    with assms(4) sub obtain qx qy where 
      q: "qx∈K" "x=f`(qx)" "qy∈K" "y=f`(qy)" 
      using func_imagedef by auto
    with assms(1-3) sub have "F`⟨x,y⟩ = f`(P`⟨qx,qy⟩)" 
      using homomor_eq by force
    moreover from assms(1,5) q(1,3) have "P`⟨qx,qy⟩ ∈ K" 
      using group0.group0_3_L6 unfolding group0_def by simp
    ultimately have "F`⟨x,y⟩  ∈ f``(K)" 
      using assms(4) sub func_imagedef by auto
  } then have  "f``(K) {is closed under} F" unfolding IsOpClosed_def 
    by simp
  ultimately show ?thesis using group0.group0_3_T3 by simp
qed

text‹The image of a group under a homomorphism is a subgroup of the target group.›

corollary image_group:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)"
  shows "IsAsubgroup(f``(G),F)"
proof - 
  from assms(1) have "restrict(P,G×G) = P" 
    using group0.group_oper_fun restrict_domain unfolding group0_def 
    by blast
  with assms show ?thesis using image_subgroup 
    unfolding Homomor_def IsAsubgroup_def by simp
qed

text‹Now we are able to prove the first isomorphism theorem. This theorem states
  that any group homomorphism $f:G\to H$ gives an isomorphism between a quotient group of $G$
  and a subgroup of $H$.›

theorem isomorphism_first_theorem:
  assumes "IsAgroup(G,P)" "IsAgroup(H,F)" "Homomor(f,G,P,H,F)" 
  defines "r ≡ QuotientGroupRel(G,P,f-``{TheNeutralElement(H,F)})" and
  "𝒫 ≡ QuotientGroupOp(G,P,f-``{TheNeutralElement(H,F)})"
  shows "∃𝔣. Homomor(𝔣,G//r,𝒫,f``(G),restrict(F,(f``(G))×(f``(G)))) ∧ 𝔣∈bij(G//r,f``(G))"
proof-
  let ?𝔣 = "{⟨r``{g},f`(g)⟩. g∈G}"
  from assms(3) have ff: "f:G→H"
    unfolding Homomor_def by simp
  from assms(1-5) have "equiv(G,r)"
    using group0.Group_ZF_2_4_L3 kernel_normal_sub 
    unfolding group0_def IsAnormalSubgroup_def by simp
  from assms(4) ff have "?𝔣 ∈ Pow((G//r)×f``(G))" 
    unfolding quotient_def using func_imagedef by auto
  moreover have "(G//r) ⊆ domain(?𝔣)" unfolding domain_def quotient_def by auto 
  moreover
  { fix x y t assume A: "⟨x,y⟩ ∈ ?𝔣" "⟨x,t⟩ ∈ ?𝔣"
    then obtain gy gr where "⟨x, y⟩=⟨r``{gy},f`(gy)⟩" "⟨x, t⟩=⟨r``{gr},f`(gr)⟩" 
      and "gr∈G" "gy∈G" by auto
    hence B: "r``{gy}=r``{gr}" "y=f`(gy)" "t=f`(gr)" by auto
    from ff ‹gy∈G› ‹gr∈G› B(2,3) have "y∈H" "t∈H" 
      using apply_type by simp_all
    with ‹equiv(G,r)› ‹gr∈G› ‹r``{gy}=r``{gr}› have "⟨gy,gr⟩∈r" 
      using same_image_equiv by simp
    with assms(4) ff have 
      "f`(P`⟨gy,GroupInv(G,P)`(gr)⟩) = TheNeutralElement(H,F)"
      unfolding QuotientGroupRel_def using func1_1_L15 by simp
    with assms(1-4) B(2,3) ‹gy∈G› ‹gr∈G› ‹y∈H› ‹t∈H› have "y=t"
      using image_inv group0.inverse_in_group group0.group0_2_L11A 
      unfolding group0_def Homomor_def IsMorphism_def by auto
  } hence "∀x y. ⟨x,y⟩ ∈ ?𝔣 ⟶ (∀z. ⟨x,z⟩∈?𝔣 ⟶ y=z)" by auto
  ultimately have ff_fun: "?𝔣:G//r→f``(G)" unfolding Pi_def function_def 
    by auto
  { fix a1 a2 assume AS: "a1∈G//r" "a2∈G//r"
    then obtain g1 g2  where "g1∈G" "g2∈G" and a: "a1=r``{g1}" "a2=r``{g2}" 
      unfolding quotient_def by auto
    with assms ‹equiv(G,r)› have "⟨𝒫`⟨a1,a2⟩,f`(P`⟨g1,g2⟩)⟩ ∈ ?𝔣"
      using Group_ZF_2_4_L5A kernel_normal_sub group0.Group_ZF_2_2_L2 group0.group_op_closed
      unfolding QuotientGroupOp_def group0_def by auto       
    with ff_fun have eq: "?𝔣`(𝒫`⟨a1,a2⟩) = f`(P`⟨g1,g2⟩)" using apply_equality  
      by simp
    from ‹g1∈G› ‹g2∈G› a have "⟨a1,f`(g1)⟩ ∈ ?𝔣" and "⟨a2,f`(g2)⟩ ∈ ?𝔣" by auto
    with assms(1,2,3) ff_fun ‹g1∈G› ‹g2∈G› eq have "F`⟨?𝔣`(a1),?𝔣`(a2)⟩ = ?𝔣`(𝒫`⟨a1,a2⟩)"
      using apply_equality unfolding Homomor_def IsMorphism_def by simp
    moreover from AS ff_fun have "?𝔣`(a1) ∈ f``(G)" "?𝔣`(a2) ∈ f``(G)" 
      using apply_type by auto 
    ultimately have "restrict(F,f``(G)×f``(G))`⟨?𝔣`(a1),?𝔣`(a2)⟩ = ?𝔣`(𝒫`⟨a1,a2⟩)" 
      by simp
  } hence 
    r: "∀a1∈G//r. ∀a2∈G//r. restrict(F,f``(G)×f``(G))`⟨?𝔣`(a1),?𝔣`(a2)⟩ = ?𝔣`(𝒫`⟨a1,a2⟩)" 
    by simp
  with ff_fun have HOM: "Homomor(?𝔣,G//r,𝒫,f``(G),restrict(F,(f``(G))×(f``(G))))"
    unfolding Homomor_def IsMorphism_def by simp
  from assms have G: "IsAgroup(G//r,𝒫)" and 
      H: "IsAgroup(f``(G), restrict(F,f``(G)×f``(G)))"
        using Group_ZF_2_4_T1 kernel_normal_sub image_group 
        unfolding IsAsubgroup_def by simp_all
  { fix b1 b2 assume AS: "?𝔣`(b1) = ?𝔣`(b2)" "b1∈G//r" "b2∈G//r"
    from G AS(3) have invb2: "GroupInv(G//r,𝒫)`(b2)∈G//r" 
      using group0.inverse_in_group unfolding group0_def by simp
    with G AS(2) have I: "𝒫`⟨b1,GroupInv(G//r,𝒫)`(b2)⟩∈G//r"
      using group0.group_op_closed unfolding group0_def by auto
    then obtain g where "g∈G" and gg: "𝒫`⟨b1,GroupInv(G//r,𝒫)`(b2)⟩=r``{g}" 
      unfolding quotient_def by auto
    from ‹g∈G› have "⟨r``{g},f`(g)⟩ ∈ ?𝔣" by blast
    with ff_fun gg have E: "?𝔣`(𝒫`⟨b1,GroupInv(G//r,𝒫)`(b2)⟩) = f`(g)"
      using apply_equality by simp
    from ff_fun invb2 have pp: "?𝔣`(GroupInv(G//r,𝒫)`(b2))∈f``(G)" 
      using apply_type by simp
    from ff_fun AS(2,3) have fff: "?𝔣`(b1) ∈ f``(G)" "?𝔣`(b2) ∈ f``(G)" 
      using apply_type by simp_all
    from fff(1) pp have 
      EE: "F`⟨?𝔣`(b1),?𝔣`(GroupInv(G//r,𝒫)`(b2))⟩=
          restrict(F,f``(G)×f``(G))`⟨?𝔣`(b1),?𝔣`(GroupInv(G//r,𝒫)`(b2))⟩"
      by auto
    from ff have "f``(G) ⊆ H" using func1_1_L6(2) by simp
    with fff have "?𝔣`(b1)∈H" "?𝔣`(b2)∈H" by auto
    with assms(1-4) G H HOM ff_fun AS(1,3) fff(2) EE have
      "TheNeutralElement(H,F) = 
        restrict(F,f``(G)×f``(G))`⟨?𝔣`(b1),?𝔣`(GroupInv(G//r,𝒫)`(b2))⟩"
      using group0.group0_2_L6(1) restrict image_inv group0.group0_3_T1 image_group 
      unfolding group0_def by simp
    also from G H HOM AS(2,3) E have "… = f`(g)"
      using group0.inverse_in_group unfolding group0_def IsMorphism_def Homomor_def
      by simp
    finally have "TheNeutralElement(H,F) = f`(g)" by simp
    with ff ‹g∈G› have "g∈f-``{TheNeutralElement(H,F)}" using func1_1_L15 
      by simp
    with assms ‹g∈G› gg have 
      "𝒫`⟨b1,GroupInv(G//r,𝒫)`(b2)⟩ = TheNeutralElement(G//r,𝒫)"
      using group0.Group_ZF_2_4_L5E kernel_normal_sub unfolding group0_def 
      by simp
    with AS(2,3) G have "b1=b2" using group0.group0_2_L11A unfolding group0_def 
      by auto
  } with ff_fun have "?𝔣 ∈ inj(G//r,f``(G))" unfolding inj_def by blast 
  moreover
  { fix m assume "m ∈ f``(G)"
    with ff obtain g where "g∈G" "m=f`(g)" using func_imagedef by auto
    hence "⟨r``{g},m⟩ ∈ ?𝔣" by blast
    with ff_fun have "?𝔣`(r``{g})=m" using apply_equality by auto
    with ‹g∈G› have "∃A∈G//r. ?𝔣`(A) = m" unfolding quotient_def by auto
  }
  ultimately have "?𝔣 ∈ bij(G//r,f``G)" unfolding bij_def surj_def 
    using ff_fun by blast
  with HOM show ?thesis by blast
qed

text‹The inverse of a bijective homomorphism is an homomorphism.
  Meaning that in the previous result, the homomorphism we found is an isomorphism.›

theorem bij_homomor:
  assumes "f∈bij(G,H)" "IsAgroup(G,P)" "Homomor(f,G,P,H,F)"
  shows "Homomor(converse(f),H,F,G,P)"
proof -
  { fix h1 h2 assume "h1∈H" "h2∈H"
    with assms(1) obtain g1 g2 where 
      g1: "g1∈G" "f`(g1)=h1" and g2: "g2∈G" "f`(g2)=h2"
      unfolding bij_def surj_def by blast
    with assms(2,3) have  
      "converse(f)`(f`(P`⟨g1,g2⟩)) = converse(f)`(F`⟨h1,h2⟩)"
      using homomor_eq by simp
    with assms(1,2) g1 g2 have
      "P`⟨converse(f)`(h1),converse(f)`(h2)⟩ = converse(f)`(F`⟨h1,h2⟩)"
      using left_inverse group0.group_op_closed unfolding group0_def bij_def
      by auto
  } with assms(1) show ?thesis using bij_converse_bij bij_is_fun 
    unfolding Homomor_def IsMorphism_def by simp
qed

text‹A very important homomorphism is given by taking every element
  to its class in a group quotient. Recall that $\lambda x\in X. p(x)$
  is an alternative notation for function defined as a set of pairs,
  see lemma ‹lambda_fun_alt› in theory ‹func1.thy›.›

lemma (in group0) quotient_map:
  assumes "IsAnormalSubgroup(G,P,H)"
  defines "r ≡ QuotientGroupRel(G,P,H)" and "q ≡ λx∈G. QuotientGroupRel(G,P,H)``{x}"
  shows "Homomor(q,G,P,G//r,QuotientGroupOp(G,P,H))"
  using groupAssum assms group_op_closed lam_funtype lamE EquivClass_1_L10 
    Group_ZF_2_4_L3 Group_ZF_2_4_L5A  Group_ZF_2_4_T1
  unfolding IsAnormalSubgroup_def QuotientGroupOp_def Homomor_def IsMorphism_def
  by simp

text‹In the context of ‹group0›, we may use all results of ‹semigr0›.›

sublocale group0 < semigroup:semigr0 G P groper "λx. Fold1(P,x)" Append Concat  
  unfolding semigr0_def using groupAssum IsAgroup_def IsAmonoid_def by auto

end