LeanPool.OrderPQ.Main #

source

theorem OrderPQ.exists_card_eq_prime_mul_prime_and_not_isCyclic_iff {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] :

(∃ (G : Type) (x : Group G), Nat.card G = p * q ∧ ¬IsCyclic G) ↔ p = q ∨ p ∣ q - 1 ∨ q ∣ p - 1

There exists a noncyclic group G of order p * q if and only if p equals q or p divides q - 1 or q divides p - 1.

source

theorem OrderPQ.nonempty_mulEquiv_of_card_eq_prime_mul_prime_of_not_isCyclic {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] {G1 : Type u_1} [Group G1] (h1 : Nat.card G1 = p * q) (h1' : ¬IsCyclic G1) {G2 : Type u_2} [Group G2] (h2 : Nat.card G2 = p * q) (h2' : ¬IsCyclic G2) :

Nonempty (G1 ≃* G2)

Any two noncyclic groups of order p * q are isomorphic.

source

theorem OrderPQ.nonempty_mulEquiv_prod_of_card_eq_prime_pow_two_of_not_isCyclic {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] (h : Nat.card G = p ^ 2) (h' : ¬IsCyclic G) :

Nonempty (G ≃* MulZMod p × MulZMod p)

Every noncyclic group of order p ^ 2 is isomorphic to the direct product of MulZMod p with itself.

source

theorem OrderPQ.nonempty_mulEquiv_semidirectProduct_of_card_eq_prime_mul_prime {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p < q) {G : Type u_1} [Group G] (h : Nat.card G = p * q) :

∃ (φ : MulZMod p →* MulAut (MulZMod q)), Nonempty (G ≃* MulZMod q ⋊[φ] MulZMod p)

If p < q, then for any noncyclic group G of order p * q there exists a homomorphism φ from MulZMod p to the automorphism group of MulZMod q such that G is isomorphic to the semidirect product of MulZMod q and MulZMod p defined by φ.

source

theorem OrderPQ.nonempty_mulEquiv_semidirectProduct_of_card_eq_prime_mul_prime_of_not_isCyclic {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p < q) {G : Type u_1} [Group G] (h : Nat.card G = p * q) (h' : ¬IsCyclic G) (φ : MulZMod p →* MulAut (MulZMod q)) (hφ : φ ≠ 1) :

Nonempty (G ≃* MulZMod q ⋊[φ] MulZMod p)

If p < q, then every noncyclic group of order p * q is isomorphic to the semidirect product of MulZMod q and MulZMod p defined by any nontrivial homomorphism from MulZMod p to the automorphism group of MulZMod q.