Classical.Structures.Group.MinimalNormal

Minimal normal subgroups and monoliths

This is the Classical.Structures.Group.MinimalNormal module of the Agda Universal Algebra Library.

A minimal normal subgroup of G is a nontrivial normal subgroup that contains no smaller one. A monolith is a minimal normal subgroup contained in every nontrivial normal subgroup.

A group has a monolith exactly when it is subdirectly irreducible: for groups, subdirect irreducibility is equivalent to having a unique minimal normal subgroup.¹

This module collects the following facts about these notions:

• the notions themselves: IsNormalSubgroup, Nontrivial, IsMinimalNormal, IsMonolithᵍ, HasMonolithᵍ;
• ∩-isNormalSubgroup: an intersection of normal subgroups is a normal subgroup;
• minimal-meets→below and minimal-meets→least: a minimal normal subgroup is contained in every nontrivial normal subgroup that it intersects nontrivially, hence is the monolith when it intersects all of them nontrivially;²
• abelian→⊆-centralizer: an abelian subgroup lies inside its own centralizer, so a normal subgroup with trivial centralizer is nonabelian;
• HasNontrivialWitness and IsMinimalNormalʷ: the witnessed readings of nontriviality and of minimality, which is what a constructive existence proof for minimal normal subgroups can deliver (Classical.Structures.Group.MinimalNormalDescent).

Two presentation notes.

• The level L. Subgroup predicates here live at the level L of the subgroup lattice (Classical.Structures.Group.SubgroupLattice), because the intersection fact is the lattice's meet (∧-isSubgroup) rather than a second proof of the same closure property; for a group at levels α = ρ = 0ℓ and base level ℓ₀ = 0ℓ, L is 0ℓ.
• ᵍ marks the group-side form. IsMonolithᵍ is the normal-subgroup reading of the congruence-lattice notion IsMonolith; the two agree through the correspondence between normal subgroups and congruences of a group.³

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.Group.MinimalNormal where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Product     using  ( _×_ ; _,_ ; Σ-syntax ; proj₁ ; proj₂ ; ∃-syntax )
open import Level            using  ( Level ; _⊔_ ) renaming ( suc to lsuc )
open import Function         using (_∘_)
open import Relation.Binary  using  ( Setoid )
open import Relation.Nullary using  ( ¬_ )
open import Relation.Unary   using  ( Pred ; _∈_ ; _⊆_ ; _∩_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Structures.Group.Basic            using  ( Group ; module Group-Op )
open import Classical.Structures.Group.Centralizer      using  ( module Centralizer )
open import Classical.Structures.Group.Conjugation      using  ( module Conjugate )
open import Classical.Structures.Group.Subgroups        using  ( IsSubgroup
                                                               ; trivialSubgroup )
open import Classical.Structures.Group.SubgroupLattice  using  ( module GroupSublattice )
open import Setoid.Algebras.Basic                       using  ( 𝕌[_] ; 𝔻[_] )

Normal subgroups, nontriviality, and trivial meets

Throughout, 𝒢 is a group and ℓ₀ the base level of its subgroup lattice; every predicate below lives at the resulting level L.

module MinimalNormal {α ρ : Level} (𝒢@(𝑮 , _) : Group α ρ) (ℓ₀ : Level) where
  private
    G : Type α
    G = 𝕌[ 𝑮 ]

  open Setoid 𝔻[ 𝑮 ]         using  ( _≈_ )
  open Group-Op 𝒢            using  ( _∙_ ; ε )
  open Centralizer 𝒢         using  ( C[_] )
  open Conjugate 𝒢           using  ( IsNormal )
  open GroupSublattice 𝒢 ℓ₀  using  ( L ; subgroup→Subᴸ ; ∧-isSubgroup )

The trivial subgroup is the ≈-class of the identity, as elsewhere in the library; a subgroup is nontrivial when it is not contained in it. (Nontriviality is stated negatively on purpose: constructively, "not every element is the identity" carries no witness, and none of the arguments of this section and the next need one. The witnessed reading, which the descent of Classical.Structures.Group.MinimalNormalDescent does need, is named separately further below.)

  -- The trivial subgroup, as a predicate.
  Triv : Pred G ρ
  Triv = trivialSubgroup 𝒢 .proj₁

  -- N is nontrivial: it is not contained in the trivial subgroup.
  Nontrivial : Pred G L → Type (α ⊔ ρ ⊔ L)
  Nontrivial N = ¬ N ⊆ Triv

  -- Two subgroups meet trivially when their intersection is trivial.
  MeetTrivially : Pred G L → Pred G L → Type (α ⊔ ρ ⊔ L)
  MeetTrivially M N = (M ∩ N) ⊆ Triv

A normal subgroup bundles the two conditions that every statement below quantifies over; it is exactly the conjunction of IsSubgroup and IsNormal, named because it appears in every hypothesis.

  record IsNormalSubgroup (N : Pred G L) : Type (α ⊔ ρ ⊔ L) where
    field
      isSubgroup  : IsSubgroup 𝒢 N    -- closed under ops and respects equality
      isNormal    : IsNormal N        -- closed under conjugation

  open IsNormalSubgroup public

An intersection of normal subgroups is a normal subgroup: the subgroup half is the meet of the subgroup lattice, and the normality half is conjugation acting componentwise.

  ∩-isNormalSubgroup : {M N : Pred G L}
    →  IsNormalSubgroup M → IsNormalSubgroup N → IsNormalSubgroup (M ∩ N)
  ∩-isNormalSubgroup {M} {N} M-nsg N-nsg .isSubgroup =
    ∧-isSubgroup  (subgroup→Subᴸ M (M-nsg .isSubgroup))
                  (subgroup→Subᴸ N (N-nsg .isSubgroup))
                  (M-nsg .isSubgroup) (N-nsg .isSubgroup)
  ∩-isNormalSubgroup M-nsg N-nsg .isNormal g (x∈M , x∈N) =
    M-nsg .isNormal g x∈M , N-nsg .isNormal g x∈N

Minimal normal subgroups

M is a minimal normal subgroup when it is a nontrivial normal subgroup and the only nontrivial normal subgroup it contains is itself.

  record IsMinimalNormal (M : Pred G L) : Type (α ⊔ ρ ⊔ lsuc L) where
    field
      normalSubgroup  : IsNormalSubgroup M
      nontrivial      : Nontrivial M
      minimal         : ∀ N → IsNormalSubgroup N → N ⊆ M → Nontrivial N → M ⊆ N

  open IsMinimalNormal public

The key step. Suppose M is a minimal normal subgroup and N is a nontrivial normal subgroup that M does not meet trivially. Then M is below N: the intersection M ∩ N is a normal subgroup inside M, and it is nontrivial precisely because M and N do not meet trivially, so minimality gives M ⊆ M ∩ N ⊆ N.

Note that no witness is extracted anywhere: Nontrivial (M ∩ N) and ¬ MeetTrivially M N are the same statement, so the argument is constructive.

  -- A minimal normal subgroup lies below every nontrivial normal subgroup that
  -- it does not meet trivially.
  minimal-meets→below : (M N : Pred G L) → IsMinimalNormal M
    → IsNormalSubgroup N → Nontrivial N → ¬ MeetTrivially M N → M ⊆ N
  minimal-meets→below M N M-min N-nsg N-nontriv MN = proj₂ ∘ M⊆MN
    where
    M⊆MN : M ⊆ (M ∩ N)
    M⊆MN = M-min .minimal (M ∩ N)
      (∩-isNormalSubgroup (M-min .normalSubgroup) N-nsg) proj₁ MN

Quantifying over N gives the form the monolith record below asks for: a minimal normal subgroup that meets every nontrivial normal subgroup nontrivially is below every one of them.

  -- A minimal normal subgroup that meets every nontrivial normal subgroup
  -- nontrivially is below every one of them.
  minimal-meets→least : (M : Pred G L) → IsMinimalNormal M
    → (  ∀ N → IsNormalSubgroup N → Nontrivial N → ¬ MeetTrivially M N)
    →    ∀ N → IsNormalSubgroup N → Nontrivial N → M ⊆ N
  minimal-meets→least M M-min meets N N-nsg N-nontriv =
    minimal-meets→below M N M-min N-nsg N-nontriv (meets N N-nsg N-nontriv)

Witnessed nontriviality, and minimality against witnessed subgroups

Nontrivial is stated negatively, and that is the right choice for the arguments above; but a proof that a minimal normal subgroup exists cannot consume it.

Over a finite group a witness can be recovered for a normal subgroup whose membership is decidable, and only for such a subgroup: witness of Classical.Structures.Group.MinimalNormalDescent does the finite search, and the no-go theorem of that module shows the unrestricted passage from Nontrivial to HasNontrivialWitness is equivalent to double-negation elimination. So the two readings are named separately here.

  -- N is nontrivial, witnessed: some member of N is not the identity.
  HasNontrivialWitness : Pred G L → Type (α ⊔ ρ ⊔ L)
  HasNontrivialWitness N = ∃[ y ] (y ∈ N × ¬ y ≈ ε)

  -- A witness refutes containment in the trivial subgroup.
  witnessed→nontrivial : {N : Pred G L} → HasNontrivialWitness N → Nontrivial N
  witnessed→nontrivial (_ , y∈N , y≉ε) N⊆Triv = y≉ε (N⊆Triv y∈N)

The matching reading of minimality quantifies over the normal subgroups that come with a witness. It is not a weakening of IsMinimalNormal in the domain of quantification; the subgroups it ranges over are arbitrary, with no decidability assumed. It is only a change in the form of the nontriviality hypothesis.

  record IsMinimalNormalʷ (M : Pred G L) : Type (α ⊔ ρ ⊔ lsuc L) where
    field
      normalSubgroupʷ  : IsNormalSubgroup M
      witnessedʷ       : HasNontrivialWitness M
      minimalʷ         : ∀ N → IsNormalSubgroup N → N ⊆ M → HasNontrivialWitness N → M ⊆ N

  open IsMinimalNormalʷ public

The gap between the two records is one named principle, and naming it keeps the classical content in a single place rather than spread over the consumers.

  -- Every nontrivial normal subgroup has a witness.
  WitnessedNontriviality : Type (α ⊔ ρ ⊔ lsuc L)
  WitnessedNontriviality =
    (N : Pred G L) → IsNormalSubgroup N → Nontrivial N → HasNontrivialWitness N

  -- Granted that principle, witnessed minimality is minimality.
  minimalʷ→minimal : WitnessedNontriviality → {M : Pred G L}
    →  IsMinimalNormalʷ M → IsMinimalNormal M
  minimalʷ→minimal wit M-min = record
    { normalSubgroup  = M-min .normalSubgroupʷ
    ; nontrivial      = witnessed→nontrivial (M-min .witnessedʷ)
    ; minimal         = λ N N-nsg N⊆M N-nontriv →
                          M-min .minimalʷ N N-nsg N⊆M (wit N N-nsg N-nontriv)
    }

Monoliths and subdirect irreducibility

A monolith is a minimal normal subgroup contained in every nontrivial normal subgroup. A group has a monolith exactly when it is subdirectly irreducible.¹ HasMonolithᵍ is therefore the group-side statement of subdirect irreducibility, and minimal-meets→least is how a pairwise form of subdirect irreducibility reaches this characterization.

  record IsMonolithᵍ (M : Pred G L) : Type (α ⊔ ρ ⊔ lsuc L) where
    field
      isMinimalNormal  : IsMinimalNormal M
      least            : (N : Pred G L) → IsNormalSubgroup N → Nontrivial N → M ⊆ N

  -- G has a monolith: a least nontrivial normal subgroup.
  HasMonolithᵍ : Type (α ⊔ ρ ⊔ lsuc L)
  HasMonolithᵍ = Σ[ M ∈ Pred G L ] IsMonolithᵍ M

The monolith is unique up to mutual containment — two least nontrivial normal subgroups are each below the other — mirroring monolith-unique of Setoid.Congruences.Monolith.

  open IsMonolithᵍ public

  monolithᵍ-unique : (m m' : HasMonolithᵍ)
    →  (proj₁ m ⊆ proj₁ m') × (proj₁ m' ⊆ proj₁ m)
  monolithᵍ-unique (μ , mono) (μ' , mono') =
       mono   .least μ' (mono' .isMinimalNormal .normalSubgroup)
                        (mono' .isMinimalNormal .nontrivial)
    ,  mono'  .least μ  (mono  .isMinimalNormal .normalSubgroup)
                        (mono  .isMinimalNormal .nontrivial)

Abelian subgroups and centralizers

A subgroup is abelian when its elements commute with one another; such a subgroup lies inside its own centralizer, so a subgroup with trivial centralizer is either trivial or nonabelian. This is the whole content of the note's remark that a parachute representation has no nontrivial abelian normal subgroup.⁴

  -- N is abelian: its elements commute with each other.
  Abelian : Pred G L → Type (α ⊔ ρ ⊔ L)
  Abelian N = ∀ x y → x ∈ N → y ∈ N → x ∙ y ≈ y ∙ x

  -- An abelian subgroup centralizes itself.
  abelian→⊆-centralizer : {N : Pred G L} → Abelian N → N ⊆ C[ N ]
  abelian→⊆-centralizer ab {x} x∈N y y∈N = ab x y x∈N y∈N

  -- Hence an abelian subgroup whose centralizer is trivial is itself trivial.
  abelian-centralizer-trivial : {N : Pred G L}
    →  Abelian N → C[ N ] ⊆ Triv → N ⊆ Triv
  abelian-centralizer-trivial ab cent z = cent (abelian→⊆-centralizer ab z)

---

---

1. See arXiv:1205.1927v4, the footnote to § 3: "Recall, for groups subdirectly irreducible is equivalent to having a unique minimal normal subgroup." The universal-algebra-side notion is IsSubdirectlyIrreducible of Setoid.Congruences.Monolith, stated for the congruence lattice of an algebra; the two are identified by the correspondence between normal subgroups of G and congruences of G of Classical.Structures.Group.Congruences (see footnote 3). ↩↩

2. This is the step that turns the pairwise form of subdirect irreducibility into the least-element form the algebra-side IsMonolith of Setoid.Congruences.Monolith uses. ↩

3. The correspondence between the normal subgroups and the congruences of a group is formalized in Classical.Structures.Group.Congruences (M6-22). The transport of HasMonolithᵍ across it to the algebra-side HasMonolith has not been carried out; until it is, the superscript keeps the two notions apart rather than pretending they are the same definition. The simplicity instance of the same identification is proved in that module: the group-theoretic notion is equivalent to the congruence-level IsSimple of Setoid.Congruences.Simple, constructively in both directions. ↩

4. arXiv:1205.1927v4, the Remark after Lemma 3.7: "If N is abelian, then N ≤ C_G(N), so (i) implies that every nontrivial normal subgroup of G is nonabelian." ↩