Monoid.PushoutI.NormalWord.normalized
theorem Monoid.PushoutI.NormalWord.normalized :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} (self : Monoid.PushoutI.NormalWord d)
(i : ι) (g : G i), ⟨i, g⟩ ∈ self.toList → g ∈ d.set i
This theorem states that for any group theory context with a certain set of groups `G` indexed by `ι`, and a group `H`, along with group homomorphisms `φ` from `H` to each `G i`, and a transversal `d` for a normal word in the pushout of these groups, any element `g` of group `G i` that appears in the list form of the normal word is also an element of the transversal's set at index `i`.
More concisely: For any normal subgroup inclusion `⨆i φ(H) ⊆ Gi` in group theory, if `d` is a transversal for a normal word and every `g` in the list form of the word lies in `Gi`, then `g` is an element of the transversal `d` at index `i`.
|
Monoid.PushoutI.of_injective
theorem Monoid.PushoutI.of_injective :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i},
(∀ (i : ι), Function.Injective ⇑(φ i)) → ∀ (i : ι), Function.Injective ⇑(Monoid.PushoutI.of i)
The theorem `Monoid.PushoutI.of_injective` states that for any type `ι`, any function `G` from `ι` to a type, and any type `H`, given that each `G i` is a group and `H` is also a group, and given a family of monoid homomorphisms `φ` from `H` to each `G i`, if every monoid homomorphism `φ i` is injective, then the function `Monoid.PushoutI.of i` (which maps each indexing group into the amalgamated product of groups, or the pushout) is also injective. In other words, if every group homomorphism in the diagram is injective, then all maps into the amalgamated product of these groups are also injective.
More concisely: If each monoid homomorphism in a commutative diagram of groups and monoids with injective group homomorphisms is an injective monoid homomorphism, then the induced homomorphism from the pushout to the amalgamated product is also injective.
|
Monoid.PushoutI.of_comp_eq_base
theorem Monoid.PushoutI.of_comp_eq_base :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
{φ : (i : ι) → H →* G i} (i : ι), (Monoid.PushoutI.of i).comp (φ i) = Monoid.PushoutI.base φ
The theorem `Monoid.PushoutI.of_comp_eq_base` states that for any index set `ι`, a family `G : ι → Type` of monoids, a base monoid `H`, and a family `φ : (i : ι) → H →* G i` of monoid homomorphisms from `H` to each `G i`, the composition of the morphism `Monoid.PushoutI.of i` (which is a map from each indexing group into the pushout) with `φ i` is equal to the morphism `Monoid.PushoutI.base φ` (which is a map from the base monoid `H` into the pushout). In other words, each `G i` and the base `H` map to the same place in the pushout via these respective maps, up to composition with the original homomorphisms `φ`.
More concisely: For any index set ι, family of monoids G : ι → Type, base monoid H, and family of monoid homomorphisms φ : (i : ι) → H →* G i, the composition of Monoid.PushoutI.of i with φ i equals Monoid.PushoutI.base φ.
|
Monoid.PushoutI.NormalWord.Transversal.one_mem
theorem Monoid.PushoutI.NormalWord.Transversal.one_mem :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι), 1 ∈ self.set i
This theorem states that for any index `ι`, any family `G` of groups indexed by `ι`, any group `H`, and any family `φ` of group homomorphisms from `H` to each group in `G`, for any transversal of the normal word in the pushout of `ι` under `φ`, the identity element of the group is included in the set corresponding to that index. Essentially, it states that the identity element of each group in the family `G` is contained in the corresponding set of the transversal of the normal word in the pushout.
More concisely: For any index `ι`, given a family `G` of groups indexed by `ι`, a group `H`, and a family `φ` of group homomorphisms from `H` to each group in `G`, the identity element of each group `G(i)` in the pushout of `ι` under `φ` is contained in the corresponding set of the transversal of the normal word.
|
Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized
theorem Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
[inst_3 : (i : ι) → DecidableEq (G i)] (w : Monoid.CoprodI.Word G) {i : ι} (h : H),
(∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) →
(∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (Monoid.CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j) → h = 1
This theorem asserts that for any type `ι`, groups `G : ι → Type u_2` and `H : Type u_3`, morphisms `φ : (i : ι) → H →* G i`, and a transversal `d` of `Monoid.PushoutI.NormalWord` with decidable equality on `ι` and each `G i`, given a word `w` in the coproduct of the groups `G`, if every letter in `w` is in the transversal and remains in the transversal when multiplied by an element `h` of the base group `H`, then the multiplying element `h` must be the identity element of the group `H`. In mathematical terms, if a multiplication operation preserves a set property under a specific mapping, the multiplier is the identity element.
More concisely: Given a transversal `d` of normal words in a coproduct of groups `G : ι → Type` with decidable equality and a morphism `φ : ∏ i : ι, H →* G i`, if every word in the image of `φ` that maps to an element `h` in `H` and contains only letters in `d` is closed under multiplication by `h`, then `h` is the identity element in `H`.
|
Monoid.PushoutI.NormalWord.Transversal.compl
theorem Monoid.PushoutI.NormalWord.Transversal.compl :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι),
Subgroup.IsComplement (↑(φ i).range) (self.set i)
This theorem states that for any index `i` and given a transversal `self` with respect to a function `φ` from a group `H` to a group `G i` for each `i`, the image of `φ i` and the set `self.set i` are complements. In other words, for every `i`, there exists a bijection between pairs formed from elements of `φ i`'s range and `self.set i` to the group `G i`, which is achieved by multiplying the elements of the pair. This concept generalizes the notions of left and right transversals, as well as complementary subgroups.
More concisely: For any transversal `self` with respect to a group homomorphism `φ` from group `H` to a group `G`, the sets `φ(i)(H)` and `self.set i` are complementary subsets of `G` for each `i` via the bijection given by multiplication.
|
Monoid.PushoutI.NormalWord.Transversal.injective
theorem Monoid.PushoutI.NormalWord.Transversal.injective :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i}, Monoid.PushoutI.NormalWord.Transversal φ → ∀ (i : ι), Function.Injective ⇑(φ i)
This theorem states that for any type `ι`, types `G` indexed by `ι`, and type `H`, given group structures on each `G i` and `H`, and a collection of homomorphisms `φ` from `H` to each `G i`, if the `φ` map is a transversal to the normal word in the monoid pushout, then each `φ i` map is injective.
In other words, if we have a set of groups indexed by `ι`, and an additional group `H`, with homomorphisms defined from `H` to each of the indexed groups, if these homomorphisms collectively satisfy the condition of being a transversal to the normal word in a specific construction called the monoid pushout, then each individual homomorphism is injective, i.e., it maps distinct elements of `H` to distinct elements in its corresponding indexed group.
More concisely: Given types `ι`, `G` indexed by `ι`, and a group `H` with homomorphisms `φ` from `H` to each `G i`, if `φ` forms a transversal to the normal subgroup in the monoid pushout and `H` is the quotient of a free group by a normal subgroup, then each `φ i` is injective.
|
Monoid.PushoutI.NormalWord.prod_smul
theorem Monoid.PushoutI.NormalWord.prod_smul :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
[inst_3 : (i : ι) → DecidableEq (G i)] (g : Monoid.PushoutI φ) (w : Monoid.PushoutI.NormalWord d),
(g • w).prod = g * w.prod
The theorem `Monoid.PushoutI.NormalWord.prod_smul` states that for any indexed collection of groups `G`, and a group `H`, given group homomorphisms `φ` from `H` to each of the groups in `G` and a transversal `d` of the normal word in the indexed pushout of the monoids, along with an element `g` of the pushout and a normal word `w`, the operation of taking the product of the normal word (function `Monoid.PushoutI.NormalWord.prod`) commutes with the scalar multiplication (`g • w`). In other words, scaling the normal word by `g` and then taking the product gives the same result as first taking the product and then scaling by `g`. This is expressed mathematically as: `Monoid.PushoutI.NormalWord.prod (g • w) = g * Monoid.PushoutI.NormalWord.prod w`.
More concisely: For any indexed collection of groups `G`, group `H`, group homomorphisms `φ` from `H` to each `G`, transversal `d` of the normal word in the indexed pushout of the monoids, and elements `g` in the pushout and `w` in the normal subgroup, we have `g * Monoid.PushoutI.NormalWord.prod w = Monoid.PushoutI.NormalWord.prod (g • w)`.
|
Monoid.PushoutI.inf_of_range_eq_base_range
theorem Monoid.PushoutI.inf_of_range_eq_base_range :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i},
(∀ (i : ι), Function.Injective ⇑(φ i)) →
∀ {i j : ι},
i ≠ j → (Monoid.PushoutI.of i).range ⊓ (Monoid.PushoutI.of j).range = (Monoid.PushoutI.base φ).range
The theorem `Monoid.PushoutI.inf_of_range_eq_base_range` states that in an algebraic structure known as a monoid pushout (which is a form of amalgamated product), the intersection of the images under the monoid homomorphisms (which are injective) from any two distinct monoids in the diagram is equal to the image under the homomorphism from the base monoid. Here, the diagram refers to a categorical one, where each object is a monoid and each arrow is a monoid homomorphism. In other words, the common elements in the images of two different monoids in a pushout are exactly those coming from the base monoid.
More concisely: In a monoid pushout diagram, the intersection of the images of two distinct monoids equals the image of the base monoid under the corresponding homomorphisms.
|
Monoid.PushoutI.Reduced.eq_empty_of_mem_range
theorem Monoid.PushoutI.Reduced.eq_empty_of_mem_range :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i},
(∀ (i : ι), Function.Injective ⇑(φ i)) →
∀ {w : Monoid.CoprodI.Word G},
Monoid.PushoutI.Reduced φ w →
Monoid.PushoutI.ofCoprodI w.prod ∈ (Monoid.PushoutI.base φ).range → w = Monoid.CoprodI.Word.empty
This theorem states that for any given word `w` in the coproduct of a collection of groups `G` indexed by `ι`, if `w` is reduced (that is, none of its letters belong to the image of the base group `H`) and `w` is not empty, then `w` is not in the image of the base group. Here, satisfying the property of being reduced means that no letter in `w` belongs to the image of any homomorphism from `H` to any `G i`. The theorem requires the condition that each of these homomorphisms is injective. If these conditions are met and `w` is found in the image of the base group, then `w` must be the empty word.
More concisely: If `w` is a non-empty, reduced word in the coproduct of a collection of groups `G` indexed by `ι`, where each homomorphism from the base group `H` to `G i` is injective, then `w` is not in the image of `H`.
|
Monoid.PushoutI.NormalWord.Pair.normalized
theorem Monoid.PushoutI.NormalWord.Pair.normalized :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι}
(self : Monoid.PushoutI.NormalWord.Pair d i) (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ self.tail.toList → g ∈ d.set i_1
This theorem states that for any given group homomorphisms and a transversal (a selection of representatives) of a normal word in a pushout of groups, every element of a pair in the normal word that appears in the list representation of the tail of the pair is in the set of the transversal corresponding to its group. In other words, all letters in the word are in the transversal.
More concisely: For any normal subgroup inclusion `H ⊆ G` and group homomorphisms `f : G → H'` and `g : H → H''`, if `t : G` is a transversal for `H` in the pushout `G ⨁ H'`, then for all `h₁, h₂ in H` with `h₁ h₂ = h₂ h₁` in `H`, the elements `f(g(h₁))` and `f(g(h₂))` in `H''` have a representative in `t` that maps to both under `f` and `g`.
|
Monoid.PushoutI.NormalWord.prod_empty
theorem Monoid.PushoutI.NormalWord.prod_empty :
∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
{φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ},
Monoid.PushoutI.NormalWord.empty.prod = 1
The theorem `Monoid.PushoutI.NormalWord.prod_empty` states that for any types `ι`, `G`, `H`, where `G` is a type dependent on `ι` and `H` is a type, and every `i` in `ι` maps to a Group `G i`, and `H` is also a Group, given a homomorphism `φ` from `H` to `G i` for all `i` in `ι`, and a transversal `d` of the normal word in the pushout monoid, the product of the empty normal word in the pushout monoid is equal to the identity element of the group. This theorem essentially asserts that the product of the empty word in the pushout monoid is the identity, mirroring the property of empty products in group theory.
More concisely: For any type ι, groups G(i) indexed by i in ι, group H, and a homomorphism φ from H to the product of the G(i)'s, the identity element in the pushout monoid of H and the product of empty words in the G(i)'s coincides.
|