MonoidHom.ker_transferSylow_isComplement'
theorem MonoidHom.ker_transferSylow_isComplement' :
∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G) (hP : P.normalizer ≤ Subgroup.centralizer ↑P)
[inst_1 : Fact p.Prime] [inst_2 : Finite (Sylow p G)] [inst_3 : P.FiniteIndex],
(MonoidHom.transferSylow P hP).ker.IsComplement' ↑P
The theorem is known as **Burnside's normal p-complement theorem**. It states that for a given group `G` and a specific prime `p`, if the normalizer of a Sylow `p`-subgroup `P` of `G` is a subset of the centralizer of `P`, then `P` has a normal complement in `G`. This means there exists a subgroup in `G` that intersects trivially with `P` and their product covers the whole group `G`. It is important to note that this theorem assumes that `p` is prime, the Sylow `p`-subgroup `G` is finite, and `P` has finite index in `G`.
More concisely: If a Sylow p-subgroup of a finite group G has its normalizer contained in its centralizer, then it has a normal complement in G.
|
AddSubgroup.leftTransversals.diff_add_diff
theorem AddSubgroup.leftTransversals.diff_add_diff :
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
(R S T : ↑(AddSubgroup.leftTransversals ↑H)) [inst_2 : H.FiniteIndex],
AddSubgroup.leftTransversals.diff ϕ R S + AddSubgroup.leftTransversals.diff ϕ S T =
AddSubgroup.leftTransversals.diff ϕ R T
This theorem states that for any additive group `G` and any subgroup `H` of `G`, if `R`, `S`, and `T` are three left transversals of `H` (sets which together with `H` form a partition of `G`), and if `ϕ` is a group homomorphism from `H` to another additive commutative group `A`, then the difference of the differences of `ϕ` on `R` and `S`, and on `S` and `T`, equals the difference of `ϕ` on `R` and `T`. This is true under the assumption that `H` has finite index in `G`, meaning the quotient group `G/H` is a finite set. In other words, this theorem expresses a kind of "associativity" for the difference operation on left transversals of an additive subgroup.
More concisely: For any additive group G, subgroup H with finite index, and three left transversals R, S, T of H, if φ is a group homomorphism from H to an additive commutative group A, then φ(r_i − s_i) − φ(s_i − t_i) = φ(r_i − t_i) for all i, where r_i, s_i, and t_i are elements of R, S, and T, respectively.
|
Subgroup.leftTransversals.diff_mul_diff
theorem Subgroup.leftTransversals.diff_mul_diff :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
(R S T : ↑(Subgroup.leftTransversals ↑H)) [inst_2 : H.FiniteIndex],
Subgroup.leftTransversals.diff ϕ R S * Subgroup.leftTransversals.diff ϕ S T =
Subgroup.leftTransversals.diff ϕ R T
This theorem, `Subgroup.leftTransversals.diff_mul_diff`, is stating that for any group `G` with a subgroup `H`, and any commutative group `A`, given a group homomorphism `ϕ` from the subgroup `H` to `A`, and three left transversals `R`, `S`, and `T` of the subgroup `H` in `G`, under the condition that `H` has finite index in `G`, the difference of `R` and `S` using the homomorphism `ϕ`, multiplied by the difference of `S` and `T` using the same homomorphism, equals the difference of `R` and `T` using the homomorphism `ϕ`. Essentially, this theorem demonstrates a distributive property of the difference operation over the multiplication operation for left transversals of subgroups.
More concisely: Given a group `G` with subgroup `H` of finite index, for any commutative group `A`, group homomorphism `ϕ` from `H` to `A`, and left transversals `R`, `S`, and `T` of `H` in `G`, we have `ϕ(R - S) * ϕ(S - T) = ϕ(R - T)`.
|
MonoidHom.transferSylow_eq_pow_aux
theorem MonoidHom.transferSylow_eq_pow_aux :
∀ {G : Type u_1} [inst : Group G] {p : ℕ} (P : Sylow p G),
P.normalizer ≤ Subgroup.centralizer ↑P →
∀ [inst_1 : Fact p.Prime] [inst_2 : Finite (Sylow p G)],
∀ g ∈ P, ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ P → g₀⁻¹ * g ^ k * g₀ = g ^ k
This theorem, `MonoidHom.transferSylow_eq_pow_aux`, states that given a group `G` and a prime number `p`, for a `p`-Sylow subgroup `P` of `G`, if the normalizer of `P` is a subset of the centralizer of `P`, then for every element `g` in `P`, and for each natural number `k` and each group element `g₀`, if the conjugate of `g` to the power of `k` by `g₀` is also in `P`, then this conjugate is equal to `g` to the power of `k`. Here, the term "conjugate of `g` to the power of `k` by `g₀`" refers to the operation `g₀⁻¹ * g ^ k * g₀`, where `^` denotes exponentiation in the group, `*` is the group multiplication, and `⁻¹` denotes the group inverse.
More concisely: If a `p`-Sylow subgroup `P` of a group `G` has its normalizer contained in the centralizer, then for all `g` in `P` and `k` and `g₀` in `G`, if `g⁰⁻¹ * gⁱ * g₀` is in `P` for some power `gⁱ = g⁰ⁱⁱⁱ⁰ⁱⁱ⁶⁰⁶⁰⁴⁶⁰⁴⁶⁰⁴⁶⁰⁴⁶⁰ (k)`, then `gⁱ = g⁰ⁱⁱⁱ⁰ⁱⁱ⁶⁰⁶⁰⁴⁶⁰⁴⁶⁰⁴⁶⁰⁴⁶⁰⁴⁶⁰ (g)`.
|
MonoidHom.transfer_eq_pow_aux
theorem MonoidHom.transfer_eq_pow_aux :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G),
(∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) → g ^ H.index ∈ H
This theorem, `MonoidHom.transfer_eq_pow_aux`, is an auxiliary lemma used in formulating `transfer_eq_pow`. For any type `G` that forms a group and any subgroup `H` of G, given an element `g` of G and assuming that for every natural number `k` and every element `g₀` of G, if the element resulting from the operation (g₀⁻¹ * g ^ k * g₀) belongs to H, then (g₀⁻¹ * g ^ k * g₀) is equal to (g ^ k), we can conclude that the element of G obtained by raising g to the power of the index of H is an element of H.
More concisely: If `g` is an element of a group `G` and `H` is a subgroup of `G` such that for all `k` and `g₀` in `G` with `g₀⁻¹ * g ^ k * g₀ in H` implies `g₀⁻¹ * g ^ k * g₀ = g ^ k`, then `g ^ (index H)` is an element of `H`.
|
MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot
theorem MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
[inst_2 : H.FiniteIndex] (g : G)
[inst_3 : Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))],
ϕ.transfer g =
Finset.univ.prod fun q =>
ϕ ⟨(Quotient.out' q.out')⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out' * Quotient.out' q.out', ⋯⟩
The theorem `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot` provides an explicit computation of the transfer homomorphism in group theory. It states that for any group `G` with a subgroup `H` and any commutative group `A`, given a group homomorphism `ϕ` from the subgroup `H` to `A`, if `H` has finite index in `G`, then for any element `g` of `G`, and assuming that the quotient set `G/H` under the action of the subgroup generated by `g` is finite (represented by `Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H))`), the transfer of `ϕ` at `g` can be calculated as the product over all elements `q` of this quotient set of `ϕ` evaluated at the element of `H` which is represented by the inverse of the representative of `q` times `g` raised to the power of the minimal period of `q` under the action of multiplication by `g`, times the representative of `q` itself.
More concisely: Given a group `G` with finite index subgroup `H`, a commutative group `A`, and a group homomorphism `ϕ` from `H` to `A`, if the quotient set `G/H` under the action of the subgroup generated by `g` is finite, then the transfer of `ϕ` at `g` is the product over representatives `q` of the quotient set of `ϕ(h)` where `h` is the element of `H` represented by the inverse of `q` times the power of `g` equal to the minimal period of `q` under multiplication by `g`.
|
Subgroup.leftTransversals.diff_self
theorem Subgroup.leftTransversals.diff_self :
∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
(T : ↑(Subgroup.leftTransversals ↑H)) [inst_2 : H.FiniteIndex], Subgroup.leftTransversals.diff ϕ T T = 1
The theorem `Subgroup.leftTransversals.diff_self` states that for any group `G`, any subgroup `H` of `G`, any commutative group `A`, any morphism `ϕ` from `H` to `A`, and any left transversal `T` of `H` in `G`, the difference between `T` and itself (according to the defined left transversal difference operation) is the identity element of the group `A`. This theorem holds when the index of the subgroup `H` in `G` is finite. In terms of algebra, it means that the difference of a left transversal with itself, under a certain defined operation involving group homomorphism, always results in the identity of the target group.
More concisely: For any group `G`, subgroup `H`, commutative group `A`, morphism `ϕ` from `H` to `A`, and left transversal `T` of `H` in `G` (with finite index), the difference `ϕ(T \ T)` equals the identity element of `A`.
|