Commensurable.commensurable_conj
theorem Commensurable.commensurable_conj :
∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (g : ConjAct G),
Commensurable H K ↔ Commensurable (g • H) (g • K)
This theorem states that for any group `G`, and any two subgroups `H` and `K` of `G`, along with a group element `g` (viewed as an element of the "conjugate action" `ConjAct`), the two subgroups `H` and `K` are commensurable if and only if the conjugates of the subgroups by `g` (i.e., `g•H` and `g•K`) are also commensurable. Here, "commensurable" means that the intersection of the two subgroups has finite index in both subgroups, and "conjugation" of a subgroup by `g` means the set of elements obtained by multiplying each element of the subgroup on the left by `g` and on the right by `g⁻¹`.
More concisely: For any group `G`, subgroups `H` and `K` of `G`, and group element `g`, `H` and `K` are commensurable if and only if their conjugates `g•H` and `g•K` are commensurable.
|
Commensurable.trans
theorem Commensurable.trans :
∀ {G : Type u_1} [inst : Group G] {H K L : Subgroup G}, Commensurable H K → Commensurable K L → Commensurable H L
The theorem `Commensurable.trans` states that for any group `G` and any subgroups `H`, `K`, and `L` of `G`, if `H` and `K` are commensurable and `K` and `L` are commensurable, then `H` and `L` are also commensurable. In other words, the commensurability relation among subgroups of a group is transitive. In group theory terms, if the relative index of `H` and `K` is nonzero (i.e., `H` has finite index in `K` and vice versa), and the same holds for `K` and `L`, then the relative index of `H` and `L` is also nonzero (i.e., `H` has finite index in `L` and vice versa).
More concisely: If subgroups `H`, `K`, and `L` of a group `G` are pairwise commensurable, then `H` and `L` are commensurable. (Two subgroups `H` and `K` of a group `G` are commensurable if they have finite index in each other.)
|