Classical.Structures.Group.Complements¶
Permuting complements in an interval of the subgroup lattice¶
This is the Classical.Structures.Group.Complements module of the Agda Universal Algebra Library.
Fix subgroups H ≤ G and an intermediate subgroup A ∈ [H , G].
A complement of A in the interval [H , G] is a subgroup B ∈ [H , G] with
A ∩ B = H and ⟨A , B⟩ = G.
This module proves Corollary 3.5 of the Interval Enforceable Properties note:1
If ℬ is a nonempty set of complements of
Ain[H , G]every member of which permutes withA, thenℬis an antichain.
The proof is one application of Dedekind's rule
(Classical.Structures.Group.Dedekind):
for all B₁ , B₂ ∈ ℬ, if B₁ ≤ B₂ then
B₁ = B₁H = B₁(A ∩ B₂) = B₁A ∩ B₂ = G ∩ B₂ = B₂.
Thus no strict containment is possible.
Complements, formalized through the complex product.
Two of the note's hypotheses — that B permutes with A (AB = BA) and that A
and B join to G — are used only through their conjunction, which is the single
statement BA = G; that is, the complex product B ∙ᶜ A of
Classical.Structures.Group.Complexes is the whole group.
We call that statement Factors and take it as the primitive.
It is exactly equivalent to the note's pair of hypotheses — for a permuting pair of
subgroups ⟨A , B⟩ = AB — and it keeps the argument free of the generated
subgroup, whose inductive presentation would otherwise have to be unfolded.
The join hypothesis is recovered where consumers need it: a factorization of G is
inherited by any subgroup containing A and B (Factors-least),
which is the universal property of the join.
The module also collects the small facts about complex products that the argument and
its downstream consumers need: a permuting product of subgroups is a subgroup
(permuting-∙ᶜ-isSubgroup), a normal subgroup permutes with
every subgroup (normal-permutes), hence NB is a subgroup for N
normal (normal-∙ᶜ-isSubgroup).
The toolkit¶
module Complements {α ρ : Level} (𝒢 : Group α ρ) where private 𝑮 : Algebra {𝑆 = Sig-Group} α ρ 𝑮 = proj₁ 𝒢 open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( Carrier to G ; refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open SetoidReasoning 𝔻[ 𝑮 ] open Group-Op 𝒢 open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ⁻¹-involutive ; ⁻¹-anti-homo-∙ ) open Complex 𝒢 using ( _∙ᶜ_ ; mem-∙ᶜ ; ∙ᶜ-respects ; ∙ᶜ-mono ; subgroup-∙ᶜ-idem ) open Conjugate 𝒢 using ( conj-syntax ; IsNormal )
A member of one factor is a member of the product, provided the other factor
contains the identity — the two one-sided inclusions P ⊆ P Q and Q ⊆ P Q.
-- p ≈ p ∙ ε, so the left factor embeds when the right one contains ε. mem-∙ᶜˡ : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} → ε ∈ Q → P ⊆ P ∙ᶜ Q mem-∙ᶜˡ {P = P} {Q} ε∈Q {x} x∈P = ∙ᶜ-respects P Q (idʳ-law x) (mem-∙ᶜ x∈P ε∈Q) -- q ≈ ε ∙ q, dually. mem-∙ᶜʳ : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} → ε ∈ P → Q ⊆ P ∙ᶜ Q mem-∙ᶜʳ {P = P} {Q} ε∈P {x} x∈Q = ∙ᶜ-respects P Q (idˡ-law x) (mem-∙ᶜ ε∈P x∈Q)
Permuting subsets¶
Two subsets permute when their complex products in the two orders agree. This
is the note's hypothesis on the members of ℬ, and it is what makes the product
A B a subgroup rather than a mere subset.
infix 4 _permutes_ -- P and Q permute: P Q = Q P as subsets. _permutes_ : Pred G ℓᵃ → Pred G ℓᵇ → Type (α ⊔ ρ ⊔ ℓᵃ ⊔ ℓᵇ) P permutes Q = P ∙ᶜ Q ≐ Q ∙ᶜ P
The product of two permuting subgroups is a subgroup. Closure under ∙ is the one
step that consumes permutation: in (a₁b₁)(a₂b₂) the middle pair b₁a₂ is
rewritten as some a₃b₃, after which associativity regroups the four factors.
permuting-∙ᶜ-isSubgroup : {A : Pred G ℓᵃ} {B : Pred G ℓᵇ} → IsSubgroup 𝒢 A → IsSubgroup 𝒢 B → A permutes B → IsSubgroup 𝒢 (A ∙ᶜ B) permuting-∙ᶜ-isSubgroup {A = A} {B} A-sg B-sg (AB⊆BA , BA⊆AB) = mkIsSubgroup 𝒢 (∙ᶜ-respects A B) ∙-c ε-c ⁻¹-c where open IsSubgroup A-sg using () renaming ( ∙-closed to A∙ ; ε-closed to Aε ; ⁻¹-closed to A⁻¹ ) open IsSubgroup B-sg using () renaming ( ∙-closed to B∙ ; ε-closed to Bε ; ⁻¹-closed to B⁻¹ ) ε-c : ε ∈ A ∙ᶜ B ε-c = ∙ᶜ-respects A B (idˡ-law ε) (mem-∙ᶜ Aε Bε) ∙-c : ∀ {x y} → x ∈ A ∙ᶜ B → y ∈ A ∙ᶜ B → x ∙ y ∈ A ∙ᶜ B ∙-c {x} {y} (a₁ , b₁ , a₁∈A , b₁∈B , x≈a₁b₁) (a₂ , b₂ , a₂∈A , b₂∈B , y≈a₂b₂) = ∙ᶜ-respects A B (≈sym regroup) (mem-∙ᶜ (A∙ a₁∈A a₃∈A) (B∙ b₃∈B b₂∈B)) where -- The middle pair b₁ a₂ lies in B A = A B, so it is some a₃ b₃. swap : b₁ ∙ a₂ ∈ A ∙ᶜ B swap = BA⊆AB (mem-∙ᶜ b₁∈B a₂∈A) a₃ b₃ : G a₃ = swap .proj₁ b₃ = swap .proj₂ .proj₁ ξ : a₃ ∈ A × b₃ ∈ B × b₁ ∙ a₂ ≈ a₃ ∙ b₃ ξ = swap .proj₂ .proj₂ a₃∈A : a₃ ∈ A a₃∈A = ξ .proj₁ b₃∈B : b₃ ∈ B b₃∈B = ξ .proj₂ .proj₁ b₁a₂≈a₃b₃ : b₁ ∙ a₂ ≈ a₃ ∙ b₃ b₁a₂≈a₃b₃ = ξ .proj₂ .proj₂ regroup : x ∙ y ≈ (a₁ ∙ a₃) ∙ (b₃ ∙ b₂) regroup = begin x ∙ y ≈⟨ ∙-cong x≈a₁b₁ y≈a₂b₂ ⟩ a₁ ∙ b₁ ∙ (a₂ ∙ b₂) ≈˘⟨ assoc-law (a₁ ∙ b₁) a₂ b₂ ⟩ a₁ ∙ b₁ ∙ a₂ ∙ b₂ ≈⟨ ∙-cong (assoc-law a₁ b₁ a₂) ≈refl ⟩ a₁ ∙ (b₁ ∙ a₂) ∙ b₂ ≈⟨ ∙-cong (∙-cong ≈refl b₁a₂≈a₃b₃) ≈refl ⟩ a₁ ∙ (a₃ ∙ b₃) ∙ b₂ ≈˘⟨ ∙-cong (assoc-law a₁ a₃ b₃) ≈refl ⟩ a₁ ∙ a₃ ∙ b₃ ∙ b₂ ≈⟨ assoc-law (a₁ ∙ a₃) b₃ b₂ ⟩ a₁ ∙ a₃ ∙ (b₃ ∙ b₂) ∎ ⁻¹-c : ∀ {x} → x ∈ A ∙ᶜ B → x ⁻¹ ∈ A ∙ᶜ B ⁻¹-c {x} (a , b , a∈A , b∈B , x≈ab) = BA⊆AB (∙ᶜ-respects B A (≈sym anti) (mem-∙ᶜ (B⁻¹ b∈B) (A⁻¹ a∈A))) where anti : x ⁻¹ ≈ b ⁻¹ ∙ a ⁻¹ anti = ≈trans (⁻¹-cong x≈ab) (⁻¹-anti-homo-∙ a b)
Normal subgroups permute with everything¶
A normal subgroup permutes with every subset: n b ≈ b (b⁻¹ n b) moves a normal
element across a factor, and (b n b⁻¹) b ≈ b n moves it back. Consequently N B
is a subgroup whenever N is normal and both are subgroups — this is the subgroup
NH of the parachute argument.
-- Moving a conjugate across a factor, in the two directions. private swapˡ : ∀ b n → b ∙ n ^ (b ⁻¹) ≈ n ∙ b swapˡ b n = begin b ∙ (b ⁻¹ ∙ n ∙ (b ⁻¹) ⁻¹) ≈⟨ ∙-cong ≈refl (∙-cong ≈refl (⁻¹-involutive b)) ⟩ b ∙ (b ⁻¹ ∙ n ∙ b) ≈˘⟨ assoc-law b (b ⁻¹ ∙ n) b ⟩ b ∙ (b ⁻¹ ∙ n) ∙ b ≈˘⟨ ∙-cong (assoc-law b (b ⁻¹) n) ≈refl ⟩ b ∙ b ⁻¹ ∙ n ∙ b ≈⟨ ∙-cong (∙-cong (invʳ-law b) ≈refl) ≈refl ⟩ ε ∙ n ∙ b ≈⟨ ∙-cong (idˡ-law n) ≈refl ⟩ n ∙ b ∎ swapʳ : ∀ b n → n ^ b ∙ b ≈ b ∙ n swapʳ b n = begin b ∙ n ∙ b ⁻¹ ∙ b ≈⟨ assoc-law (b ∙ n) (b ⁻¹) b ⟩ b ∙ n ∙ (b ⁻¹ ∙ b) ≈⟨ ∙-cong ≈refl (invˡ-law b) ⟩ b ∙ n ∙ ε ≈⟨ idʳ-law (b ∙ n) ⟩ b ∙ n ∎ -- A normal subset permutes with every subset. normal-permutes : {N : Pred G ℓⁿ} (B : Pred G ℓᵇ) → IsNormal N → N permutes B normal-permutes {N = N} B N-normal = to , from where to : N ∙ᶜ B ⊆ B ∙ᶜ N to (n , b , n∈N , b∈B , x≈nb) = b , n ^ (b ⁻¹) , b∈B , N-normal (b ⁻¹) n∈N , ≈trans x≈nb (≈sym (swapˡ b n)) from : B ∙ᶜ N ⊆ N ∙ᶜ B from (b , n , b∈B , n∈N , x≈bn) = n ^ b , b , N-normal b n∈N , b∈B , ≈trans x≈bn (≈sym (swapʳ b n)) -- Hence the product of a normal subgroup with any subgroup is a subgroup. normal-∙ᶜ-isSubgroup : {N : Pred G ℓⁿ} {B : Pred G ℓᵇ} → IsNormal N → IsSubgroup 𝒢 N → IsSubgroup 𝒢 B → IsSubgroup 𝒢 (N ∙ᶜ B) normal-∙ᶜ-isSubgroup {B = B} N-normal N-sg B-sg = permuting-∙ᶜ-isSubgroup N-sg B-sg (normal-permutes B N-normal)
Factorizations of the group¶
Factors P Q says the complex product P Q exhausts the group. For subgroups
this is the note's "P and Q permute and ⟨P , Q⟩ = G", packaged as one
statement: it is symmetric (invert a factorization elementwise), and it is inherited
by every subgroup above both factors, which is the join's universal property.
-- Every element of the group is a product of a member of P and a member of Q. Factors : Pred G ℓᵃ → Pred G ℓᵇ → Type (α ⊔ ρ ⊔ ℓᵃ ⊔ ℓᵇ) Factors P Q = ∀ (x : G) → x ∈ P ∙ᶜ Q -- A factorization of the group by subgroups may be read in either order: -- x ⁻¹ ≈ p ∙ q gives x ≈ q ⁻¹ ∙ p ⁻¹. Factors-sym : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} → IsSubgroup 𝒢 P → IsSubgroup 𝒢 Q → Factors P Q → Factors Q P Factors-sym {P = P} {Q} P-sg Q-sg fact x = ∙ᶜ-respects Q P (≈sym anti) mem where open IsSubgroup P-sg using () renaming ( ⁻¹-closed to P⁻¹ ) open IsSubgroup Q-sg using () renaming ( ⁻¹-closed to Q⁻¹ ) p q : G p = fact (x ⁻¹) .proj₁ q = fact (x ⁻¹) .proj₂ .proj₁ ξ : p ∈ P × q ∈ Q × x ⁻¹ ≈ p ∙ q ξ = fact (x ⁻¹) .proj₂ .proj₂ p∈P : p ∈ P p∈P = ξ .proj₁ q∈Q : q ∈ Q q∈Q = ξ .proj₂ .proj₁ x⁻¹≈pq : x ⁻¹ ≈ p ∙ q x⁻¹≈pq = ξ .proj₂ .proj₂ anti : x ≈ q ⁻¹ ∙ p ⁻¹ anti = begin x ≈˘⟨ ⁻¹-involutive x ⟩ (x ⁻¹) ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈pq ⟩ (p ∙ q) ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ p q ⟩ q ⁻¹ ∙ p ⁻¹ ∎ mem : q ⁻¹ ∙ p ⁻¹ ∈ Q ∙ᶜ P mem = mem-∙ᶜ (Q⁻¹ q∈Q) (P⁻¹ p∈P) -- A factorization of the group is inherited by any subgroup containing both -- factors: this is "⟨P , Q⟩ = G" in its universal-property form. Factors-least : {P : Pred G ℓᵃ} {Q : Pred G ℓᵇ} {C : Pred G ℓᶜ} → IsSubgroup 𝒢 C → P ⊆ C → Q ⊆ C → Factors P Q → (x : G) → x ∈ C Factors-least {C = C} C-sg P⊆C Q⊆C fact x = proj₁ (subgroup-∙ᶜ-idem C-sg) (∙ᶜ-mono P⊆C Q⊆C (fact x))
Corollary 3.5: comparable permuting complements collapse¶
The heart of the matter, in the form the parachute argument uses: if B₁ ≤ B₂ are
subgroups of the interval [H , G], if B₂ meets A at H, and if B₁ A = G,
then already B₂ ≤ B₁. Reading the note's chain of equalities from the right, an
element x ∈ B₂ lies in B₁A ∩ B₂, hence in B₁(A ∩ B₂) (by Dedekind's rule, which
applies because B₁ ≤ B₂ and B₂ is a subgroup). The meet hypothesis
shrinks the second factor to H ⊆ B₁, and B₁B₁ = B₁ collapses the product.
complement-⊆-collapse : {H : Pred G ℓʰ} {A : Pred G ℓᵃ} {B₁ B₂ : Pred G ℓᵇ} → IsSubgroup 𝒢 B₁ → IsSubgroup 𝒢 B₂ → H ⊆ B₁ → B₁ ⊆ B₂ → A ∩ B₂ ⊆ H → Factors B₁ A → B₂ ⊆ B₁ complement-⊆-collapse {A = A} {B₁} {B₂} B₁-sg B₂-sg H⊆B₁ B₁⊆B₂ meet-⊆ fact {x} x∈B₂ = proj₁ (subgroup-∙ᶜ-idem B₁-sg) inside where -- x lies in B₁A and in B₂ ... step₁ : x ∈ (B₁ ∙ᶜ A) ∩ B₂ step₁ = fact x , x∈B₂ -- ... hence in B₁(A ∩ B₂), by Dedekind's rule ... step₂ : x ∈ B₁ ∙ᶜ (A ∩ B₂) step₂ = proj₂ (dedekindˡ 𝒢 B₂-sg B₁⊆B₂) step₁ -- ... and A ∩ B₂ ⊆ H ⊆ B₁ turns that into a product of two members of B₁. inside : x ∈ B₁ ∙ᶜ B₁ inside = ∙ᶜ-mono id (H⊆B₁ ∘ meet-⊆ ) step₂
An antichain of subgroups, indexed by a type I, is a family in which no member
is contained in another except when the containment reverses — the constructive
reading of "pairwise incomparable" for subsets ordered by inclusion, where equality
is mutual containment.
Corollary 3.5. If H ≤ A ≤ G and if every group in ℬ ⊆ [H , G] permutes with
A, then ℬ is an antichain.
-- No strict containments: a containment between members is mutual. Antichain : {I : Type ℓᶜ} → (I → Pred G ℓᵇ) → Type (ℓᶜ ⊔ α ⊔ ℓᵇ) Antichain {I = I} ℬ = (i j : I) → ℬ i ⊆ ℬ j → ℬ j ⊆ ℬ i -- Corollary 3.5 (cor:dedekind1 of the note). complements-antichain : {I : Type ℓᶜ} {H : Pred G ℓʰ} {A : Pred G ℓᵃ} (ℬ : I → Pred G ℓᵇ) → (∀ i → IsSubgroup 𝒢 (ℬ i)) → (∀ i → H ⊆ ℬ i) -- every member lies in the interval [H , G] → (∀ i → A ∩ ℬ i ⊆ H) -- every member meets A in H → (∀ i → Factors (ℬ i) A) -- every member permutes with A and joins it to G → Antichain ℬ complements-antichain ℬ ℬ-sg H⊆ℬ meet fact i j ℬi⊆ℬj = complement-⊆-collapse (ℬ-sg i) (ℬ-sg j) (H⊆ℬ i) ℬi⊆ℬj (meet j) (fact i)
-
Interval enforceable properties of finite groups, arXiv:1205.1927v4, § 3.2 (Dedekind's rule) and § 3.3 (parachute lattices). ↩