Classical.Structures.Group.RegularAction¶
The regular action and its congruence–subgroup correspondence¶
This is the Classical.Structures.Group.RegularAction module of the Agda Universal Algebra Library.
Instantiating the coset G-set of Classical.Structures.Group.GSet at the
trivial subgroup gives the (left-)regular action G ↷ G, packaged as a unary
algebra whose operations are the left translations x ↦ g ∙ x. This module
records the classical correspondence for that instance.
- congruence ⟶ subgroup (
Kθ): theθ-class of the identity is a subgroup, decided (at Layer D) byθ's own decision procedure at the pair(ε , g); - subgroup ⟶ congruence (
cosetCon): the left-coset relationx ⁻¹ ∙ y ∈ Kof any equality-respecting subgroupKis a congruence of the regular action, decided by one group multiplication once membership inKis decidable; - the two maps are mutually inverse (
cosetCon-Kθ,Kθ-cosetCon) and monotone in both directions (cosetCon-mono,cosetCon-reflect).
In words: the congruence lattice of the regular action is the full subgroup
lattice Sub(G). This is the H = 1 instance of the Pálfy–Pudlák
correspondence Con (G ↷ G/H) ≅ [H , G], whose general form, stated over the
respecting interval at both layers, is the WP-3 bridge FLRP.Bridge. The
instance is restated here, in the Classical/ tree, for two reasons.
First, layering: Classical/ cannot import FLRP/, and the consumers of the
regular action are not FLRP-specific (any development wanting Sub G as a
concrete congruence lattice can use this module).
Second, the trivial-subgroup instance needs none of the interval apparatus:
"subgroup above the trivial subgroup" is no constraint at all; reflexivity of the
coset congruence over the carrier's coset equality is exactly ε-closedness plus
respects. Therefore, the statements simplify to plain
Subgroups and DecSubgroups.
The FLRP consumer of this module is the ambient-closedness step of Snow's
filter-ideal lemma: both concrete filter-ideal instances present their ambient
lattice as Sub(G) = Con (G ↷ G), with the translations as the ambient
operations, so "every congruence respecting the translations is a coset
partition" is cosetCon-Kθ; no unary-reduction theorem is
consumed.
A note on opacity¶
Several definitions below are sealed in opaque blocks; the
scale at which this module is used makes the use of opaque
load-bearing rather than stylistic. A concrete instance, the alternating group
A5 on 60 points (used in the L16 representation) carries group-law witnesses
that are from-yes of decision sweeps over the whole carrier.
Those witnesses sit inside the group bundle that every type here mentions, so a
goal comparing the coset congruences of two named subgroups will, if nothing
blocks it, normalize the entire tower; measured, one such comparison exhausted a
32 GB heap. Sealing the proofs stops the unfolding at a name and costs nothing,
since no consumer needs a subgroup axiom or a round-trip proof to compute, only
to exist.
Two further consequences shape the code below: the coset relation is written out
directly instead of through a Coset module application (a module
application at a concrete subgroup re-instantiates that module, and
Algebra.Properties.Group with it), and every function taking a subgroup reads it
through proj₁ / proj₂ rather than a pattern match,
so its result reduces without forcing the argument open.
The regular action¶
The development is parameterized by a group; the coset machinery is
instantiated at the trivial subgroup, so the carrier's coset equality _∼_
identifies exactly the ≈-equal elements (via one group computation), and the
CosetAction exports below are the regular action.
module Regular {α ρ : Level} (𝒢@(𝑮 , _) : Group α ρ) where open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; idˡ-law ; idʳ-law ; invˡ-law ) open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ε⁻¹≈ε ; \\-leftDividesˡ ) -- The trivial subgroup (the ≈-class of ε) and its coset machinery. H₁ : Pred 𝕌[ 𝑮 ] ρ H₁ = trivialSubgroup 𝒢 .proj₁ H₁-sg : IsSubgroup 𝒢 H₁ H₁-sg = trivialSubgroup 𝒢 .proj₂ open Coset 𝒢 H₁ H₁-sg using ( _∼_ ; ≈⇒∼ ; ∼-dec ; ∼-refl ) open CosetAction 𝒢 H₁ H₁-sg public using ( cosetAlgebra ; cosetAlgebra-FiniteAlgebra ) -- Membership in the trivial subgroup is decided by one equality test, so a -- finite group makes the regular action a finite algebra. regular-FiniteAlgebra : FiniteAlgebra 𝑮 → FiniteAlgebra cosetAlgebra regular-FiniteAlgebra fin = cosetAlgebra-FiniteAlgebra fin (∼-dec (_≟ ε)) where open FiniteAlgebra fin
Elementary facts about a congruence of the regular action¶
As in the general bridge: a congruence is reflexive over the coset equality,
symmetric, transitive, and invariant under every left translation. One
group-arithmetic fact (ε⁻¹∙) serves the round trips.
module _ {ℓ : Level} where private module _ ((_θ_ , θcon) : Con cosetAlgebra ℓ) where θ-refl : ∀ {a b} → a ∼ b → a θ b θ-refl = reflexive θcon θ-sym : ∀ {a b} → a θ b → b θ a θ-sym = IsEquivalence.sym (is-equivalence θcon) θ-trans : ∀ {a b c} → a θ b → b θ c → a θ c θ-trans = IsEquivalence.trans (is-equivalence θcon) -- Compatibility of θ with the unary operation symbol g: left translation. θ-transl : (g : 𝕌[ 𝑮 ]) {a b : 𝕌[ 𝑮 ]} → a θ b → (g ∙ a) θ (g ∙ b) θ-transl g {a} {b} p = is-compatible θcon g {λ _ → a} {λ _ → b} (λ _ → p) ε⁻¹∙ : (a : 𝕌[ 𝑮 ]) → ε ⁻¹ ∙ a ≈ a ε⁻¹∙ a = ≈trans (∙-cong ε⁻¹≈ε ≈refl) (idˡ-law a)
Congruence to subgroup: the class of the identity¶
Kθ θ is the θ-class of ε, read as a predicate on the
carrier. The subgroup obligations are the same short congruence computations
as in the general bridge, unchanged by the specialization.
-- The θ-class of the identity. Kθ : Con cosetAlgebra ℓ → Pred 𝕌[ 𝑮 ] ℓ Kθ (_θ_ , _) g = ε θ g private Kθ-ε : (θ : Con cosetAlgebra ℓ) → ε ∈ Kθ θ Kθ-ε θ = θ-refl θ ∼-refl -- IsEquivalence.refl (is-equivalence θcon) Kθ-∙ : (θ : Con cosetAlgebra ℓ) {x y : 𝕌[ 𝑮 ]} → x ∈ Kθ θ → y ∈ Kθ θ → x ∙ y ∈ Kθ θ Kθ-∙ θ {x} {y} εx εy = θ-trans θ εx (θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law x)))) (θ-transl θ x εy)) Kθ-⁻¹ : (θ : Con cosetAlgebra ℓ) {x : 𝕌[ 𝑮 ]} → x ∈ Kθ θ → x ⁻¹ ∈ Kθ θ Kθ-⁻¹ θ {x} εx = θ-sym θ (θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law (x ⁻¹))))) (θ-trans θ (θ-transl θ (x ⁻¹) εx) (θ-refl θ (≈⇒∼ (invˡ-law x))))) Kθ-resp : (θ : Con cosetAlgebra ℓ) → ∀ {x y} → x ≈ y → x ∈ Kθ θ → y ∈ Kθ θ Kθ-resp θ x≈y εx = θ-trans θ εx (θ-refl θ (≈⇒∼ x≈y)) -- The θ-class of the identity is a subgroup; the axioms are sealed. opaque Kθ-isSubgroup : (θ : Con cosetAlgebra ℓ) → IsSubgroup 𝒢 (Kθ θ) Kθ-isSubgroup θ = mkIsSubgroup 𝒢 (Kθ-resp θ) (Kθ-∙ θ) (Kθ-ε θ) (Kθ-⁻¹ θ) Kθ-subgroup : Con cosetAlgebra ℓ → Subgroup 𝒢 ℓ Kθ-subgroup θ = Kθ θ , Kθ-isSubgroup θ -- At Layer D: a decidable congruence decides membership in its own -- ε-class, by running its decision procedure at (ε , g). Kθᵈ : DecCon cosetAlgebra ℓ → DecSubgroup 𝒢 ℓ Kθᵈ (θ , θdec) = Kθ-subgroup θ , θdec ε
Subgroup to congruence: the coset partition¶
For any subgroup K, the left-coset relation of K is a congruence of the
regular action. Reflexivity over the (trivial-subgroup) coset equality is where
"every subgroup lies above the trivial subgroup" enters: an element of the trivial
subgroup is ≈ ε, hence in K by respects and ε-closedness. The
equivalence and translation-compatibility are the stock Coset
lemmas at K; this is consumed once, generically, inside the opaque block, so
that no call site re-instantiates them.
-- The left-coset relation of K: x and y agree modulo K. cosetRel : Subgroup 𝒢 ℓ → 𝕌[ 𝑮 ] → 𝕌[ 𝑮 ] → Type ℓ cosetRel (K , _) x y = x ⁻¹ ∙ y ∈ K opaque cosetIsCongruence : (𝑲 : Subgroup 𝒢 ℓ) → IsCongruence cosetAlgebra (cosetRel 𝑲) cosetIsCongruence (K , K-sg) = mkcon reflx ∼-isEquivalence compatx where open Coset 𝒢 K K-sg using (∼-isEquivalence ; ∼-congˡ) open IsSubgroup K-sg using (respects ; ε-closed) reflx : {a b : 𝕌[ 𝑮 ]} → a ∼ b → cosetRel (K , K-sg) a b reflx a∼b = respects (≈sym a∼b) ε-closed compatx : cosetAlgebra ∣≈ cosetRel (K , K-sg) compatx g h = ∼-congˡ g (h 0F) cosetCon : Subgroup 𝒢 ℓ → Con cosetAlgebra ℓ cosetCon K = cosetRel K , cosetIsCongruence K -- At Layer D: the coset partition of a decidable subgroup is decided by -- one group multiplication and one membership test. cosetConᵈ : DecSubgroup 𝒢 ℓ → DecCon cosetAlgebra ℓ cosetConᵈ (𝑲 , 𝑲-dec) = cosetCon 𝑲 , λ x y → 𝑲-dec (x ⁻¹ ∙ y)
Mutual inverseness and monotonicity¶
Every congruence of the regular action is the coset partition of its ε-class
(cosetCon-Kθ); this is the ambient-closedness fact the
filter-ideal applications consume. Every subgroup is recovered from its coset
partition (Kθ-cosetCon). Containment transfers both ways, so the
correspondence is an order isomorphism between Con (G ↷ G) and Sub(G).
opaque -- Round trip on congruences: the coset partition of the ε-class is θ. cosetCon-Kθ : (θ : Con cosetAlgebra ℓ) → cosetCon (Kθ-subgroup θ) ≑ θ cosetCon-Kθ θ = fwd , bwd where fwd : cosetCon (Kθ-subgroup θ) ⊑ θ fwd {x} {y} q = θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law x)))) (θ-trans θ (θ-transl θ x q) (θ-refl θ (≈⇒∼ (\\-leftDividesˡ x y)))) bwd : θ ⊑ cosetCon (Kθ-subgroup θ) bwd {x} {y} p = θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (invˡ-law x)))) (θ-transl θ (x ⁻¹) p) -- Round trip on subgroups: the ε-class of the coset partition is K. Kθ-cosetCon : (K : Subgroup 𝒢 ℓ) → (Kθ (cosetCon K) ⊆ K .proj₁) × (K .proj₁ ⊆ Kθ (cosetCon K)) Kθ-cosetCon (_ , K-sg) = (λ {g} → respects (ε⁻¹∙ g)) , λ {g} → respects (≈sym (ε⁻¹∙ g)) where open IsSubgroup K-sg using (respects) -- Subgroup containment forwards to coset-partition containment ... cosetCon-mono : (K L : Subgroup 𝒢 ℓ) → proj₁ K ⊆ proj₁ L → cosetCon K ⊑ cosetCon L cosetCon-mono K L K⊆L p = K⊆L p -- ... and reflects back, through the ε-class. cosetCon-reflect : (K L : Subgroup 𝒢 ℓ) → cosetCon K ⊑ cosetCon L → K .proj₁ ⊆ L .proj₁ cosetCon-reflect (_ , Ksub) (_ , Lsub) sub {x} x∈K = IsSubgroup.respects Lsub (ε⁻¹∙ x) (sub (IsSubgroup.respects Ksub (≈sym (ε⁻¹∙ x)) x∈K))