Monoid.CoprodI.NeWord.of_word
theorem Monoid.CoprodI.NeWord.of_word :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M),
w ≠ Monoid.CoprodI.Word.empty → ∃ i j w', w'.toWord = w
This theorem states that for any nonempty word 'w' in the monoidal coproduct 'M', where 'M' is a type family over some indexing type 'ι' and each 'M i' is a monoid, it can always be constructed as a 'NeWord M i j' for some 'i', 'j' and 'w''. In other words, any non-empty reduced word in the monoidal coproduct can be seen as a non-empty word with specific starting and ending indices.
More concisely: For any nonempty word in the monoidal coproduct of a type family of monoids, there exist indices i and j such that the word equals the non-empty NeWord at those indices.
|
Monoid.CoprodI.ext_hom
theorem Monoid.CoprodI.ext_hom :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N]
(f g : Monoid.CoprodI M →* N), (∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of) → f = g
This theorem states that for any index type `ι`, any family of monoids `M` indexed by `ι`, and any monoid `N`, if we have two monoid homomorphisms `f` and `g` from the free product of the family `M` to `N`, then `f` and `g` are equal if and only if their compositions with the inclusion of every summand into the free product are equal. This theorem allows us to perform an extensionality argument when working with homomorphisms from the free product of a family of monoids.
More concisely: For any index type `ι`, any family of monoids `M` indexed by `ι`, and any monoids `N` and monoid homomorphisms `f` and `g` from the free product of `M` to `N`, `f` and `g` are equal if and only if their compositions with the inclusion of every summand into the free product are equal.
|
Monoid.CoprodI.Word.equivPair_symm
theorem Monoid.CoprodI.Word.equivPair_symm :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)]
[inst_2 : DecidableEq ι] (i : ι) (p : Monoid.CoprodI.Word.Pair M i),
(Monoid.CoprodI.Word.equivPair i).symm p = Monoid.CoprodI.Word.rcons p
The theorem `Monoid.CoprodI.Word.equivPair_symm` asserts that for any type `ι`, any function `M` mapping elements of `ι` to types, any monoid structure on each `M i`, any decidable equality on each `M i` and on `ι`, for any `i` in `ι` and any pair `p` in the word pair of the coproduct of monoids `M i`, applying the inverse of the equivalence `Monoid.CoprodI.Word.equivPair` on `p` yields the same result as applying the function `Monoid.CoprodI.Word.rcons` on `p`. Specifically, `Monoid.CoprodI.Word.rcons` forms a word by prepending the `head` of the pair to the `tail`, except if the `head` is the unit element of the monoid, in which case it just returns the `tail`. This theorem asserts that this process of forming a word is in a sense inverse to the operation `Monoid.CoprodI.Word.equivPair`.
More concisely: For any monoid family `M` over a type `ι`, the inverse of the equivalence `Monoid.CoprodI.Word.equivPair` on a pair in the coproduct of words equals applying the function `Monoid.CoprodI.Word.rcons` to the pair.
|
Monoid.CoprodI.lift_injective_of_ping_pong
theorem Monoid.CoprodI.lift_injective_of_ping_pong :
∀ {ι : Type u_1} [hnontriv : Nontrivial ι] {G : Type u_4} [inst : Group G] {H : ι → Type u_5}
[inst_1 : (i : ι) → Group (H i)] (f : (i : ι) → H i →* G),
(3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
(∀ (i : ι), (X i).Nonempty) →
(Pairwise fun i j => Disjoint (X i) (X j)) →
(Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
Function.Injective ⇑(Monoid.CoprodI.lift f)
The **Ping-Pong Lemma** states that given a group action of a group `G` on a set `X`, where each subgroup `H i` acts in a specific way on disjoint subsets `X i`, we can prove that the function `lift f` is injective. This implies that the image of `lift f` is isomorphic to the free product of the `H i`.
This lemma is often stated for subgroups `H i` that generate the whole group; however, our version generalizes to arbitrary group homomorphisms `f i : H i →* G` and does not require the group to be generated by the images.
Typically, the Ping-Pong Lemma requires that one group `H i` has at least three elements. We only need this condition if the cardinality of `ι` is 2, and alternatively, we accept `3 ≤ # ι`.
More concisely: The Ping-Pong Lemma asserts that if a group `G` acts on a set `X` such that each subgroup `H i` (with at least 3 elements if `X` has more than two parts) acts freely and transitively on its disjoint subset `X i`, then the induced function `lift f : ⨄(H i) →* G` is injective and its image is isomorphic to the free product of the `H i`.
|
Monoid.CoprodI.Word.of_smul_def
theorem Monoid.CoprodI.Word.of_smul_def :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)]
[inst_2 : DecidableEq ι] (i : ι) (w : Monoid.CoprodI.Word M) (m : M i),
Monoid.CoprodI.of m • w =
Monoid.CoprodI.Word.rcons
(let __src := (Monoid.CoprodI.Word.equivPair i) w;
{ head := m * ((Monoid.CoprodI.Word.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯ })
The theorem `Monoid.CoprodI.Word.of_smul_def` states that for any type `ι`, function `M : ι → Type u_2`, where each `M i` is a monoid, and each `M i` and `ι` have decidable equality, for any `i : ι`, word `w : Monoid.CoprodI.Word M` and element `m : M i`, the operation of the inclusion of `m` into the free product acting on `w` is equal to the operation of constructing a new word by prepending `m` multiplied by the head of `w` (when `w` is viewed as a pair) to the tail of `w`, unless this product is the identity of the monoid `M i`, in which case we just return the tail of `w`. In other words, this means that the action of the inclusion of `m` into the free product on a word is defined by multiplication on the leftmost element of the word from `M i`.
More concisely: For any monoid-valued family `M : ι → Type` and decidably equal types `ι` and `M i`, the operation of including an element `m : M i` into the free product of `M i` acting on a `Monoid.CoprodI.Word w : Monoid.CoprodI.Word M i` is equal to prepending the product of `m` and the head of `w`, or the tail of `w` if the product is the identity of `M i`.
|
Monoid.CoprodI.lift_of
theorem Monoid.CoprodI.lift_of :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
(fi : (i : ι) → M i →* N) {i : ι} (m : M i), (Monoid.CoprodI.lift fi) (Monoid.CoprodI.of m) = (fi i) m
The theorem `Monoid.CoprodI.lift_of` states that for any types `ι` and `M`, where `M` is a function from `ι` to a type, and for every index `i` in `ι` there is a monoid structure on `M i`, and given any type `N` with a monoid structure and a function `fi` that maps each `i` in `ι` and each element of `M i` to `N`, if you lift `fi` over the coproduct of the monoids `M i` and then apply it to the coproduct inclusion of an element `m` from `M i`, the result is the same as if you had applied `fi` directly to `i` and `m`. In other words, the theorem asserts the property of the `Monoid.CoprodI.lift` operation behaving as expected with respect to the `Monoid.CoprodI.of` operation in the context of monoid homomorphisms.
More concisely: For any type `ι` and function `M : ι → Type` with each `M i` being a monoid, and given a monoid `N` and a function `fi : ∀ i, M i → N`, the monoid homomorphism `Monoid.CoprodI.lift fi` satisfies `fi (Monoid.CoprodI.of i m) = Monoid.lift (fi i) m`, for all `i ∈ ι` and `m ∈ M i`.
|
Monoid.CoprodI.Word.ne_one
theorem Monoid.CoprodI.Word.ne_one :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M),
∀ l ∈ self.toList, l.snd ≠ 1
This theorem asserts that in any reduced word of a coproduct of monoids, there is no element equal to the identity element (`1`). More precisely, given an indexing type `ι`, a family of monoids `M` indexed by `ι`, and a reduced word `self` in the coproduct of these monoids, for any element `l` in the list representation of `self`, the second component of `l` (which corresponds to an element of one of the monoids `M i`) is not the identity of that monoid.
More concisely: In the coproduct of monoids indexed by type `ι`, no identity element occurs in any reduced word.
|
FreeGroup.injective_lift_of_ping_pong
theorem FreeGroup.injective_lift_of_ping_pong :
∀ {ι : Type u_1} [inst : Nontrivial ι] {G : Type u_1} [inst : Group G] (a : ι → G) {α : Type u_4}
[inst_1 : MulAction G α] (X Y : ι → Set α),
(∀ (i : ι), (X i).Nonempty) →
(Pairwise fun i j => Disjoint (X i) (X j)) →
(Pairwise fun i j => Disjoint (Y i) (Y j)) →
(∀ (i j : ι), Disjoint (X i) (Y j)) →
(∀ (i : ι), a i • (Y i)ᶜ ⊆ X i) →
(∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i) → Function.Injective ⇑(FreeGroup.lift a)
The Ping-Pong Lemma in this context states that: given a group `G` acting on a type `α` in such a way that the generators of the free groups act on disjoint subsets `X i` and `Y i` in predefined ways, if certain conditions regarding these sets and the group action are met, then the lift function `lift f` from the free group to `G` is injective. This implies that the image of `lift f` is isomorphic to the free group. The specific conditions for this result are: each set `X i` is nonempty, the sets `X i` are pairwise disjoint, as are the sets `Y i`, and each `X i` is disjoint from each `Y j`. Additionally, for each `i`, the action of `a i` on the complement of `Y i` is a subset of `X i`, and the action of the inverse `a⁻¹ i` on the complement of `X i` is a subset of `Y i`. The lemma is a generalization as it applies to arbitrary group homomorphisms from the free group to `G` and does not require the group `G` to be generated by specific elements.
More concisely: Given a group action of a free group on disjoint sets `X i` and `Y i` such that the generators act on disjoint subsets with specific conditions on their actions outside of these sets, any group homomorphism from the free group to the target group maps distinct generators to distinct elements.
|
Monoid.CoprodI.induction_on
theorem Monoid.CoprodI.induction_on :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {C : Monoid.CoprodI M → Prop}
(m : Monoid.CoprodI M),
C 1 →
(∀ (i : ι) (m : M i), C (Monoid.CoprodI.of m)) → (∀ (x y : Monoid.CoprodI M), C x → C y → C (x * y)) → C m
This theorem, named `Monoid.CoprodI.induction_on`, is a principle of induction for the free product of an indexed family of monoids. In detail, it states that for any type `ι`, any indexed family of monoids `M` indexed by `ι`, and any property `C` pertaining to the elements of the free product of `M`, if the property `C` holds for the multiplicative identity `1`, for any element obtained by the inclusion of a summand into the free product, and is closed under multiplication, then `C` must hold for any element of the free product of `M`.
More concisely: Given an indexed family of monoids `M` and a property `C` that holds for the multiplicative identity of each monoid and is closure under multiplication, `C` holds for any element in the free product of `M`.
|
Monoid.CoprodI.Word.chain_ne
theorem Monoid.CoprodI.Word.chain_ne :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (self : Monoid.CoprodI.Word M),
List.Chain' (fun l l' => l.fst ≠ l'.fst) self.toList
The theorem `Monoid.CoprodI.Word.chain_ne` asserts that for any type `ι`, any type `M` mapped from `ι`, and any instance of a monoid over `M i` for each `i` in `ι`, for every word in the coproduct of monoids, the first element of each adjacent pair in the list representation of the word is not equal. In simpler terms, this theorem states that no two adjacent elements in the list representation of the word come from the same summand in the coproduct of monoids.
More concisely: For any type `ι`, any type `M` mapping from `ι` with a monoid structure over each `M i`, the list representation of any word in the coproduct of these monoids does not contain adjacent elements from the same summand.
|
Monoid.CoprodI.Word.Pair.fstIdx_ne
theorem Monoid.CoprodI.Word.Pair.fstIdx_ne :
∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (self : Monoid.CoprodI.Word.Pair M i),
self.tail.fstIdx ≠ some i
This theorem states that for any type `ι`, any type function `M` from `ι` to another type, and any `ι`-indexed monoid instance, the first index of the tail of a `Pair M i` within a monoid coproduct word is not equal to `i`. In other words, the next element in the sequence after a pair in a monoid coproduct word can't have the same index as the pair itself.
More concisely: For any type `ι`, any type function `M : ι → Type`, and any monoid instance for the `Pair M` coproduct, the indices of consecutive pairs in a monoid coproduct word are distinct.
|