IsPGroup.exists_card_eq
theorem IsPGroup.exists_card_eq :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fact p.Prime] [inst_2 : Fintype G],
IsPGroup p G → ∃ n, Fintype.card G = p ^ n
This theorem, also known as the forward direction of `IsPGroup.iff_card`, states that for any natural number `p` and any Fintype group `G`, if `p` is a prime number and `G` is a p-group (meaning that every element in `G` has an order which is a power of `p`), then there exists a natural number `n` such that the number of elements in `G` (denoted by `Fintype.card G`) is equal to `p` raised to the power of `n`.
More concisely: If `p` is a prime number and `G` is a p-group, then there exists a natural number `n` such that the order of `G` is `p^n`.
|
IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq
theorem IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] [inst_2 : Fact p.Prime],
Fintype.card G = p ^ 2 → IsCyclic (G ⧸ Subgroup.center G)
This theorem states that for any given prime number `p` and any group `G` with a finite number of elements, if the number of elements in the group `G` is equal to the square of `p` (i.e., `p ^ 2`), then the quotient of the group `G` by its center is a cyclic group.
Here, the center of a group `G` is the set of all elements that commute with every element in `G`, and a cyclic group is a group that can be generated by a single element. The quotient of a group by its subgroup is a group formed by the set of cosets of the subgroup, and in this case, the subgroup is the center of `G`.
More concisely: For any prime number `p` and finite group `G` of order `p^2`, the quotient of `G` by its center is a cyclic group.
|
IsPGroup.to_le
theorem IsPGroup.to_le :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G}, IsPGroup p ↥K → H ≤ K → IsPGroup p ↥H
The theorem `IsPGroup.to_le` states that for any natural number `p` and any group `G`, given two subgroups `H` and `K` of `G`, if `K` is a p-group (i.e., every element in `K` has an order that is a power of `p`), and if `H` is a subgroup of `K`, then `H` is also a p-group. In other words, if every element in subgroup `K` of some group `G` has an order that is a power of a prime number `p`, and if another subgroup `H` is a subset of `K`, then every element in `H` also has an order that is a power of `p`.
More concisely: If `H` is a subgroup of the p-group `K` in a group `G`, then `H` is also a p-group.
|
IsPGroup.iff_orderOf
theorem IsPGroup.iff_orderOf :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact p.Prime], IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
This theorem states that for any natural number `p` and a type `G` that forms a group, if `p` is a prime number, then `G` is a p-group if and only if for every element `g` in the group, there exists a natural number `k` such that the order of `g` is equal to `p` raised to the power `k`. A p-group is a group in which every element's order is a power of a prime number. The order of an element `g` is the smallest positive natural number `n` such that `g` raised to the power `n` is the identity of the group, or `0` if no such `n` exists (i.e., `g` has infinite order).
More concisely: For a prime number `p` and group `G`, `G` is a `p`-group if and only if for each `g` in `G`, there exists a natural number `k` such that the order of `g` equals `p^k`.
|
IsPGroup.disjoint_of_ne
theorem IsPGroup.disjoint_of_ne :
∀ {G : Type u_1} [inst : Group G] (p₁ p₂ : ℕ) [hp₁ : Fact p₁.Prime] [hp₂ : Fact p₂.Prime],
p₁ ≠ p₂ → ∀ (H₁ H₂ : Subgroup G), IsPGroup p₁ ↥H₁ → IsPGroup p₂ ↥H₂ → Disjoint H₁ H₂
The theorem `IsPGroup.disjoint_of_ne` states that for any given group `G`, and two different prime numbers `p₁` and `p₂`, if `H₁` and `H₂` are subgroups of `G` such that `H₁` is a `p₁`-group and `H₂` is a `p₂`-group (i.e., every element of `H₁` and `H₂` respectively has order that is a power of `p₁` and `p₂`), then `H₁` and `H₂` are disjoint. Here, two subgroups being disjoint means that the greatest element that is less than or equal to any element from both subgroups is the bottom element of the lattice structure of the group.
More concisely: If `G` is a group, and `p₁` and `p₂` are distinct prime numbers, then subgroups `H₁` of `G` being a `p₁`-group and `H₂` being a `p₂`-group imply that `H₁ ∩ H₂` equals the identity element of `G`.
|
IsPGroup.card_modEq_card_fixedPoints
theorem IsPGroup.card_modEq_card_fixedPoints :
∀ {p : ℕ} {G : Type u_1} [inst : Group G],
IsPGroup p G →
∀ [hp : Fact p.Prime] (α : Type u_2) [inst_1 : MulAction G α] [inst_2 : Fintype α]
[inst_3 : Fintype ↑(MulAction.fixedPoints G α)],
p.ModEq (Fintype.card α) (Fintype.card ↑(MulAction.fixedPoints G α))
This theorem states that if `G` is a `p`-group (a group in which every element has order that is a power of a prime `p`) acting on a finite set `α`, then the number of fixed points under the group action is congruent modulo `p` to the cardinality (number of elements) of `α`. In other words, the size of the set of elements that are not changed under the group action is equal to the size of the original set `α` up to a multiple of `p`. This is a result in the field of group actions in algebra.
More concisely: If `G` is a `p`-group acting on a finite set `α`, then the number of fixed points under the group action is congruent to the cardinality of `α` modulo `p`.
|
IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card
theorem IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card :
∀ {p : ℕ} {G : Type u_1} [inst : Group G],
IsPGroup p G →
∀ [hp : Fact p.Prime] (α : Type u_2) [inst_1 : MulAction G α] [inst_2 : Fintype α],
¬p ∣ Fintype.card α →
∀ [inst_3 : Finite ↑(MulAction.fixedPoints G α)], (MulAction.fixedPoints G α).Nonempty
This theorem states that if a p-group, a group in which every element has an order that is a power of a prime number p, acts on a set `α`, and if the cardinality (the number of elements) of `α` is not divisible by p, then there exists at least one fixed point under the group action. A fixed point is an element of `α` that remains unchanged by the action of any element of the group. The prime number p is assured to be a prime number. Furthermore, it is ensured that the set of fixed points under the action is finite.
More concisely: If `G` is a p-group acting on a finite set `α` of cardinality not divisible by the prime `p`, then `G` has a fixed point.
|
IsPGroup.of_card
theorem IsPGroup.of_card :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {n : ℕ}, Fintype.card G = p ^ n → IsPGroup p G := by
sorry
This theorem states that for any natural number `p`, any type `G` equipped with a group structure, and any natural number `n`, if the number of elements in `G` (its cardinality) equals `p` raised to the `n`-th power, then `G` is a p-group. In other words, if the cardinality of a group is a power of a prime number `p`, then every element in the group can be expressed as `g` raised to the power of `p` raised to a natural number `k` equals the identity element of the group (or `g ^ p ^ k = 1` in Lean syntax).
More concisely: If the cardinality of a group `G` is a power `p^n` of a prime number `p`, then every element in `G` is of the form `g^(p^k)` for some natural number `k`.
|
IsPGroup.coprime_card_of_ne
theorem IsPGroup.coprime_card_of_ne :
∀ {G : Type u_1} [inst : Group G] {G₂ : Type u_2} [inst_1 : Group G₂] (p₁ p₂ : ℕ) [hp₁ : Fact p₁.Prime]
[hp₂ : Fact p₂.Prime],
p₁ ≠ p₂ →
∀ (H₁ : Subgroup G) (H₂ : Subgroup G₂) [inst_2 : Fintype ↥H₁] [inst_3 : Fintype ↥H₂],
IsPGroup p₁ ↥H₁ → IsPGroup p₂ ↥H₂ → (Fintype.card ↥H₁).Coprime (Fintype.card ↥H₂)
This theorem states that if we have two finite p-groups, where a p-group is a group in which every element has prime power order, with different primes `p₁` and `p₂`, then the orders of these groups (i.e., their sizes, given by `Fintype.card` of the subgroups `H₁` and `H₂`) are coprime. This means that the greatest common divisor of the orders of the two groups is 1. Here, `p₁ ≠ p₂` signifies that the primes corresponding to the two groups are distinct. The `IsPGroup` condition ensures that every element in each subgroup has order that is a power of their respective prime `p₁` or `p₂`.
More concisely: If `G₁` and `G₂` are finite p-groups with distinct prime orders `p₁` and `p₂`, then `Fintype.card G₁` and `Fintype.card G₂` are coprime.
|
IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point
theorem IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point :
∀ {p : ℕ} {G : Type u_1} [inst : Group G],
IsPGroup p G →
∀ [hp : Fact p.Prime] (α : Type u_2) [inst_1 : MulAction G α] [inst_2 : Fintype α],
p ∣ Fintype.card α → ∀ {a : α}, a ∈ MulAction.fixedPoints G α → ∃ b ∈ MulAction.fixedPoints G α, a ≠ b
The theorem states that, given a p-group that acts on a set `α` (where a p-group is a group in which every element has an order that is a power of a prime number), if the cardinality (number of elements) of `α` is a multiple of the prime number, and the action has a fixed point, then there must exist another fixed point that is different from the first one.
Here, a fixed point refers to an element of `α` that remains the same under the action of any element of the group.
More concisely: In a p-group acting on a set of cardinality a multiple of the prime order, if there exists a fixed point, then there exists another distinct fixed point.
|
IsPGroup.commutative_of_card_eq_prime_sq
theorem IsPGroup.commutative_of_card_eq_prime_sq :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] [inst_2 : Fact p.Prime],
Fintype.card G = p ^ 2 → ∀ (a b : G), a * b = b * a
The theorem `IsPGroup.commutative_of_card_eq_prime_sq` states that for any natural number `p` and any type `G` that has a group structure and a finite number of elements, if `p` is a prime number and the number of elements in `G` is equal to the square of `p`, then the group `G` is commutative. In other words, for any two elements `a` and `b` in `G`, the operation of the group on `a` followed by `b` is the same as the operation on `b` followed by `a`. This is commonly referred to in group theory as the statement "A group of order `p^2` for a prime `p` is always commutative."
More concisely: For any prime number `p` and finite group `G` of order `p^2`, `G` is commutative.
|
IsPGroup.card_center_eq_prime_pow
theorem IsPGroup.card_center_eq_prime_pow :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] [inst_2 : Fact p.Prime] {n : ℕ},
Fintype.card G = p ^ n →
0 < n → ∀ [inst_3 : Fintype ↥(Subgroup.center G)], ∃ k > 0, Fintype.card ↥(Subgroup.center G) = p ^ k
The theorem `IsPGroup.card_center_eq_prime_pow` states that for any positive integer `p` and a type `G` which forms a group (with `G` being a finite type), if `p` is a prime number and the cardinality of `G` (the number of elements in `G`) is `p` raised to the power `n` with `n` being a positive integer, then the cardinality of the center of `G` (the set of elements that commute with all elements in `G`) is `p` raised to the power `k` where `k` is a positive integer. This theorem essentially describes a property of the central subgroup of a `p`-group.
More concisely: The order of the center of a finite p-group of order p^n is p^k for some positive integer k.
|
IsPGroup.of_surjective
theorem IsPGroup.of_surjective :
∀ {p : ℕ} {G : Type u_1} [inst : Group G],
IsPGroup p G → ∀ {H : Type u_2} [inst_1 : Group H] (ϕ : G →* H), Function.Surjective ⇑ϕ → IsPGroup p H
The theorem `IsPGroup.of_surjective` states that if `G` is a p-group (that is, for every element `g` in `G`, there is some integer `k` such that `g` raised to the power `p` to the power `k` equals the group's identity element), then for any other group `H` and any surjective homomorphism `ϕ` from `G` to `H` (that is, a function such that every element in `H` is the image of some element in `G` under `ϕ`), `H` is also a p-group. In other words, the property of being a p-group is preserved under surjective homomorphisms.
More concisely: If `G` is a p-group and `ϕ : G → H` is a surjective homomorphism, then `H` is also a p-group.
|
IsPGroup.comap_of_ker_isPGroup
theorem IsPGroup.comap_of_ker_isPGroup :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
IsPGroup p ↥H →
∀ {K : Type u_2} [inst_1 : Group K] (ϕ : K →* G), IsPGroup p ↥ϕ.ker → IsPGroup p ↥(Subgroup.comap ϕ H)
The theorem `IsPGroup.comap_of_ker_isPGroup` states that for any natural number `p`, any group `G`, any subgroup `H` of `G`, if `H` is a p-group (i.e., every element of `H` has order a power of `p`), and for any group `K` and any monoid homomorphism `ϕ` from `K` to `G`, if the kernel of `ϕ` is also a p-group, then the preimage of `H` under `ϕ`, which is a subgroup of `K`, is also a p-group. In other words, the preimage of a p-group under a monoid homomorphism is also a p-group, provided that the kernel of the homomorphism is a p-group.
More concisely: If `H` is a p-group subgroup of a group `G`, and `ϕ` is a monoid homomorphism from a group `K` to `G` with p-group kernel, then the preimage of `H` under `ϕ` is a p-group subgroup of `K`.
|
IsPGroup.map
theorem IsPGroup.map :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Subgroup G},
IsPGroup p ↥H → ∀ {K : Type u_2} [inst_1 : Group K] (ϕ : G →* K), IsPGroup p ↥(Subgroup.map ϕ H)
The theorem `IsPGroup.map` states that if `H` is a p-group in the group `G` for a given prime number `p`, then its image under any group homomorphism `ϕ` from `G` to another group `K` is also a p-group. Here, a p-group is defined as a group in which every element has an order that is a power of the prime `p`. The image of a subgroup under a group homomorphism is defined as another subgroup in the target group.
More concisely: If `G` is a group, `p` is a prime number, `H` is a p-subgroup of `G`, and `ϕ` is a group homomorphism from `G` to another group `K`, then `ϕ(H)` is a p-subgroup of `K`.
|
IsPGroup.iff_card
theorem IsPGroup.iff_card :
∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fact p.Prime] [inst_2 : Fintype G],
IsPGroup p G ↔ ∃ n, Fintype.card G = p ^ n
The theorem `IsPGroup.iff_card` states that for any natural number `p` and any type `G` with a group structure, where `p` is a prime number and `G` is finite, `G` is a p-group (i.e., every element of the group has an order that is a power of `p`) if and only if there exists a natural number `n` such that the cardinality of `G` (i.e., the number of elements in `G`) is equal to `p` raised to the power of `n`. In mathematical terms, a group is a p-group if and only if its order is a power of a prime `p`.
More concisely: A finite group of prime order `p` is a `p`-group if and only if its cardinality equals `p^n` for some natural number `n`.
|