Classical.Structures.Group.SubgroupLattice¶
The subgroup lattice of an arbitrary group¶
This is the Classical.Structures.Group.SubgroupLattice module of the Agda Universal Algebra Library.
For a group 𝑮 over Sig-Group, the
subuniverses of the underlying algebra form a complete lattice under inclusion — this
is exactly the Sublattice 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, generalizing what
Examples.Setoid.SubgroupLattice does concretely for the Klein four-group.
Opening GroupSublattice 𝑮 ℓ₀ re-exports the whole Sublattice kit
specialized to the group algebra — the carrier Subᴸ, the inclusion
order _≤_, binary _∧_/_∨_, bounds
0ˢ/1ˢ, infinitary ⨅/⨆,
and the stdlib lattice bundles — and adds the group-specific facts below.
On the relationship with IsSubgroup 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
(subgroup→Subᴸ), and the respecting property is preserved by the meets
(∧-isSubgroup, ⨅-isSubgroup) 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.
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).
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.
-- 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 field.
-- 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.
-- 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.
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.
module SubInterval (B C : Subᴸ) (B≤C : B ≤ C) = IntervalLattice Sub-Lattice B C B≤C