feat(data/zmod/quotient): More API for orbit_zpowers_equiv (#14181)

This PR adds another `symm_apply` API lemma for `orbit_zpowers_equiv`, taking `(k : ℤ)` rather than `(k : zmod (minimal_period ((•) a) b))`.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/data/zmod/quotient.lean

@@ -94,19 +94,18 @@ end add_action
 
 namespace mul_action
 
-open subgroup function
+open add_action subgroup add_subgroup function
 
 variables {α β : Type*} [group α] (a : α) [mul_action α β] (b : β)
 
 /-- The quotient `(a ^ ℤ) ⧸ (stabilizer b)` is cyclic of order `minimal_period ((•) a) b`. -/
 noncomputable def zpowers_quotient_stabilizer_equiv :
   zpowers a ⧸ stabilizer (zpowers a) b ≃* multiplicative (zmod (minimal_period ((•) a) b)) :=
-let f := add_action.zmultiples_quotient_stabilizer_equiv (additive.of_mul a) b in
+let f := zmultiples_quotient_stabilizer_equiv (additive.of_mul a) b in
 ⟨f.to_fun, f.inv_fun, f.left_inv, f.right_inv, f.map_add'⟩
 
 lemma zpowers_quotient_stabilizer_equiv_symm_apply (n : zmod (minimal_period ((•) a) b)) :
-  (zpowers_quotient_stabilizer_equiv a b).symm n =
-    (⟨a, mem_zpowers a⟩ : zpowers a) ^ (n : ℤ) :=
+  (zpowers_quotient_stabilizer_equiv a b).symm n = (⟨a, mem_zpowers a⟩ : zpowers a) ^ (n : ℤ) :=
 rfl
 
 /-- The orbit `(a ^ ℤ) • b` is a cycle of order `minimal_period ((•) a) b`. -/
@@ -116,18 +115,37 @@ noncomputable def orbit_zpowers_equiv : orbit (zpowers a) b ≃ zmod (minimal_pe
 /-- The orbit `(ℤ • a) +ᵥ b` is a cycle of order `minimal_period ((+ᵥ) a) b`. -/
 noncomputable def _root_.add_action.orbit_zmultiples_equiv
   {α β : Type*} [add_group α] (a : α) [add_action α β] (b : β) :
-  add_action.orbit (add_subgroup.zmultiples a) b ≃ zmod (minimal_period ((+ᵥ) a) b) :=
-(add_action.orbit_equiv_quotient_stabilizer (add_subgroup.zmultiples a) b).trans
-  (add_action.zmultiples_quotient_stabilizer_equiv a b).to_equiv
+  add_action.orbit (zmultiples a) b ≃ zmod (minimal_period ((+ᵥ) a) b) :=
+(add_action.orbit_equiv_quotient_stabilizer (zmultiples a) b).trans
+  (zmultiples_quotient_stabilizer_equiv a b).to_equiv
 
 attribute [to_additive orbit_zmultiples_equiv] orbit_zpowers_equiv
 
 @[to_additive orbit_zmultiples_equiv_symm_apply]
-lemma orbit_zpowers_equiv_symm_apply
-  (k : zmod (minimal_period ((•) a) b)) : (orbit_zpowers_equiv a b).symm k =
-  (⟨a, mem_zpowers a⟩ : zpowers a) ^ (k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
+lemma orbit_zpowers_equiv_symm_apply (k : zmod (minimal_period ((•) a) b)) :
+  (orbit_zpowers_equiv a b).symm k =
+    (⟨a, mem_zpowers a⟩ : zpowers a) ^ (k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
 rfl
 
+lemma orbit_zpowers_equiv_symm_apply' (k : ℤ) :
+  (orbit_zpowers_equiv a b).symm k =
+    (⟨a, mem_zpowers a⟩ : zpowers a) ^ k • ⟨b, mem_orbit_self b⟩ :=
+begin
+  rw [orbit_zpowers_equiv_symm_apply, zmod.coe_int_cast],
+  exact subtype.ext (zpow_smul_mod_minimal_period _ _ k),
+end
+
+lemma _root_.add_action.orbit_zmultiples_equiv_symm_apply'
+  {α β : Type*} [add_group α] (a : α) [add_action α β] (b : β) (k : ℤ) :
+  (add_action.orbit_zmultiples_equiv a b).symm k =
+    (k • (⟨a, mem_zmultiples a⟩ : zmultiples a)) +ᵥ ⟨b, add_action.mem_orbit_self b⟩ :=
+begin
+  rw [add_action.orbit_zmultiples_equiv_symm_apply, zmod.coe_int_cast],
+  exact subtype.ext (zsmul_vadd_mod_minimal_period _ _ k),
+end
+
+attribute [to_additive orbit_zmultiples_equiv_symm_apply'] orbit_zpowers_equiv_symm_apply'
+
 @[to_additive] lemma minimal_period_eq_card [fintype (orbit (zpowers a) b)] :
   minimal_period ((•) a) b = fintype.card (orbit (zpowers a) b) :=
 by rw [←fintype.of_equiv_card (orbit_zpowers_equiv a b), zmod.card]

src/dynamics/periodic_pts.lean

@@ -403,4 +403,16 @@ begin
         dvd_neg, int.coe_nat_dvd, pow_smul_eq_iff_minimal_period_dvd] },
 end
 
+variables (a b)
+
+@[simp, to_additive] lemma pow_smul_mod_minimal_period (n : ℕ) :
+  a ^ (n % function.minimal_period ((•) a) b) • b = a ^ n • b :=
+by conv_rhs { rw [← nat.mod_add_div n (minimal_period ((•) a) b), pow_add, mul_smul,
+    pow_smul_eq_iff_minimal_period_dvd.mpr (dvd_mul_right _ _)] }
+
+@[simp, to_additive] lemma zpow_smul_mod_minimal_period (n : ℤ) :
+  a ^ (n % (function.minimal_period ((•) a) b : ℤ)) • b = a ^ n • b :=
+by conv_rhs { rw [← int.mod_add_div n (minimal_period ((•) a) b), zpow_add, mul_smul,
+    zpow_smul_eq_iff_minimal_period_dvd.mpr (dvd_mul_right _ _)] }
+
 end mul_action