Skip to content

Commit 893f77f

Browse files
winstonyinwinstonyin
committed
feat: port Dynamics.Basic (#1120)
1 parent e4f636e commit 893f77f

File tree

4 files changed

+213
-5
lines changed

4 files changed

+213
-5
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -267,6 +267,7 @@ import Mathlib.Data.UInt
267267
import Mathlib.Data.ULift
268268
import Mathlib.Data.UnionFind
269269
import Mathlib.Data.Vector
270+
import Mathlib.Dynamics.Basic
270271
import Mathlib.GroupTheory.EckmannHilton
271272
import Mathlib.GroupTheory.GroupAction.Defs
272273
import Mathlib.GroupTheory.GroupAction.Option

‎Mathlib/Dynamics/Basic.lean‎

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
/-
2+
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yury Kudryashov
5+
6+
! This file was ported from Lean 3 source module dynamics.fixed_points.basic
7+
! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Data.Set.Function
12+
import Mathlib.Logic.Function.Iterate
13+
import Mathlib.GroupTheory.Perm.Basic
14+
15+
/-!
16+
# Fixed points of a self-map
17+
18+
In this file we define
19+
20+
* the predicate `IsFixedPt f x := f x = x`;
21+
* the set `fixedPoints f` of fixed points of a self-map `f`.
22+
23+
We also prove some simple lemmas about `IsFixedPt` and `∘`, `iterate`, and `semiconj`.
24+
25+
## Tags
26+
27+
fixed point
28+
-/
29+
30+
31+
open Equiv
32+
33+
universe u v
34+
35+
variable {α : Type u} {β : Type v} {f fa g : α → α} {x y : α} {fb : β → β} {m n k : ℕ} {e : Perm α}
36+
37+
namespace Function
38+
39+
/-- A point `x` is a fixed point of `f : α → α` if `f x = x`. -/
40+
def IsFixedPt (f : α → α) (x : α) :=
41+
f x = x
42+
#align function.is_fixed_pt Function.IsFixedPt
43+
44+
/-- Every point is a fixed point of `id`. -/
45+
theorem isFixedPt_id (x : α) : IsFixedPt id x :=
46+
(rfl : _)
47+
#align function.is_fixed_pt_id Function.isFixedPt_id
48+
49+
namespace IsFixedPt
50+
51+
instance instDecidable [h : DecidableEq α] {f : α → α} {x : α} : Decidable (IsFixedPt f x) :=
52+
h (f x) x
53+
54+
/-- If `x` is a fixed point of `f`, then `f x = x`. This is useful, e.g., for `rw` or `simp`.-/
55+
protected theorem eq (hf : IsFixedPt f x) : f x = x :=
56+
hf
57+
#align function.is_fixed_pt.eq Function.IsFixedPt.eq
58+
59+
/-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`. -/
60+
protected theorem comp (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x :=
61+
calc
62+
f (g x) = f x := congr_arg f hg
63+
_ = x := hf
64+
65+
#align function.is_fixed_pt.comp Function.IsFixedPt.comp
66+
67+
/-- If `x` is a fixed point of `f`, then it is a fixed point of `f^[n]`. -/
68+
protected theorem iterate (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt (f^[n]) x :=
69+
iterate_fixed hf n
70+
#align function.is_fixed_pt.iterate Function.IsFixedPt.iterate
71+
72+
/-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`. -/
73+
theorem left_of_comp (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x :=
74+
calc
75+
f x = f (g x) := congr_arg f hg.symm
76+
_ = x := hfg
77+
78+
#align function.is_fixed_pt.left_of_comp Function.IsFixedPt.left_of_comp
79+
80+
/-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
81+
point of `g`. -/
82+
theorem to_leftInverse (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x :=
83+
calc
84+
g x = g (f x) := congr_arg g hf.symm
85+
_ = x := h x
86+
87+
#align function.is_fixed_pt.to_left_inverse Function.IsFixedPt.to_leftInverse
88+
89+
/-- If `g` (semi)conjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
90+
of `fb`. -/
91+
protected theorem map {x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) :
92+
IsFixedPt fb (g x) :=
93+
calc
94+
fb (g x) = g (fa x) := (h.eq x).symm
95+
_ = g x := congr_arg g hx
96+
97+
#align function.is_fixed_pt.map Function.IsFixedPt.map
98+
99+
protected theorem apply {x : α} (hx : IsFixedPt f x) : IsFixedPt f (f x) := by convert hx
100+
#align function.is_fixed_pt.apply Function.IsFixedPt.apply
101+
102+
theorem preimage_iterate {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) :
103+
IsFixedPt (Set.preimage (f^[n])) s := by
104+
rw [Set.preimage_iterate_eq]
105+
exact h.iterate n
106+
#align function.is_fixed_pt.preimage_iterate Function.IsFixedPt.preimage_iterate
107+
108+
protected theorem equiv_symm (h : IsFixedPt e x) : IsFixedPt e.symm x :=
109+
h.to_leftInverse e.leftInverse_symm
110+
#align function.is_fixed_pt.equiv_symm Function.IsFixedPt.equiv_symm
111+
112+
protected theorem perm_inv (h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x :=
113+
h.equiv_symm
114+
#align function.is_fixed_pt.perm_inv Function.IsFixedPt.perm_inv
115+
116+
protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x := by
117+
rw [← Equiv.Perm.iterate_eq_pow]
118+
exact h.iterate _
119+
#align function.is_fixed_pt.perm_pow Function.IsFixedPt.perm_pow
120+
121+
protected theorem perm_zpow (h : IsFixedPt e x) : ∀ n : ℤ, IsFixedPt (⇑(e ^ n)) x
122+
| Int.ofNat _ => h.perm_pow _
123+
| Int.negSucc n => (h.perm_pow <| n + 1).perm_inv
124+
#align function.is_fixed_pt.perm_zpow Function.IsFixedPt.perm_zpow
125+
126+
end IsFixedPt
127+
128+
@[simp]
129+
theorem Injective.isFixedPt_apply_iff (hf : Injective f) {x : α} :
130+
IsFixedPt f (f x) ↔ IsFixedPt f x :=
131+
⟨fun h => hf h.eq, IsFixedPt.apply⟩
132+
#align function.injective.is_fixed_pt_apply_iff Function.Injective.isFixedPt_apply_iff
133+
134+
/-- The set of fixed points of a map `f : α → α`. -/
135+
def fixedPoints (f : α → α) : Set α :=
136+
{ x : α | IsFixedPt f x }
137+
#align function.fixed_points Function.fixedPoints
138+
139+
instance fixedPoints.instDecidable [DecidableEq α] (f : α → α) (x : α) :
140+
Decidable (x ∈ fixedPoints f) :=
141+
IsFixedPt.instDecidable
142+
#align function.fixed_points.decidable Function.fixedPoints.instDecidable
143+
144+
@[simp]
145+
theorem mem_fixedPoints : x ∈ fixedPoints f ↔ IsFixedPt f x :=
146+
Iff.rfl
147+
#align function.mem_fixed_points Function.mem_fixedPoints
148+
149+
theorem mem_fixedPoints_iff {α : Type _} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x := by
150+
rfl
151+
#align function.mem_fixed_points_iff Function.mem_fixedPoints_iff
152+
153+
@[simp]
154+
theorem fixedPoints_id : fixedPoints (@id α) = Set.univ :=
155+
Set.ext fun _ => by simpa using isFixedPt_id _
156+
#align function.fixed_points_id Function.fixedPoints_id
157+
158+
theorem fixedPoints_subset_range : fixedPoints f ⊆ Set.range f := fun x hx => ⟨x, hx⟩
159+
#align function.fixed_points_subset_range Function.fixedPoints_subset_range
160+
161+
/-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
162+
of `fb`. -/
163+
theorem Semiconj.maps_to_fixedPoints {g : α → β} (h : Semiconj g fa fb) :
164+
Set.MapsTo g (fixedPoints fa) (fixedPoints fb) := fun _ hx => hx.map h
165+
#align function.semiconj.maps_to_fixed_pts Function.Semiconj.maps_to_fixedPoints
166+
167+
/-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
168+
of `f ∘ g` and `g ∘ f`, respectively. -/
169+
theorem invOn_fixedPoints_comp (f : α → β) (g : β → α) :
170+
Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
171+
⟨fun _ => id, fun _ => id⟩
172+
#align function.inv_on_fixed_pts_comp Function.invOn_fixedPoints_comp
173+
174+
/-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`. -/
175+
theorem maps_to_fixedPoints_comp (f : α → β) (g : β → α) :
176+
Set.MapsTo f (fixedPoints <| g ∘ f) (fixedPoints <| f ∘ g) := fun _ hx => hx.map fun _ => rfl
177+
#align function.maps_to_fixed_pts_comp Function.maps_to_fixedPoints_comp
178+
179+
/-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
180+
of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `invOn_fixedPoints_comp`. -/
181+
theorem bijOn_fixedPoints_comp (f : α → β) (g : β → α) :
182+
Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
183+
(invOn_fixedPoints_comp f g).bijOn (maps_to_fixedPoints_comp g f) (maps_to_fixedPoints_comp f g)
184+
#align function.bij_on_fixed_pts_comp Function.bijOn_fixedPoints_comp
185+
186+
/-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points
187+
of `f ∘ g`. This is a particular case of `function.invOn_fixedPoints_comp`. -/
188+
theorem Commute.invOn_fixedPoints_comp (h : Commute f g) :
189+
Set.InvOn f g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
190+
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g
191+
#align function.commute.inv_on_fixed_pts_comp Function.Commute.invOn_fixedPoints_comp
192+
193+
/-- If self-maps `f` and `g` commute, then `f` is bijective on the set of fixed points of `f ∘ g`.
194+
This is a particular case of `function.bijOn_fixedPoints_comp`. -/
195+
theorem Commute.left_bijOn_fixedPoints_comp (h : Commute f g) :
196+
Set.BijOn f (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
197+
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f
198+
#align function.commute.left_bij_on_fixed_pts_comp Function.Commute.left_bijOn_fixedPoints_comp
199+
200+
/-- If self-maps `f` and `g` commute, then `g` is bijective on the set of fixed points of `f ∘ g`.
201+
This is a particular case of `function.bijOn_fixedPoints_comp`. -/
202+
theorem Commute.right_bijOn_fixedPoints_comp (h : Commute f g) :
203+
Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g) := by
204+
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g
205+
#align function.commute.right_bij_on_fixed_pts_comp Function.Commute.right_bijOn_fixedPoints_comp
206+
207+
end Function

‎Mathlib/Logic/Equiv/Defs.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -293,9 +293,9 @@ theorem eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :
293293
theorem trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
294294
(ab.trans bc).trans cd = ab.trans (bc.trans cd) := Equiv.ext fun _ => rfl
295295

296-
theorem left_inverse_symm (f : Equiv α β) : LeftInverse f.symm f := f.left_inv
296+
theorem leftInverse_symm (f : Equiv α β) : LeftInverse f.symm f := f.left_inv
297297

298-
theorem right_inverse_symm (f : Equiv α β) : Function.RightInverse f.symm f := f.right_inv
298+
theorem rightInverse_symm (f : Equiv α β) : Function.RightInverse f.symm f := f.right_inv
299299

300300
theorem injective_comp (e : α ≃ β) (f : β → γ) : Injective (f ∘ e) ↔ Injective f :=
301301
EquivLike.injective_comp e f

‎Mathlib/Logic/Equiv/Set.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ protected theorem subset_image' {α β} (e : α ≃ β) (s : Set α) (t : Set β
7777

7878
@[simp]
7979
theorem symm_image_image {α β} (e : α ≃ β) (s : Set α) : e.symm '' (e '' s) = s :=
80-
e.left_inverse_symm.image_image s
80+
e.leftInverse_symm.image_image s
8181
#align equiv.symm_image_image Equiv.symm_image_image
8282

8383
theorem eq_image_iff_symm_image_eq {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
@@ -106,12 +106,12 @@ protected theorem image_compl {α β} (f : Equiv α β) (s : Set α) : f '' sᶜ
106106

107107
@[simp]
108108
theorem symm_preimage_preimage {α β} (e : α ≃ β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s :=
109-
e.right_inverse_symm.preimage_preimage s
109+
e.rightInverse_symm.preimage_preimage s
110110
#align equiv.symm_preimage_preimage Equiv.symm_preimage_preimage
111111

112112
@[simp]
113113
theorem preimage_symm_preimage {α β} (e : α ≃ β) (s : Set α) : e ⁻¹' (e.symm ⁻¹' s) = s :=
114-
e.left_inverse_symm.preimage_preimage s
114+
e.leftInverse_symm.preimage_preimage s
115115
#align equiv.preimage_symm_preimage Equiv.preimage_symm_preimage
116116

117117
@[simp]

0 commit comments

Comments
 (0)