Complementary results to p-primary subgroups

theorem CommMonoid.mem_primaryComponent (G : Type u_1) [CommMonoid G] (p : ℕ) [Fact (Nat.Prime p)] (g : G) : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), orderOf g = p ^ n

TODO: go to mathlib

theorem AddCommMonoid.mem_primaryComponent (G : Type u_1) [AddCommMonoid G] (p : ℕ) [Fact (Nat.Prime p)] (g : G) : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), addOrderOf g = p ^ n

theorem CommGroup.mem_primaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (g : G) : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), orderOf g = p ^ n

TODO: go to mathlib

theorem AddCommGroup.mem_primaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (g : G) : g ∈ primaryComponent G p ↔ ∃ (n : ℕ), addOrderOf g = p ^ n

def CommMonoid.primeToComponent (G : Type u_1) [CommMonoid G] (n : ℕ) : Submonoid G

The prime-to-n component is the submonoid of elements with order prime to n.

Equations

• CommMonoid.primeToComponent G n = { carrier := {g : G | (orderOf g).Coprime n}, mul_mem' := ⋯, one_mem' := ⋯ }

def AddCommMonoid.primeToComponent (G : Type u_1) [AddCommMonoid G] (n : ℕ) : AddSubmonoid G

The prime-to-n component is the submonoid of elements with additive order prime to n.

Equations

• AddCommMonoid.primeToComponent G n = { carrier := {g : G | (addOrderOf g).Coprime n}, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem AddCommMonoid.coe_primeToComponent (G : Type u_1) [AddCommMonoid G] (n : ℕ) : ↑(primeToComponent G n) = {g : G | (addOrderOf g).Coprime n}

@[simp]

theorem CommMonoid.coe_primeToComponent (G : Type u_1) [CommMonoid G] (n : ℕ) : ↑(primeToComponent G n) = {g : G | (orderOf g).Coprime n}

def CommGroup.primeToComponent (G : Type u_1) [CommGroup G] (n : ℕ) : Subgroup G

The prime-to-n component is the subgroup of elements with order prime to n.

Equations

• CommGroup.primeToComponent G n = { toSubmonoid := CommMonoid.primeToComponent G n, inv_mem' := ⋯ }

def AddCommGroup.primeToComponent (G : Type u_1) [AddCommGroup G] (n : ℕ) : AddSubgroup G

The prime-to-n component is the subgroup of elements with additive order prime to n.

Equations

• AddCommGroup.primeToComponent G n = { toAddSubmonoid := AddCommMonoid.primeToComponent G n, neg_mem' := ⋯ }

@[simp]

theorem AddCommGroup.coe_primeToComponent (G : Type u_1) [AddCommGroup G] (n : ℕ) : ↑(primeToComponent G n) = {g : G | (addOrderOf g).Coprime n}

@[simp]

theorem CommGroup.coe_primeToComponent (G : Type u_1) [CommGroup G] (n : ℕ) : ↑(primeToComponent G n) = {g : G | (orderOf g).Coprime n}

theorem CommMonoid.mem_primeToComponent (G : Type u_1) [CommMonoid G] (n : ℕ) (g : G) : g ∈ primeToComponent G n ↔ (orderOf g).Coprime n

theorem AddCommMonoid.mem_primeToComponent (G : Type u_1) [AddCommMonoid G] (n : ℕ) (g : G) : g ∈ primeToComponent G n ↔ (addOrderOf g).Coprime n

theorem CommGroup.mem_primeToComponent (G : Type u_1) [CommGroup G] (n : ℕ) (g : G) : g ∈ primeToComponent G n ↔ (orderOf g).Coprime n

theorem AddCommGroup.mem_primeToComponent (G : Type u_1) [AddCommGroup G] (n : ℕ) (g : G) : g ∈ primeToComponent G n ↔ (addOrderOf g).Coprime n

theorem CommGroup.card_primeToComponent_coprime (G : Type u_1) [CommGroup G] [Finite G] (n : ℕ) : (Nat.card ↥(primeToComponent G n)).Coprime n

theorem AddCommGroup.card_primeToComponent_coprime (G : Type u_1) [AddCommGroup G] [Finite G] (n : ℕ) : (Nat.card ↥(primeToComponent G n)).Coprime n

theorem orderOf_zpow_dvd {G : Type u_2} [Group G] {x : G} (n : ℤ) : orderOf (x ^ n) ∣ orderOf x

TODO: go to mathlib

theorem addOrderOf_zsmul_dvd {G : Type u_2} [AddGroup G] {x : G} (n : ℤ) : addOrderOf (n • x) ∣ addOrderOf x

theorem orderOf_zpow_eq_orderOf_pow_natAbs {G : Type u_2} [Group G] {x : G} (n : ℤ) : orderOf (x ^ n) = orderOf (x ^ n.natAbs)

TODO: go to mathlib

theorem addOrderOf_zsmul_eq_addOrderOf_nsmul_natAbs {G : Type u_2} [AddGroup G] {x : G} (n : ℤ) : addOrderOf (n • x) = addOrderOf (n.natAbs • x)

noncomputable def CommGroup.equivPrimeToComponentProdPrimaryComponent (G : Type u_1) [CommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (ht : Monoid.IsTorsion G) : G ≃* ↥(primeToComponent G p) × ↥(primaryComponent G p)

A torsion abelian group is canonically isomorphic to the product of its prime-to-p component and its p-primary component.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGroup.equivPrimeToComponentProdPrimaryComponent (G : Type u_1) [AddCommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (ht : AddMonoid.IsTorsion G) : G ≃+ ↥(primeToComponent G p) × ↥(primaryComponent G p)

A torsion additive abelian group is canonically isomorphic to the product of its prime-to-p component and its p-primary component.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroup.equivPrimeToComponentProdPrimaryComponent_symm_apply (G : Type u_1) [CommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (ht : Monoid.IsTorsion G) (g : ↥(primeToComponent G p) × ↥(primaryComponent G p)) : (equivPrimeToComponentProdPrimaryComponent G p ht).symm g = ↑g.1 * ↑g.2

@[simp]

theorem AddCommGroup.equivPrimeToComponentProdPrimaryComponent_symm_apply (G : Type u_1) [AddCommGroup G] (p : ℕ) [Fact (Nat.Prime p)] (ht : AddMonoid.IsTorsion G) (g : ↥(primeToComponent G p) × ↥(primaryComponent G p)) : (equivPrimeToComponentProdPrimaryComponent G p ht).symm g = ↑g.1 + ↑g.2

theorem CommGroup.card_primaryComponent (G : Type u_1) [CommGroup G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] : Nat.card ↥(primaryComponent G p) = p ^ (Nat.card G).factorization p

theorem CommGroup.card_primeToComponent (G : Type u_1) [CommGroup G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] : Nat.card ↥(primeToComponent G p) = Nat.card G / p ^ (Nat.card G).factorization p