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 ⊲ (G⦇carrier := A⦈)" 
      by (simp add: A2 normal_axioms normal_invE(1) normal_restrict_supergroup)
    have A3: "A' = rcosets⇘G⦇carrier := A⦈⇙ H"
      unfolding A_def using factgroup_subgroup_union_factor A'normal normal_imp_subgroup by auto
    from A1 interpret normalHA: normal H "(G⦇carrier := 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 (G⦇carrier := A⦈ Mod H) = {𝟭⇘(G⦇carrier := 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 ⊲ (G⦇carrier := A⦈)" by (metis A(1) inv_op_closed2 is_subgroup normal_inv_iff normal_restrict_supergroup)
      then interpret normalHA: normal H "(G⦇carrier := A⦈)" by simp
      from finite have finiteA: "finite A"
        by (meson A(1) normal_inv_iff finite_subset subgroup.subset)
      have "rcosets⇘(G⦇carrier := A⦈)⇙ H ⊲ G Mod H"
        by (simp add: A(1) HA normal_axioms normality_factorization) 
      with simple have "rcosets⇘(G⦇carrier := A⦈)⇙ H = {𝟭⇘G Mod H⇙} ∨ rcosets⇘(G⦇carrier := A⦈)⇙ H = carrier (G Mod H)"
        unfolding simple_group_def simple_group_axioms_def by auto
      thus "False"
      proof
        assume "rcosets⇘G⦇carrier := A⦈⇙ H = {𝟭⇘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: "rcosets⇘G⦇carrier := A⦈⇙ H = 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 ∈ rcosets⇘G⦇carrier := A⦈⇙ H" unfolding FactGroup_def by simp
            then obtain x' where x': "x' ∈ A" "H #>x = H #>⇘G⦇carrier := A⦈⇙ x'" 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