Classical.Structures.Group.Subgroups¶
Subgroups of an arbitrary group¶
This is the Classical.Structures.Group.Subgroups module of the Agda Universal Algebra Library.
For a group 𝑮 presented as a Σ-typed structure over
Sig-Group (per Classical.Structures.Group), a
subgroup is a subset of the carrier that is closed under the three basic
operations; that is, a subuniverse of the underlying algebra in the sense of
Setoid.Subalgebras.Subuniverses.
This module generalizes the concrete treatment of the Klein four-group in Examples.Setoid.SubgroupLattice to an arbitrary group.
Because the carrier of a setoid algebra comes with a setoid equality
_≈_, a subset that is to play the role of a subgroup in
theorems (conjugation, cosets, Dedekind's rule) must also be compatible with
that equality. We therefore package a subgroup predicate as a record
IsSubgroup with two fields:
respects: the predicate respects the setoid equality (B Respects _≈_);isSubuniverse: the predicate is closed under the interpreted operations.
The first field is invisible in the classical (_≡_-setoid) case, where it holds by
subst, and is exactly what setoid-based group theory needs.
The second field alone already suffices to place the subgroup in the subuniverse lattice of Setoid.Subalgebras.CompleteLattice (see Classical.Structures.Group.SubgroupLattice).
The module also provides the curried closure toolkit: a subuniverse of a group
algebra is closed under the curried _∙_, contains ε,
and is closed under _⁻¹; and conversely those three closure properties
(together with respects) make a predicate a subgroup
(mkIsSubgroup). The trivial subgroup { x ∣ x ≈ ε } and the
full subgroup close the module.
Tuple-vs-curried interpretation bridges¶
The subuniverse machinery speaks of tuple-indexed operations (f ^ 𝑨) a, while
group theory speaks of the curried x ∙ y, ε, x ⁻¹ of Group-Op.
The two agree up to the setoid equality: (f ^ 𝑨) a applied to an arbitrary tuple
a equals the curried operation applied to the components of a, by congruence of
the interpretation (interp-cong). These three bridges are the only
place the mismatch is handled; everything downstream uses them.
module _ (𝑮 : Group α ρ) where private 𝑨 = proj₁ 𝑮 A = 𝕌[ 𝑨 ] open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open Group-Op 𝑮 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; ⁻¹-cong ; idˡ-law ) open GroupProperties ⟨ 𝑮 ⟩ᵍᵖ using ( ε⁻¹≈ε ) -- The binary operation on an arbitrary 2-tuple is the curried ∙ of its components. interp-tuple-∙ : (a : Fin 2 → A) → (∙-Op ^ 𝑨) a ≈ a 0F ∙ a 1F interp-tuple-∙ a = interp-cong 𝑨 ∙-Op λ { 0F → ≈refl ; 1F → ≈refl } -- The nullary operation on an arbitrary 0-tuple is the identity element ε. interp-tuple-ε : (a : Fin 0 → A) → (ε-Op ^ 𝑨) a ≈ ε interp-tuple-ε a = interp-cong 𝑨 ε-Op λ () -- The unary operation on an arbitrary 1-tuple is the curried ⁻¹ of its component. interp-tuple-⁻¹ : (a : Fin 1 → A) → (⁻¹-Op ^ 𝑨) a ≈ a 0F ⁻¹ interp-tuple-⁻¹ a = interp-cong 𝑨 ⁻¹-Op λ { 0F → ≈refl }
The curried closure toolkit¶
A subuniverse of the group algebra is closed under each curried operation. These are
definitional consequences of closure under the tuple-indexed operations, because the
curried accessors of Group-Op are defined by applying the interpreted
symbol to a canonical tuple.
module _ (B : Pred A ℓ) (B-sub : B ∈ Subuniverses 𝑨) where -- A subuniverse is closed under the curried group multiplication. sub-∙-closed : ∀ {x y} → x ∈ B → y ∈ B → x ∙ y ∈ B sub-∙-closed {x} {y} x∈B y∈B = B-sub ∙-Op (pair x y) im where im : (i : Fin 2) → pair x y i ∈ B im 0F = x∈B im 1F = y∈B -- A subuniverse contains the identity element (the nullary operation forces it). sub-ε-closed : ε ∈ B sub-ε-closed = B-sub ε-Op (λ ()) (λ ()) -- A subuniverse is closed under the curried inverse. sub-⁻¹-closed : ∀ {x} → x ∈ B → x ⁻¹ ∈ B sub-⁻¹-closed {x} x∈B = B-sub ⁻¹-Op (λ _ → x) (λ _ → x∈B)
The subgroup predicate¶
IsSubgroup B says the predicate B cuts out a subgroup: it respects the setoid
equality and is a subuniverse of the group algebra. The record module re-exports the
curried closure properties, so open IsSubgroup H-isSubgroup puts
∙-closed, ε-closed, ⁻¹-closed, and
respects in scope for a fixed subgroup.
record IsSubgroup (B : Pred A ℓ) : Type (α ⊔ ρ ⊔ ℓ) where field respects : B Respects _≈_ isSubuniverse : B ∈ Subuniverses 𝑨 ∙-closed : ∀ {x y} → x ∈ B → y ∈ B → x ∙ y ∈ B ∙-closed = sub-∙-closed B isSubuniverse ε-closed : ε ∈ B ε-closed = sub-ε-closed B isSubuniverse ⁻¹-closed : ∀ {x} → x ∈ B → x ⁻¹ ∈ B ⁻¹-closed = sub-⁻¹-closed B isSubuniverse
Conversely, an equality-respecting predicate that is closed under the three curried
operations is a subgroup: the tuple-indexed closure required by
Subuniverses follows from the curried closure by rewriting along the
interpretation bridges (this is the one direction that genuinely uses
respects).
mkIsSubgroup : {B : Pred A ℓ} → B Respects _≈_ → (∀ {x y} → x ∈ B → y ∈ B → x ∙ y ∈ B) → ε ∈ B → (∀ {x} → x ∈ B → x ⁻¹ ∈ B) → IsSubgroup B mkIsSubgroup {B = B} resp ∙-c ε-c ⁻¹-c = record { respects = resp ; isSubuniverse = isSub } where isSub : B ∈ Subuniverses 𝑨 isSub ∙-Op a im = resp (≈sym (interp-tuple-∙ a)) (∙-c (im 0F) (im 1F)) isSub ε-Op a im = resp (≈sym (interp-tuple-ε a)) ε-c isSub ⁻¹-Op a im = resp (≈sym (interp-tuple-⁻¹ a)) (⁻¹-c (im 0F))
The type of subgroups¶
A subgroup of 𝑮 at predicate level ℓ is a predicate on the carrier together with
a proof that it is a subgroup.
Subgroup : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ) Subgroup ℓ = Σ[ B ∈ Pred A ℓ ] IsSubgroup B
A decidable subgroup bundles a subgroup with a decision procedure for its
membership; this is the Layer-D presentation of a subgroup (ADR-008), mirroring how
DecCon of Setoid.Congruences.Finite.Basic bundles a
congruence with its decider. Decidability is genuine data here: it cannot be
derived from carrier finiteness, since a predicate on a finite carrier need
not be decidable.
DecSubgroup : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ) DecSubgroup ℓ = Σ[ B ∈ Subgroup ℓ ] (∀ x → Dec (x ∈ proj₁ B))
The trivial and full subgroups¶
The trivial subgroup is the ≈-class of the identity, { x ∣ x ≈ ε }; over a setoid
carrier the class, not the syntactic singleton, is the right notion. The full
subgroup is the whole carrier.
trivialSubgroup : Subgroup ρ trivialSubgroup = (λ x → x ≈ ε) , mkIsSubgroup resp ∙-c ε-c ⁻¹-c where resp : (λ x → x ≈ ε) Respects _≈_ resp x≈y x≈ε = ≈trans (≈sym x≈y) x≈ε ∙-c : ∀ {x y} → x ≈ ε → y ≈ ε → x ∙ y ≈ ε ∙-c x≈ε y≈ε = ≈trans (∙-cong x≈ε y≈ε) (idˡ-law ε) ε-c : ε ≈ ε ε-c = ≈refl ⁻¹-c : ∀ {x} → x ≈ ε → x ⁻¹ ≈ ε ⁻¹-c x≈ε = ≈trans (⁻¹-cong x≈ε) ε⁻¹≈ε fullSubgroup : (ℓ : Level) → Subgroup ℓ fullSubgroup ℓ = (λ _ → Lift ℓ ⊤) , mkIsSubgroup (λ _ _ → lift tt) (λ _ _ → lift tt) (lift tt) (λ _ → lift tt)