Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Subgroup.range_zpowersHom theorem

(g : G) : (zpowersHom G g).range = zpowers g

Full source

theorem range_zpowersHom (g : G) : (zpowersHom G g).range = zpowers g := rfl

Range of Integer Powers Homomorphism Equals Subgroup Generated by Element

Informal description

For any element $g$ in a group $G$, the range of the homomorphism `zpowersHom G g` (which maps integers to integer powers of $g$) is equal to the subgroup generated by $g$, denoted as $\text{zpowers } g$.

Subgroup.instCountableSubtypeMemZpowers instance

(a : G) : Countable (zpowers a)

Full source

@[to_additive]
instance (a : G) : Countable (zpowers a) := Set.surjective_onto_range.countable

Countability of Cyclic Subgroups

Informal description

For any element $a$ in a group $G$, the subgroup generated by $a$ (denoted $\langle a \rangle$) is countable.

AddSubgroup.range_zmultiplesHom theorem

(a : A) : (zmultiplesHom A a).range = zmultiples a

Full source

@[simp]
theorem range_zmultiplesHom (a : A) : (zmultiplesHom A a).range = zmultiples a :=
  rfl

Range of Integer Multiples Homomorphism Equals Additive Subgroup Generated by Element

Informal description

For any element $a$ in an additive group $A$, the range of the homomorphism `zmultiplesHom A a` (which maps integers to integer multiples of $a$) is equal to the additive subgroup generated by $a$, denoted as $\text{zmultiples } a$.

AddSubgroup.intCast_mul_mem_zmultiples theorem

: ↑(k : ℤ) * r ∈ zmultiples r

Full source

@[simp]
theorem intCast_mul_mem_zmultiples : ↑(k : ℤ) * r ∈ zmultiples r := by
  simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k

Integer multiples belong to additive cyclic subgroup

Informal description

For any integer $k$ and any element $r$ in an additive group, the element $k \cdot r$ belongs to the additive subgroup generated by $r$, i.e., $k \cdot r \in \langle r \rangle_{\text{add}}$.

AddSubgroup.intCast_mem_zmultiples_one theorem

: ↑(k : ℤ) ∈ zmultiples (1 : R)

Full source

@[simp]
theorem intCast_mem_zmultiples_one : ↑(k : ℤ) ∈ zmultiples (1 : R) :=
  mem_zmultiples_iff.mp ⟨k, by simp⟩

Integer multiples of identity belong to additive cyclic subgroup

Informal description

For any integer $k$ and any ring $R$, the element $k \cdot 1$ belongs to the additive subgroup generated by the multiplicative identity $1$ in $R$, i.e., $k \in \langle 1 \rangle_{\text{add}}$.

Int.range_castAddHom theorem

{A : Type*} [AddGroupWithOne A] : (Int.castAddHom A).range = AddSubgroup.zmultiples 1

Full source

@[simp] lemma Int.range_castAddHom {A : Type*} [AddGroupWithOne A] :
    (Int.castAddHom A).range = AddSubgroup.zmultiples 1 := by
  ext a
  simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]

Range of Integer Cast Homomorphism Equals Additive Cyclic Subgroup Generated by One

Informal description

For any additive group with one $A$, the range of the canonical additive homomorphism $\text{Int.castAddHom} : \mathbb{Z} \to A$ is equal to the additive subgroup generated by the multiplicative identity $1 \in A$, i.e., $\text{range}(\text{Int.castAddHom}) = \langle 1 \rangle_{\text{add}}$.

Subgroup.centralizer_closure theorem

(S : Set G) : centralizer (closure S : Set G) = ⨅ g ∈ S, centralizer (zpowers g : Set G)

Full source

@[to_additive]
theorem centralizer_closure (S : Set G) :
    centralizer (closure S : Set G) = ⨅ g ∈ S, centralizer (zpowers g : Set G) :=
  le_antisymm
      (le_iInf fun _ => le_iInf fun hg => centralizer_le <| zpowers_le.2 <| subset_closure hg) <|
    le_centralizer_iff.1 <|
      (closure_le _).2 fun g =>
        SetLike.mem_coeSetLike.mem_coe.2 ∘ zpowers_le.1 ∘ le_centralizer_iff.1 ∘ iInf_le_of_le g ∘ iInf_le _

Centralizer of Generated Subgroup Equals Infimum of Centralizers of Cyclic Subgroups

Informal description

For any subset $S$ of a group $G$, the centralizer of the subgroup generated by $S$ is equal to the infimum over all $g \in S$ of the centralizers of the cyclic subgroups generated by $g$. In other words, \[ \text{centralizer}(\langle S \rangle) = \bigsqcap_{g \in S} \text{centralizer}(\langle g \rangle). \]

Subgroup.center_eq_iInf theorem

(S : Set G) (hS : closure S = ⊤) : center G = ⨅ g ∈ S, centralizer (zpowers g)

Full source

@[to_additive]
theorem center_eq_iInf (S : Set G) (hS : closure S = ⊤) :
    center G = ⨅ g ∈ S, centralizer (zpowers g) := by
  rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]

Center as Infimum of Centralizers of Cyclic Subgroups for Generating Set

Informal description

For any subset $S$ of a group $G$ such that the subgroup generated by $S$ is the entire group $G$, the center of $G$ is equal to the infimum over all $g \in S$ of the centralizers of the cyclic subgroups generated by $g$. In other words, \[ \text{center}(G) = \bigsqcap_{g \in S} \text{centralizer}(\langle g \rangle). \]

Subgroup.center_eq_infi' theorem

(S : Set G) (hS : closure S = ⊤) : center G = ⨅ g : S, centralizer (zpowers (g : G))

Full source

@[to_additive]
theorem center_eq_infi' (S : Set G) (hS : closure S = ⊤) :
    center G = ⨅ g : S, centralizer (zpowers (g : G)) := by
  rw [center_eq_iInf S hS, ← iInf_subtype'']

Center as Infimum of Centralizers of Cyclic Subgroups for Generating Set

Informal description

For any subset $S$ of a group $G$ such that the subgroup generated by $S$ is the entire group $G$, the center of $G$ is equal to the infimum over all $g \in S$ of the centralizers of the cyclic subgroups generated by $g$. In other words, \[ \text{center}(G) = \bigsqcap_{g \in S} \text{centralizer}(\langle g \rangle). \]

Tags