Theory MaximalNormalSubgroups

(*  Title:      A locale for and a characterization of maximal normal subgroups
    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
    Maintainer: Jakob von Raumer <jakob.raumer@student.kit.edu>
*)

theory MaximalNormalSubgroups
imports "HOL-Algebra.Algebra"
begin

section ‹Facts about maximal normal subgroups›

text ‹A maximal normal subgroup of $G$ is a normal subgroup which is not contained in other any proper
  normal subgroup of $G$.›

locale max_normal_subgroup = normal +
  assumes proper: "H  carrier G"
  assumes max_normal: "J. J  G  J  H  J  carrier G  ¬ (H  J)"

text ‹Another characterization of maximal normal subgroups: The factor group is simple.›

theorem (in normal) max_normal_simple_quotient:
  assumes finite: "finite (carrier G)"
  shows "max_normal_subgroup H G = simple_group (G Mod H)"
proof
  assume "max_normal_subgroup H G"
  then interpret maxH: max_normal_subgroup H G.
  show "simple_group (G Mod H)" unfolding simple_group_def simple_group_axioms_def
  proof (intro conjI factorgroup_is_group allI impI disjCI)
    have gt0: "0 < card (rcosets H)"
      by (metis gr_zeroI lagrange_finite assms mult_is_0 order_gt_0_iff_finite subgroup_axioms)
    from maxH.proper finite have "carrier (G Mod H)  {𝟭G Mod H}" using fact_group_trivial_iff by auto
    hence "1  order (G Mod H)" using factorgroup_is_group group.order_one_triv_iff by metis
    with gt0 show "1 < order (G Mod H)" unfolding order_def FactGroup_def by auto
  next
    fix A'
    assume A'normal: "A'  G Mod H" and A'nottriv: "A'  {𝟭G Mod H}"
    define A where "A = A'"
    have A2: "A  G" using A'normal unfolding A_def by (rule factgroup_subgroup_union_normal)
    have "H  A'" using A'normal normal_imp_subgroup subgroup.one_closed unfolding FactGroup_def by force
    hence "H  A" unfolding A_def by auto
    hence A1: "H  (Gcarrier := A)" 
      by (simp add: A2 normal_axioms normal_invE(1) normal_restrict_supergroup)
    have A3: "A' = rcosetsGcarrier := AH"
      unfolding A_def using factgroup_subgroup_union_factor A'normal normal_imp_subgroup by auto
    from A1 interpret normalHA: normal H "(Gcarrier := A)" by metis
    have "H  A" using normalHA.is_subgroup subgroup.subset by force
    with A2 have "A = H  A = carrier G" using maxH.max_normal by auto
    thus "A' = carrier (G Mod H)"
    proof 
      assume "A = H"
      hence "carrier (Gcarrier := A Mod H) = {𝟭(Gcarrier := A Mod H)}"
        using cosets_finite subgroup_in_rcosets subset assms normalHA.fact_group_trivial_iff by force
      then have "A' = {𝟭G Mod H}" 
        using A3 unfolding FactGroup_def by simp
      with A'nottriv show ?thesis..
    next
      assume "A = carrier G"
      thus "A' = carrier (G Mod H)" using A3 unfolding FactGroup_def by simp
    qed
  qed
next
  assume simple: "simple_group (G Mod H)"
  show "max_normal_subgroup H G"
  proof
    from simple have "carrier (G Mod H)  {𝟭G Mod H}" unfolding simple_group_def simple_group_axioms_def order_def by auto
    with finite fact_group_trivial_iff show "H  carrier G" by auto
  next
    fix A
    assume A: "A  G" "A  H" "A  carrier G"
    show "¬ H  A"
    proof
      assume HA: "H  A"
      hence "H  (Gcarrier := A)" by (metis A(1) inv_op_closed2 is_subgroup normal_inv_iff normal_restrict_supergroup)
      then interpret normalHA: normal H "(Gcarrier := A)" by simp
      from finite have finiteA: "finite A"
        by (meson A(1) normal_inv_iff finite_subset subgroup.subset)
      have "rcosets(Gcarrier := A)H  G Mod H"
        by (simp add: A(1) HA normal_axioms normality_factorization) 
      with simple have "rcosets(Gcarrier := A)H = {𝟭G Mod H}  rcosets(Gcarrier := A)H = carrier (G Mod H)"
        unfolding simple_group_def simple_group_axioms_def by auto
      thus "False"
      proof
        assume "rcosetsGcarrier := AH = {𝟭G Mod H}"
        with finiteA have "H = A" 
          using normalHA.fact_group_trivial_iff unfolding FactGroup_def by auto
        with A(2) show ?thesis by simp
      next
        assume AHGH: "rcosetsGcarrier := AH = carrier (G Mod H)"
        have "A = carrier G" unfolding FactGroup_def RCOSETS_def
        proof
          show "A  carrier G" using A(1) normal_imp_subgroup subgroup.subset by metis
        next
          show "carrier G  A"
          proof
            fix x
            assume x: "x  carrier G"
            hence "H #> x  rcosets H" unfolding RCOSETS_def by auto
            with AHGH have "H #> x  rcosetsGcarrier := AH" unfolding FactGroup_def by simp
            then obtain x' where x': "x'  A" "H #>x = H #>Gcarrier := Ax'" unfolding RCOSETS_def by auto
            hence "H #> x = H #> x'" unfolding r_coset_def by auto
            hence "x  H #> x'" by (metis is_subgroup rcos_self x)
            hence "x  A #> x'" using HA unfolding r_coset_def by auto
            thus "x  A" using x'(1) unfolding r_coset_def using subgroup.m_closed A(1) normal_imp_subgroup by force
          qed
        qed
        with A(3) show ?thesis by simp
      qed
    qed
  qed
qed

end