Classical.Structures.Group.Congruences¶
Normal subgroups and congruences of a group¶
This is the Classical.Structures.Group.Congruences module of the Agda Universal Algebra Library.
The normal subgroups of a group 𝒢 correspond to the congruences of the underlying
Sig-Group-algebra. This module establishes that correspondence as an order
isomorphism of posets, between the congruence poset (Con 𝑮 ℓ , ≑ , ⊑) of
Setoid.Congruences.Lattice and the poset (NormalSubgroup ℓ , ≈ⁿ , ≤ⁿ) of normal
subgroups under inclusion, which is built here.
Both sides carry more structure than a poset: at the absorbing level L the
congruences form a complete lattice (Setoid.Congruences.CompleteLattice). The
corresponding isomorphism of complete lattices is
Classical.Structures.Group.NormalSubgroupLattice, which stands on the poset
isomorphism proved here. The split is deliberate: the correspondence below holds at
every relation level, whereas a lattice needs the single absorbing level at which
the join — a generated congruence — stays put, so bundling them would have narrowed
the theorem to the level the lattice happens to need.
The correspondence has two mutually inverse, order-preserving maps.
-
N ↦ θ_N(congruenceOf). A normal subgroupNmaps to the relationNormalRelN, defined byx θ_N y ⟺ x ∙ y ⁻¹ ∈ N. We prove that this is an equivalence containing the setoid equality (for whichNbeing an equality-respecting subgroup is enough) and compatible with the three operations ofSig-Group, which is where normality is consumed. -
θ ↦ N_θ(normalOf). A congruenceθmaps to theθ-class of the identity; we define the latter asIdentityClassθ, which represents the predicate{ x ∣ x θ ε }. We prove it is a normal, equality-respecting subgroup.
The two maps are monotone and mutually inverse — up to ≑ on
congruences and mutual inclusion on normal subgroups — so together they are an
OrderIso of Order.Iso.
This is the bridge that Classical.Structures.Group.MinimalNormal was written
without: it lets us apply the library's IsSubdirectlyIrreducible of
Setoid.Congruences.Monolith — a statement about Con 𝑨 — to a
group, whose subdirect irreducibility the group theorist states as "there is a
least nontrivial normal subgroup". The final step of that identification,
HasMonolithᵍ → HasMonolith, is deliberately not taken here; see What this module
does not do below.
Four points about the formal statement deserve to be recorded up front, because in each case the informal slogan "congruences are normal subgroups" conceals a choice that the mechanized version has to make.
-
The correspondence is level-uniform, not level-collapsing. It relates
Con 𝑮 ℓtoNormalSubgroup ℓfor each fixed relation levelℓ, sinceNormalRelof aPred G ℓis aBinaryRel G ℓandIdentityClassof aCon 𝑮 ℓis aPred G ℓ. It says nothing about congruences at one level versus normal subgroups at another. Three instances matter downstream:ℓ = ρ, where the congruence side is theCon 𝑮 ρofIsMonolithand the subgroup side containstrivialSubgroup, itself aSubgroup ρ;ℓ = α ⊔ ρ ⊔ ℓ₀, the absorbing level of the congruence lattice, which is where Classical.Structures.Group.NormalSubgroupLattice instantiates it; andℓ = α ⊔ ℓ₀, the predicate levelLat whichGroupSublattice 𝒢 ℓ₀of Classical.Structures.Group.SubgroupLattice holds its elements, for a consumer that wants to compose with the subgroup lattice. -
Equality on each side is mutual containment, not propositional equality. On the congruence side this is
_≑_of Setoid.Congruences.Lattice, for the reasons given there (upgrading it would need propositional extensionality, which--safe --cubical-compatibledoes not provide); on the subgroup side we take the matching_≈ⁿ_. Soto∘fromandfrom∘toare bi-implications of membership, not equalities of predicates. -
The round trip on subgroups uses the
respectsfield. RecoveringNfromθ_Nproduces{ x ∣ x ∙ ε ⁻¹ ∈ N }, and identifying that withNmoves membership acrossx ∙ ε ⁻¹ ≈ x. A normal subuniverse that does not respect the setoid equality therefore need not be recovered by the round trip, exactly as in the respecting-interval finding of FLRP.Bridge. This is whyNormalSubgroupis built onIsSubgroup(which carriesrespects) rather than on bareSubuniverses. -
Normality is consumed only by compatibility, and it is consumed exactly. For an arbitrary equality-respecting subgroup
N,NormalRel Nis already an equivalence relation containing_≈_; this isSubgroupRelbelow, and it holds with no normality hypothesis. What needs normality is compatibility with∙-Opand⁻¹-Op, so the separation is stated rather than folded into one monolithic lemma — and the conversecongruence→normalis proved, so that "the correspondence is with the normal subgroups" is a theorem of the module and not a claim its prose makes on the development's behalf.
On the choice of relation. x ∙ y ⁻¹ ∈ N is the right-coset relation of
N, whereas Coset._∼_ of
Classical.Structures.Group.Cosets — the relation FLRP.Bridge uses — is the
left-coset relation x ⁻¹ ∙ y ∈ N. For a general subgroup the two need not agree;
for a normal subgroup they do, which we prove (rel→coset,
coset→rel) rather than assume, so that either presentation may be used
downstream.
What this module does not do. Issue #508 also asks that
HasMonolithᵍ of Classical.Structures.Group.MinimalNormal be
transported to HasMonolith, that the ᵍ superscript be retired, and
that 𝒢₂ of FLRP.Reductions be restated. Those steps are held back until the pull
request that introduces MinimalNormal lands; everything above is independent of them.
The Nonzero/nontriviality equivalences proved here
(nonzero→nontrivial and friends) are precisely the ingredient that
transport will need beyond the isomorphism itself.
The ambient group¶
Everything below is developed inside one parameterized module, so that the group, its carrier, its curried operations, and the conjugation vocabulary are fixed once.
module GroupCongruences {α ρ : Level} (𝒢 : Group α ρ) where private 𝑮 = proj₁ 𝒢 G = 𝕌[ 𝑮 ] open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open SetoidReasoning 𝔻[ 𝑮 ] open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; assoc-law ; idˡ-law ; idʳ-law ; invˡ-law ; invʳ-law ) open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ε⁻¹≈ε ; ⁻¹-involutive ; ⁻¹-anti-homo-∙ ; \\-leftDividesʳ ) open Conjugate 𝒢 using ( conj-syntax ; conj-ε ; IsNormal )
Four facts of group arithmetic¶
The correspondence rests on four small identities, each named so that no proof below
has to inline an equational chain about them. The first two say that x ∙ y ⁻¹ ≈ ε
is equivalent to x ≈ y — this is what makes the relation x ∙ y ⁻¹ ∈ N collapse to
the setoid equality exactly when N is trivial. The third is right-cancellation in the
form the round trip needs, and the fourth is the unit law that identifies x ∙ ε ⁻¹
with x.
-- x ∙ y ⁻¹ ≈ ε implies x ≈ y (multiply on the right by y). ∙⁻¹≈ε→≈ : ∀ {x y} → x ∙ y ⁻¹ ≈ ε → x ≈ y ∙⁻¹≈ε→≈ {x} {y} h = begin x ≈˘⟨ idʳ-law x ⟩ x ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law y) ⟩ x ∙ (y ⁻¹ ∙ y) ≈˘⟨ assoc-law x (y ⁻¹) y ⟩ x ∙ y ⁻¹ ∙ y ≈⟨ ∙-cong h ≈refl ⟩ ε ∙ y ≈⟨ idˡ-law y ⟩ y ∎ -- ... and conversely, equal elements have trivial right quotient. ≈→∙⁻¹≈ε : ∀ {x y} → x ≈ y → x ∙ y ⁻¹ ≈ ε ≈→∙⁻¹≈ε {x} {y} x≈y = ≈trans (∙-cong x≈y ≈refl) (invʳ-law y) -- Right cancellation: the right quotient by y, multiplied back by y, is the identity. ∙⁻¹∙ : ∀ x y → x ∙ y ⁻¹ ∙ y ≈ x ∙⁻¹∙ x y = begin x ∙ y ⁻¹ ∙ y ≈⟨ assoc-law x (y ⁻¹) y ⟩ x ∙ (y ⁻¹ ∙ y) ≈⟨ ∙-cong ≈refl (invˡ-law y) ⟩ x ∙ ε ≈⟨ idʳ-law x ⟩ x ∎ -- The right quotient by the identity is the identity map. ∙ε⁻¹ : ∀ x → x ∙ ε ⁻¹ ≈ x ∙ε⁻¹ x = ≈trans (∙-cong ≈refl ε⁻¹≈ε) (idʳ-law x)
Normal subgroups as an ordered object¶
A normal subgroup of 𝒢 at predicate level ℓ is a
predicate on the carrier together with a proof that it is an equality-respecting
subgroup and a proof that it is closed under conjugation. This is
Subgroup of Classical.Structures.Group.Subgroups with
IsNormal of Classical.Structures.Group.Conjugation adjoined; it is
introduced here rather than there because normality is the only extra datum the
correspondence needs, and no earlier module had cause to bundle it.
Normal subgroups are ordered by inclusion of the underlying predicates, with equality
mutual inclusion — the same shape as _⊑_ and _≑_ on
congruences, so that the isomorphism below can be stated without any bridging
construction on either side.
-- A normal subgroup: an equality-respecting subgroup closed under conjugation. NormalSubgroup : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ) NormalSubgroup ℓ = Σ[ N ∈ Pred G ℓ ] (IsSubgroup 𝒢 N × IsNormal N) -- The underlying predicate of a normal subgroup ... set : NormalSubgroup ℓ → Pred G ℓ set (N , _ , _) = N -- ... and its two proof components. set-isSubgroup : (𝑵 : NormalSubgroup ℓ) → IsSubgroup 𝒢 (set 𝑵) set-isSubgroup (_ , isSubgroup , _) = isSubgroup set-normal : (𝑵 : NormalSubgroup ℓ) → IsNormal (set 𝑵) set-normal (_ , _ , isNormal) = isNormal infix 4 _≤ⁿ_ _≈ⁿ_ -- The inclusion order on normal subgroups ... _≤ⁿ_ : NormalSubgroup ℓ → NormalSubgroup ℓ → Type (α ⊔ ℓ) 𝑴 ≤ⁿ 𝑵 = set 𝑴 ⊆ set 𝑵 -- ... and the equivalence of mutual inclusion it is antisymmetric over. _≈ⁿ_ : NormalSubgroup ℓ → NormalSubgroup ℓ → Type (α ⊔ ℓ) 𝑴 ≈ⁿ 𝑵 = 𝑴 ≤ⁿ 𝑵 × 𝑵 ≤ⁿ 𝑴
Calling the correspondence an order isomorphism presupposes that both sides really
are ordered, so the partial-order laws are proved rather than assumed. They are the
laws of _⊆_ on predicates, and antisymmetry holds by construction:
_≈ⁿ_ is mutual inclusion. This mirrors
⊆-isPartialOrder and Con-Poset on the congruence
side, down to the same implicit-argument discipline — _≤ⁿ_ is a
defined relation, not an injective type former, so Agda cannot recover the endpoint
arguments of the helper lemmas from the expected field types and they are forwarded by
hand.
≤ⁿ-refl : {𝑵 : NormalSubgroup ℓ} → 𝑵 ≤ⁿ 𝑵 ≤ⁿ-refl p = p ≤ⁿ-trans : {𝑳 𝑴 𝑵 : NormalSubgroup ℓ} → 𝑳 ≤ⁿ 𝑴 → 𝑴 ≤ⁿ 𝑵 → 𝑳 ≤ⁿ 𝑵 ≤ⁿ-trans 𝑳≤𝑴 𝑴≤𝑵 p = 𝑴≤𝑵 (𝑳≤𝑴 p) ≈ⁿ-refl : {𝑵 : NormalSubgroup ℓ} → 𝑵 ≈ⁿ 𝑵 ≈ⁿ-refl = (λ p → p) , (λ p → p) ≈ⁿ-sym : {𝑴 𝑵 : NormalSubgroup ℓ} → 𝑴 ≈ⁿ 𝑵 → 𝑵 ≈ⁿ 𝑴 ≈ⁿ-sym = swap ≈ⁿ-trans : {𝑳 𝑴 𝑵 : NormalSubgroup ℓ} → 𝑳 ≈ⁿ 𝑴 → 𝑴 ≈ⁿ 𝑵 → 𝑳 ≈ⁿ 𝑵 ≈ⁿ-trans (𝑳≤𝑴 , 𝑴≤𝑳) (𝑴≤𝑵 , 𝑵≤𝑴) = (λ p → 𝑴≤𝑵 (𝑳≤𝑴 p)) , (λ p → 𝑴≤𝑳 (𝑵≤𝑴 p)) ≈ⁿ-isEquivalence : IsEquivalence (_≈ⁿ_ {ℓ}) ≈ⁿ-isEquivalence {ℓ} = record { refl = λ {𝑵} → ≈ⁿ-refl {ℓ} {𝑵} ; sym = λ {𝑴} {𝑵} → ≈ⁿ-sym {ℓ} {𝑴} {𝑵} ; trans = λ {𝑳} {𝑴} {𝑵} → ≈ⁿ-trans {ℓ} {𝑳} {𝑴} {𝑵} } ≤ⁿ-isPartialOrder : IsPartialOrder (_≈ⁿ_ {ℓ}) _≤ⁿ_ ≤ⁿ-isPartialOrder {ℓ} = record { isPreorder = record { isEquivalence = ≈ⁿ-isEquivalence {ℓ} ; reflexive = proj₁ ; trans = λ {𝑳} {𝑴} {𝑵} → ≤ⁿ-trans {ℓ} {𝑳} {𝑴} {𝑵} } ; antisym = _,_ } -- The poset of normal subgroups, the counterpart of `Con-Poset` of -- [Setoid.Congruences.Lattice][]. NormalSubgroup-Poset : (ℓ : Level) → Poset (α ⊔ ρ ⊔ suc ℓ) (α ⊔ ℓ) (α ⊔ ℓ) NormalSubgroup-Poset ℓ = record { Carrier = NormalSubgroup ℓ ; _≈_ = _≈ⁿ_ ; _≤_ = _≤ⁿ_ ; isPartialOrder = ≤ⁿ-isPartialOrder }
The relation attached to a subgroup¶
NormalRel N is the relation "x and y differ by an element of
N", written with the right quotient x ∙ y ⁻¹. It is defined for an arbitrary
predicate, so that the hypotheses each of its properties needs can be stated exactly.
-- x and y are related when their right quotient lies in N. NormalRel : Pred G ℓ → BinaryRel G ℓ NormalRel N x y = x ∙ y ⁻¹ ∈ N
For an equality-respecting subgroup N — with no normality hypothesis —
NormalRel N is an equivalence relation that contains the setoid
equality. Each clause is one closure property of N transported along one
line of group arithmetic, exactly as in Coset of
Classical.Structures.Group.Cosets for the left-handed relation.
module SubgroupRel {ℓ : Level} (N : Pred G ℓ) (N-sg : IsSubgroup 𝒢 N) where open IsSubgroup N-sg using ( respects ; ∙-closed ; ε-closed ; ⁻¹-closed ) infix 4 _∼_ _∼_ : BinaryRel G ℓ _∼_ = NormalRel N -- Reflexivity is ε ∈ N transported along x ∙ x ⁻¹ ≈ ε. ∼-refl : ∀ {x} → x ∼ x ∼-refl {x} = respects (≈sym (invʳ-law x)) ε-closed -- Symmetry is closure under inverses, since (x ∙ y ⁻¹) ⁻¹ ≈ y ∙ x ⁻¹. ∼-sym : ∀ {x y} → x ∼ y → y ∼ x ∼-sym {x} {y} x∼y = respects inv-eq (⁻¹-closed x∼y) where inv-eq : (x ∙ y ⁻¹) ⁻¹ ≈ y ∙ x ⁻¹ inv-eq = begin (x ∙ y ⁻¹) ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩ (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-cong (⁻¹-involutive y) ≈refl ⟩ y ∙ x ⁻¹ ∎ -- Transitivity is closure under products, since (x ∙ y ⁻¹) ∙ (y ∙ z ⁻¹) ≈ x ∙ z ⁻¹. ∼-trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z ∼-trans {x} {y} {z} x∼y y∼z = respects prod-eq (∙-closed x∼y y∼z) where prod-eq : (x ∙ y ⁻¹) ∙ (y ∙ z ⁻¹) ≈ x ∙ z ⁻¹ prod-eq = begin (x ∙ y ⁻¹) ∙ (y ∙ z ⁻¹) ≈⟨ assoc-law x (y ⁻¹) (y ∙ z ⁻¹) ⟩ x ∙ (y ⁻¹ ∙ (y ∙ z ⁻¹)) ≈⟨ ∙-cong ≈refl (\\-leftDividesʳ y (z ⁻¹)) ⟩ x ∙ z ⁻¹ ∎ ∼-isEquivalence : IsEquivalence _∼_ ∼-isEquivalence = record { refl = ∼-refl ; sym = ∼-sym ; trans = ∼-trans } -- The setoid equality refines the relation (this is the `reflexive` field a -- congruence must supply, and it is what makes the relation contain the diagonal). ≈⇒∼ : ∀ {x y} → x ≈ y → x ∼ y ≈⇒∼ x≈y = respects (≈sym (≈→∙⁻¹≈ε x≈y)) ε-closed -- Consequently the relation may be transported along ≈ in either argument. ∼-resp : ∀ {x x' y y'} → x ≈ x' → y ≈ y' → x ∼ y → x' ∼ y' ∼-resp x≈x' y≈y' p = ∼-trans (∼-trans (≈⇒∼ (≈sym x≈x')) p) (≈⇒∼ y≈y')
From a normal subgroup to a congruence¶
Adding normality makes the relation compatible with the three operations of
Sig-Group, hence a congruence.
Compatibility with ∙-Op is the substantive clause and the
only one that uses normality in an essential way: from x ∙ y ⁻¹ ∈ N and
u ∙ v ⁻¹ ∈ N we must produce (x ∙ u) ∙ (y ∙ v) ⁻¹ ∈ N, and the two given elements do
not multiply to it — one of them must first be moved past x, which is
precisely conjugation. Compatibility with ⁻¹-Op is one
conjugation as well; with ε-Op it is reflexivity.
module NormalCon {ℓ : Level} (𝑵 : NormalSubgroup ℓ) where private N : Pred G ℓ N = set 𝑵 open IsSubgroup (set-isSubgroup 𝑵) using ( respects ; ∙-closed ) open SubgroupRel N (set-isSubgroup 𝑵) public normal : IsNormal N normal = set-normal 𝑵 -- Compatibility with the curried multiplication. The element x ∙ y ⁻¹ is on the -- wrong side of x ∙ u, so u ∙ v ⁻¹ is first conjugated by x — the one step that -- normality supplies and that fails for a non-normal subgroup. ∼-∙ : ∀ {x y u v} → x ∼ y → u ∼ v → (x ∙ u) ∼ (y ∙ v) ∼-∙ {x} {y} {u} {v} p q = respects step (∙-closed (normal x q) p) where step : x ∙ (u ∙ v ⁻¹) ∙ x ⁻¹ ∙ (x ∙ y ⁻¹) ≈ x ∙ u ∙ (y ∙ v) ⁻¹ step = begin x ∙ (u ∙ v ⁻¹) ∙ x ⁻¹ ∙ (x ∙ y ⁻¹) ≈⟨ assoc-law (x ∙ (u ∙ v ⁻¹)) (x ⁻¹) (x ∙ y ⁻¹) ⟩ x ∙ (u ∙ v ⁻¹) ∙ (x ⁻¹ ∙ (x ∙ y ⁻¹)) ≈⟨ ∙-cong ≈refl (\\-leftDividesʳ x (y ⁻¹)) ⟩ x ∙ (u ∙ v ⁻¹) ∙ y ⁻¹ ≈˘⟨ ∙-cong (assoc-law x u (v ⁻¹)) ≈refl ⟩ x ∙ u ∙ v ⁻¹ ∙ y ⁻¹ ≈⟨ assoc-law (x ∙ u) (v ⁻¹) (y ⁻¹) ⟩ x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹) ≈˘⟨ ∙-cong ≈refl (⁻¹-anti-homo-∙ y v) ⟩ x ∙ u ∙ (y ∙ v) ⁻¹ ∎ -- Compatibility with the curried inverse: conjugating x ∙ y ⁻¹ by x ⁻¹ produces -- y ⁻¹ ∙ (x ⁻¹) ⁻¹, which is the relation the other way round. ∼-⁻¹ : ∀ {x y} → x ∼ y → x ⁻¹ ∼ y ⁻¹ ∼-⁻¹ {x} {y} p = ∼-sym (respects step (normal (x ⁻¹) p)) where step : x ⁻¹ ∙ (x ∙ y ⁻¹) ∙ (x ⁻¹) ⁻¹ ≈ y ⁻¹ ∙ (x ⁻¹) ⁻¹ step = ∙-cong (\\-leftDividesʳ x (y ⁻¹)) ≈refl -- Compatibility with every operation symbol. Each clause is the corresponding -- curried fact, transported across the tuple-vs-curried interpretation bridges of -- [Classical.Structures.Group.Subgroups]. ∼-compatible : 𝑮 ∣≈ _∼_ ∼-compatible ∙-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-∙ 𝒢 u)) (≈sym (interp-tuple-∙ 𝒢 v)) (∼-∙ (p 0F) (p 1F)) ∼-compatible ε-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-ε 𝒢 u)) (≈sym (interp-tuple-ε 𝒢 v)) ∼-refl ∼-compatible ⁻¹-Op {u} {v} p = ∼-resp (≈sym (interp-tuple-⁻¹ 𝒢 u)) (≈sym (interp-tuple-⁻¹ 𝒢 v)) (∼-⁻¹ (p 0F)) -- The relation of a normal subgroup is a congruence of the group algebra. ∼-isCongruence : IsCongruence 𝑮 _∼_ ∼-isCongruence = mkcon ≈⇒∼ ∼-isEquivalence ∼-compatible
For a normal subgroup the right-handed relation used here agrees with the left-handed
coset relation Coset._∼_ of Classical.Structures.Group.Cosets,
which is the one FLRP.Bridge builds on. Both directions are one application of
∼-⁻¹ followed by an involutivity rewrite, so nothing about the
development depends on which of the two presentations a consumer prefers.
-- The right-coset relation of a normal subgroup is its left-coset relation ... rel→coset : ∀ {x y} → x ∼ y → Coset._∼_ 𝒢 N (set-isSubgroup 𝑵) x y rel→coset {x} {y} p = respects (∙-cong ≈refl (⁻¹-involutive y)) (∼-⁻¹ p) -- ... and conversely. coset→rel : ∀ {x y} → Coset._∼_ 𝒢 N (set-isSubgroup 𝑵) x y → x ∼ y coset→rel {x} {y} p = ∼-resp (⁻¹-involutive x) (⁻¹-involutive y) (∼-⁻¹ (respects (∙-cong ≈refl (≈sym (⁻¹-involutive y))) p))
The forward map of the correspondence packages the relation with its congruence proof.
-- N ↦ θ_N : a normal subgroup gives a congruence of the group algebra. congruenceOf : NormalSubgroup ℓ → Con 𝑮 ℓ congruenceOf 𝑵 = NormalRel (set 𝑵) , NormalCon.∼-isCongruence 𝑵
From a congruence to a normal subgroup¶
In the other direction the ingredients are the curried consequences of a congruence's
compatibility: it is preserved by multiplication, by inversion, and hence by
conjugation. These are read off from is-compatible at the canonical
tuples, with no interpretation bridge needed — the curried accessors of
Group-Op are defined by applying the interpreted symbol to exactly
those tuples.
module ConNormal {ℓ : Level} ((_θ_ , θcon) : Con 𝑮 ℓ) where θ-refl : ∀ {x} → x θ x θ-refl = IsEquivalence.refl (is-equivalence θcon) θ-trans : ∀ {x y z} → x θ y → y θ z → x θ z θ-trans = IsEquivalence.trans (is-equivalence θcon) -- A congruence relates ≈-equal elements. θ-reflexive : ∀ {x y} → x ≈ y → x θ y θ-reflexive = reflexive θcon -- Compatibility with the curried multiplication ... θ-∙ : ∀ {x y u v} → x θ y → u θ v → (x ∙ u) θ (y ∙ v) θ-∙ {x} {y} {u} {v} p q = is-compatible θcon ∙-Op λ { 0F → p ; 1F → q } -- ... and with the curried inverse. θ-⁻¹ : ∀ {x y} → x θ y → (x ⁻¹) θ (y ⁻¹) θ-⁻¹ p = is-compatible θcon ⁻¹-Op (λ _ → p) -- Hence conjugation by any element preserves the congruence. θ-conj : ∀ g {x y} → x θ y → x ^ g θ y ^ g θ-conj g {x} {y} p = θ-∙ (θ-∙ (θ-refl {x = g}) p) (θ-refl {x = g ⁻¹})
The class of the identity is an equality-respecting subgroup, and it is normal.
Membership is x θ ε, so each subgroup law is one application of the corresponding
compatibility fact followed by a ≈-step that renormalizes the right-hand side back to
ε: ε ∙ ε ≈ ε, ε ⁻¹ ≈ ε, and conj g ε ≈ ε.
-- The θ-class of the identity. IdentityClass : Pred G ℓ IdentityClass x = x θ ε -- It respects the setoid equality, because a congruence contains it. IdentityClass-respects : IdentityClass Respects _≈_ IdentityClass-respects x≈y p = θ-trans (θ-reflexive (≈sym x≈y)) p IdentityClass-ε : ε ∈ IdentityClass IdentityClass-ε = θ-refl IdentityClass-∙ : ∀ {x y} → x ∈ IdentityClass → y ∈ IdentityClass → x ∙ y ∈ IdentityClass IdentityClass-∙ p q = θ-trans (θ-∙ p q) (θ-reflexive (idˡ-law ε)) IdentityClass-⁻¹ : ∀ {x} → x ∈ IdentityClass → x ⁻¹ ∈ IdentityClass IdentityClass-⁻¹ p = θ-trans (θ-⁻¹ p) (θ-reflexive ε⁻¹≈ε) -- The identity class is an equality-respecting subgroup ... IdentityClass-isSubgroup : IsSubgroup 𝒢 IdentityClass IdentityClass-isSubgroup = mkIsSubgroup 𝒢 IdentityClass-respects IdentityClass-∙ IdentityClass-ε IdentityClass-⁻¹ -- ... and it is normal, since conjugation fixes the identity. IdentityClass-normal : IsNormal IdentityClass IdentityClass-normal g p = θ-trans (θ-conj g p) (θ-reflexive (conj-ε g))
The backward map of the correspondence packages the class with its two proofs.
-- θ ↦ N_θ : a congruence gives a normal subgroup of the group. normalOf : Con 𝑮 ℓ → NormalSubgroup ℓ normalOf θ = ConNormal.IdentityClass θ , ConNormal.IdentityClass-isSubgroup θ , ConNormal.IdentityClass-normal θ
Normality is necessary, not merely sufficient¶
NormalCon shows normality suffices for NormalRel N to
be a congruence. The converse holds too, and is worth proving rather than asserting:
were it left as prose, the claim "the correspondence is with the normal subgroups"
would be doing work the formal development had not done, and nothing would rule out the
relation of some non-normal subgroup slipping into Con 𝑮 ℓ.
The proof needs no new group arithmetic. If NormalRel N is a
congruence, its identity class is normal by
IdentityClass-normal — and that class is
{ x ∣ x ∙ ε ⁻¹ ∈ N }, which respects identifies with
N itself.
-- If the relation of an equality-respecting subgroup is a congruence, the subgroup -- is normal. With `NormalCon.∼-isCongruence` this makes normality *equivalent* to -- compatibility, so `NormalSubgroup ℓ` is exactly the source of the correspondence. congruence→normal : {ℓ : Level} (N : Pred G ℓ) → IsSubgroup 𝒢 N → IsCongruence 𝑮 (NormalRel N) → IsNormal N congruence→normal N N-sg isCon g {x} x∈N = respects (∙ε⁻¹ (x ^ g)) (ConNormal.IdentityClass-normal (NormalRel N , isCon) g (respects (≈sym (∙ε⁻¹ x)) x∈N)) where open IsSubgroup N-sg using ( respects )
Monotonicity¶
Both maps act by (co)restriction of the underlying predicates and relations, so monotonicity is immediate in each direction.
-- The congruence-to-subgroup map is monotone. normalOf-mono : (θ φ : Con 𝑮 ℓ) → θ ⊑ φ → normalOf θ ≤ⁿ normalOf φ normalOf-mono _ _ θ⊑φ p = θ⊑φ p -- The subgroup-to-congruence map is monotone. congruenceOf-mono : (𝑴 𝑵 : NormalSubgroup ℓ) → 𝑴 ≤ⁿ 𝑵 → congruenceOf 𝑴 ⊑ congruenceOf 𝑵 congruenceOf-mono _ _ 𝑴≤𝑵 p = 𝑴≤𝑵 p
OrderIso asks only for monotonicity, not for the maps to be well defined
on equivalence classes, so that latter property — which "isomorphism of posets" is
usually taken to include — is recorded here rather than left implicit. It costs
nothing: each equivalence is mutual containment, so applying the matching
monotonicity twice suffices.
-- Both maps respect the equivalences of the two sides. normalOf-cong : (θ φ : Con 𝑮 ℓ) → θ ≑ φ → normalOf θ ≈ⁿ normalOf φ normalOf-cong θ φ (θ⊑φ , φ⊑θ) = normalOf-mono θ φ θ⊑φ , normalOf-mono φ θ φ⊑θ congruenceOf-cong : (𝑴 𝑵 : NormalSubgroup ℓ) → 𝑴 ≈ⁿ 𝑵 → congruenceOf 𝑴 ≑ congruenceOf 𝑵 congruenceOf-cong 𝑴 𝑵 (𝑴≤𝑵 , 𝑵≤𝑴) = congruenceOf-mono 𝑴 𝑵 𝑴≤𝑵 , congruenceOf-mono 𝑵 𝑴 𝑵≤𝑴
Mutual inverseness¶
On congruences, θ_{N_θ} ≑ θ: the relation θ_{N_θ} holds at (x , y) when
(x ∙ y ⁻¹) θ ε, and multiplying on the right by y converts that to
x θ y through ∙⁻¹∙ and the unit law — while multiplying x θ y on
the right by y ⁻¹ converts it back through invʳ-law.
-- Round trip on congruences: θ_{N_θ} ≑ θ. congruenceOf∘normalOf : (θ : Con 𝑮 ℓ) → congruenceOf (normalOf θ) ≑ θ congruenceOf∘normalOf θ = fwd , bwd where open ConNormal θ -- From (x ∙ y ⁻¹) θ ε derive x θ y. fwd : congruenceOf (normalOf θ) ⊑ θ fwd {x} {y} p = θ-trans (θ-reflexive (≈sym (∙⁻¹∙ x y))) (θ-trans (θ-∙ p θ-refl) (θ-reflexive (idˡ-law y))) -- From x θ y derive (x ∙ y ⁻¹) θ ε. bwd : θ ⊑ congruenceOf (normalOf θ) bwd {x} {y} p = θ-trans (θ-∙ p (θ-refl {y ⁻¹})) (θ-reflexive (invʳ-law y))
On normal subgroups, N_{θ_N} ≈ⁿ N: an element x lies in N_{θ_N} when
x ∙ ε ⁻¹ ∈ N, and x ∙ ε ⁻¹ ≈ x, so the respects proof carried by the
subgroup identifies the two. This is the step that consumes the
respects field, and the sole place the correspondence would break for a
normal subuniverse not closed under the setoid equality.
-- Round trip on normal subgroups: N_{θ_N} ≈ⁿ N (needs the respecting field). normalOf∘congruenceOf : (𝑵 : NormalSubgroup ℓ) → normalOf (congruenceOf 𝑵) ≈ⁿ 𝑵 normalOf∘congruenceOf 𝑵 = fwd , bwd where open IsSubgroup (set-isSubgroup 𝑵) using ( respects ) -- x ∙ ε ⁻¹ ∈ N and x ∙ ε ⁻¹ ≈ x give x ∈ N. fwd : normalOf (congruenceOf 𝑵) ≤ⁿ 𝑵 fwd {x} p = respects (∙ε⁻¹ x) p -- x ∈ N and x ≈ x ∙ ε ⁻¹ give x ∙ ε ⁻¹ ∈ N. bwd : 𝑵 ≤ⁿ normalOf (congruenceOf 𝑵) bwd {x} p = respects (≈sym (∙ε⁻¹ x)) p
The order isomorphism¶
Assembling the four facts — two maps, both monotone, mutually inverse — gives the
correspondence as an OrderIso between the congruence containment order of
the group algebra and the inclusion order on normal subgroups. (The endpoint implicits
of the monotone maps are bound and forwarded explicitly: Con and
NormalSubgroup are defined functions, not injective type formers, so
Agda cannot recover them from the field types.)
-- The order isomorphism Con 𝑮 ℓ ≅ NormalSubgroup ℓ. NormalCongruenceIso : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ) NormalCongruenceIso ℓ = OrderIso (_≑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_⊑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_≈ⁿ_ {ℓ}) (_≤ⁿ_ {ℓ}) normal-congruence-iso : (ℓ : Level) → NormalCongruenceIso ℓ normal-congruence-iso ℓ = record { to = normalOf ; from = congruenceOf ; to-mono = λ {θ} {φ} → normalOf-mono θ φ ; from-mono = λ {𝑴} {𝑵} → congruenceOf-mono 𝑴 𝑵 ; to∘from = normalOf∘congruenceOf ; from∘to = congruenceOf∘normalOf }
The reverse isomorphism presents the normal subgroups of 𝒢 as the
congruence poset of its underlying algebra — the form a representability argument wants.
NormalCongruenceIso⁻¹ : (ℓ : Level) → Type (α ⊔ ρ ⊔ suc ℓ) NormalCongruenceIso⁻¹ ℓ = OrderIso (_≈ⁿ_ {ℓ}) (_≤ⁿ_ {ℓ}) (_≑_ {𝑨 = 𝑮} {ℓ = ℓ}) (_⊑_ {𝑨 = 𝑮} {ℓ = ℓ}) normal-congruence-iso⁻¹ : (ℓ : Level) → NormalCongruenceIso⁻¹ ℓ normal-congruence-iso⁻¹ ℓ = record { to = congruenceOf ; from = normalOf ; to-mono = λ {𝑴} {𝑵} → congruenceOf-mono 𝑴 𝑵 ; from-mono = λ {θ} {φ} → normalOf-mono θ φ ; to∘from = congruenceOf∘normalOf ; from∘to = normalOf∘congruenceOf }
Nonzero congruences and nontrivial normal subgroups¶
The order isomorphism alone does not say that the two sides agree on which elements are
above the bottom; that has to be proved, and it is what the monolith transport will
consume. The bottom of the subgroup side is trivialSubgroup of
Classical.Structures.Group.Subgroups — the ≈-class of the identity, which over a
setoid carrier is the right notion of the one-element subgroup — and the bottom of the
congruence side is the diagonal, whose "at the bottom" predicate is
BelowDiagonal of Setoid.Congruences.Monolith.
-- N is contained in the trivial subgroup { x ∣ x ≈ ε }. BelowTrivial : Pred G ℓ → Type (α ⊔ ρ ⊔ ℓ) BelowTrivial N = N ⊆ proj₁ (trivialSubgroup 𝒢) -- N is nontrivial: it is not contained in the trivial subgroup. Nontrivialᴺ : Pred G ℓ → Type (α ⊔ ρ ⊔ ℓ) Nontrivialᴺ N = ¬ BelowTrivial N
The two positive statements are equivalent on each side, constructively and in both
directions; Nonzero and Nontrivialᴺ are their
negations, so the equivalence of the negations follows by contraposition with no
classical input. We state the four positive implications first, since a downstream
proof usually wants one of them directly rather than the negated form.
-- If N is trivial then θ_N relates only equal elements ... below-trivial→below-diagonal : (𝑵 : NormalSubgroup ℓ) → BelowTrivial (set 𝑵) → BelowDiagonal 𝑮 (congruenceOf 𝑵) below-trivial→below-diagonal 𝑵 N⊆1 p = ∙⁻¹≈ε→≈ (N⊆1 p) -- ... and conversely, if θ_N relates only equal elements then N is trivial. below-diagonal→below-trivial : (𝑵 : NormalSubgroup ℓ) → BelowDiagonal 𝑮 (congruenceOf 𝑵) → BelowTrivial (set 𝑵) below-diagonal→below-trivial 𝑵 θ⊆Δ {x} x∈N = θ⊆Δ (respects (≈sym (∙ε⁻¹ x)) x∈N) where open IsSubgroup (set-isSubgroup 𝑵) using ( respects ) -- If θ relates only equal elements then its identity class is trivial ... con-below-diagonal→below-trivial : (θ : Con 𝑮 ℓ) → BelowDiagonal 𝑮 θ → BelowTrivial (set (normalOf θ)) con-below-diagonal→below-trivial θ θ⊆Δ x∈N = θ⊆Δ x∈N -- ... and conversely, a trivial identity class forces θ below the diagonal. con-below-trivial→below-diagonal : (θ : Con 𝑮 ℓ) → BelowTrivial (set (normalOf θ)) → BelowDiagonal 𝑮 θ con-below-trivial→below-diagonal θ N⊆1 {x} {y} p = ∙⁻¹≈ε→≈ (N⊆1 (θ-trans (θ-∙ p (θ-refl {y ⁻¹})) (θ-reflexive (invʳ-law y)))) where open ConNormal θ
Negating both sides gives the statement the monolith transport needs: under the correspondence, a congruence is nonzero exactly when the matching normal subgroup is nontrivial.
-- θ_N is nonzero iff N is nontrivial. nonzero→nontrivial : (𝑵 : NormalSubgroup ℓ) → Nonzero 𝑮 (congruenceOf 𝑵) → Nontrivialᴺ (set 𝑵) nonzero→nontrivial 𝑵 nz N⊆1 = nz (below-trivial→below-diagonal 𝑵 N⊆1) nontrivial→nonzero : (𝑵 : NormalSubgroup ℓ) → Nontrivialᴺ (set 𝑵) → Nonzero 𝑮 (congruenceOf 𝑵) nontrivial→nonzero 𝑵 nt θ⊆Δ = nt (below-diagonal→below-trivial 𝑵 θ⊆Δ) -- N_θ is nontrivial iff θ is nonzero. con-nonzero→nontrivial : (θ : Con 𝑮 ℓ) → Nonzero 𝑮 θ → Nontrivialᴺ (set (normalOf θ)) con-nonzero→nontrivial θ nz N⊆1 = nz (con-below-trivial→below-diagonal θ N⊆1) con-nontrivial→nonzero : (θ : Con 𝑮 ℓ) → Nontrivialᴺ (set (normalOf θ)) → Nonzero 𝑮 θ con-nontrivial→nonzero θ nt θ⊆Δ = nt (con-below-diagonal→below-trivial θ θ⊆Δ)