Mathlib.Data.ZMod.QuotientGroup

Int.quotientZMultiplesNatEquivZMod definition

: ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n

Full source

/-- `ℤ` modulo multiples of `n : ℕ` is `ZMod n`. -/
def quotientZMultiplesNatEquivZMod : ℤℤ ⧸ AddSubgroup.zmultiples (n : ℤ)ℤ ⧸ AddSubgroup.zmultiples (n : ℤ) ≃+ ZMod n :=
  (quotientAddEquivOfEq (ZMod.ker_intCastAddHom _)).symm.trans <|
    quotientKerEquivOfRightInverse (Int.castAddHom (ZMod n)) cast intCast_zmod_cast

Equivalence between $\mathbb{Z}/n\mathbb{Z}$ and integers modulo $n$

Informal description

The additive equivalence between the quotient group $\mathbb{Z} / n\mathbb{Z}$ (where $n\mathbb{Z}$ is the additive subgroup of $\mathbb{Z}$ consisting of integer multiples of $n$) and the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$). This equivalence is constructed by first identifying the kernel of the canonical homomorphism $\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}$ with $n\mathbb{Z}$, and then using the first isomorphism theorem for additive groups.

Int.quotientZMultiplesEquivZMod definition

(a : ℤ) : ℤ ⧸ AddSubgroup.zmultiples a ≃+ ZMod a.natAbs

Full source

/-- `ℤ` modulo multiples of `a : ℤ` is `ZMod a.natAbs`. -/
def quotientZMultiplesEquivZMod (a : ℤ) : ℤℤ ⧸ AddSubgroup.zmultiples aℤ ⧸ AddSubgroup.zmultiples a ≃+ ZMod a.natAbs :=
  (quotientAddEquivOfEq (zmultiples_natAbs a)).symm.trans (quotientZMultiplesNatEquivZMod a.natAbs)

Equivalence between $\mathbb{Z}/a\mathbb{Z}$ and integers modulo $|a|$

Informal description

For any integer $a$, the additive equivalence between the quotient group $\mathbb{Z} / a\mathbb{Z}$ (where $a\mathbb{Z}$ is the additive subgroup of $\mathbb{Z}$ consisting of integer multiples of $a$) and the integers modulo $|a|$ ($\mathbb{Z}/|a|\mathbb{Z}$). This equivalence is constructed by first identifying the kernel of the canonical homomorphism $\mathbb{Z} \to \mathbb{Z}/|a|\mathbb{Z}$ with $a\mathbb{Z}$, and then using the first isomorphism theorem for additive groups.

Int.index_zmultiples theorem

(a : ℤ) : (AddSubgroup.zmultiples a).index = a.natAbs

Full source

@[simp]
lemma index_zmultiples (a : ℤ) : (AddSubgroup.zmultiples a).index = a.natAbs := by
  rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]

Index of Integer Multiples Subgroup Equals Absolute Value

Informal description

For any integer $a$, the index of the additive subgroup $a\mathbb{Z}$ (the subgroup of integer multiples of $a$) in $\mathbb{Z}$ is equal to the absolute value of $a$ as a natural number, i.e., $[\mathbb{Z} : a\mathbb{Z}] = |a|$.

AddAction.zmultiplesQuotientStabilizerEquiv definition

: zmultiples a ⧸ stabilizer (zmultiples a) b ≃+ ZMod (minimalPeriod (a +ᵥ ·) b)

Full source

/-- The quotient `(ℤ ∙ a) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod (a +ᵥ ·) b`. -/
noncomputable def zmultiplesQuotientStabilizerEquiv :
    zmultipleszmultiples a ⧸ stabilizer (zmultiples a) bzmultiples a ⧸ stabilizer (zmultiples a) b ≃+ ZMod (minimalPeriod (a +ᵥ ·) b) :=
  (ofBijective
          (map _ (stabilizer (zmultiples a) b) (zmultiplesHom (zmultiples a) ⟨a, mem_zmultiples a⟩)
            (by
              rw [zmultiples_le, mem_comap, mem_stabilizer_iff, zmultiplesHom_apply, natCast_zsmul]
              simp_rw [← vadd_iterate]
              exact isPeriodicPt_minimalPeriod (a +ᵥ ·) b))
          ⟨by
            rw [← ker_eq_bot_iff, eq_bot_iff]
            refine fun q => induction_on q fun n hn => ?_
            rw [mem_bot, eq_zero_iff, Int.mem_zmultiples_iff, ←
              zsmul_vadd_eq_iff_minimalPeriod_dvd]
            exact (eq_zero_iff _).mp hn, fun q =>
            induction_on q fun ⟨_, n, rfl⟩ => ⟨n, rfl⟩⟩).symm.trans
    (Int.quotientZMultiplesNatEquivZMod (minimalPeriod (a +ᵥ ·) b))

Equivalence between quotient of integer multiples and ZMod for minimal period action

Informal description

The quotient group $(ℤ ∙ a) ⧸ \text{stabilizer}(b)$ is additively equivalent to the integers modulo the minimal period of the action of $a$ on $b$, denoted as $\mathbb{Z}/n\mathbb{Z}$ where $n$ is the minimal period of the function $x \mapsto a +ᵥ x$ at $b$. Here: - $ℤ ∙ a$ denotes the additive subgroup of $\mathbb{Z}$ generated by $a$ - $\text{stabilizer}(b)$ is the stabilizer subgroup of $b$ under the action - $a +ᵥ x$ denotes the action of $a$ on $x$ - The minimal period is the smallest positive integer $n$ such that $(a +ᵥ)^n b = b$

AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply theorem

 (n : ZMod (minimalPeriod (a +ᵥ ·) b)) :
  (zmultiplesQuotientStabilizerEquiv a b).symm n = (cast n : ℤ) • (⟨a, mem_zmultiples a⟩ : zmultiples a)

Full source

theorem zmultiplesQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a +ᵥ ·) b)) :
    (zmultiplesQuotientStabilizerEquiv a b).symm n =
      (cast n : ℤ) • (⟨a, mem_zmultiples a⟩ : zmultiples a) :=
  rfl

Inverse Image of Additive Equivalence between Quotient of Integer Multiples and $\mathbb{Z}/k\mathbb{Z}$

Informal description

For any integer $a$ and element $b$ in an additive action, and for any $n \in \mathbb{Z}/k\mathbb{Z}$ where $k$ is the minimal period of the action $x \mapsto a +ᵥ x$ at $b$, the inverse of the additive equivalence $\text{zmultiplesQuotientStabilizerEquiv}$ maps $n$ to the coset represented by the integer multiple $(n \bmod k) \cdot a$ in the quotient group $(\mathbb{Z} \cdot a) / \text{stabilizer}(b)$. Here: - $\mathbb{Z} \cdot a$ denotes the additive subgroup of $\mathbb{Z}$ generated by $a$ - $\text{stabilizer}(b)$ is the stabilizer subgroup of $b$ under the action - $a +ᵥ x$ denotes the action of $a$ on $x$ - The minimal period $k$ is the smallest positive integer such that $(a +ᵥ)^k b = b$

MulAction.zpowersQuotientStabilizerEquiv definition

: zpowers a ⧸ stabilizer (zpowers a) b ≃* Multiplicative (ZMod (minimalPeriod (a • ·) b))

Full source

/-- The quotient `(a ^ ℤ) ⧸ (stabilizer b)` is cyclic of order `minimalPeriod ((•) a) b`. -/
noncomputable def zpowersQuotientStabilizerEquiv :
    zpowerszpowers a ⧸ stabilizer (zpowers a) bzpowers a ⧸ stabilizer (zpowers a) b ≃* Multiplicative (ZMod (minimalPeriod (a • ·) b)) :=
  letI f := zmultiplesQuotientStabilizerEquiv (Additive.ofMul a) b
  AddEquiv.toMultiplicative f

Multiplicative equivalence between quotient of powers and ZMod for minimal period action

Informal description

The quotient group $(⟨a⟩) ⧸ \text{stabilizer}(b)$ is multiplicatively equivalent to the multiplicative group of integers modulo the minimal period of the action of $a$ on $b$, denoted as $(\mathbb{Z}/n\mathbb{Z})^\times$ where $n$ is the minimal period of the function $x \mapsto a \cdot x$ at $b$. Here: - $⟨a⟩$ denotes the multiplicative subgroup generated by $a$ - $\text{stabilizer}(b)$ is the stabilizer subgroup of $b$ under the action - $a \cdot x$ denotes the action of $a$ on $x$ - The minimal period is the smallest positive integer $n$ such that $(a \cdot)^n b = b$

MulAction.zpowersQuotientStabilizerEquiv_symm_apply theorem

 (n : ZMod (minimalPeriod (a • ·) b)) :
  (zpowersQuotientStabilizerEquiv a b).symm n = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast n : ℤ)

Full source

theorem zpowersQuotientStabilizerEquiv_symm_apply (n : ZMod (minimalPeriod (a • ·) b)) :
    (zpowersQuotientStabilizerEquiv a b).symm n = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast n : ℤ) :=
  rfl

Inverse Image of Multiplicative Equivalence between Quotient of Cyclic Subgroup and $\mathbb{Z}/k\mathbb{Z}$

Informal description

For any element $a$ in a group acting on a type, and any element $b$ in that type, the inverse of the multiplicative equivalence $\text{zpowersQuotientStabilizerEquiv}$ maps an element $n$ of $\mathbb{Z}/k\mathbb{Z}$ (where $k$ is the minimal period of the action $x \mapsto a \cdot x$ at $b$) to the coset represented by $a^{\text{cast}(n)}$ in the quotient group $(\langle a \rangle) / \text{stabilizer}(b)$. Here: - $\langle a \rangle$ denotes the cyclic subgroup generated by $a$ - $\text{stabilizer}(b)$ is the stabilizer subgroup of $b$ under the group action - $a \cdot x$ denotes the action of $a$ on $x$ - The minimal period $k$ is the smallest positive integer such that $(a \cdot)^k b = b$ - $\text{cast}(n)$ denotes the canonical map from $\mathbb{Z}/k\mathbb{Z}$ to $\mathbb{Z}$

MulAction.orbitZPowersEquiv definition

: orbit (zpowers a) b ≃ ZMod (minimalPeriod (a • ·) b)

Full source

/-- The orbit `(a ^ ℤ) • b` is a cycle of order `minimalPeriod ((•) a) b`. -/
noncomputable def orbitZPowersEquiv : orbitorbit (zpowers a) b ≃ ZMod (minimalPeriod (a • ·) b) :=
  (orbitEquivQuotientStabilizer _ b).trans (zpowersQuotientStabilizerEquiv a b).toEquiv

Bijection between orbit under cyclic group action and integers modulo minimal period

Informal description

Given a group element $ a $ acting on a type $ \beta $ and an element $ b \in \beta $, there is a bijection between the orbit of $ b $ under the action of the cyclic subgroup generated by $ a $ and the integers modulo the minimal period of the function $ x \mapsto a \cdot x $ at $ b $. Here: - The orbit $ \text{orbit}(\langle a \rangle, b) $ is the set of all elements $ a^k \cdot b $ for $ k \in \mathbb{Z} $. - The minimal period is the smallest positive integer $ n $ such that $ a^n \cdot b = b $. - The bijection is constructed by composing the orbit-stabilizer bijection with the equivalence between the quotient of the cyclic subgroup by the stabilizer and $ \mathbb{Z}/n\mathbb{Z} $.

AddAction.orbitZMultiplesEquiv definition

 {α β : Type*} [AddGroup α] (a : α) [AddAction α β] (b : β) :
  AddAction.orbit (zmultiples a) b ≃ ZMod (minimalPeriod (a +ᵥ ·) b)

Full source

/-- The orbit `(ℤ • a) +ᵥ b` is a cycle of order `minimalPeriod (a +ᵥ ·) b`. -/
noncomputable def _root_.AddAction.orbitZMultiplesEquiv {α β : Type*} [AddGroup α] (a : α)
    [AddAction α β] (b : β) :
    AddAction.orbitAddAction.orbit (zmultiples a) b ≃ ZMod (minimalPeriod (a +ᵥ ·) b) :=
  (AddAction.orbitEquivQuotientStabilizer (zmultiples a) b).trans
    (zmultiplesQuotientStabilizerEquiv a b).toEquiv

Equivalence between orbit under integer multiples action and ZMod of minimal period

Informal description

Given an additive group $\alpha$ acting on a type $\beta$, for any element $a \in \alpha$ and $b \in \beta$, the orbit of $b$ under the action of the additive subgroup generated by $a$ is in bijection with the integers modulo the minimal period of the function $x \mapsto a +ᵥ x$ at $b$. Here: - $zmultiples\, a$ denotes the additive subgroup of $\alpha$ generated by $a$ - The minimal period is the smallest positive integer $n$ such that $(a +ᵥ)^n b = b$ - The bijection is constructed via the orbit-stabilizer theorem and the equivalence between the quotient of the integer multiples and $\mathbb{Z}/n\mathbb{Z}$.

MulAction.orbitZPowersEquiv_symm_apply theorem

 (k : ZMod (minimalPeriod (a • ·) b)) :
  (orbitZPowersEquiv a b).symm k = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast k : ℤ) • ⟨b, mem_orbit_self b⟩

Full source

@[to_additive]
theorem orbitZPowersEquiv_symm_apply (k : ZMod (minimalPeriod (a • ·) b)) :
    (orbitZPowersEquiv a b).symm k =
      (⟨a, mem_zpowers a⟩ : zpowers a) ^ (cast k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
  rfl

Inverse of Orbit-Cyclic Group Bijection: Action of $a^{\text{cast}(k)}$ on $b$

Informal description

For any group element $a$ acting on a type $\beta$ and any element $b \in \beta$, the inverse of the bijection $\text{orbit}(\langle a \rangle, b) \simeq \mathbb{Z}/n\mathbb{Z}$ (where $n$ is the minimal period of $x \mapsto a \cdot x$ at $b$) maps an element $k \in \mathbb{Z}/n\mathbb{Z}$ to the group action of $a^{\text{cast}(k)}$ on $b$, where $\text{cast}(k)$ is the canonical lift of $k$ to $\mathbb{Z}$.

MulAction.orbitZPowersEquiv_symm_apply' theorem

(k : ℤ) : (orbitZPowersEquiv a b).symm k = (⟨a, mem_zpowers a⟩ : zpowers a) ^ k • ⟨b, mem_orbit_self b⟩

Full source

theorem orbitZPowersEquiv_symm_apply' (k : ℤ) :
    (orbitZPowersEquiv a b).symm k =
      (⟨a, mem_zpowers a⟩ : zpowers a) ^ k • ⟨b, mem_orbit_self b⟩ := by
  rw [orbitZPowersEquiv_symm_apply, ZMod.coe_intCast]
  exact Subtype.ext (zpow_smul_mod_minimalPeriod _ _ k)

Inverse of Orbit-Cyclic Group Bijection Evaluated at Integer: $(\text{orbitZPowersEquiv}\, a\, b)^{-1}(k) = a^k \cdot b$

Informal description

For any group element $a$ acting on a type $\beta$ and any element $b \in \beta$, the inverse of the bijection $\text{orbit}(\langle a \rangle, b) \simeq \mathbb{Z}/n\mathbb{Z}$ (where $n$ is the minimal period of the function $x \mapsto a \cdot x$ at $b$) evaluated at an integer $k \in \mathbb{Z}$ is given by the group action of $a^k$ on $b$, i.e., $$ (\text{orbitZPowersEquiv}\, a\, b)^{-1}(k) = a^k \cdot b. $$

AddAction.orbitZMultiplesEquiv_symm_apply' theorem

 {α β : Type*} [AddGroup α] (a : α) [AddAction α β] (b : β) (k : ℤ) :
  (AddAction.orbitZMultiplesEquiv a b).symm k =
    k • (⟨a, mem_zmultiples a⟩ : zmultiples a) +ᵥ ⟨b, AddAction.mem_orbit_self b⟩

Full source

theorem _root_.AddAction.orbitZMultiplesEquiv_symm_apply' {α β : Type*} [AddGroup α] (a : α)
    [AddAction α β] (b : β) (k : ℤ) :
    (AddAction.orbitZMultiplesEquiv a b).symm k =
      k • (⟨a, mem_zmultiples a⟩ : zmultiples a) +ᵥ ⟨b, AddAction.mem_orbit_self b⟩ := by
  rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]
  -- Making `a` explicit turns this from ~190000 heartbeats to ~700.
  exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a _ k)

Inverse of Orbit-ZMultiples Equivalence Evaluated at Integer

Informal description

Let $\alpha$ be an additive group acting on a type $\beta$, and let $a \in \alpha$ and $b \in \beta$. For any integer $k$, the inverse of the equivalence $\text{AddAction.orbitZMultiplesEquiv}$ evaluated at $k$ is given by the action of $k \cdot a$ on $b$, where $k \cdot a$ is the $k$-th multiple of $a$ in the additive subgroup generated by $a$. More precisely, we have: \[ (\text{AddAction.orbitZMultiplesEquiv}\, a\, b)^{-1}(k) = k \cdot a +ᵥ b, \] where $+ᵥ$ denotes the action of $\alpha$ on $\beta$.

MulAction.minimalPeriod_eq_card theorem

[Fintype (orbit (zpowers a) b)] : minimalPeriod (a • ·) b = Fintype.card (orbit (zpowers a) b)

Full source

@[to_additive]
theorem minimalPeriod_eq_card [Fintype (orbit (zpowers a) b)] :
    minimalPeriod (a • ·) b = Fintype.card (orbit (zpowers a) b) := by
  rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), ZMod.card]

Minimal Period Equals Orbit Cardinality for Cyclic Group Action

Informal description

For a finite orbit of an element $b$ under the action of the cyclic subgroup generated by $a$ in a group, the minimal period of the function $x \mapsto a \cdot x$ at $b$ is equal to the cardinality of the orbit. That is, if the orbit $\text{orbit}(\langle a \rangle, b)$ is finite, then \[ \text{minimalPeriod}\, (a \cdot \cdot)\, b = |\text{orbit}(\langle a \rangle, b)|. \]

MulAction.minimalPeriod_pos instance

[Finite <| orbit (zpowers a) b] : NeZero <| minimalPeriod (a • ·) b

Full source

@[to_additive]
instance minimalPeriod_pos [Finite <| orbit (zpowers a) b] :
    NeZero <| minimalPeriod (a • ·) b :=
  ⟨by
    cases nonempty_fintype (orbit (zpowers a) b)
    haveI : Nonempty (orbit (zpowers a) b) := (orbit_nonempty b).to_subtype
    rw [minimalPeriod_eq_card]
    exact Fintype.card_ne_zero⟩

Nonzero Minimal Period for Finite Cyclic Group Orbits

Informal description

For any element $b$ in a type $\alpha$ acted upon by a group, if the orbit of $b$ under the action of the cyclic subgroup generated by $a$ is finite, then the minimal period of the function $x \mapsto a \cdot x$ at $b$ is nonzero.

Nat.card_zpowers theorem

: Nat.card (zpowers a) = orderOf a

Full source

/-- See also `Fintype.card_zpowers`. -/
@[to_additive (attr := simp) "See also `Fintype.card_zmultiples`."]
theorem Nat.card_zpowers : Nat.card (zpowers a) = orderOf a := by
  have := Nat.card_congr (MulAction.orbitZPowersEquiv a (1 : α))
  rwa [Nat.card_zmod, orbit_subgroup_one_eq_self] at this

Cardinality of Cyclic Subgroup Equals Order of Generator

Informal description

For any element $a$ in a group, the cardinality of the cyclic subgroup generated by $a$ is equal to the order of $a$, i.e., $\mathrm{card}(\langle a \rangle) = \mathrm{orderOf}(a)$.

finite_zpowers theorem

: (zpowers a : Set α).Finite ↔ IsOfFinOrder a

Full source

@[to_additive (attr := simp)]
lemma finite_zpowers : (zpowers a : Set α).Finite ↔ IsOfFinOrder a := by
  simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe,
    nonempty_coe_sort, Nat.card_pos_iff, Set.finite_coe_iff, Subgroup.coe_nonempty, true_and]

Finite Powers of an Element if and only if the Element has Finite Order

Informal description

For an element $a$ in a group $\alpha$, the set $\text{zpowers}(a) = \{a^n \mid n \in \mathbb{Z}\}$ is finite if and only if $a$ has finite order (i.e., there exists a positive integer $n$ such that $a^n = 1$).

infinite_zpowers theorem

: (zpowers a : Set α).Infinite ↔ ¬IsOfFinOrder a

Full source

@[to_additive (attr := simp)]
lemma infinite_zpowers : (zpowers a : Set α).Infinite ↔ ¬IsOfFinOrder a := finite_zpowers.not

Infinite Powers of an Element if and only if the Element has Infinite Order

Informal description

For an element $a$ in a group $\alpha$, the set $\text{zpowers}(a) = \{a^n \mid n \in \mathbb{Z}\}$ is infinite if and only if $a$ does not have finite order (i.e., there does not exist a positive integer $n$ such that $a^n = 1$).

Subgroup.quotientEquivSigmaZMod definition

: G ⧸ H ≃ Σ q : orbitRel.Quotient (zpowers g) (G ⧸ H), ZMod (minimalPeriod (g • ·) q.out)

Full source

/-- Partition `G ⧸ H` into orbits of the action of `g : G`. -/
noncomputable def quotientEquivSigmaZMod :
    G ⧸ HG ⧸ H ≃ Σq : orbitRel.Quotient (zpowers g) (G ⧸ H), ZMod (minimalPeriod (g • ·) q.out) :=
  (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)).trans
    (sigmaCongrRight fun q => orbitZPowersEquiv g q.out)

Decomposition of quotient group into cyclic group orbits

Informal description

Given a group $G$, a subgroup $H$, and an element $g \in G$, there is a natural equivalence between the quotient group $G/H$ and the disjoint union of copies of $\mathbb{Z}/n\mathbb{Z}$, where each copy corresponds to an orbit of the action of the cyclic subgroup $\langle g \rangle$ on $G/H$, and $n$ is the minimal period of the action of $g$ on a representative of that orbit. More precisely, the equivalence is: $$ G/H \simeq \bigsqcup_{q \in (G/H)/\langle g \rangle} \mathbb{Z}/n_q\mathbb{Z} $$ where $n_q$ is the minimal positive integer such that $g^{n_q} \cdot q = q$ for a representative $q$ of each $\langle g \rangle$-orbit in $G/H$.

Subgroup.quotientEquivSigmaZMod_symm_apply theorem

 (q : orbitRel.Quotient (zpowers g) (G ⧸ H)) (k : ZMod (minimalPeriod (g • ·) q.out)) :
  (quotientEquivSigmaZMod H g).symm ⟨q, k⟩ = g ^ (cast k : ℤ) • q.out

Full source

lemma quotientEquivSigmaZMod_symm_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
    (k : ZMod (minimalPeriod (g • ·) q.out)) :
    (quotientEquivSigmaZMod H g).symm ⟨q, k⟩ = g ^ (cast k : ℤ) • q.out := rfl

Inverse of Quotient Group Decomposition into Cyclic Orbits

Informal description

Let $G$ be a group, $H$ a subgroup of $G$, and $g \in G$. For any equivalence class $q$ in the quotient $(G/H)/\langle g \rangle$ of the orbit relation induced by the cyclic subgroup $\langle g \rangle$ acting on $G/H$, and for any element $k$ in $\mathbb{Z}/n_q\mathbb{Z}$ (where $n_q$ is the minimal period of the action of $g$ on a representative of $q$), the inverse of the quotient equivalence map satisfies: $$ (\text{quotientEquivSigmaZMod}\, H\, g)^{-1}\langle q, k\rangle = g^{\text{cast}(k)} \cdot \text{out}(q) $$ where $\text{out}(q)$ is a representative of the equivalence class $q$ in $G/H$, and $\text{cast}(k)$ converts $k$ to an integer.

Subgroup.quotientEquivSigmaZMod_apply theorem

(q : orbitRel.Quotient (zpowers g) (G ⧸ H)) (k : ℤ) : quotientEquivSigmaZMod H g (g ^ k • q.out) = ⟨q, k⟩

Full source

lemma quotientEquivSigmaZMod_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H)) (k : ℤ) :
    quotientEquivSigmaZMod H g (g ^ k • q.out) = ⟨q, k⟩ := by
  rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
    zpow_smul_mod_minimalPeriod]

Forward map of quotient group decomposition into cyclic orbits

Informal description

Let $G$ be a group, $H$ a subgroup of $G$, and $g \in G$. For any equivalence class $q$ in the quotient $(G/H)/\langle g \rangle$ of the orbit relation induced by the cyclic subgroup $\langle g \rangle$ acting on $G/H$, and for any integer $k$, the equivalence map satisfies: $$ \text{quotientEquivSigmaZMod}\, H\, g (g^k \cdot \text{out}(q)) = \langle q, k \rangle $$ where $\text{out}(q)$ is a representative of the equivalence class $q$ in $G/H$.

Mathlib.Data.ZMod.QuotientGroup

Main definitions

Tags