---
layout: default
file: "src/Classical/Structures/Group/Complements.lagda.md"
title: "Classical.Structures.Group.Complements module"
date: "2026-07-25"
author: "the agda-algebras development team"
---
### Permuting complements in an interval of the subgroup lattice
This is the [Classical.Structures.Group.Complements][] module of the [Agda Universal Algebra Library][].
Fix subgroups `H ≤ G` and an intermediate subgroup `A ∈ [H , G]`.
A **complement of `A` in the interval `[H , G]`** is a subgroup `B ∈ [H , G]` with
`A ∩ B = H` and `⟨A , B⟩ = G`.
This module proves Corollary 3.5 of the *Interval Enforceable Properties* note:[^1]
> If ℬ is a nonempty set of complements of `A` in `[H , G]` every member of which
> permutes with `A`, then `ℬ` is an antichain.
The proof is one application of Dedekind's rule
([Classical.Structures.Group.Dedekind][]):
for all `B₁ , B₂ ∈ ℬ`, if `B₁ ≤ B₂` then
B₁ = B₁H = B₁(A ∩ B₂) = B₁A ∩ B₂ = G ∩ B₂ = B₂.
Thus no strict containment is possible.
**Complements, formalized through the complex product**.
Two of the note's hypotheses — that `B` permutes with `A` (`AB = BA`) and that `A`
and `B` join to `G` — are used only through their conjunction, which is the single
statement `BA = G`; that is, the *complex product* `B ∙ᶜ A` of
[Classical.Structures.Group.Complexes][] is the whole group.
We call that statement `Factors`{.AgdaFunction} and take it as the primitive.
It is exactly equivalent to the note's pair of hypotheses — for a permuting pair of
subgroups `⟨A , B⟩ = AB` — and it keeps the argument free of the *generated*
subgroup, whose inductive presentation would otherwise have to be unfolded.
The join hypothesis is recovered where consumers need it: a factorization of `G` is
inherited by any subgroup containing `A` and `B` (`Factors-least`{.AgdaFunction}),
which is the universal property of the join.
The module also collects the small facts about complex products that the argument and
its FLRP consumers need: a permuting product of subgroups is a subgroup
(`permuting-∙ᶜ-isSubgroup`{.AgdaFunction}), a normal subgroup permutes with
every subgroup (`normal-permutes`{.AgdaFunction}), hence `NB` is a subgroup for `N`
normal (`normal-∙ᶜ-isSubgroup`{.AgdaFunction}).
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Classical.Structures.Group.Complements where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Product using ( _,_ ; proj₁ ; proj₂ ; _×_)
open import Level using ( Level ; _⊔_ )
open import Function using ( id ; _∘_ )
open import Relation.Binary using ( Setoid )
open import Relation.Unary using ( Pred ; _∈_ ; _⊆_ ; _∩_ ; _≐_ )
import Algebra.Properties.Group as GroupProperties
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Classical.Bundles.Group using ( ⟨_⟩ᵍᵖ )
open import Classical.Signatures.Group using ( Sig-Group )
open import Classical.Structures.Group.Basic using ( Group ; module Group-Op )
open import Classical.Structures.Group.Complexes using ( module Complex )
open import Classical.Structures.Group.Conjugation using ( module Conjugate )
open import Classical.Structures.Group.Dedekind using ( dedekindˡ )
open import Classical.Structures.Group.Subgroups using ( IsSubgroup ; mkIsSubgroup )
open import Setoid.Algebras.Basic using ( Algebra ; 𝕌[_] ; 𝔻[_] )
private variable ℓᵃ ℓᵇ ℓᶜ ℓʰ ℓⁿ : Level
```
-->
#### The toolkit
```agda
module Complements {α ρ : Level} (𝒢 : Group α ρ) where
private
𝑮 : Algebra {𝑆 = Sig-Group} α ρ
𝑮 = proj₁ 𝒢
open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( Carrier to G ; refl to ≈refl
; sym to ≈sym ; trans to ≈trans )
open SetoidReasoning 𝔻[ 𝑮 ]
open Group-Op 𝒢
open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ⁻¹-involutive ; ⁻¹-anti-homo-∙ )
open Complex 𝒢 using ( _∙ᶜ_ ; mem-∙ᶜ ; ∙ᶜ-respects ; ∙ᶜ-mono ; subgroup-∙ᶜ-idem )
open Conjugate 𝒢 using ( conj-syntax ; IsNormal )
```
A member of one factor is a member of the product, provided the *other* factor
contains the identity — the two one-sided inclusions `P ⊆ P Q` and `Q ⊆ P Q`.
```agda
mem-∙ᶜˡ : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} → ε ∈ Q → P ⊆ P ∙ᶜ Q
mem-∙ᶜˡ {P = P} {Q} ε∈Q {x} x∈P = ∙ᶜ-respects P Q (idʳ-law x) (mem-∙ᶜ x∈P ε∈Q)
mem-∙ᶜʳ : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} → ε ∈ P → Q ⊆ P ∙ᶜ Q
mem-∙ᶜʳ {P = P} {Q} ε∈P {x} x∈Q = ∙ᶜ-respects P Q (idˡ-law x) (mem-∙ᶜ ε∈P x∈Q)
```
#### Permuting subsets
Two subsets **permute** when their complex products in the two orders agree. This
is the note's hypothesis on the members of `ℬ`, and it is what makes the product
`A B` a subgroup rather than a mere subset.
```agda
infix 4 _permutes_
_permutes_ : Pred G ℓᵃ → Pred G ℓᵇ → Type (α ⊔ ρ ⊔ ℓᵃ ⊔ ℓᵇ)
P permutes Q = P ∙ᶜ Q ≐ Q ∙ᶜ P
```
The product of two permuting subgroups is a subgroup. Closure under `∙` is the one
step that consumes permutation: in `(a₁b₁)(a₂b₂)` the middle pair `b₁a₂` is
rewritten as some `a₃b₃`, after which associativity regroups the four factors.
```agda
permuting-∙ᶜ-isSubgroup : {A : Pred G ℓᵃ} {B : Pred G ℓᵇ}
→ IsSubgroup 𝒢 A → IsSubgroup 𝒢 B → A permutes B → IsSubgroup 𝒢 (A ∙ᶜ B)
permuting-∙ᶜ-isSubgroup {A = A} {B} A-sg B-sg (AB⊆BA , BA⊆AB) =
mkIsSubgroup 𝒢 (∙ᶜ-respects A B) ∙-c ε-c ⁻¹-c
where
open IsSubgroup A-sg using () renaming ( ∙-closed to A∙ ; ε-closed to Aε ; ⁻¹-closed to A⁻¹ )
open IsSubgroup B-sg using () renaming ( ∙-closed to B∙ ; ε-closed to Bε ; ⁻¹-closed to B⁻¹ )
ε-c : ε ∈ A ∙ᶜ B
ε-c = ∙ᶜ-respects A B (idˡ-law ε) (mem-∙ᶜ Aε Bε)
∙-c : ∀ {x y} → x ∈ A ∙ᶜ B → y ∈ A ∙ᶜ B → x ∙ y ∈ A ∙ᶜ B
∙-c {x} {y} (a₁ , b₁ , a₁∈A , b₁∈B , x≈a₁b₁) (a₂ , b₂ , a₂∈A , b₂∈B , y≈a₂b₂) =
∙ᶜ-respects A B (≈sym regroup) (mem-∙ᶜ (A∙ a₁∈A a₃∈A) (B∙ b₃∈B b₂∈B))
where
swap : b₁ ∙ a₂ ∈ A ∙ᶜ B
swap = BA⊆AB (mem-∙ᶜ b₁∈B a₂∈A)
a₃ b₃ : G
a₃ = swap .proj₁
b₃ = swap .proj₂ .proj₁
ξ : a₃ ∈ A × b₃ ∈ B × b₁ ∙ a₂ ≈ a₃ ∙ b₃
ξ = swap .proj₂ .proj₂
a₃∈A : a₃ ∈ A
a₃∈A = ξ .proj₁
b₃∈B : b₃ ∈ B
b₃∈B = ξ .proj₂ .proj₁
b₁a₂≈a₃b₃ : b₁ ∙ a₂ ≈ a₃ ∙ b₃
b₁a₂≈a₃b₃ = ξ .proj₂ .proj₂
regroup : x ∙ y ≈ (a₁ ∙ a₃) ∙ (b₃ ∙ b₂)
regroup = begin
x ∙ y ≈⟨ ∙-cong x≈a₁b₁ y≈a₂b₂ ⟩
a₁ ∙ b₁ ∙ (a₂ ∙ b₂) ≈˘⟨ assoc-law (a₁ ∙ b₁) a₂ b₂ ⟩
a₁ ∙ b₁ ∙ a₂ ∙ b₂ ≈⟨ ∙-cong (assoc-law a₁ b₁ a₂) ≈refl ⟩
a₁ ∙ (b₁ ∙ a₂) ∙ b₂ ≈⟨ ∙-cong (∙-cong ≈refl b₁a₂≈a₃b₃) ≈refl ⟩
a₁ ∙ (a₃ ∙ b₃) ∙ b₂ ≈˘⟨ ∙-cong (assoc-law a₁ a₃ b₃) ≈refl ⟩
a₁ ∙ a₃ ∙ b₃ ∙ b₂ ≈⟨ assoc-law (a₁ ∙ a₃) b₃ b₂ ⟩
a₁ ∙ a₃ ∙ (b₃ ∙ b₂) ∎
⁻¹-c : ∀ {x} → x ∈ A ∙ᶜ B → x ⁻¹ ∈ A ∙ᶜ B
⁻¹-c {x} (a , b , a∈A , b∈B , x≈ab) =
BA⊆AB (∙ᶜ-respects B A (≈sym anti) (mem-∙ᶜ (B⁻¹ b∈B) (A⁻¹ a∈A)))
where
anti : x ⁻¹ ≈ b ⁻¹ ∙ a ⁻¹
anti = ≈trans (⁻¹-cong x≈ab) (⁻¹-anti-homo-∙ a b)
```
#### Normal subgroups permute with everything
A normal subgroup permutes with every subset: `n b ≈ b (b⁻¹ n b)` moves a normal
element across a factor, and `(b n b⁻¹) b ≈ b n` moves it back. Consequently `N B`
is a subgroup whenever `N` is normal and both are subgroups — this is the subgroup
`NH` of the parachute argument.
```agda
private
swapˡ : ∀ b n → b ∙ n ^ (b ⁻¹) ≈ n ∙ b
swapˡ b n = begin
b ∙ (b ⁻¹ ∙ n ∙ (b ⁻¹) ⁻¹) ≈⟨ ∙-cong ≈refl (∙-cong ≈refl (⁻¹-involutive b)) ⟩
b ∙ (b ⁻¹ ∙ n ∙ b) ≈˘⟨ assoc-law b (b ⁻¹ ∙ n) b ⟩
b ∙ (b ⁻¹ ∙ n) ∙ b ≈˘⟨ ∙-cong (assoc-law b (b ⁻¹) n) ≈refl ⟩
b ∙ b ⁻¹ ∙ n ∙ b ≈⟨ ∙-cong (∙-cong (invʳ-law b) ≈refl) ≈refl ⟩
ε ∙ n ∙ b ≈⟨ ∙-cong (idˡ-law n) ≈refl ⟩
n ∙ b ∎
swapʳ : ∀ b n → n ^ b ∙ b ≈ b ∙ n
swapʳ b n = begin
b ∙ n ∙ b ⁻¹ ∙ b ≈⟨ assoc-law (b ∙ n) (b ⁻¹) b ⟩
b ∙ n ∙ (b ⁻¹ ∙ b) ≈⟨ ∙-cong ≈refl (invˡ-law b) ⟩
b ∙ n ∙ ε ≈⟨ idʳ-law (b ∙ n) ⟩
b ∙ n ∎
normal-permutes : {N : Pred G ℓⁿ} (B : Pred G ℓᵇ) → IsNormal N → N permutes B
normal-permutes {N = N} B N-normal = to , from
where
to : N ∙ᶜ B ⊆ B ∙ᶜ N
to (n , b , n∈N , b∈B , x≈nb) =
b , n ^ (b ⁻¹) , b∈B , N-normal (b ⁻¹) n∈N , ≈trans x≈nb (≈sym (swapˡ b n))
from : B ∙ᶜ N ⊆ N ∙ᶜ B
from (b , n , b∈B , n∈N , x≈bn) =
n ^ b , b , N-normal b n∈N , b∈B , ≈trans x≈bn (≈sym (swapʳ b n))
normal-∙ᶜ-isSubgroup : {N : Pred G ℓⁿ} {B : Pred G ℓᵇ}
→ IsNormal N → IsSubgroup 𝒢 N → IsSubgroup 𝒢 B → IsSubgroup 𝒢 (N ∙ᶜ B)
normal-∙ᶜ-isSubgroup {B = B} N-normal N-sg B-sg =
permuting-∙ᶜ-isSubgroup N-sg B-sg (normal-permutes B N-normal)
```
#### Factorizations of the group
`Factors P Q` says the complex product `P Q` exhausts the group. For subgroups
this is the note's "`P` and `Q` permute and `⟨P , Q⟩ = G`", packaged as one
statement: it is symmetric (invert a factorization elementwise), and it is inherited
by every subgroup above both factors, which is the join's universal property.
```agda
Factors : Pred G ℓᵃ → Pred G ℓᵇ → Type (α ⊔ ρ ⊔ ℓᵃ ⊔ ℓᵇ)
Factors P Q = ∀ (x : G) → x ∈ P ∙ᶜ Q
Factors-sym : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ}
→ IsSubgroup 𝒢 P → IsSubgroup 𝒢 Q → Factors P Q → Factors Q P
Factors-sym {P = P} {Q} P-sg Q-sg fact x = ∙ᶜ-respects Q P (≈sym anti) mem
where
open IsSubgroup P-sg using () renaming ( ⁻¹-closed to P⁻¹ )
open IsSubgroup Q-sg using () renaming ( ⁻¹-closed to Q⁻¹ )
p q : G
p = fact (x ⁻¹) .proj₁
q = fact (x ⁻¹) .proj₂ .proj₁
ξ : p ∈ P × q ∈ Q × x ⁻¹ ≈ p ∙ q
ξ = fact (x ⁻¹) .proj₂ .proj₂
p∈P : p ∈ P
p∈P = ξ .proj₁
q∈Q : q ∈ Q
q∈Q = ξ .proj₂ .proj₁
x⁻¹≈pq : x ⁻¹ ≈ p ∙ q
x⁻¹≈pq = ξ .proj₂ .proj₂
anti : x ≈ q ⁻¹ ∙ p ⁻¹
anti = begin
x ≈˘⟨ ⁻¹-involutive x ⟩
(x ⁻¹) ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈pq ⟩
(p ∙ q) ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ p q ⟩
q ⁻¹ ∙ p ⁻¹ ∎
mem : q ⁻¹ ∙ p ⁻¹ ∈ Q ∙ᶜ P
mem = mem-∙ᶜ (Q⁻¹ q∈Q) (P⁻¹ p∈P)
Factors-least : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} {C : Pred G ℓᶜ}
→ IsSubgroup 𝒢 C → P ⊆ C → Q ⊆ C → Factors P Q → (x : G) → x ∈ C
Factors-least {C = C} C-sg P⊆C Q⊆C fact x =
proj₁ (subgroup-∙ᶜ-idem C-sg) (∙ᶜ-mono P⊆C Q⊆C (fact x))
```
#### Corollary 3.5: comparable permuting complements collapse
The heart of the matter, in the form the parachute argument uses: if `B₁ ≤ B₂` are
subgroups of the interval `[H , G]`, if `B₂` meets `A` at `H`, and if `B₁ A = G`,
then already `B₂ ≤ B₁`. Reading the note's chain of equalities from the right, an
element `x ∈ B₂` lies in `B₁A ∩ B₂`, hence in `B₁(A ∩ B₂)` (by Dedekind's rule, which
applies because `B₁ ≤ B₂` and `B₂` is a subgroup). The meet hypothesis
shrinks the second factor to `H ⊆ B₁`, and `B₁B₁ = B₁` collapses the product.
```agda
complement-⊆-collapse : {H : Pred G ℓʰ} {A : Pred G ℓᵃ} {B₁ B₂ : Pred G ℓᵇ}
→ IsSubgroup 𝒢 B₁ → IsSubgroup 𝒢 B₂
→ H ⊆ B₁ → B₁ ⊆ B₂ → A ∩ B₂ ⊆ H → Factors B₁ A → B₂ ⊆ B₁
complement-⊆-collapse {A = A} {B₁} {B₂} B₁-sg B₂-sg H⊆B₁ B₁⊆B₂ meet-⊆ fact {x} x∈B₂ =
proj₁ (subgroup-∙ᶜ-idem B₁-sg) inside
where
step₁ : x ∈ (B₁ ∙ᶜ A) ∩ B₂
step₁ = fact x , x∈B₂
step₂ : x ∈ B₁ ∙ᶜ (A ∩ B₂)
step₂ = proj₂ (dedekindˡ 𝒢 B₂-sg B₁⊆B₂) step₁
inside : x ∈ B₁ ∙ᶜ B₁
inside = ∙ᶜ-mono id (H⊆B₁ ∘ meet-⊆ ) step₂
```
An **antichain** of subgroups, indexed by a type `I`, is a family in which no member
is contained in another except when the containment reverses — the constructive
reading of "pairwise incomparable" for subsets ordered by inclusion, where equality
*is* mutual containment.
**Corollary 3.5**. If `H ≤ A ≤ G` and if every group in `ℬ ⊆ [H , G]` permutes with
`A`, then `ℬ` is an antichain.
```agda
Antichain : {I : Type ℓᶜ} → (I → Pred G ℓᵇ) → Type (ℓᶜ ⊔ α ⊔ ℓᵇ)
Antichain {I = I} ℬ = (i j : I) → ℬ i ⊆ ℬ j → ℬ j ⊆ ℬ i
complements-antichain : {I : Type ℓᶜ} {H : Pred G ℓʰ} {A : Pred G ℓᵃ}
(ℬ : I → Pred G ℓᵇ) → (∀ i → IsSubgroup 𝒢 (ℬ i))
→ (∀ i → H ⊆ ℬ i)
→ (∀ i → A ∩ ℬ i ⊆ H)
→ (∀ i → Factors (ℬ i) A)
→ Antichain ℬ
complements-antichain ℬ ℬ-sg H⊆ℬ meet fact i j ℬi⊆ℬj =
complement-⊆-collapse (ℬ-sg i) (ℬ-sg j) (H⊆ℬ i) ℬi⊆ℬj (meet j) (fact i)
```
---
[^1]: `docs/papers/flrp/ieprops/IEProps-1205.1927v4.tex`, § 3.2 (Dedekind's rule)
and § 3.3 (parachute lattices); see also
[`docs/notes/flrp-research-roadmap.md`](docs/notes/flrp-research-roadmap.md) § 4
and the design note `docs/notes/flrp-rp1-parachutes.md`.