Classical.Structures.Group.Product¶
Binary direct products of groups¶
This is the Classical.Structures.Group.Product module of the Agda Universal Algebra Library.
For groups 𝒢 and 𝒦 presented as Σ-typed structures over
Sig-Group, this module constructs the
binary direct product 𝒢 ×ᵍ 𝒦: the algebra on the product setoid
whose operations act componentwise, together with componentwise proofs of the five
group laws. The library's indexed product ⨅ of
Setoid.Algebras.Products would give a product with a function-typed carrier
∀ i → 𝕌[ 𝒜 i ]; the binary product here instead has the pair carrier G × K, which
is the form the fattening arguments of the FLRP program consume (a fattened subgroup
is literally a predicate composed with proj₁). The construction is
level-general (Group α ρ → Group β σ → Group (α ⊔ β) (ρ ⊔ σ)), since full
generality costs nothing here.
Besides the product itself, the module provides the ingredients of the
fattening lemma [H × K, G × K] ≅ [H, G] (the remark following Lemma
lemma:ie-prop-and-neg in the note vendored at docs/papers/flrp/ieprops/; see
docs/notes/flrp-research-roadmap.md § 4):
- the fattened subgroup predicates
H ×ᶠ 𝒦(subgroup in the first coordinate, full second factor) and𝒢 ᶠ× J(mirrored), each anIsSubgroupof the product whenever the input is one — the superscriptᶠpoints at the factor that is taken full; - the slice toolkit (
Slice₁,Slice₂): for a respecting subgroupMof the product lying above a fattened subgroup, membership does not depend on the fattened coordinate —(g , k) ∈ M ⟺ (g , ε) ∈ M— because(g , k) ≈ (g , ε) ∙ (ε , k)and(ε , k)lies inH ×ᶠ 𝒦 ⊆ M; hence the restriction ofMto one coordinate is again a respecting subgroup.
The order-isomorphism packaging of the fattening lemma lives in FLRP.Enforceable,
which consumes exactly these lemmas; everything here is plain group theory, kept in
the Classical/ tree per the roadmap's placement discipline.
Following the Cubical-port discipline, the underlying equivalence of the product is
isolated in G×K — the pointwise pair of the component
equivalences — so it can be mechanically substituted on the eventual port.
The fattened subgroup predicates¶
The fattened predicates are pure predicate transformers — they mention no group
structure beyond the carrier of the full factor — so they are defined up front, ahead
of the product construction that proves them subgroups. H ×ᶠ 𝒦
holds at a pair exactly when the first coordinate lies in H; the second coordinate
ranges over all of 𝒦 (the fattened, full factor, marked by ᶠ). The mirror
𝒢 ᶠ× J fattens the first coordinate instead.
infix 7 _×ᶠ_ _ᶠ×_ -- The subgroup H of the first factor, fattened by the full group 𝒦. _×ᶠ_ : {G : Type α} (H : Pred G ℓ) ((𝑲 , _) : Group β σ) → Pred (G × 𝕌[ 𝑲 ]) ℓ (H ×ᶠ 𝒦) (g , _) = H g -- The subgroup J of the second factor, fattened by the full group 𝒢. _ᶠ×_ : ((𝑮 , _) : Group α ρ) {K : Type β} (J : Pred K ℓ) → Pred (𝕌[ 𝑮 ] × K) ℓ (𝒢 ᶠ× J) (_ , k) = J k
The product construction¶
GroupProduct 𝒢 𝒦 packages the whole development for a fixed pair
of groups; opening it provides the product algebra, the product group, the pointwise
descriptions of its curried operations, the subgroup lemmas for the fattened
predicates, and the slice toolkit.
module GroupProduct (𝒢 : Group α ρ) (𝒦 : Group β σ) where private 𝑮 = proj₁ 𝒢 𝑲 = proj₁ 𝒦 G = 𝕌[ 𝑮 ] K = 𝕌[ 𝑲 ] open Setoid 𝔻[ 𝑮 ] using () renaming ( _≈_ to _≈₁_ ; refl to refl₁ ; sym to sym₁ ; trans to trans₁ ) open Setoid 𝔻[ 𝑲 ] using () renaming ( _≈_ to _≈₂_ ; refl to refl₂ ; sym to sym₂ ; trans to trans₂ )
The carrier of the product is the pair type G × K, and its equivalence is the
pointwise pair of the component equivalences — this is the isolated-equality locus
for the Cubical port.
G×K : Setoid (α ⊔ β) (ρ ⊔ σ) G×K = record { Carrier = G × K ; _≈_ = λ p q → (proj₁ p ≈₁ proj₁ q) × (proj₂ p ≈₂ proj₂ q) ; isEquivalence = record { refl = refl₁ , refl₂ ; sym = λ e → sym₁ (proj₁ e) , sym₂ (proj₂ e) ; trans = λ (d₁ , d₂) (e₁ , e₂) → trans₁ d₁ e₁ , trans₂ d₂ e₂ } } open Setoid G×K using () renaming ( _≈_ to _≈ₓ_ ; trans to transₓ )
Each operation symbol acts componentwise: the interpretation of f at a tuple of
pairs is the pair of the component interpretations at the projected tuples. The
congruence proof is the pair of the component congruences, via the shared
interp-cong primitive.
𝑮×𝑲 : Algebra {𝑆 = Sig-Group} (α ⊔ β) (ρ ⊔ σ) 𝑮×𝑲 = mkAlgebra G×K interp interp-congruence where interp : (o : OperationSymbolsOf Sig-Group) → Op (ArityOf Sig-Group o) (G × K) interp o a = (o ^ 𝑮) (proj₁ ∘ a) , (o ^ 𝑲) (proj₂ ∘ a) interp-congruence : ∀ o {u v : ArityOf Sig-Group o → G × K} → (∀ i → u i ≈ₓ v i) → interp o u ≈ₓ interp o v interp-congruence o e = interp-cong 𝑮 o (λ i → proj₁ (e i)) , interp-cong 𝑲 o (λ i → proj₂ (e i))
Componentwise term interpretation¶
Satisfaction of the group theory transfers componentwise, and the engine is the following term-induction lemma: the interpretation of any term in the product is (setoid-)equal to the pair of its interpretations in the factors, under the projected environments. The variable case is definitional; the node case pairs the component congruences applied to the induction hypotheses.
open Environment 𝑮×𝑲 using () renaming ( ⟦_⟧ to ⟦_⟧G×K ) open Environment 𝑮 using () renaming ( ⟦_⟧ to ⟦_⟧G ) open Environment 𝑲 using () renaming ( ⟦_⟧ to ⟦_⟧K ) interp-factor : {X : Type χ} (t : Term X) (η : X → G × K) → ⟦ t ⟧G×K ⟨$⟩ η ≈ₓ (⟦ t ⟧G ⟨$⟩ (proj₁ ∘ η) , ⟦ t ⟧K ⟨$⟩ (proj₂ ∘ η)) interp-factor (ℊ x) η = refl₁ , refl₂ interp-factor (node f args) η = interp-cong 𝑮 f (λ i → proj₁ (interp-factor (args i) η)) , interp-cong 𝑲 f (λ i → proj₂ (interp-factor (args i) η))
Every group equation now holds in the product by one uniform argument: factor the two sides into components, apply the component groups' satisfaction proofs, and refold. No case analysis on the equation is needed.
×ᵍ-⊨ : 𝑮×𝑲 ⊨ᵍᵖ Th-Group ×ᵍ-⊨ i η = trans₁ (proj₁ (interp-factor lhs η)) (trans₁ (proj₂ 𝒢 i (proj₁ ∘ η)) (sym₁ (proj₁ (interp-factor rhs η)))) , trans₂ (proj₂ (interp-factor lhs η)) (trans₂ (proj₂ 𝒦 i (proj₂ ∘ η)) (sym₂ (proj₂ (interp-factor rhs η)))) where lhs rhs : Term (Fin 3) lhs = proj₁ (Th-Group i) rhs = proj₂ (Th-Group i) -- The direct product group. ×ᵍ-Group : Group (α ⊔ β) (ρ ⊔ σ) ×ᵍ-Group = 𝑮×𝑲 , ×ᵍ-⊨
Pointwise descriptions of the curried operations¶
The curried accessors of Group-Op applied to the product agree, up to
≈ₓ, with the pairs of the component accessors. (They are not definitionally equal:
the curried form routes the arguments through a canonical pair tuple, and Fin-
indexed tuples lack η under --cubical-compatible; each bridge is one
interp-cong per component, the standard resolution.)
open Group-Op 𝒢 using () renaming ( _∙_ to _∙₁_ ; ε to ε₁ ; _⁻¹ to _⁻¹₁ ; idʳ-law to idʳ-law₁ ; invʳ-law to invʳ-law₁ ) open Group-Op 𝒦 using () renaming ( _∙_ to _∙₂_ ; ε to ε₂ ; _⁻¹ to _⁻¹₂ ; idˡ-law to idˡ-law₂ ; idʳ-law to idʳ-law₂ ; invʳ-law to invʳ-law₂ ) open Group-Op ×ᵍ-Group using () renaming ( _∙_ to _∙ₓ_ ; ε to εₓ ; _⁻¹ to _⁻¹ₓ ) open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using () renaming ( ε⁻¹≈ε to ε⁻¹≈ε₁ ) open GroupProperties ⟨ 𝒦 ⟩ᵍᵖ using () renaming ( ε⁻¹≈ε to ε⁻¹≈ε₂ ) -- The product multiplication is componentwise. ∙ₓ-pointwise : ∀ x y → (x ∙ₓ y) ≈ₓ (proj₁ x ∙₁ proj₁ y , proj₂ x ∙₂ proj₂ y) ∙ₓ-pointwise x y = interp-cong 𝑮 ∙-Op (λ { 0F → refl₁ ; 1F → refl₁ }) , interp-cong 𝑲 ∙-Op (λ { 0F → refl₂ ; 1F → refl₂ }) -- The product identity is the pair of identities. εₓ-pointwise : εₓ ≈ₓ (ε₁ , ε₂) εₓ-pointwise = interp-cong 𝑮 ε-Op (λ ()) , interp-cong 𝑲 ε-Op (λ ()) -- The product inverse is componentwise. ⁻¹ₓ-pointwise : ∀ x → (x ⁻¹ₓ) ≈ₓ (proj₁ x ⁻¹₁ , proj₂ x ⁻¹₂) ⁻¹ₓ-pointwise x = interp-cong 𝑮 ⁻¹-Op (λ { 0F → refl₁ }) , interp-cong 𝑲 ⁻¹-Op (λ { 0F → refl₂ })
The fattened predicates are subgroups¶
A fattened predicate is a subuniverse of the product definitionally: the first component of an interpreted operation of the product is the corresponding interpreted operation of the first factor, so closure is inherited with no equational reasoning at all. Respecting the product equality is likewise inherited from the respected factor.
module _ {H : Pred G ℓ} where -- H ×ᶠ 𝒦 respects the product equality whenever H respects ≈₁. ×ᶠ-respects : H Respects _≈₁_ → (H ×ᶠ 𝒦) Respects _≈ₓ_ ×ᶠ-respects resp e h = resp (proj₁ e) h -- H ×ᶠ 𝒦 is closed under the product operations whenever H is closed (definitional). ×ᶠ-isSubuniverse : H ∈ Subuniverses 𝑮 → (H ×ᶠ 𝒦) ∈ Subuniverses 𝑮×𝑲 ×ᶠ-isSubuniverse H-sub f a im = H-sub f (proj₁ ∘ a) im -- Fattening a subgroup of 𝒢 by the full 𝒦 yields a subgroup of the product. ×ᶠ-isSubgroup : IsSubgroup 𝒢 H → IsSubgroup ×ᵍ-Group (H ×ᶠ 𝒦) ×ᶠ-isSubgroup H-sg = record { respects = ×ᶠ-respects (IsSubgroup.respects H-sg) ; isSubuniverse = ×ᶠ-isSubuniverse (IsSubgroup.isSubuniverse H-sg) } module _ {J : Pred K ℓ} where -- Mirror image: 𝒢 ᶠ× J respects the product equality whenever J respects ≈₂. ᶠ×-respects : J Respects _≈₂_ → (𝒢 ᶠ× J) Respects _≈ₓ_ ᶠ×-respects resp e j = resp (proj₂ e) j -- 𝒢 ᶠ× J is closed under the product operations whenever J is closed (definitional). ᶠ×-isSubuniverse : J ∈ Subuniverses 𝑲 → (𝒢 ᶠ× J) ∈ Subuniverses 𝑮×𝑲 ᶠ×-isSubuniverse J-sub f a im = J-sub f (proj₂ ∘ a) im -- Fattening a subgroup of 𝒦 by the full 𝒢 yields a subgroup of the product. ᶠ×-isSubgroup : IsSubgroup 𝒦 J → IsSubgroup ×ᵍ-Group (𝒢 ᶠ× J) ᶠ×-isSubgroup J-sg = record { respects = ᶠ×-respects (IsSubgroup.respects J-sg) ; isSubuniverse = ᶠ×-isSubuniverse (IsSubgroup.isSubuniverse J-sg) }
The slice toolkit, first coordinate¶
Fix a subgroup H of 𝒢 and a respecting subgroup M of the product with
H ×ᶠ 𝒦 ⊆ M. Because M contains the whole column {ε₁} × K (the identity of
𝒢 lies in H), membership in M is insensitive to the second coordinate:
(g , k) ∈ M iff (g , ε₂) ∈ M. The two directions are
slice-out and slice-in; each multiplies by a
column element and rewrites along the pointwise description of ∙ₓ — this is the
note's observation that (g , k) ≈ (g , ε) ∙ (ε , k) with (ε , k) ∈ H ×ᶠ 𝒦 ⊆ M.
Consequently the restriction λ g → M (g , ε₂) is a respecting subgroup of 𝒢
containing H, and pulling it back along proj₁ recovers M — the mutually
inverse maps of the fattening lemma.
module Slice₁ (H : Pred G ℓ) (H-sg : IsSubgroup 𝒢 H) (M : Pred (G × K) ℓᴹ) (M-sub : M ∈ Subuniverses 𝑮×𝑲) (M-resp : M Respects _≈ₓ_) (HK⊆M : (H ×ᶠ 𝒦) ⊆ M) where -- M contains the column {ε₁} × K, because ε₁ ∈ H. ε-column : (k : K) → (ε₁ , k) ∈ M ε-column k = HK⊆M (IsSubgroup.ε-closed H-sg) -- Forgetting the second coordinate: (g , k) ∈ M implies (g , ε₂) ∈ M. slice-out : ∀ {g k} → (g , k) ∈ M → (g , ε₂) ∈ M slice-out {g} {k} m = M-resp (transₓ (∙ₓ-pointwise (g , k) (ε₁ , k ⁻¹₂)) (idʳ-law₁ g , invʳ-law₂ k)) (sub-∙-closed ×ᵍ-Group M M-sub m (ε-column (k ⁻¹₂))) -- Reinstating any second coordinate: (g , ε₂) ∈ M implies (g , k) ∈ M. slice-in : ∀ {g k} → (g , ε₂) ∈ M → (g , k) ∈ M slice-in {g} {k} m = M-resp (transₓ (∙ₓ-pointwise (g , ε₂) (ε₁ , k)) (idʳ-law₁ g , idˡ-law₂ k)) (sub-∙-closed ×ᵍ-Group M M-sub m (ε-column k)) -- The restriction of M to the first coordinate. restrict₁ : Pred G ℓᴹ restrict₁ g = M (g , ε₂) -- The restriction is a respecting subgroup of 𝒢. restrict₁-isSubgroup : IsSubgroup 𝒢 restrict₁ restrict₁-isSubgroup = mkIsSubgroup 𝒢 resp ∙-closed ε-closed ⁻¹-closed where resp : restrict₁ Respects _≈₁_ resp e m = M-resp (e , refl₂) m ∙-closed : ∀ {x y} → restrict₁ x → restrict₁ y → restrict₁ (x ∙₁ y) ∙-closed {x} {y} mx my = M-resp (transₓ (∙ₓ-pointwise (x , ε₂) (y , ε₂)) (refl₁ , idˡ-law₂ ε₂)) (sub-∙-closed ×ᵍ-Group M M-sub mx my) ε-closed : restrict₁ ε₁ ε-closed = ε-column ε₂ ⁻¹-closed : ∀ {x} → restrict₁ x → restrict₁ (x ⁻¹₁) ⁻¹-closed {x} m = M-resp (transₓ (⁻¹ₓ-pointwise (x , ε₂)) (refl₁ , ε⁻¹≈ε₂)) (sub-⁻¹-closed ×ᵍ-Group M M-sub m) -- The restriction contains H (specialize HK⊆M to pairs (g , ε₂)). restrict₁-⊇H : H ⊆ restrict₁ restrict₁-⊇H h = HK⊆M h -- Round trip: pulling the restriction back along proj₁ recovers M. restrict₁-pull-⊆ : (λ p → restrict₁ (proj₁ p)) ⊆ M restrict₁-pull-⊆ m = slice-in m restrict₁-pull-⊇ : M ⊆ (λ p → restrict₁ (proj₁ p)) restrict₁-pull-⊇ m = slice-out m
The slice toolkit, second coordinate¶
The mirror of Slice₁: for a respecting subgroup M ⊇ 𝒢 ᶠ× J of the
product, membership is insensitive to the first coordinate, the restriction
λ k → M (ε₁ , k) is a respecting subgroup of 𝒦 containing J, and pulling back
along proj₂ recovers M. The proofs are the coordinatewise mirrors of the ones
above.
module Slice₂ (J : Pred K ℓ) (J-sg : IsSubgroup 𝒦 J) (M : Pred (G × K) ℓᴹ) (M-sub : M ∈ Subuniverses 𝑮×𝑲) (M-resp : M Respects _≈ₓ_) (GJ⊆M : (𝒢 ᶠ× J) ⊆ M) where -- M contains the row G × {ε₂}, because ε₂ ∈ J. ε-row : (g : G) → (g , ε₂) ∈ M ε-row g = GJ⊆M (IsSubgroup.ε-closed J-sg) -- Forgetting the first coordinate: (g , k) ∈ M implies (ε₁ , k) ∈ M. slice-out : ∀ {g k} → (g , k) ∈ M → (ε₁ , k) ∈ M slice-out {g} {k} m = M-resp (transₓ (∙ₓ-pointwise (g , k) (g ⁻¹₁ , ε₂)) (invʳ-law₁ g , idʳ-law₂ k)) (sub-∙-closed ×ᵍ-Group M M-sub m (ε-row (g ⁻¹₁))) -- Reinstating any first coordinate: (ε₁ , k) ∈ M implies (g , k) ∈ M. slice-in : ∀ {g k} → (ε₁ , k) ∈ M → (g , k) ∈ M slice-in {g} {k} m = M-resp (transₓ (∙ₓ-pointwise (g , ε₂) (ε₁ , k)) (idʳ-law₁ g , idˡ-law₂ k)) (sub-∙-closed ×ᵍ-Group M M-sub (ε-row g) m) -- The restriction of M to the second coordinate. restrict₂ : Pred K ℓᴹ restrict₂ k = M (ε₁ , k) -- The restriction is a respecting subgroup of 𝒦. restrict₂-isSubgroup : IsSubgroup 𝒦 restrict₂ restrict₂-isSubgroup = mkIsSubgroup 𝒦 resp ∙-closed ε-closed ⁻¹-closed where resp : restrict₂ Respects _≈₂_ resp e m = M-resp (refl₁ , e) m ∙-closed : ∀ {x y} → restrict₂ x → restrict₂ y → restrict₂ (x ∙₂ y) ∙-closed {x} {y} mx my = M-resp (transₓ (∙ₓ-pointwise (ε₁ , x) (ε₁ , y)) (idʳ-law₁ ε₁ , refl₂)) (sub-∙-closed ×ᵍ-Group M M-sub mx my) ε-closed : restrict₂ ε₂ ε-closed = ε-row ε₁ ⁻¹-closed : ∀ {x} → restrict₂ x → restrict₂ (x ⁻¹₂) ⁻¹-closed {x} m = M-resp (transₓ (⁻¹ₓ-pointwise (ε₁ , x)) (ε⁻¹≈ε₁ , refl₂)) (sub-⁻¹-closed ×ᵍ-Group M M-sub m) -- The restriction contains J. restrict₂-⊇J : J ⊆ restrict₂ restrict₂-⊇J j = GJ⊆M j -- Round trip: pulling the restriction back along proj₂ recovers M. restrict₂-pull-⊆ : (λ p → restrict₂ (proj₂ p)) ⊆ M restrict₂-pull-⊆ m = slice-in m restrict₂-pull-⊇ : M ⊆ (λ p → restrict₂ (proj₂ p)) restrict₂-pull-⊇ m = slice-out m
The product as a binary operation on groups¶
The infix form, for use at call sites.
infixr 7 _×ᵍ_ _×ᵍ_ : Group α ρ → Group β σ → Group (α ⊔ β) (ρ ⊔ σ) 𝒢 ×ᵍ 𝒦 = GroupProduct.×ᵍ-Group 𝒢 𝒦