HNNExtension.NormalWord.ReducedWord.chain
theorem HNNExtension.NormalWord.ReducedWord.chain :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (self : HNNExtension.NormalWord.ReducedWord G A B),
List.Chain' (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) self.toList
This theorem states that in the context of a group `G` and two subgroups `A` and `B` of `G`, for any reduced word in the Higman–Neumann–Neumann (HNN) extension of `G` with respect to `A` and `B`, there are no sequences in the form `t^u * g * t^-u` where `g` belongs to the subgroup determined by function `toSubgroup A B u`. Here, `t` is any element of the group and `u` is either `1` or `-1`. This is captured by the condition that if `a` and `b` are two consecutive elements of the representation of the reduced word as a list, and `a`'s second component belongs to the subgroup determined by `toSubgroup A B a.1`, then `a`'s first component and `b`'s first component must be equal.
More concisely: In the context of a group `G` and two subgroups `A` and `B` of `G`, for any reduced word in the HNN extension of `G` with respect to `A` and `B`, if for consecutive elements `a` and `b` of the representation as a list, `a.2` is in the subgroup generated by `A` and `B` at position `a.1`, then `a.1` and `b.1` must be equal.
|
HNNExtension.NormalWord.mem_set
theorem HNNExtension.NormalWord.mem_set :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B}
(self : HNNExtension.NormalWord d) (u : ℤˣ) (g : G), (u, g) ∈ self.toList → g ∈ d.set u
This theorem states that for any group `G` and any two subgroups `A` and `B` of `G`, and given a transversal pair `d` in the group `G` for the subgroups `A` and `B`, any normal word `self` on this transversal pair and any non-zero integer `u` and element `g` of the group `G`, if the pair `(u, g)` is in the list representation of `self`, then `g` is an element of the set `d.set u` defined by the transversal pair `d`. Effectively, it states that every element of the group in the list representation of the normal word is the chosen element of its coset.
More concisely: Given any group `G`, subgroups `A` and `B` with transversal pair `d`, and normal word `self` on `d` with integer `u` and element `g` in its list representation, if `(u, g)` is in `self`, then `g` belongs to `d.set u`.
|
HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq
theorem HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B)
{w₁ w₂ : HNNExtension.NormalWord.ReducedWord G A B},
HNNExtension.NormalWord.ReducedWord.prod φ w₁ = HNNExtension.NormalWord.ReducedWord.prod φ w₂ →
List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧
∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ HNNExtension.toSubgroup A B (-u)
The theorem `HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq` states that for any group `G` and its subgroups `A` and `B`, and an isomorphism `φ` between `A` and `B`, if we have two reduced words `w₁` and `w₂` representing the same element of the HNN extension of `G` with respect to `A`, `B`, and `φ`, then their corresponding lists, obtained by mapping the first projection function (`Prod.fst`), are the same, and furthermore, for any `u` which is the exponent of the first occurrence of `t` in the word, if `u` exists in the first element of the list of `w₁`, then the inverse of the first element of `w₁` times the first element of `w₂` belongs to a specific subgroup, determined by `A`, `B` and `-u` using the `HNNExtension.toSubgroup` function.
In simpler terms, this theorem ensures that two reduced words that represent the same element in the HNN extension have an identical pattern of occurrences of `t^1` and `t^(-1)`, and their starting elements belong to the same left coset of a specific subgroup.
More concisely: In the HNN extension of a group with respect to two subgroups and an isomorphism between them, two reduced words representing the same element have identical lists obtained by applying the first projection function, and the inverses of the initial segments of the first word times the initial segments of the second word belong to a specific subgroup determined by the subgroups and the inverses of their exponents in the first word.
|
HNNExtension.NormalWord.not_cancels_of_cons_hyp
theorem HNNExtension.NormalWord.not_cancels_of_cons_hyp :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ)
(w : HNNExtension.NormalWord d),
(∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') →
¬HNNExtension.NormalWord.Cancels u w
This theorem, `HNNExtension.NormalWord.not_cancels_of_cons_hyp`, states that for any type `G` that forms a group, any two subgroups `A` and `B` of this group, and a specific transversal pair `d` in the normal word extension of this group, for any integer unit `u` and normal word `w`, if for all `u'` in the mapping of the first projection of the head of the list representation of `w` onto `Option`, the head of `w` belongs to the subgroup derived from `A`, `B`, and `u`, and `u` is equal to `u'`, then it is not the case that the operation `t^u` cancels with some occurrence of `t^-u` when multiplying `t^u` by `w`. In mathematical terms, if for any `u'` in the image of the function `Option.map Prod.fst` applied to `w.toList.head?`, the head of `w` is an element of the derived subgroup determined by `u`, and `u` is equal to `u'`, then `t^u` does not cancel with some occurrence of `t^-u` in the multiplication of `t^u` by `w`.
More concisely: For any group `G`, subgroups `A` and `B`, transversal pair `d` in the normal word extension of `G`, integer unit `u`, and normal word `w`, if the head of `w` belongs to the subgroup generated by `A`, `B`, and `u` for all `u'` in the image of the function `Option.map fst` applied to `w.toList.head?`, then there is no cancellation between `t^u` and some occurrence of `t^-u` in the product `t^u * w`.
|
HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range
theorem HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (w : HNNExtension.NormalWord.ReducedWord G A B),
HNNExtension.NormalWord.ReducedWord.prod φ w ∈ HNNExtension.of.range → w.toList = []
**Britton's Lemma** states that for any reduced word, in the context of Higman–Neumann–Neumann (HNN) extensions, whose product is an element of a group `G`, this word contains no occurrences of the letter `t`. More specifically, for any group `G` and its subgroups `A` and `B`, with an isomorphism `φ` between `A` and `B`, if the product of a reduced word `w`, computed with the `HNNExtension.NormalWord.ReducedWord.prod` function, belongs to the range of the canonical embedding `HNNExtension.of` from `G` to its HNN extension, then the list representation of `w` must be empty.
More concisely: In the context of Higman-Neumann-Neumann extensions, if a reduced word in a group `G` belongs to the range of the canonical embedding from `G` to its HNN extension generated by a subgroup `A` and an isomorphism `φ` between `A` and a subgroup `B`, then the word contains no occurrences of the generator `t` from `B`.
|
HNNExtension.NormalWord.TransversalPair.compl
theorem HNNExtension.NormalWord.TransversalPair.compl :
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (self : HNNExtension.NormalWord.TransversalPair G A B)
(u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (self.set u)
This theorem states that for any given type `G` that forms a group, any two subgroups `A` and `B` of `G`, an instance of `HNNExtension.NormalWord.TransversalPair` for the group `G` and the subgroups `A` and `B`, and any unit integer `u`, the subgroup obtained from `HNNExtension.toSubgroup` for `A`, `B`, and `u`, and the set generated by the `HNNExtension.NormalWord.TransversalPair` instance using `u`, are complements. In other words, the function that maps each pair of elements from these two sets to their product in the group `G` is a bijection, which means that every element of the group can be expressed uniquely as a product of an element from the subgroup and an element from the set.
More concisely: For any group `G`, subgroups `A` and `B`, and a unit integer `u`, the subgroups generated by `HNNExtension.NormalWord.TransversalPair` for `A`, `B`, and `u`, are complements in `G`. That is, their product forms every element of `G` exactly once.
|