Skip to content

Classical.Structures.Group.MaximalSubgroup

Maximal subgroups

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

A maximal subgroup of G is a proper subgroup H such that no subgroup lies strictly between H and G; equivalently, the interval [H , G] in the subgroup lattice is the two-element chain. Groups with a core-free maximal subgroup are classically exactly the groups with a faithful primitive permutation action, which is why the notion matters to the enforcement catalog of FLRP.Reductions: core-free interval enforceability via a two-element chain constrains precisely this class of groups.

The definition is stated in the form the proofs consume, and that form deserves a constructive health warning. The field classify places every intermediate subgroup at H or at G as a disjunction, and producing that disjunction for an arbitrary equality-respecting predicate is oracle-strength data: a subgroup can encode an arbitrary proposition in its membership predicate (for any proposition P, the predicate Ξ» x β†’ x ∈ H ⊎ P respects equality and is closed under the group operations), so classify applied to such a predicate decides the proposition up to double negation. Consequently no concrete group can inhabit IsMaximalSubgroup in safe Agda; the record is a named classical hypothesis in the sense of the FLRP assumption discipline, inhabited by classical mathematics (where it is ordinary maximality) and consumed by theorems that are honest about assuming it. A decidable-membership sibling in the Layer-D style of ADR-008, quantifying only over subgroups packaged with decision procedures, would be constructible for concrete finite groups; it is deliberately not defined here because no present consumer needs it.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Structures.Group.MaximalSubgroup where

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

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Product     using  ( proj₁ )
open import Data.Sum.Base    using  ( _⊎_ )
open import Level            using  ( Level ; _βŠ”_ ) renaming ( suc to lsuc )
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 )
open import Classical.Structures.Group.Subgroups        using  ( IsSubgroup )
open import Classical.Structures.Group.SubgroupLattice  using  ( module GroupSublattice )
open import Setoid.Algebras.Basic                       using  ( π•Œ[_] )

The maximality record

Throughout, 𝒒 is a group and β„“β‚€ the base level of its subgroup lattice; subgroup predicates live at the resulting level L, exactly as in Classical.Structures.Group.MinimalNormal.

IsMaximalSubgroup H bundles the three conditions: H is a subgroup, it is proper (not every element lies in it, stated negatively because no argument below needs a witness), and every subgroup between H and the whole group is one of the two endpoints. Given H βŠ† K, the first disjunct K βŠ† H says the two predicates have the same extent, and the second says K is everything.

module MaximalSubgroup {Ξ± ρ : Level} (𝒒 : Group Ξ± ρ) (β„“β‚€ : Level) where
  private
    G = π•Œ[ proj₁ 𝒒 ]

  open GroupSublattice 𝒒 β„“β‚€  using  ( L )

  record IsMaximalSubgroup (H : Pred G L) : Type (Ξ± βŠ” ρ βŠ” lsuc L) where
    field
      isSubgroup  : IsSubgroup 𝒒 H
      proper      : Β¬ (βˆ€ x β†’ x ∈ H)
      classify    : (K : Pred G L) β†’ IsSubgroup 𝒒 K β†’ H βŠ† K
                  β†’ (K βŠ† H) ⊎ (βˆ€ x β†’ x ∈ K)

  open IsMaximalSubgroup public