Classical.Structures.Group.GSet¶
The coset G-set as a unary algebra¶
This is the Classical.Structures.Group.GSet module of the Agda Universal Algebra Library.
The transitive action of a group G on the coset space G / H is packaged here
as an ordinary unary algebra: the signature is
Sig-Unary applied to the carrier of G
(one operation symbol per group element, each of arity one) and the algebra's
domain is the quotient setoid cosetSetoid of
Classical.Structures.Group.Cosets. The symbol g acts by left translation,
x ↦ g ∙ x, which respects the coset equality by ∼-congˡ.
This encoding is chosen so that the library's congruence machinery applies to the
G-set verbatim: cosetAlgebra is an Algebra over
an ordinary signature, so Con cosetAlgebra means exactly what it means for any
algebra. (The module ends with a private demonstration.)1
We occasionally write G ↷ G / H to denote that the group G acts on the coset
space G / H, but we also use it to mean the algebra cosetAlgebra
that encodes this action; the context should make clear which is intended.
Note on the symbol set. Operation symbols form a type with propositional
equality, so two setoid-equal but distinct carrier elements give two symbols; they
act identically on G / H (by ∼-congˡ and ≈⇒∼), and a signature is raw syntax,
so this is harmless.
The action laws are stated with the curried operations, which is no loss: by the
definition of mkAlgebra, the interpretation of the symbol g at
x is definitionally g ∙ x, so act-identity and
act-compatible are literally the unit and compatibility laws of
the group action G ↷ G / H, and act-transitive says the action
is transitive: any coset is reached from any other by some group element.
The coset algebra¶
module CosetAction {α ρ : Level} (𝒢 : Group α ρ) {ℓ : Level} (H : Pred 𝕌[ proj₁ 𝒢 ] ℓ) (H-isSubgroup : IsSubgroup 𝒢 H) where private 𝑮 = proj₁ 𝒢 G = 𝕌[ 𝑮 ] open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; assoc-law ; idˡ-law ) open Coset 𝒢 H H-isSubgroup using ( _∼_ ; ∼-congˡ ; ≈⇒∼ ; cosetSetoid ) open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( //-rightDividesˡ ) -- The algebra G ↷ G / H over the unary signature on the carrier of G: -- the symbol g acts on the coset of x by left translation, g ∙ x. cosetAlgebra : Algebra {𝑆 = Sig-Unary G} α ℓ cosetAlgebra = mkAlgebra cosetSetoid (λ g a → g ∙ a 0F) (λ g u∼v → ∼-congˡ g (u∼v 0F))
Action laws and transitivity¶
As explained above, the coset space is a G-set: G acts on G / H by left
translation. The first two results we prove are the action laws; the third,
transitivity, is not an axiom but a further property this particular action
happens to have. Each is a one-line consequence of a group law transported across
≈⇒∼. (Recall, ≈⇒∼ says setoid equality refines coset equality:
∀ {x y} → x ≈ y → x ∼ y.)
act-identity: acting byεdoes nothing, fromidˡ-law.act-compatible: acting byg ∙ his acting byhand then byg, fromassoc-law.act-transitive: the action is transitive, and the witness is explicit:y ∙ x ⁻¹carries the coset ofxto that ofy.
Transitivity is the substantive one: it says G / H is a single orbit, which is
why a coset space is the model case of a transitive action. Since it is proved by
exhibiting a witness, the group element, rather than by an existence argument, the
result it usable computationally.
-- The identity element acts as the identity on cosets. act-identity : (x : G) → (ε ∙ x) ∼ x act-identity x = ≈⇒∼ (idˡ-law x) -- Acting by g ∙ h is acting by h, then by g. act-compatible : (g h x : G) → (g ∙ h) ∙ x ∼ g ∙ (h ∙ x) act-compatible g h x = ≈⇒∼ (assoc-law g h x) -- The action is transitive: y ∙ x ⁻¹ carries the coset of x to the coset of y. act-transitive : (x y : G) → Σ[ g ∈ G ] (g ∙ x) ∼ y act-transitive x y = y ∙ x ⁻¹ , ≈⇒∼ (//-rightDividesˡ x y)
Note that _∙_ has higher precedence than _∼_, so we could have written
(ε ∙ x) ∼ x as ε ∙ x ∼ x without ambiguity. Also, since _∙_ is
left-associative, we could have written g ∙ h ∙ x ∼ g ∙ (h ∙ x) in
act-compatible. We chose instead to make the laws readable even
without thinking about precedence conventions or associativity handedness.
Finiteness of the coset algebra¶
Carrier finiteness of the coset algebra is inherited from the group. The coset
space is the same carrier under the coarser equality _∼_, so the
group's surjective enumeration still hits every element (the finer _≈_
refines _∼_ by ≈⇒∼), and decidable coset equality
is exactly the decidability of _∼_, which is supplied by
∼-dec of Classical.Structures.Group.Cosets whenever membership
in H is decidable.2
open FiniteAlgebra -- A finite group with decidable coset equality has a finite coset algebra. cosetAlgebra-FiniteAlgebra : FiniteAlgebra 𝑮 → (∀ x y → Dec (x ∼ y)) → FiniteAlgebra cosetAlgebra cosetAlgebra-FiniteAlgebra fin dec ._≟_ = dec cosetAlgebra-FiniteAlgebra fin dec .card = fin .card cosetAlgebra-FiniteAlgebra fin dec .enum = fin .enum cosetAlgebra-FiniteAlgebra fin dec .enum-sur x = fin .enum-sur x .proj₁ , ≈⇒∼ (fin .enum-sur x .proj₂)
The congruence machinery applies verbatim¶
cosetAlgebra is an ordinary algebra, so its congruence lattice needs no new
definitions. The demonstration below type-checks against the stock
Con of Setoid.Congruences.Basic. Classically, this type is
isomorphic (as a lattice) to the interval [H, G] in Sub(G).1
private _ : Type (α ⊔ suc ℓ) _ = Con cosetAlgebra ℓ
-
The isomorphism
Con (G ↷ G / H) ≅ [H, G]is classical; it underlies the theorem of Pálfy and Pudlák (Algebra Universalis 11, 1980) relating congruence lattices of finite algebras to intervals in subgroup lattices of finite groups. ↩↩ -
This discharges, constructively, the finiteness hypothesis that applications of the Pálfy–Pudlák theorem place on the coset algebra. ↩