Theory Group_ZF_2

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

    Copyright (C) 2005, 2006  Slawomir Kolodynski

    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 2›

theory Group_ZF_2 imports AbelianGroup_ZF func_ZF EquivClass1

begin

text‹This theory continues Group\_ZF.thy and considers lifting the group 
  structure to function spaces and projecting the group structure to 
  quotient spaces, in particular the quotient qroup.›

subsection‹Lifting groups to function spaces›

text‹If we have a monoid (group) $G$ than we get a monoid (group) 
  structure on a space of functions valued in 
  in $G$ by defining $(f\cdot g)(x) := f(x)\cdot g(x)$. 
  We call this process ''lifting the monoid (group) to function space''.
  This section formalizes this lifting.›

text‹The lifted operation is an operation on the function space.›

lemma (in monoid0) Group_ZF_2_1_L0A:
  assumes A1: "F = f {lifted to function space over} X"
  shows "F : (X→G)×(X→G)→(X→G)"
proof -
  from monoidAssum have "f : G×G→G"
    using IsAmonoid_def IsAssociative_def by simp
  with A1 show ?thesis
    using func_ZF_1_L3 group0_1_L3B by auto
qed

text‹The result of the lifted operation is in the function space.›

lemma (in monoid0) Group_ZF_2_1_L0: 
  assumes A1:"F = f {lifted to function space over} X"
  and A2:"s:X→G" "r:X→G"
  shows "F`⟨ s,r⟩ : X→G"
proof -
  from A1 have "F : (X→G)×(X→G)→(X→G)"
    using Group_ZF_2_1_L0A
    by simp
  with A2 show ?thesis using apply_funtype
    by simp
qed
    
text‹The lifted monoid operation has a neutral element, namely
  the constant function with the neutral element as the value.›

lemma (in monoid0) Group_ZF_2_1_L1: 
  assumes A1: "F = f {lifted to function space over} X"
  and A2: "E = ConstantFunction(X,TheNeutralElement(G,f))"
  shows "E : X→G ∧ (∀s∈X→G. F`⟨ E,s⟩ = s ∧ F`⟨ s,E⟩ = s)"
proof
  from A2 show T1:"E : X→G"
    using unit_is_neutral func1_3_L1 by simp
  show "∀s∈X→G. F`⟨ E,s⟩ = s ∧ F`⟨ s,E⟩ = s"
  proof
    fix s assume A3:"s:X→G"
    from monoidAssum have T2:"f : G×G→G"
      using IsAmonoid_def IsAssociative_def by simp
    from A3 A1 T1 have 
      "F`⟨ E,s⟩ : X→G" "F`⟨ s,E⟩ : X→G" "s : X→G"
      using Group_ZF_2_1_L0 by auto
    moreover from T2 A1 T1 A2 A3 have
      "∀x∈X. (F`⟨ E,s⟩)`(x) = s`(x)"
      "∀x∈X. (F`⟨ s,E⟩)`(x) = s`(x)"
      using func_ZF_1_L4 group0_1_L3B func1_3_L2 
	apply_type unit_is_neutral by auto
    ultimately show 
      "F`⟨ E,s⟩ = s ∧ F`⟨ s,E⟩ = s"
      using fun_extension_iff by auto
  qed
qed

text‹Monoids can be lifted to a function space.›

lemma (in monoid0) Group_ZF_2_1_T1: 
  assumes A1: "F = f {lifted to function space over} X"
  shows "IsAmonoid(X→G,F)"
proof -
  from monoidAssum A1 have 
    "F {is associative on} (X→G)"
    using IsAmonoid_def func_ZF_2_L4 group0_1_L3B
    by auto
  moreover from A1 have 
    "∃ E ∈ X→G. ∀s ∈ X→G. F`⟨ E,s⟩ = s ∧ F`⟨ s,E⟩ = s"
    using Group_ZF_2_1_L1 by blast
  ultimately show ?thesis using IsAmonoid_def
    by simp
qed

text‹The constant function with the neutral element as the value is the
  neutral element of the lifted monoid.›

lemma Group_ZF_2_1_L2:
  assumes A1: "IsAmonoid(G,f)"
  and A2: "F = f {lifted to function space over} X"
  and A3: "E = ConstantFunction(X,TheNeutralElement(G,f))"
  shows "E = TheNeutralElement(X→G,F)"
proof - 
  from A1 A2 have 
     T1:"monoid0(G,f)" and T2:"monoid0(X→G,F)"
    using monoid0_def monoid0.Group_ZF_2_1_T1
    by auto
  from T1 A2 A3 have 
    "E : X→G ∧ (∀s∈X→G. F`⟨ E,s⟩ = s ∧ F`⟨ s,E⟩ = s)"
    using monoid0.Group_ZF_2_1_L1 by simp
  with T2 show ?thesis
    using monoid0.group0_1_L4 by auto
qed

text‹The lifted operation acts on the functions in a natural way defined
  by the monoid operation.›

lemma (in monoid0) lifted_val:
  assumes "F = f {lifted to function space over} X"
  and "s:X→G"  "r:X→G"
  and "x∈X"
  shows "(F`⟨s,r⟩)`(x) = s`(x) ⊕ r`(x)"
  using monoidAssum assms IsAmonoid_def IsAssociative_def
      group0_1_L3B func_ZF_1_L4
  by auto

text‹The lifted operation acts on the functions in a natural way defined
  by the group operation. This is the same as ‹lifted_val›, but
  in the ‹group0› context.›

lemma (in group0) Group_ZF_2_1_L3:
  assumes "F = P {lifted to function space over} X"
  and "s:X→G" "r:X→G"
  and "x∈X"
  shows "(F`⟨s,r⟩)`(x) = s`(x)⋅r`(x)"
  using assms group0_2_L1 monoid0.lifted_val by simp
    
text‹In the group0 context we can apply theorems proven in monoid0 context
  to the lifted monoid.›

lemma (in group0) Group_ZF_2_1_L4:
  assumes A1: "F = P {lifted to function space over} X"
  shows "monoid0(X→G,F)"
proof -
  from A1 show ?thesis
    using group0_2_L1 monoid0.Group_ZF_2_1_T1 monoid0_def
    by simp
qed

text‹The compostion of a function $f:X\rightarrow G$ with the group inverse
  is a right inverse for the lifted group.›

lemma (in group0) Group_ZF_2_1_L5: 
  assumes A1: "F = P {lifted to function space over} X"
  and A2: "s : X→G"
  and A3: "i = GroupInv(G,P) O s"
  shows "i: X→G" and "F`⟨ s,i⟩ = TheNeutralElement(X→G,F)"
proof -
  let ?E = "ConstantFunction(X,𝟭)"
  have "?E : X→G" 
    using group0_2_L2 func1_3_L1 by simp
  moreover from groupAssum A2 A3 A1 have
    "F`⟨ s,i⟩ :  X→G" using group0_2_T2 comp_fun 
      Group_ZF_2_1_L4 monoid0.group0_1_L1
    by simp
  moreover from groupAssum A2 A3 A1 have 
    "∀x∈X. (F`⟨ s,i⟩)`(x) = ?E`(x)"
    using group0_2_T2 comp_fun Group_ZF_2_1_L3 
      comp_fun_apply apply_funtype group0_2_L6 func1_3_L2
    by simp
  moreover from groupAssum A1 have
    "?E = TheNeutralElement(X→G,F)"
    using IsAgroup_def Group_ZF_2_1_L2 by simp
  ultimately show "F`⟨ s,i⟩ = TheNeutralElement(X→G,F)"
    using fun_extension_iff IsAgroup_def Group_ZF_2_1_L2
    by simp
  from groupAssum A2 A3 show "i: X→G" 
    using group0_2_T2 comp_fun by simp
qed

text‹Groups can be lifted to the function space.›

theorem (in group0) Group_ZF_2_1_T2:
  assumes A1: "F = P {lifted to function space over} X"
  shows "IsAgroup(X→G,F)"
proof -
  from A1 have "IsAmonoid(X→G,F)"
    using group0_2_L1 monoid0.Group_ZF_2_1_T1
    by simp
  moreover have 
    "∀s∈X→G. ∃i∈X→G. F`⟨ s,i⟩ = TheNeutralElement(X→G,F)"
  proof
    fix s assume A2: "s : X→G"
    let ?i = "GroupInv(G,P) O s"
    from groupAssum A2 have "?i:X→G"
      using group0_2_T2 comp_fun by simp
    moreover from A1 A2 have 
      "F`⟨ s,?i⟩ = TheNeutralElement(X→G,F)"
      using Group_ZF_2_1_L5 by fast
   ultimately show "∃i∈X→G. F`⟨ s,i⟩ = TheNeutralElement(X→G,F)" 
      by auto
  qed
  ultimately show ?thesis using IsAgroup_def
    by simp
qed

text‹The propositions proven in the ‹group0› context are valid in the same context
  when applied to the function space with the lifted group operation.›

lemma (in group0) group0_valid_fun_space: 
  shows "group0(X→G,P {lifted to function space over} X)"
  using Group_ZF_2_1_T2 unfolding group0_def by simp

text‹What is the group inverse for the lifted group?›

lemma (in group0) Group_ZF_2_1_L6: 
  assumes A1: "F = P {lifted to function space over} X"
  shows "∀s∈(X→G). GroupInv(X→G,F)`(s) = GroupInv(G,P) O s"
proof -
  from A1 have  "group0(X→G,F)"
    using group0_def Group_ZF_2_1_T2 
    by simp
  moreover from A1 have "∀s∈X→G. GroupInv(G,P) O s : X→G ∧ 
    F`⟨ s,GroupInv(G,P) O s⟩ = TheNeutralElement(X→G,F)"
    using Group_ZF_2_1_L5 by simp
  ultimately have 
    "∀s∈(X→G).  GroupInv(G,P) O s = GroupInv(X→G,F)`(s)"
    by (rule group0.group0_2_L9A)
  thus ?thesis by simp
qed

text‹What is the value of the group inverse for the lifted group?›

corollary (in group0) lift_gr_inv_val:  
  assumes "F = P {lifted to function space over} X" and
  "s : X→G" and "x∈X"
  shows  "(GroupInv(X→G,F)`(s))`(x) = (s`(x))¯"
  using groupAssum assms Group_ZF_2_1_L6 group0_2_T2 comp_fun_apply
  by simp

text‹What is the group inverse in a subgroup of the lifted group?›

lemma (in group0) Group_ZF_2_1_L6A:
  assumes A1: "F = P {lifted to function space over} X"
  and A2: "IsAsubgroup(H,F)"
  and A3: "g = restrict(F,H×H)"
  and A4: "s∈H"
  shows "GroupInv(H,g)`(s) = GroupInv(G,P) O s"
proof -
  from A1 have T1: "group0(X→G,F)"
    using group0_def Group_ZF_2_1_T2 
    by simp
  with A2 A3 A4 have "GroupInv(H,g)`(s) = GroupInv(X→G,F)`(s)"
    using group0.group0_3_T1 restrict by simp
  moreover from T1 A1 A2 A4 have
    "GroupInv(X→G,F)`(s) = GroupInv(G,P) O s"
    using group0.group0_3_L2 Group_ZF_2_1_L6 by blast
  ultimately show ?thesis by simp
qed

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

lemma (in group0) lift_group_subgr_neut:
  assumes "F = P {lifted to function space over} X" and "IsAsubgroup(H,F)"
  shows "TheNeutralElement(H,restrict(F,H×H)) = ConstantFunction(X,𝟭)"
proof -
  from assms have 
    "TheNeutralElement(H,restrict(F,H×H)) = TheNeutralElement(X→G,F)"
    using group0_valid_fun_space group0.group0_3_L4 by blast
  also from groupAssum assms(1) have "... = ConstantFunction(X,𝟭)"
    using Group_ZF_2_1_L2 unfolding IsAgroup_def by simp
  finally show ?thesis by simp
qed

text‹If a group is abelian, then its lift to a function space is also 
  abelian.›

lemma (in group0) Group_ZF_2_1_L7: 
  assumes A1: "F = P {lifted to function space over} X"
  and A2: "P {is commutative on} G"
  shows "F {is commutative on} (X→G)"
proof-
  from A1 A2  have
    "F {is commutative on} (X→range(P))"
    using group_oper_fun func_ZF_2_L2
    by simp
  moreover from groupAssum have "range(P) = G"
    using group0_2_L1 monoid0.group0_1_L3B
    by simp
  ultimately show ?thesis by simp
qed
    
subsection‹Equivalence relations on groups›

text‹The goal of this section is to establish that (under some conditions) 
  given an equivalence
  relation on a group or (monoid )we can project the group (monoid)
  structure on the quotient and obtain another group.›

text‹The neutral element class is neutral in the projection.›

lemma (in monoid0) Group_ZF_2_2_L1: 
  assumes A1: "equiv(G,r)" and A2:"Congruent2(r,f)"
  and A3: "F = ProjFun2(G,r,f)" 
  and A4: "e = TheNeutralElement(G,f)"
  shows "r``{e} ∈ G//r ∧ 
  (∀c ∈ G//r. F`⟨ r``{e},c⟩ = c ∧  F`⟨ c,r``{e}⟩ = c)"
proof
  from A4 show T1:"r``{e} ∈ G//r"
    using unit_is_neutral quotientI
    by simp
  show 
    "∀c ∈ G//r. F`⟨ r``{e},c⟩ = c ∧  F`⟨ c,r``{e}⟩ = c"
  proof
    fix c assume A5:"c ∈ G//r"
    then obtain g where D1:"g∈G" "c = r``{g}"
      using quotient_def by auto
    with A1 A2 A3 A4 D1 show 
      "F`⟨ r``{e},c⟩ = c ∧  F`⟨ c,r``{e}⟩ = c"
      using unit_is_neutral EquivClass_1_L10 (*group0_1_L3*)
      by simp
  qed
qed

text‹The projected structure is a monoid.›

theorem (in monoid0) Group_ZF_2_2_T1:
  assumes A1: "equiv(G,r)" and A2: "Congruent2(r,f)"
  and A3: "F = ProjFun2(G,r,f)"
  shows "IsAmonoid(G//r,F)"
proof -
  let ?E = "r``{TheNeutralElement(G,f)}"
  from A1 A2 A3 have 
    "?E ∈ G//r ∧ (∀c∈G//r. F`⟨ ?E,c⟩ = c ∧ F`⟨ c,?E⟩ = c)"
    using Group_ZF_2_2_L1 by simp
  hence
    "∃E∈G//r. ∀ c∈G//r. F`⟨ E,c⟩ = c ∧ F`⟨ c,E⟩ = c"
    by auto
  with monoidAssum A1 A2 A3 show ?thesis
    using IsAmonoid_def EquivClass_2_T2
    by simp
qed

text‹The class of the neutral element is the neutral element of the
  projected monoid.›

lemma Group_ZF_2_2_L1:
  assumes A1: "IsAmonoid(G,f)"
  and A2: "equiv(G,r)" and A3: "Congruent2(r,f)"
  and A4: "F = ProjFun2(G,r,f)"
  and A5: "e = TheNeutralElement(G,f)"
  shows " r``{e} = TheNeutralElement(G//r,F)"
proof -
  from A1 A2 A3 A4 have 
    T1:"monoid0(G,f)" and T2:"monoid0(G//r,F)"
    using monoid0_def monoid0.Group_ZF_2_2_T1 by auto
  from T1 A2 A3 A4 A5 have "r``{e} ∈ G//r ∧ 
    (∀c ∈ G//r. F`⟨ r``{e},c⟩ = c ∧  F`⟨ c,r``{e}⟩ = c)"
    using monoid0.Group_ZF_2_2_L1 by simp
  with T2 show ?thesis using monoid0.group0_1_L4
    by auto
qed

text‹The projected operation can be defined in terms of the group operation
  on representants in a natural way.›

lemma (in group0) Group_ZF_2_2_L2:
  assumes A1: "equiv(G,r)" and A2: "Congruent2(r,P)"
  and A3: "F = ProjFun2(G,r,P)"
  and A4: "a∈G" "b∈G"
  shows "F`⟨ r``{a},r``{b}⟩ = r``{a⋅b}"
proof -
  from A1 A2 A3 A4 show ?thesis
    using EquivClass_1_L10 by simp
qed

text‹The class of the inverse is a right inverse of the class.›

lemma (in group0) Group_ZF_2_2_L3:
  assumes A1: "equiv(G,r)" and A2: "Congruent2(r,P)"
  and A3: "F = ProjFun2(G,r,P)"
  and A4: "a∈G"
  shows "F`⟨r``{a},r``{a¯}⟩ = TheNeutralElement(G//r,F)"
proof -
  from A1 A2 A3 A4 have
    "F`⟨r``{a},r``{a¯}⟩ = r``{𝟭}"
    using inverse_in_group Group_ZF_2_2_L2 group0_2_L6 
    by simp
  with groupAssum A1 A2 A3 show ?thesis
    using IsAgroup_def Group_ZF_2_2_L1 by simp
qed

text‹The group structure can be projected to the quotient space.›

theorem (in group0) Group_ZF_3_T2:
  assumes A1: "equiv(G,r)" and A2: "Congruent2(r,P)"
  shows "IsAgroup(G//r,ProjFun2(G,r,P))"
proof -
  let ?F = "ProjFun2(G,r,P)"
  let ?E = "TheNeutralElement(G//r,?F)"
  from groupAssum A1 A2 have "IsAmonoid(G//r,?F)"
    using IsAgroup_def monoid0_def monoid0.Group_ZF_2_2_T1
    by simp
  moreover have
    "∀c∈G//r. ∃b∈G//r. ?F`⟨ c,b⟩ = ?E"
  proof
    fix c assume A3: "c ∈ G//r"
    then obtain g where D1: "g∈G"  "c = r``{g}"
      using quotient_def by auto
    let ?b = "r``{g¯}"
    from D1 have "?b ∈ G//r"
      using inverse_in_group quotientI
      by simp
    moreover from A1 A2 D1 have 
      "?F`⟨ c,?b⟩ = ?E"
      using Group_ZF_2_2_L3 by simp
    ultimately show "∃b∈G//r. ?F`⟨ c,b⟩ = ?E"
      by auto
  qed
  ultimately show ?thesis
    using IsAgroup_def by simp
qed

text‹The group inverse (in the projected group) of a class is the class
  of the inverse.›

lemma (in group0) Group_ZF_2_2_L4:
  assumes A1: "equiv(G,r)" and 
  A2: "Congruent2(r,P)" and 
  A3: "F = ProjFun2(G,r,P)" and
  A4: "a∈G"
  shows "r``{a¯} = GroupInv(G//r,F)`(r``{a})"
proof -
  from A1 A2 A3 have "group0(G//r,F)"
    using Group_ZF_3_T2 group0_def by simp
  moreover from A4 have 
    "r``{a} ∈ G//r"  "r``{a¯} ∈ G//r"
    using inverse_in_group quotientI by auto
  moreover from A1 A2 A3 A4 have
     "F`⟨r``{a},r``{a¯}⟩ = TheNeutralElement(G//r,F)"
    using Group_ZF_2_2_L3 by simp
  ultimately show ?thesis
    by (rule group0.group0_2_L9)
qed

subsection‹Normal subgroups and quotient groups›

text‹If $H$ is a subgroup of $G$, then for every $a\in G$
  we can cosider the sets $\{a\cdot h. h \in H\}$ 
  and $\{ h\cdot a. h \in H\}$ (called a left and right ''coset of H'', resp.)
  These sets sometimes form a group, called the ''quotient group''.
  This section discusses the notion of quotient groups.›

text‹A normal subgorup $N$ of a group $G$ is such that $aba^{-1}$ belongs to 
  $N$ if $a\in G, b\in N$.›

definition
  "IsAnormalSubgroup(G,P,N) ≡ IsAsubgroup(N,P) ∧ 
  (∀n∈N.∀g∈G. P`⟨  P`⟨  g,n ⟩,GroupInv(G,P)`(g) ⟩ ∈ N)"

text‹Having a group and a normal subgroup $N$ 
  we can create another group
  consisting of eqivalence classes of the relation 
  $a\sim b \equiv a\cdot b^{-1} \in N$.  We will refer to this relation
  as the quotient group relation. The classes of this relation are in 
  fact cosets of subgroup $H$.›

definition
  "QuotientGroupRel(G,P,H) ≡ 
  {⟨ a,b⟩ ∈ G×G. P`⟨ a, GroupInv(G,P)`(b)⟩ ∈ H}"

text‹Next we define the operation in the quotient group as the
  projection of the group operation on the classses of the
  quotient group relation.›

definition
  "QuotientGroupOp(G,P,H) ≡ ProjFun2(G,QuotientGroupRel(G,P,H ),P)"

text‹Definition of a normal subgroup in a more readable notation.›

lemma (in group0) Group_ZF_2_4_L0: 
  assumes "IsAnormalSubgroup(G,P,H)"
  and "g∈G" "n∈H"
  shows "g⋅n⋅g¯ ∈ H"
  using assms IsAnormalSubgroup_def by simp

text‹The quotient group relation is reflexive.›

lemma (in group0) Group_ZF_2_4_L1: 
  assumes "IsAsubgroup(H,P)"
  shows "refl(G,QuotientGroupRel(G,P,H))"
  using assms  group0_2_L6 group0_3_L5 
    QuotientGroupRel_def refl_def by simp

text‹The quotient group relation is symmetric.›

lemma (in group0) Group_ZF_2_4_L2:
  assumes A1:"IsAsubgroup(H,P)"
  shows "sym(QuotientGroupRel(G,P,H))"
proof -
  {  
    fix a b assume A2: "⟨ a,b⟩ ∈ QuotientGroupRel(G,P,H)"
    with A1 have "(a⋅b¯)¯ ∈ H" 
      using QuotientGroupRel_def group0_3_T3A
      by simp
    moreover from A2 have "(a⋅b¯)¯ =  b⋅a¯"
      using QuotientGroupRel_def group0_2_L12
      by simp
    ultimately have "b⋅a¯ ∈ H" by simp
    with A2 have "⟨ b,a⟩ ∈ QuotientGroupRel(G,P,H)"
      using QuotientGroupRel_def by simp 
  }
  then show ?thesis using symI by simp
qed

text‹The quotient group relation is transistive.›

lemma (in group0) Group_ZF_2_4_L3A:
  assumes A1: "IsAsubgroup(H,P)" and 
  A2: "⟨ a,b⟩ ∈ QuotientGroupRel(G,P,H)" and 
  A3: "⟨ b,c⟩ ∈ QuotientGroupRel(G,P,H)"
  shows "⟨ a,c⟩ ∈ QuotientGroupRel(G,P,H)"
proof -
  let ?r = "QuotientGroupRel(G,P,H)"
  from A2 A3 have T1:"a∈G" "b∈G" "c∈G"
    using QuotientGroupRel_def by auto
  from A1 A2 A3 have "(a⋅b¯)⋅(b⋅c¯) ∈ H"
    using  QuotientGroupRel_def group0_3_L6
    by simp
  moreover from T1 have 
    "a⋅c¯ = (a⋅b¯)⋅(b⋅c¯)"
    using group0_2_L14A by blast
  ultimately have "a⋅c¯ ∈ H" 
    by simp
  with T1 show ?thesis using QuotientGroupRel_def
    by simp
qed

text‹The quotient group relation is an equivalence relation. Note
  we do not need the subgroup to be normal for this to be true.›

lemma (in group0) Group_ZF_2_4_L3: assumes A1:"IsAsubgroup(H,P)"
  shows "equiv(G,QuotientGroupRel(G,P,H))"
proof -
  let ?r = "QuotientGroupRel(G,P,H)"
  from A1 have 
     "∀a b c. (⟨a, b⟩ ∈ ?r  ∧  ⟨b, c⟩ ∈ ?r ⟶ ⟨a, c⟩ ∈ ?r)"
    using Group_ZF_2_4_L3A by blast
  then have "trans(?r)"
    using Fol1_L2 by blast
  with A1 show ?thesis 
    using Group_ZF_2_4_L1 Group_ZF_2_4_L2 
      QuotientGroupRel_def equiv_def
    by auto
qed

text‹The next lemma states the essential condition for congruency of 
  the group operation with respect to the quotient group relation.›

lemma (in group0) Group_ZF_2_4_L4: 
  assumes A1: "IsAnormalSubgroup(G,P,H)"
  and A2: "⟨a1,a2⟩ ∈ QuotientGroupRel(G,P,H)"
  and A3: "⟨b1,b2⟩ ∈ QuotientGroupRel(G,P,H)"
  shows "⟨a1⋅b1, a2⋅b2⟩ ∈ QuotientGroupRel(G,P,H)"
proof -
  from A2 A3 have T1:
    "a1∈G"  "a2∈G"  "b1∈G"  "b2∈G"
    "a1⋅b1 ∈ G"  "a2⋅b2 ∈ G"
    "b1⋅b2¯ ∈ H"  "a1⋅a2¯ ∈ H"
    using QuotientGroupRel_def group0_2_L1 monoid0.group0_1_L1
    by auto
  with A1 show ?thesis using
    IsAnormalSubgroup_def group0_3_L6 group0_2_L15
    QuotientGroupRel_def by simp
qed

text‹If the subgroup is normal, the group operation is congruent 
  with respect to the quotient group relation.›

lemma Group_ZF_2_4_L5A:
  assumes "IsAgroup(G,P)"
  and "IsAnormalSubgroup(G,P,H)" 
  shows "Congruent2(QuotientGroupRel(G,P,H),P)"
  using assms group0_def group0.Group_ZF_2_4_L4 Congruent2_def
  by simp

text‹The quotient group is indeed a group.›

theorem Group_ZF_2_4_T1:
  assumes "IsAgroup(G,P)" and "IsAnormalSubgroup(G,P,H)"
  shows   
  "IsAgroup(G//QuotientGroupRel(G,P,H),QuotientGroupOp(G,P,H))"
  using assms group0_def group0.Group_ZF_2_4_L3 IsAnormalSubgroup_def
    Group_ZF_2_4_L5A group0.Group_ZF_3_T2 QuotientGroupOp_def
  by simp

text‹The class (coset) of the neutral element is the neutral
  element of the quotient group.›

lemma Group_ZF_2_4_L5B: 
  assumes "IsAgroup(G,P)" and "IsAnormalSubgroup(G,P,H)"
  and "r = QuotientGroupRel(G,P,H)"
  and "e = TheNeutralElement(G,P)"
  shows " r``{e} = TheNeutralElement(G//r,QuotientGroupOp(G,P,H))"
  using assms IsAnormalSubgroup_def group0_def
    IsAgroup_def group0.Group_ZF_2_4_L3 Group_ZF_2_4_L5A
    QuotientGroupOp_def Group_ZF_2_2_L1
  by simp

text‹A group element is equivalent to the neutral element iff it is in the
  subgroup we divide the group by.›

lemma (in group0) Group_ZF_2_4_L5C: assumes "a∈G"
  shows "⟨a,𝟭⟩ ∈ QuotientGroupRel(G,P,H) ⟷ a∈H"
  using assms QuotientGroupRel_def group_inv_of_one group0_2_L2
  by auto

text‹A group element is in $H$ iff its class is the neutral element of
  $G/H$.›

lemma (in group0) Group_ZF_2_4_L5D:
  assumes A1: "IsAnormalSubgroup(G,P,H)" and 
  A2: "a∈G" and 
  A3: "r = QuotientGroupRel(G,P,H)" and
  A4: "TheNeutralElement(G//r,QuotientGroupOp(G,P,H)) = e"
  shows "r``{a} = e ⟷ ⟨a,𝟭⟩ ∈ r"
proof
  assume "r``{a} = e"
  with groupAssum assms have 
    "r``{𝟭} = r``{a}" and I: "equiv(G,r)"
    using Group_ZF_2_4_L5B IsAnormalSubgroup_def Group_ZF_2_4_L3
    by auto
  with A2 have "⟨𝟭,a⟩ ∈ r" using eq_equiv_class 
    by simp
  with I show "⟨a,𝟭⟩ ∈ r" by (rule equiv_is_sym)
next assume "⟨a,𝟭⟩ ∈ r"
  moreover from A1 A3 have "equiv(G,r)"
    using IsAnormalSubgroup_def Group_ZF_2_4_L3
    by simp
  ultimately have "r``{a} = r``{𝟭}"
    using equiv_class_eq by simp
  with groupAssum A1 A3 A4 show "r``{a} = e"
    using Group_ZF_2_4_L5B by simp
qed
  
text‹The class of $a\in G$ is the neutral 
  element of the quotient $G/H$ iff $a\in H$.›

lemma (in group0) Group_ZF_2_4_L5E: 
  assumes "IsAnormalSubgroup(G,P,H)" and 
  "a∈G" and "r = QuotientGroupRel(G,P,H)" and 
  "TheNeutralElement(G//r,QuotientGroupOp(G,P,H)) = e"
  shows "r``{a} = e ⟷ a∈H"
  using assms Group_ZF_2_4_L5C  Group_ZF_2_4_L5D
  by simp

text‹Essential condition to show that every subgroup of an abelian group 
  is normal.›

lemma (in group0) Group_ZF_2_4_L5:
  assumes A1: "P {is commutative on} G" 
  and A2: "IsAsubgroup(H,P)"
  and A3: "g∈G"  "h∈H" 
  shows "g⋅h⋅g¯ ∈ H"
proof -
  from A2 A3 have T1:"h∈G" "g¯ ∈ G" 
    using group0_3_L2 inverse_in_group by auto
  with A3 A1 have "g⋅h⋅g¯ = g¯⋅g⋅h"
    using group0_4_L4A by simp
  with A3 T1 show ?thesis using
    group0_2_L6 group0_2_L2
    by simp
qed

text‹Every subgroup of an abelian group is normal. Moreover, the quotient
  group is also abelian.›

lemma Group_ZF_2_4_L6:
  assumes A1: "IsAgroup(G,P)"
  and A2: "P {is commutative on} G" 
  and A3: "IsAsubgroup(H,P)"
  shows  "IsAnormalSubgroup(G,P,H)"
  "QuotientGroupOp(G,P,H) {is commutative on} (G//QuotientGroupRel(G,P,H))"
proof -
  from A1 A2 A3 show T1: "IsAnormalSubgroup(G,P,H)" using
    group0_def IsAnormalSubgroup_def group0.Group_ZF_2_4_L5 
    by simp
  let ?r = "QuotientGroupRel(G,P,H)"
  from A1 A3 T1 have "equiv(G,?r)" "Congruent2(?r,P)"
    using group0_def group0.Group_ZF_2_4_L3 Group_ZF_2_4_L5A
    by auto
  with A2 show 
    "QuotientGroupOp(G,P,H) {is commutative on} (G//QuotientGroupRel(G,P,H))"
    using EquivClass_2_T1 QuotientGroupOp_def
    by simp
qed

text‹The group inverse (in the quotient group) of a class (coset) is the class
  of the inverse.›

lemma (in group0) Group_ZF_2_4_L7: 
  assumes "IsAnormalSubgroup(G,P,H)" 
  and "a∈G" and "r = QuotientGroupRel(G,P,H)" 
  and "F = QuotientGroupOp(G,P,H)"
  shows "r``{a¯} = GroupInv(G//r,F)`(r``{a})"
  using groupAssum assms IsAnormalSubgroup_def Group_ZF_2_4_L3 
    Group_ZF_2_4_L5A QuotientGroupOp_def Group_ZF_2_2_L4
  by simp

subsection‹Function spaces as monoids›

text‹On every space of functions $\{f : X\rightarrow X\}$ 
  we can define a natural 
  monoid structure with composition as the operation. This section explores 
  this fact.›

text‹The next lemma states that composition has a neutral element, 
  namely the identity function on $X$ 
  (the one that maps $x\in X$ into itself).›
  
lemma Group_ZF_2_5_L1: assumes A1: "F = Composition(X)"
  shows "∃I∈(X→X). ∀f∈(X→X). F`⟨ I,f⟩ = f ∧ F`⟨ f,I⟩ = f"
proof-
  let ?I = "id(X)"
  from A1 have 
    "?I ∈ X→X ∧ (∀f∈(X→X). F`⟨ ?I,f⟩ = f ∧ F`⟨ f,?I⟩ = f)" 
    using id_type func_ZF_6_L1A by simp
  thus ?thesis by auto
qed

text‹The space of functions that map a set $X$ into 
  itsef is a monoid with composition as operation and the identity function
  as the neutral element.›

lemma Group_ZF_2_5_L2: shows
  "IsAmonoid(X→X,Composition(X))"
  "id(X) = TheNeutralElement(X→X,Composition(X))"
proof -
  let ?I = "id(X)"
  let ?F = "Composition(X)"
  show "IsAmonoid(X→X,Composition(X))" 
    using func_ZF_5_L5 Group_ZF_2_5_L1 IsAmonoid_def
    by auto  
  then have "monoid0(X→X,?F)"
    using monoid0_def by simp
  moreover have
    "?I ∈ X→X ∧ (∀f∈(X→X). ?F`⟨ ?I,f⟩ = f ∧ ?F`⟨ f,?I⟩ = f)"
    using id_type func_ZF_6_L1A by simp
  ultimately show "?I = TheNeutralElement(X→X,?F)"
    using monoid0.group0_1_L4 by auto
qed

end