Subgroup.isComplement_univ_singleton
theorem Subgroup.isComplement_univ_singleton :
∀ {G : Type u_1} [inst : Group G] {g : G}, Subgroup.IsComplement Set.univ {g}
This theorem states that for any given type `G` that has a group structure and for any element `g` of `G`, the universal set in `G` and the singleton set containing only `g` are complements. In other words, the function that takes a pair of elements from the universal set and the singleton set, respectively, and multiplies them (following group operation) is a bijection. This extends to saying that every element in the group can be uniquely expressed as a product of an element from the universal set and `g`.
More concisely: For any group `G` and its element `g`, the functions from `G` to the universal set of `G` and the singleton set containing `g` are mutually inverse bijections.
|
Subgroup.range_mem_leftTransversals
theorem Subgroup.range_mem_leftTransversals :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : G ⧸ H → G},
(∀ (q : G ⧸ H), ↑(f q) = q) → Set.range f ∈ Subgroup.leftTransversals ↑H
This theorem states that for any group `G` and subgroup `H` of `G`, and for any function `f` from the quotient group `G ⧸ H` to `G` (where `G ⧸ H` is the set of all left cosets of `H` in `G`), if the function `f` maps each element of `G ⧸ H` to a representative of that element in `G` (i.e., for all `q` in `G ⧸ H`, the coset of `f(q)` is `q`), then the range of `f` is a left complement of `H` in `G`.
In simpler terms, the theorem ensures that if we choose one representative from each coset of `H` in `G`, the set of all such representatives forms a left complement of `H` in `G`. A left complement of `H` in `G` is a subset of `G` such that every element of `G` can be uniquely written as the product of an element from the subset and an element from `H`.
More concisely: If `f` is a function from the quotient group `G ⧸ H` to `G` such that for all `q` in `G �agi H`, the coset of `f(q)` is `q`, then the range of `f` is a left complement of `H` in `G`.
|
Subgroup.MemRightTransversals.mul_inv_toFun_mem
theorem Subgroup.MemRightTransversals.mul_inv_toFun_mem :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : S ∈ Subgroup.rightTransversals ↑H) (g : G),
g * (↑(Subgroup.MemRightTransversals.toFun hS g))⁻¹ ∈ H
The theorem `Subgroup.MemRightTransversals.mul_inv_toFun_mem` states that for any group `G`, subgroup `H` of `G`, and any set `S` that is a right transversal of `H` (i.e., `S` is in the set of right transversals of `H`), for any element `g` of the group `G`, the product of `g` and the inverse of the chosen representative of the right coset of `g` (which is obtained by applying the function `Subgroup.MemRightTransversals.toFun` to `g`) is an element of the subgroup `H`. In simpler terms, this theorem captures the property that multiplying an element of a group by the inverse of its representative from a right transversal, gives us an element of the original subgroup.
More concisely: For any group G, subgroup H, and right transversal S of H, the product of any g in G and the inverse of its representative in S belongs to H.
|
Subgroup.exists_right_transversal_of_le
theorem Subgroup.exists_right_transversal_of_le :
∀ {G : Type u_1} [inst : Group G] {H' H : Subgroup G},
H' ≤ H → ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
This theorem states that, given two subgroups `H'` and `H` of a group `G`, where `H'` is a subset of `H`, there exists a right transversal to `H'` within `H`. A right transversal is a set `S` such that the right cosets of `H'` by elements of `S` partition `H`. Furthermore, the theorem asserts that the product of the cardinalities of `H'` and `S` (interpreted as natural numbers) equals the cardinality of `H`. If `H'` or `S` is infinite, its cardinality is considered to be zero.
More concisely: Given two subgroups `H'` and `H` of a group `G` with `H'` a subset of `H`, there exists a right transversal `S` of `H'` in `H` such that the cardinalities of `H'` and `S` sum to the cardinality of `H`.
|
Subgroup.IsComplement.equiv_snd_eq_inv_mul
theorem Subgroup.IsComplement.equiv_snd_eq_inv_mul :
∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (g : G),
↑(hST.equiv g).2 = (↑(hST.equiv g).1)⁻¹ * g
This theorem states that for any type `G` that forms a group, and any two sets `S` and `T` of `G` such that `S` and `T` are complements, given a specific element `g` of `G`, the second component of the tuple obtained by applying the equivalence between `G` and the cartesian product of `S` and `T` to `g` (denoted as `((Subgroup.IsComplement.equiv hST) g).2`) is equal to the product of the inverse of the first component of the same tuple (denoted as `((Subgroup.IsComplement.equiv hST) g).1)⁻¹`) and `g`. In simpler terms, if we have an element from a group which can be expressed as a pair of elements from two complementary subsets, then that element times the inverse of the first component of the pair is equal to the second component of the pair.
More concisely: For any group `G` with complementary subsets `S` and `T`, and for any `g` in `G`, we have `g = (S.complement T).1.inv * (S.complement T).2 g`.
|
AddSubgroup.isComplement_iff_existsUnique
theorem AddSubgroup.isComplement_iff_existsUnique :
∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G},
AddSubgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 + ↑x.2 = g
This theorem states that for any additve group `G` and sets `S` and `T` within that group, `S` and `T` are complements if and only if for every element `g` in the group, there exists a unique pair of elements `(x.1, x.2)`, one from each set, such that the sum of these elements equals `g`. In other words, every element in the group can be expressed uniquely as the sum of an element from `S` and an element from `T`. This concept of complementarity involves a bijection between the pairs from `S` and `T` and the group `G`.
More concisely: For any additive group `G` and sets `S` and `T` within it, `S` and `T` are complements if and only if for each group element `g`, there exists a unique pair `(x.1, x.2)` with `x.1 ∈ S` and `x.2 ∈ T` such that `g = x.1 + x.2`.
|
Subgroup.mem_leftTransversals_iff_bijective
theorem Subgroup.mem_leftTransversals_iff_bijective :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G},
S ∈ Subgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
This theorem states that for any type `G` that has a group structure and any subgroup `H` of `G`, a set `S` is a left transversal of the elements of `H` if and only if the function that restricts `S` to the quotient of `G` by the equivalence relation `Setoid.r` is bijective. In other words, `S` contains exactly one representative from each coset of `H` in `G` (i.e., it is a left transversal) if and only if every element in the quotient space can be uniquely associated with an element in `S` and every element in `S` is associated with some element in the quotient space (i.e., the restriction function is bijective).
More concisely: A set S is a left transversal of a subgroup H in a group G if and only if the restriction function from S to the quotient G/H is bijective.
|
AddSubgroup.range_mem_rightTransversals
theorem AddSubgroup.range_mem_rightTransversals :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : Quotient (QuotientAddGroup.rightRel H) → G},
(∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q) →
Set.range f ∈ AddSubgroup.rightTransversals ↑H
The theorem `AddSubgroup.range_mem_rightTransversals` states that for any given type `G` that has an additive group structure, a subgroup `H` of `G`, and a function `f` from the quotient group of `G` by `H` to `G` satisfying the property that for all elements `q` of the quotient group, applying `f` to `q` and then taking the equivalence class (using `Quotient.mk''`) results in `q` itself, then the range of function `f` is a right transversal of the subgroup `H`. In other words, every additive group element in `G` can be expressed uniquely as an element of `H` plus an element from the range of `f`.
More concisely: If `f` is a function from the quotient group of an additive group `G` by a subgroup `H` such that `Quotient.mk'' (q) = f(q)` for all `q` in the quotient group, then the range of `f` is a right transversal of `H` in `G`.
|
Subgroup.IsComplement'.symm
theorem Subgroup.IsComplement'.symm :
∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → K.IsComplement' H
The theorem states that for any type `G` with a group structure, and any subgroups `H` and `K` of `G`, if `H` and `K` are complements of each other, meaning the operation `(*) : H × K → G` is a bijection, then `K` and `H` are also complements of each other. This is the symmetry property of the subclass of group complements which says that the order of the subgroups does not matter in the definition of complement.
More concisely: If two subgroups `H` and `K` of a group `G` are complements of each other, i.e., their product is bijective, then they are mutual complements, i.e., each is the subgroup of `G` whose complement is the other.
|
AddSubgroup.exists_left_transversal_of_le
theorem AddSubgroup.exists_left_transversal_of_le :
∀ {G : Type u_1} [inst : AddGroup G] {H' H : AddSubgroup G},
H' ≤ H → ∃ S, S + ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
This theorem states that, given two additive subgroups `H'` and `H` of an additive group `G` where `H'` is a subset of `H`, there exists a set `S` that is a left transversal to `H'` inside `H`. A left transversal means that every element of `H` can be represented as an element of `S` plus an element of `H'`. Additionally, the cardinality of `H` (which is the natural number equivalent of the size of `H` if `H` is finite or zero if `H` is infinite) equals the product of the cardinalities of `S` and `H'`.
More concisely: Given two additive subgroups `H'` and `H` of an additive group `G` with `H'` a subset of `H`, there exists a left transversal `S` such that every element in `H` can be written as the sum of an element in `S` and an element in `H'`, and the cardinality of `H` equals the product of the cardinalities of `S` and `H'`.
|
Subgroup.exists_right_transversal
theorem Subgroup.exists_right_transversal :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (g : G), ∃ S ∈ Subgroup.rightTransversals ↑H, g ∈ S
In the context of a group `G`, the theorem `Subgroup.exists_right_transversal` states that for any subgroup `H` of `G` and any element `g` in `G`, there exists a set `S` which is a right transversal of `H` (i.e., a set `S` that complements `H` in `G` such that every element of `G` can be uniquely written as the product of an element of `H` and an element of `S`), and this set `S` contains the element `g`.
More concisely: For any group `G` and subgroup `H`, there exists a right transversal `S` of `H` in `G` containing an element `g` in `G`.
|
Subgroup.exists_left_transversal_of_le
theorem Subgroup.exists_left_transversal_of_le :
∀ {G : Type u_1} [inst : Group G] {H' H : Subgroup G},
H' ≤ H → ∃ S, S * ↑H' = ↑H ∧ Nat.card ↑S * Nat.card ↥H' = Nat.card ↥H
This theorem states that for any type `G` with a group structure, given two subgroups `H'` and `H` of `G` such that `H'` is a subset of `H`, there exists a set `S` which is a left transversal to `H'` inside `H`. This means that the left cosets of `H'` by elements in `S` partition `H` (i.e, `S * H' = H`) and the cardinality of `S` times the cardinality of `H'` equals the cardinality of `H`. Here, `Nat.card` refers to the cardinality of a set as a natural number.
More concisely: For any group `G` and subgroups `H` and `H'` with `H'` a subset of `H`, there exists a left transversal `S` such that `S * H' = H` and `Nat.card S * Nat.card H' = Nat.card H`.
|
Subgroup.range_mem_rightTransversals
theorem Subgroup.range_mem_rightTransversals :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {f : Quotient (QuotientGroup.rightRel H) → G},
(∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q) →
Set.range f ∈ Subgroup.rightTransversals ↑H
This theorem states that for any group `G` and any subgroup `H` within `G`, given a function `f` that maps from the quotient of `G` by the right coset equivalence relation of `H` to `G`, if it holds that for all quotients, the equivalence class of the function's output for the quotient under the setoid `s₁` is equal to the original quotient, then the range of the function `f` is a right transversal of `H` in `G`. In other words, it is a set that complements `H` to form `G` under group operation.
More concisely: If a function from the quotient of a group by the right coset equivalence relation of a subgroup to the group satisfies the property that the equivalence class of the output for each quotient equals the original quotient under a given setoid, then the range of the function is a right transversal of the subgroup in the group.
|
Subgroup.IsComplement.equiv_fst_eq_mul_inv
theorem Subgroup.IsComplement.equiv_fst_eq_mul_inv :
∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) (g : G),
↑(hST.equiv g).1 = g * (↑(hST.equiv g).2)⁻¹
This theorem states that for any group `G` and any sets `S` and `T` of `G`, if `S` and `T` are complements, meaning that the function which multiplies an element of `S` with an element of `T` is a bijection, then for any element `g` of the group, the first component of the equivalence of `g` under the established bijection equals `g` times the inverse of the second component of the equivalence of `g`. In simpler terms, it's saying that if `S` and `T` perfectly cover `G` when multiplied together, then a certain property holds true for every element in the group, specifically concerning the element's representation under the bijection.
More concisely: For any group `G` and complementary sets `S` and `T` such that the function `x ↦ x * y` is a bijection for all `x ∈ S` and `y ∈ T`, then for all `g ∈ G`, we have `(eq.refl g).1 = g * inv (eq.refl g).2`.
|
AddSubgroup.mem_leftTransversals_iff_bijective
theorem AddSubgroup.mem_leftTransversals_iff_bijective :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
S ∈ AddSubgroup.leftTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
This theorem, `AddSubgroup.mem_leftTransversals_iff_bijective`, states that for any type `G` with an additive group structure, any additive subgroup `H` of `G`, and any set `S` of `G`, the set `S` is a left transversal of the subgroup `H` if and only if the restriction of the quotient map to `S` is a bijective function. In other words, 'S' is a left transversal of the subgroup 'H' if every element of the quotient group 'G/H' can be uniquely represented by an element of 'S'.
More concisely: For an additive group (G, +) and its subgroup H, a set S of G is a left transversal of H if and only if the restriction of the quotient map G -> G/H to S is a bijective function.
|
Subgroup.isComplement_iff_existsUnique
theorem Subgroup.isComplement_iff_existsUnique :
∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g := by
sorry
This theorem states that for any group `G` and sets `S` and `T` of elements in `G`, the property of `S` and `T` being complements (`Subgroup.IsComplement S T`) is equivalent to the condition that for every element `g` in `G`, there exists a unique pair `x` such that the product of the first and second elements of `x` equals `g`. In other words, `S` and `T` are complements if and only if each `g` in `G` can be uniquely expressed as the product of an element of `S` and an element of `T`.
More concisely: For any group `G` and sets `S` and `T` of elements in `G`, `Subgroup.IsComplement S T` if and only if for each `g` in `G`, there exists a unique pair `(s, t)` in `S × T` such that `g = s * t`.
|
AddSubgroup.exists_right_transversal_of_le
theorem AddSubgroup.exists_right_transversal_of_le :
∀ {G : Type u_1} [inst : AddGroup G] {H' H : AddSubgroup G},
H' ≤ H → ∃ S, ↑H' + S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
This theorem states that for any given two subgroups `H'` and `H` of an additive group `G`, where `H'` is a subset of `H`, there exists a right transversal `S` of `H'` in `H`. This right transversal `S` has the property that the set `H'` plus `S` is equal to `H` and the cardinality of `H'` times the cardinality of `S` is equal to the cardinality of `H`.
More concisely: For any additive group G and subgroups H and H' with H containing H', there exists a right transversal S of H' in H such that H' + S = H and |H'| * |S| = |H|.
|
AddSubgroup.isComplement_univ_singleton
theorem AddSubgroup.isComplement_univ_singleton :
∀ {G : Type u_1} [inst : AddGroup G] {g : G}, AddSubgroup.IsComplement Set.univ {g}
This theorem states that for any given type `G` that has an additive group structure, and any element `g` of `G`, the set of all elements of `G` (denoted by `Set.univ`) and the singleton set containing just the element `g` are complements. Here, two sets `S` and `T` being complements (in the context of additive groups) means that the function that adds an element of `S` to an element of `T` is a bijection, i.e., every element of the group `G` can be written uniquely as the sum of an element from `S` and an element from `T`. So, every element of the group `G` can be uniquely expressed as the sum of some other element of `G` and the specific element `g`.
More concisely: For any additive group `G` and element `g` in `G`, the sets `Set.univ` and the singleton set `{g}` are complementary in the sense that their elements can be paired to form every element in `G` in a unique way.
|
AddSubgroup.range_mem_leftTransversals
theorem AddSubgroup.range_mem_leftTransversals :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : G ⧸ H → G},
(∀ (q : G ⧸ H), ↑(f q) = q) → Set.range f ∈ AddSubgroup.leftTransversals ↑H
This theorem states that for any type `G` which forms an additive group (`AddGroup G`), for any subgroup `H` of `G`, and for any function `f` mapping from the quotient group `G ⧸ H` to `G`, if for all elements `q : G ⧸ H`, `f(q)` equals `q` when lifted to `G` (i.e., `↑(f q) = q`), then the range of `f` is a left transversal of subgroup `H`. In other words, the range of `f` complements `H` on the left side in the group `G`, which means that every element in `G` can be written uniquely as an element from the range of `f` plus an element of `H`.
More concisely: For any additive group `G`, subgroup `H`, and function `f` from the quotient `G / H` to `G` such that `↑(f (q + H)) = q + H` for all `q : G / H`, the range of `f` is a left transversal of `H` in `G`.
|
Subgroup.mem_rightTransversals_iff_bijective
theorem Subgroup.mem_rightTransversals_iff_bijective :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G},
S ∈ Subgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
This theorem states that for any group `G`, subgroup `H` of `G`, and set `S` of type `G`, the set `S` is in the right transversals of the subgroup `H` if and only if the restriction of the function `Quotient.mk''` to the set `S` is bijective. The function `Quotient.mk''` generates an equivalence class for each element of `G`. Therefore, in simpler terms, the theorem states that a set `S` can be considered a right transversal of a subgroup `H` if every equivalence class of `G` elements contains exactly one element from `S`.
More concisely: A set `S` is a right transversal of a subgroup `H` in a group `G` if and only if the restriction of `Quotient.mk''` to `S` is a bijection.
|
AddSubgroup.mem_rightTransversals_iff_bijective
theorem AddSubgroup.mem_rightTransversals_iff_bijective :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
S ∈ AddSubgroup.rightTransversals ↑H ↔ Function.Bijective (S.restrict Quotient.mk'')
This theorem states that, for any type `G` with an additive group structure and its subgroup `H`, and any set `S` of elements of `G`, `S` belongs to the right transversals of the subgroup `H` if and only if the function that restricts `S` to the quotient is bijective. In other words, a set `S` is a right transversal of a subgroup `H` when every element of the group can be expressed uniquely as the sum of an element from `H` and an element from `S`, which corresponds to the function from `S` to the quotient group being bijective.
More concisely: A set `S` is a right transversal of a subgroup `H` in a group `G` if and only if the restriction of `S` to the quotient group `G/H` is a bijective function.
|