---
layout: default
file: "src/Classical/Structures/Group/SubgroupLattice.lagda.md"
title: "Classical.Structures.Group.SubgroupLattice module"
date: "2026-07-11"
author: "the agda-algebras development team"
---

### The subgroup lattice of an arbitrary group

This is the [Classical.Structures.Group.SubgroupLattice][] module of the [Agda Universal Algebra Library][].

For a group `𝑮`{.AgdaBound} over [`Sig-Group`][Classical.Signatures.Group], the
subuniverses of the underlying algebra form a complete lattice under inclusion — this
is exactly the `Sublattice`{.AgdaModule} construction of
[Setoid.Subalgebras.CompleteLattice][], instantiated at the group algebra.  Because
`Sig-Group` carries the binary `∙-Op`, the nullary `ε-Op`, and the unary `⁻¹-Op`, a
subuniverse of the group algebra is precisely a subgroup, so this instance *is* the
subgroup lattice `Sub(G)`.  This module packages the instantiation once, as the
parameterized module `GroupSublattice`{.AgdaModule}, generalizing what
[Examples.Setoid.SubgroupLattice][] does concretely for the Klein four-group.

Opening `GroupSublattice 𝑮 ℓ₀` re-exports the whole `Sublattice`{.AgdaModule} kit
specialized to the group algebra — the carrier `Subᴸ`{.AgdaFunction}, the inclusion
order `_≤_`{.AgdaFunction}, binary `_∧_`{.AgdaFunction}/`_∨_`{.AgdaFunction}, bounds
`0ˢ`{.AgdaFunction}/`1ˢ`{.AgdaFunction}, infinitary `⨅`{.AgdaFunction}/`⨆`{.AgdaFunction},
and the stdlib lattice bundles — and adds the group-specific facts below.

On the relationship with `IsSubgroup`{.AgdaRecord} of
[Classical.Structures.Group.Subgroups][]: the lattice elements are *bare*
subuniverses, which is all the lattice structure needs; equality-respecting subgroups
embed into the lattice by forgetting `respects`{.AgdaField}
(`subgroup→Subᴸ`{.AgdaFunction}), and the respecting property is preserved by the meets
(`∧-isSubgroup`{.AgdaFunction}, `⨅-isSubgroup`{.AgdaFunction}) since these are plain
intersections.  It is *not* automatically preserved by the joins, because the join is
the inductively *generated* subuniverse `Sg (B ∪ C)`, whose `app` constructor pins
exact elements rather than ≈-classes; a respecting join would take the ≈-saturation of
`Sg`, which we leave for future work.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Structures.Group.SubgroupLattice where

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

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Product    using ( _,_ ; proj₁ ; proj₂ )
open import Level           using ( Level )
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.Subgroups  using ( IsSubgroup ; sub-ε-closed )
open import Order.Interval                        using ( module IntervalLattice )
open import Setoid.Algebras.Basic                 using ( 𝕌[_] )
open import Setoid.Subalgebras.CompleteLattice    using ( module Sublattice )
```
-->

#### The instantiation

`GroupSublattice 𝑮 ℓ₀` is `Sublattice` applied to the underlying algebra of `𝑮`,
with the base level `ℓ₀` of the `Sublattice` construction left as a parameter (the
lattice's predicates live at the absorbing level `L = α ⊔ ℓ₀`, since the two
signature levels of `Sig-Group` are zero).

```agda
module GroupSublattice {α ρ : Level} (𝒢 : Group α ρ) (ℓ₀ : Level) where
  private
    𝑮 = proj₁ 𝒢
    G = 𝕌[ 𝑮 ]

  open Group-Op 𝒢 using ( ε )

  open Sublattice 𝑮 ℓ₀ public
```

#### Group-specific facts

Every subuniverse of a group algebra contains the identity element — the nullary
operation symbol `ε-Op` forces it.  In particular every lattice element is nonempty,
and the lattice bottom `0ˢ = Sg ∅` is the subuniverse generated by the identity.

```agda
  -- Every member of the subgroup lattice contains the identity element.
  ε-mem : (B : Subᴸ) → ε ∈ proj₁ B
  ε-mem (B , Bsub) = sub-ε-closed 𝒢 B Bsub
```

An equality-respecting subgroup (at the lattice's predicate level `L`) is an element
of the lattice, by forgetting the `respects`{.AgdaField} field.

```agda
  -- Embed a respecting subgroup into the subuniverse lattice.
  subgroup→Subᴸ : (B : Pred G L) → IsSubgroup 𝒢 B → Subᴸ
  subgroup→Subᴸ B B-sg = B , IsSubgroup.isSubuniverse B-sg
```

The meet operations preserve the respecting property, because binary meet and
infinitary meet are the (pointwise) intersections of the underlying predicates.

```agda
  -- The binary meet of two respecting subgroups is a respecting subgroup.
  ∧-isSubgroup : (B C : Subᴸ)
    →  IsSubgroup 𝒢 (proj₁ B) → IsSubgroup 𝒢 (proj₁ C)
    →  IsSubgroup 𝒢 (proj₁ (B ∧ C))
  ∧-isSubgroup B C B-sg C-sg = record
    { respects       = λ x≈y x∈ →  IsSubgroup.respects B-sg x≈y (proj₁ x∈)
                                ,  IsSubgroup.respects C-sg x≈y (proj₂ x∈)
    ; isSubuniverse  = proj₂ (B ∧ C)
    }

  -- The infinitary meet of a family of respecting subgroups is a respecting subgroup.
  ⨅-isSubgroup : {I : Type ℓ₀} (𝒜 : I → Subᴸ)
    →  (∀ i → IsSubgroup 𝒢 (proj₁ (𝒜 i)))
    →  IsSubgroup 𝒢 (proj₁ (⨅ 𝒜))
  ⨅-isSubgroup 𝒜 sg = record
    { respects       = λ x≈y x∈ i → IsSubgroup.respects (sg i) x≈y (x∈ i)
    ; isSubuniverse  = proj₂ (⨅ 𝒜)
    }
```

#### Upper intervals

An upper interval `[B, C]` in the subgroup lattice — the subgroups sandwiched
between `B` and `C` — is a bounded lattice, by the generic interval construction of
[Order.Interval][] applied to the lattice bundle `Sub-Lattice`{.AgdaFunction}.
Opening `SubInterval B C B≤C` provides the interval carrier, its order, and the
`Lattice`/`BoundedLattice` bundles; the FLRP-side intervals `[H, G]` of the
Pálfy–Pudlák correspondence are the instances with `C` the full subgroup.

```agda
  module SubInterval (B C : Subᴸ) (B≤C : B ≤ C) = IntervalLattice Sub-Lattice B C B≤C
```