Sylow.normalizer_sup_eq_top'
theorem Sylow.normalizer_sup_eq_top' :
∀ {G : Type u_1} [inst : Group G] {p : ℕ} [inst_1 : Fact p.Prime] {N : Subgroup G} [inst_2 : N.Normal]
[inst_3 : Finite (Sylow p ↥N)] (P : Sylow p G), ↑P ≤ N → P.normalizer ⊔ N = ⊤
**Frattini's Argument**: Given a group `G`, let `N` be a normal subgroup of `G` and `P` be a Sylow `p`-subgroup of `N`, where `p` is a prime number. The theorem states that the join of the normalizer of `P` in `G` and the subgroup `N` equals the whole group `G`. In other words, any element of the group `G` can be expressed as a combination of elements from the normalizer of `P` in `G` and the subgroup `N`.
More concisely: The normalizer of a Sylow p-subgroup in a group G, intersected with a normal subgroup N, equals G.
|
Sylow.normalizer_sup_eq_top
theorem Sylow.normalizer_sup_eq_top :
∀ {G : Type u_1} [inst : Group G] {p : ℕ} [inst_1 : Fact p.Prime] {N : Subgroup G} [inst_2 : N.Normal]
[inst_3 : Finite (Sylow p ↥N)] (P : Sylow p ↥N), (Subgroup.map N.subtype ↑P).normalizer ⊔ N = ⊤
**Frattini's Argument**: Given a group `G` and a subgroup `N` which is normal within `G`, if `P` is a Sylow `p`-subgroup of `N` (where `p` is a prime number), then the join of the normalizer of `P` in `G` and `N` equals the whole group `G`. This means that every element of `G` is either in `N` or in the normalizer of `P` in `G`.
More concisely: If `G` is a group, `N` is a normal subgroup of `G`, and `P` is a Sylow p-subgroup of `N`, then the normalizer of `P` in `G` and `N` generate `G`, i.e., `normalizer P in G ⋊ N = G`.
|
Sylow.exists_comap_eq_of_ker_isPGroup
theorem Sylow.exists_comap_eq_of_ker_isPGroup :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (P : Sylow p H) {f : H →* G},
IsPGroup p ↥f.ker → ∃ Q, Subgroup.comap f ↑Q = ↑P
The theorem `Sylow.exists_comap_eq_of_ker_isPGroup` states that for any prime number `p`, groups `G` and `H`, a Sylow `p`-subgroup `P` of `H`, and a group homomorphism `f` from `H` to `G`, if the kernel of `f` forms a `p`-group, then there exists a subgroup `Q` of `H` such that the preimage of `Q` under `f` is exactly `P`. In other words, we can find a subgroup `Q` in `H` where all elements map to the Sylow `p`-subgroup `P` in `G` under the homomorphism `f` provided the kernel of `f` is a `p`-group.
More concisely: Given a prime number `p`, groups `G` and `H`, a Sylow `p`-subgroup `P` of `H`, and a group homomorphism `f` from `H` to `G` with kernel being a `p`-group, there exists a subgroup `Q` of `H` such that `f(Q) = P`.
|
Sylow.card_quotient_normalizer_modEq_card_quotient
theorem Sylow.card_quotient_normalizer_modEq_card_quotient :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p n : ℕ} [hp : Fact p.Prime] {H : Subgroup G},
Fintype.card ↥H = p ^ n →
p.ModEq (Fintype.card (↥H.normalizer ⧸ Subgroup.comap H.normalizer.subtype H)) (Fintype.card (G ⧸ H))
This theorem states that for any group `G` with a subgroup `H` that is a `p`-group (meaning that the number of elements in `H` is equal to `p` raised to the power `n`, where `p` is a prime number), the index of `H` within its normalizer is congruent modulo `p` to the index of `H` in `G`. The normalizer of a group is a superset containing all elements that can multiply with an element of the group to produce another element within the group. The index of a subgroup in a group is the number of distinct left (or right) cosets of the subgroup in the group.
More concisely: For any prime number `p` and group `G` with subgroup `H` of order `p^n`, the index of `H` in its normalizer `N(H)` is congruent to the index of `H` in `G` modulo `p`.
|
Sylow.card_normalizer_modEq_card
theorem Sylow.card_normalizer_modEq_card :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p n : ℕ} [hp : Fact p.Prime] {H : Subgroup G},
Fintype.card ↥H = p ^ n → (p ^ (n + 1)).ModEq (Fintype.card ↥H.normalizer) (Fintype.card G)
This theorem, named `Sylow.card_normalizer_modEq_card`, asserts that for any group `G`, positive integer `p` which is prime, an integer `n`, and a subgroup `H` of `G`, if the number of elements in `H` is equal to `p` raised to the power `n`, then the cardinality of the normalizer of `H` is congruent to the cardinality of `G` modulo `p` raised to the power `(n + 1)`. The normalizer of `H` in `G` is essentially the set of all elements in `G` that commute with every element in `H`, and the cardinality of a set is the number of elements in the set. The congruence relation 'modulo `n`' means that when the larger number is divided by `n`, it leaves the same remainder as the smaller number.
More concisely: For any prime number p and a subgroup H of finite order p^n in a group G, the order of the normalizer of H modulo p is congruent to the order of G modulo p^(n+1).
|
IsPGroup.exists_le_sylow
theorem IsPGroup.exists_le_sylow :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Subgroup G}, IsPGroup p ↥P → ∃ Q, P ≤ ↑Q
This theorem represents a generalization of Sylow's first theorem. It states that for any natural number `p` and any type `G` with a group structure, given a `p`-subgroup `P` of `G` satisfying the property of being a `p`-group, there exists a Sylow `p`-subgroup `Q` of `G` such that `P` is contained in `Q`. In mathematical terms, for every `p`-group (a group where every element has order a power of a prime `p`), it is always possible to find a Sylow `p`-subgroup that contains it.
More concisely: For any prime number `p` and `p`-group `P` in a group `G`, there exists a Sylow `p`-subgroup `Q` of `G` containing `P`.
|
Sylow.prime_dvd_card_quotient_normalizer
theorem Sylow.prime_dvd_card_quotient_normalizer :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p n : ℕ} [hp : Fact p.Prime],
p ^ (n + 1) ∣ Fintype.card G →
∀ {H : Subgroup G},
Fintype.card ↥H = p ^ n → p ∣ Fintype.card (↥H.normalizer ⧸ Subgroup.comap H.normalizer.subtype H)
The theorem `Sylow.prime_dvd_card_quotient_normalizer` states that for any finite group `G`, if `H` is a subgroup of `G` such that the order (number of elements) of `H` is `p^n` for some prime `p` and integer `n`, but `G` is not a Sylow `p`-subgroup (i.e., the order of `G` is not `p^(n+1)`), then `p` divides the index of `H` in its normalizer. The index is the number of cosets of `H` in its normalizer, which can be calculated as the quotient of the order of the normalizer of `H` by the order of `H`.
More concisely: If a subgroup of prime power order `p^n` in a finite group `G` is not a Sylow `p`-subgroup, then the prime `p` divides the index of the subgroup in its normalizer.
|
Sylow.exists_subgroup_card_pow_succ
theorem Sylow.exists_subgroup_card_pow_succ :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p n : ℕ} [hp : Fact p.Prime],
p ^ (n + 1) ∣ Fintype.card G →
∀ {H : Subgroup G}, Fintype.card ↥H = p ^ n → ∃ K, Fintype.card ↥K = p ^ (n + 1) ∧ H ≤ K
The theorem `Sylow.exists_subgroup_card_pow_succ` states that for any finite group `G` and any prime number `p`, if there is a subgroup `H` of `G` that has cardinality (number of elements) `p^n`, and if `p^(n+1)` divides the cardinality of `G`, then `H` is contained in another subgroup `K` of `G` that has cardinality `p^(n+1)`. This is a part of the Sylow theorems in group theory.
More concisely: If a finite group `G` has a subgroup of prime power order `p^n` and `p^(n+1)` divides the order of `G`, then `G` contains a subgroup of order `p^(n+1)`.
|
Sylow.prime_pow_dvd_card_normalizer
theorem Sylow.prime_pow_dvd_card_normalizer :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p n : ℕ} [_hp : Fact p.Prime],
p ^ (n + 1) ∣ Fintype.card G →
∀ {H : Subgroup G}, Fintype.card ↥H = p ^ n → p ^ (n + 1) ∣ Fintype.card ↥H.normalizer
The theorem `Sylow.prime_pow_dvd_card_normalizer` states that for any group `G` and a prime number `p`, if `H` is a subgroup of `G` of order `p ^ n` but not a Sylow `p`-subgroup, and `p ^ (n + 1)` divides the order of the group `G`, then `p ^ (n + 1)` also divides the order of the normalizer of the subgroup `H`. Here, the normalizer of a subgroup `H` in a group `G` is the set of all elements `g` in `G` such that `gHg⁻¹ = H`. In other words, it asserts that the cardinality of the normalizer of a proper `p`-subgroup in a group is divisible by a higher power of the prime `p` than the order of the subgroup itself.
More concisely: If `H` is a proper subgroup of order `p^n` in a group `G` where `p` is a prime and `p^(n+1)` divides the order of `G`, then the order of `H`'s normalizer in `G` is a multiple of `p^(n+1)`.
|
Sylow.card_eq_multiplicity
theorem Sylow.card_eq_multiplicity :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G),
Fintype.card ↥↑P = p ^ (Fintype.card G).factorization p
The theorem `Sylow.card_eq_multiplicity` states that for any group `G` of finite type and a prime number `p`, the cardinality (or the number of elements) of a Sylow `p`-subgroup `P` of `G` is equal to `p` raised to the power of the multiplicity of `p` in the order of the group `G`. The multiplicity of `p` in the order of the group `G` is given by the `factorization` of the cardinality of `G` with respect to `p`. A Sylow `p`-subgroup is a maximal subgroup of `G` whose order is a power of a prime `p`.
More concisely: The cardinality of a Sylow p-subgroup of a finite group G is equal to p raised to the power of the multiplicity of p in the order of G.
|
Sylow.card_coprime_index
theorem Sylow.card_coprime_index :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] {p : ℕ} [hp : Fact p.Prime] (P : Sylow p G),
(Fintype.card ↥↑P).Coprime P.index
This theorem states that for any group `G` (which is a finite type), and for a given prime number `p`, the cardinality of a Sylow `p`-subgroup `P` of `G` is coprime with the index of `P`. In other words, the number of elements in the Sylow `p`-subgroup and the index of the subgroup have no common factors other than 1. This is a property of Sylow subgroups within the context of group theory.
More concisely: The order of a Sylow p-subgroup of a finite group G is coprime with the index of G/P, where P is a Sylow p-subgroup of G.
|
Sylow.exists_subgroup_card_pow_prime
theorem Sylow.exists_subgroup_card_pow_prime :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] (p : ℕ) {n : ℕ} [inst_2 : Fact p.Prime],
p ^ n ∣ Fintype.card G → ∃ K, Fintype.card ↥K = p ^ n
This theorem is a generalization of Sylow's first theorem in group theory. It states that for any group 'G' of finite size, if the cardinality (number of elements) of 'G' is divisible by a prime number 'p' raised to the power 'n', then there exists a subgroup within 'G' with the cardinality equal to 'p' raised to the power 'n'. The prime nature of 'p' is given as a fact.
More concisely: For any finite group G and prime number p dividing its order, there exists a subgroup of G of order p^n for some n.
|
Sylow.exists_subgroup_le_card_pow_prime_of_le_card
theorem Sylow.exists_subgroup_le_card_pow_prime_of_le_card :
∀ {G : Type u} [inst : Group G] {n p : ℕ},
p.Prime → IsPGroup p G → ∀ {H : Subgroup G}, p ^ n ≤ Nat.card ↥H → ∃ H' ≤ H, Nat.card ↥H' = p ^ n
This is a special case of Sylow's first theorem. It states that, for any group `G` that is a `p`-group and a subgroup `H` of size at least `p` to the power of `n`, where `p` is a prime number, there exists a subgroup `H'` of `H` such that its cardinality equals `p` to the power of `n`. The theorem requires that `p` is a prime number and that every element of group `G` has an order which is a power of `p`.
More concisely: In a `p`-group `G`, any subgroup of size a power of `p` greater than or equal to `p^n` contains a subgroup of order `p^n`.
|
Sylow.exists_subgroup_card_pow_prime_of_le_card
theorem Sylow.exists_subgroup_card_pow_prime_of_le_card :
∀ {G : Type u} [inst : Group G] {n p : ℕ}, p.Prime → IsPGroup p G → p ^ n ≤ Nat.card G → ∃ H, Nat.card ↥H = p ^ n
This is a special case of Sylow's first theorem. The theorem states that for any group `G` which is a `p`-group and has cardinality at least `p^n` (`n` and `p` are natural numbers and `p` is prime), there exists a subgroup `H` within `G` such that the cardinality of `H` equals `p^n`. In simpler terms, it assures that in a group of sufficient size, there is always a subgroup with a cardinality equal to a given power of a prime number.
More concisely: In a `p`-group `G` of cardinality `p^n` (`n` and `p` natural numbers, `p` prime), there exists a subgroup of order `p^n`.
|
not_dvd_index_sylow
theorem not_dvd_index_sylow :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact p.Prime] [inst_1 : Finite (Sylow p G)] (P : Sylow p G),
P.relindex P.normalizer ≠ 0 → ¬p ∣ P.index
This theorem, `not_dvd_index_sylow`, asserts that for any prime number `p` and any group `G`, supposing `p` is a Sylow prime of `G` and `G` is finite, for any Sylow `p`-subgroup `P` of `G`, if the relative index of `P` in its normalizer is not zero, then `p` does not divide the index of `P` in `G`. In other words, under the given conditions, the prime number `p` cannot be a divisor of the index of the Sylow `p`-subgroup `P` in `G` if the relative index of `P` in its normalizer is non-zero.
More concisely: If a prime number `p` is a Sylow prime of a finite group `G`, and a Sylow `p`-subgroup `P` of `G` has non-zero relative index in its normalizer, then `p` does not divide the index of `P` in `G`.
|
card_sylow_modEq_one
theorem card_sylow_modEq_one :
∀ (p : ℕ) (G : Type u_1) [inst : Group G] [inst_1 : Fact p.Prime] [inst_2 : Fintype (Sylow p G)],
p.ModEq (Fintype.card (Sylow p G)) 1
This theorem is a generalization of Sylow's third theorem. It states that for any natural number `p` and any type `G` that forms a group, given that `p` is prime and the set of Sylow `p`-subgroups of `G` is finite (a "fintype"), the number of Sylow `p`-subgroups is congruent to `1` modulo `p`. In mathematical terms, if we let `n` be the number of Sylow `p`-subgroups, then `n ≡ 1 (mod p)`. This is an important result in the field of group theory.
More concisely: For a prime number `p` and a finite group `G`, the number of Sylow `p`-subgroups is congruent to 1 modulo `p`.
|
Sylow.exists_subgroup_le_card_le
theorem Sylow.exists_subgroup_le_card_le :
∀ {G : Type u} [inst : Group G] {k p : ℕ},
p.Prime →
IsPGroup p G →
∀ {H : Subgroup G}, k ≤ Nat.card ↥H → k ≠ 0 → ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
This theorem, a special case of Sylow's first theorem, asserts that for any group `G` that is a `p`-group and any subgroup `H` of `G` with cardinality at least `k`, where `p` is a prime number, there exists a subgroup `H'` of `H` such that the cardinality of `H'` is between `k/p` and `k`. In other words, if a group is a `p`-group and it has a subgroup of size `k` or more, then it also has a subgroup whose size is no more than `k` but less than `p` times the size of that subgroup. This size of the subgroup `H'` thus lies in a range determined by the size `k` of the original subgroup and the prime `p` that characterizes the `p`-group.
More concisely: In a p-group G, any subgroup H of size k (p-prime in G) contains a subgroup H' of size between k/p and k.
|
Sylow.exists_subgroup_card_pow_prime_le
theorem Sylow.exists_subgroup_card_pow_prime_le :
∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G] (p : ℕ) {n m : ℕ} [_hp : Fact p.Prime],
p ^ m ∣ Fintype.card G →
∀ (H : Subgroup G), Fintype.card ↥H = p ^ n → n ≤ m → ∃ K, Fintype.card ↥K = p ^ m ∧ H ≤ K
The theorem `Sylow.exists_subgroup_card_pow_prime_le` states the following: for any group `G` and a prime number `p`, if there is a subgroup `H` of `G` of size `p` to the power `n`, and if `p` to the power `m` divides the size of `G` where `n` is less than or equal to `m`, then there exists a subgroup `K` of `G` of size `p` to the power `m` which contains the subgroup `H`. This theorem is a part of the Sylow theorems in group theory, and is used to explain the structure of finite groups.
More concisely: If a prime `p` divides the order of a group `G` to the power `m`, and `p` raises to the power `n` (where `n <= m`) is the size of a subgroup `H` of `G`, then there exists a subgroup `K` of `G` of order `p` raised to the power `m` containing `H`.
|
Sylow.ext
theorem Sylow.ext : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P Q : Sylow p G}, ↑P = ↑Q → P = Q
This theorem, known as "Sylow.ext", states that for any natural number `p`, any group `G` of type `u_1`, and any two Sylow subgroups `P` and `Q` of `G`, if the underlying sets of `P` and `Q` (denoted by `↑P` and `↑Q` respectively) are equal, then `P` and `Q` are the same Sylow subgroup. In other words, a Sylow subgroup is uniquely determined by its underlying set.
More concisely: If two Sylow subgroups of a group have equal underlying sets, then they are equal as subgroups.
|