feat(Dynamics/Flow): define semiconjugacy, factor and orbit (leanprover-community#28000)

We add definitions relating to flows.

This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.

Co-authored-by: figud <40865765+figud@users.noreply.github.com>

Author: daefigueroa

Mathlib/CategoryTheory/Galois/Examples.lean

@@ -120,7 +120,7 @@ theorem Action.pretransitive_of_isConnected (X : Action FintypeCat G)
     have : IsIso i := by
       apply IsConnected.noTrivialComponent T' i
       apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
-      exact Set.Nonempty.coe_sort (MulAction.orbit_nonempty x)
+      exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)
     have hb : Function.Bijective i.hom := by
       apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
       exact map_isIso (forget₂ _ FintypeCat) i

Mathlib/Data/ZMod/QuotientGroup.lean

@@ -139,7 +139,7 @@ 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
+    haveI : Nonempty (orbit (zpowers a) b) := (nonempty_orbit b).to_subtype
     rw [minimalPeriod_eq_card]
     exact Fintype.card_ne_zero⟩
 

Mathlib/Dynamics/Flow.lean

@@ -6,6 +6,7 @@ Authors: Jean Lo
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.Topology.Algebra.Group.Defs
+import Mathlib.Algebra.Order.Monoid.Submonoid
 
 /-!
 # Flows and invariant sets
@@ -22,9 +23,9 @@ if `ϕₜ s ⊆ s` for all `t`. In many cases `ϕ` will be a flow on
 commutative) monoid, we additionally define forward invariance, where
 `t` ranges over those elements which are nonnegative.
 
-Additionally, we define such constructions as the restriction of a
-flow onto an invariant subset, and the time-reversal of a flow by a
-group.
+Additionally, we define such constructions as the (forward) orbit, a
+semiconjugacy between flows, a factor of a flow, the restriction of a
+flow onto an invariant subset, and the time-reversal of a flow by a group.
 -/
 
 
@@ -47,24 +48,35 @@ theorem isInvariant_iff_image : IsInvariant ϕ s ↔ ∀ t, ϕ t '' s ⊆ s := b
   simp_rw [IsInvariant, mapsTo_iff_image_subset]
 
 /-- A set `s ⊆ α` is forward-invariant under `ϕ : τ → α → α` if `ϕ t s ⊆ s` for all `t ≥ 0`. -/
-def IsFwInvariant [Preorder τ] [Zero τ] (ϕ : τ → α → α) (s : Set α) : Prop :=
+def IsForwardInvariant [Preorder τ] [Zero τ] (ϕ : τ → α → α) (s : Set α) : Prop :=
   ∀ ⦃t⦄, 0 ≤ t → MapsTo (ϕ t) s s
 
-theorem IsInvariant.isFwInvariant [Preorder τ] [Zero τ] {ϕ : τ → α → α} {s : Set α}
-    (h : IsInvariant ϕ s) : IsFwInvariant ϕ s := fun t _ht => h t
+@[deprecated (since := "2025-09-25")] alias IsFwInvariant := IsForwardInvariant
+
+theorem IsInvariant.isForwardInvariant [Preorder τ] [Zero τ] {ϕ : τ → α → α} {s : Set α}
+    (h : IsInvariant ϕ s) : IsForwardInvariant ϕ s := fun t _ht => h t
+
+@[deprecated (since := "2025-09-25")]
+alias IsInvariant.isFwInvariant := IsInvariant.isForwardInvariant
 
 /-- If `τ` is a `CanonicallyOrderedAdd` monoid (e.g., `ℕ` or `ℝ≥0`), then the notions
-`IsFwInvariant` and `IsInvariant` are equivalent. -/
-theorem IsFwInvariant.isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ]
+`IsForwardInvariant` and `IsInvariant` are equivalent. -/
+theorem IsForwardInvariant.isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ]
     {ϕ : τ → α → α} {s : Set α}
-    (h : IsFwInvariant ϕ s) : IsInvariant ϕ s := fun t => h (zero_le t)
+    (h : IsForwardInvariant ϕ s) : IsInvariant ϕ s := fun t => h (zero_le t)
+
+@[deprecated (since := "2025-09-25")]
+alias IsFwInvariant.isInvariant := IsForwardInvariant.isInvariant
 
 /-- If `τ` is a `CanonicallyOrderedAdd` monoid (e.g., `ℕ` or `ℝ≥0`), then the notions
-`IsFwInvariant` and `IsInvariant` are equivalent. -/
-theorem isFwInvariant_iff_isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ]
+`IsForwardInvariant` and `IsInvariant` are equivalent. -/
+theorem isForwardInvariant_iff_isInvariant [AddMonoid τ] [PartialOrder τ] [CanonicallyOrderedAdd τ]
     {ϕ : τ → α → α} {s : Set α} :
-    IsFwInvariant ϕ s ↔ IsInvariant ϕ s :=
-  ⟨IsFwInvariant.isInvariant, IsInvariant.isFwInvariant⟩
+    IsForwardInvariant ϕ s ↔ IsInvariant ϕ s :=
+  ⟨IsForwardInvariant.isInvariant, IsInvariant.isForwardInvariant⟩
+
+@[deprecated (since := "2025-09-25")]
+alias isFwInvariant_iff_isInvariant := isForwardInvariant_iff_isInvariant
 
 end Invariant
 
@@ -131,6 +143,109 @@ def restrict {s : Set α} (h : IsInvariant ϕ s) : Flow τ (↥s) where
   map_add' _ _ _ := Subtype.ext (map_add _ _ _ _)
   map_zero' _ := Subtype.ext (map_zero_apply _ _)
 
+@[simp]
+theorem coe_restrict_apply {s : Set α} (h : IsInvariant ϕ s) (t : τ) (x : s) :
+    restrict ϕ h t x = ϕ t x := rfl
+
+/-- Convert a flow to an additive monoid action. -/
+def toAddAction : AddAction τ α where
+  vadd      := ϕ
+  add_vadd  := ϕ.map_add'
+  zero_vadd := ϕ.map_zero'
+
+/-- Restrict a flow by `τ` to a flow by an additive submonoid of `τ`. -/
+def restrictAddSubmonoid (S : AddSubmonoid τ) : Flow S α where
+  toFun t x := ϕ t x
+  cont' := ϕ.continuous (continuous_subtype_val.comp continuous_fst) continuous_snd
+  map_add' t₁ t₂ x := ϕ.map_add' t₁ t₂ x
+  map_zero' := ϕ.map_zero'
+
+theorem restrictAddSubmonoid_apply (S : AddSubmonoid τ) (t : S) (x : α) :
+    restrictAddSubmonoid ϕ S t x = ϕ t x := rfl
+
+section Orbit
+
+/-- The orbit of a point under a flow. -/
+def orbit (x : α) : Set α := ϕ.toAddAction.orbit _ x
+
+theorem orbit_eq_range (x : α) : orbit ϕ x = Set.range (fun t => ϕ t x) := rfl
+
+theorem mem_orbit_iff {x₁ x₂ : α} : x₂ ∈ orbit ϕ x₁ ↔ ∃ t : τ, ϕ t x₁ = x₂ :=
+  ϕ.toAddAction.mem_orbit_iff
+
+theorem mem_orbit (x : α) (t : τ) : ϕ t x ∈ orbit ϕ x := ϕ.toAddAction.mem_orbit ..
+
+theorem mem_orbit_self (x : α) : x ∈ orbit ϕ x := ϕ.toAddAction.mem_orbit_self x
+
+theorem nonempty_orbit (x : α) : Set.Nonempty (orbit ϕ x) := ϕ.toAddAction.nonempty_orbit x
+
+theorem mem_orbit_of_mem_orbit {x₁ x₂ : α} (t : τ) (h : x₂ ∈ orbit ϕ x₁) : ϕ t x₂ ∈ orbit ϕ x₁ :=
+  ϕ.toAddAction.mem_orbit_of_mem_orbit t h
+
+/-- The orbit of a point under a flow `ϕ` is invariant under `ϕ`. -/
+theorem isInvariant_orbit (x : α) : IsInvariant ϕ (orbit ϕ x) :=
+  fun t _ => ϕ.toAddAction.mem_orbit_of_mem_orbit t
+
+theorem orbit_restrict (s : Set α) (hs : IsInvariant ϕ s) (x : s) :
+    orbit (ϕ.restrict hs) x = Subtype.val ⁻¹' orbit ϕ x :=
+  Set.ext (fun x => by simp [orbit_eq_range, Subtype.ext_iff])
+
+variable [Preorder τ] [AddLeftMono τ]
+
+/-- Restrict a flow by `τ` to a flow by the additive submonoid of nonnegative elements of `τ`. -/
+def restrictNonneg : Flow (AddSubmonoid.nonneg τ) α := ϕ.restrictAddSubmonoid (.nonneg τ)
+
+/-- The forward orbit of a point under a flow. -/
+def forwardOrbit (x : α) : Set α := orbit ϕ.restrictNonneg x
+
+theorem forwardOrbit_eq_range_nonneg (x : α) :
+    forwardOrbit ϕ x = Set.range (fun t : {t : τ // 0 ≤ t} => ϕ t x) := rfl
+
+/-- The forward orbit of a point under a flow `ϕ` is forward-invariant under `ϕ`. -/
+theorem isForwardInvariant_forwardOrbit (x : α) : IsForwardInvariant ϕ (forwardOrbit ϕ x) :=
+  fun t h => IsInvariant.isForwardInvariant (isInvariant_orbit ϕ.restrictNonneg x) (t := ⟨t, h⟩) h
+
+/-- The forward orbit of a point `x` is contained in the orbit of `x`. -/
+theorem forwardOrbit_subset_orbit (x : α) : forwardOrbit ϕ x ⊆ orbit ϕ x :=
+  ϕ.toAddAction.orbit_addSubmonoid_subset (AddSubmonoid.nonneg τ) x
+
+theorem mem_orbit_of_mem_forwardOrbit {x₁ x₂ : α} (h : x₁ ∈ forwardOrbit ϕ x₂) : x₁ ∈ orbit ϕ x₂ :=
+  ϕ.forwardOrbit_subset_orbit x₂ h
+
+end Orbit
+
+variable {β γ : Type*} [TopologicalSpace β] [TopologicalSpace γ] (ψ : Flow τ β) (χ : Flow τ γ)
+
+/-- Given flows `ϕ` by `τ` on `α` and `ψ` by `τ` on `β`, a function `π : α → β` is called a
+*semiconjugacy* from `ϕ` to `ψ` if `π` is continuous and surjective, and `π ∘ (ϕ t) = (ψ t) ∘ π` for
+all `t : τ`. -/
+structure IsSemiconjugacy (π : α → β) (ϕ : Flow τ α) (ψ : Flow τ β) : Prop where
+  cont : Continuous π
+  surj : Function.Surjective π
+  semiconj : ∀ t, Function.Semiconj π (ϕ t) (ψ t)
+
+/-- The composition of semiconjugacies is a semiconjugacy. -/
+theorem IsSemiconjugacy.comp {π : α → β} {ρ : β → γ}
+    (h₁ : IsSemiconjugacy π ϕ ψ) (h₂ : IsSemiconjugacy ρ ψ χ) : IsSemiconjugacy (ρ ∘ π) ϕ χ :=
+  ⟨h₂.cont.comp h₁.cont, h₂.surj.comp h₁.surj, fun t => (h₂.semiconj t).comp_left (h₁.semiconj t)⟩
+
+/-- The identity is a semiconjugacy from `ϕ` to `ψ` if and only if `ϕ` and `ψ` are equal. -/
+theorem isSemiconjugacy_id_iff_eq (ϕ ψ : Flow τ α) : IsSemiconjugacy id ϕ ψ ↔ ϕ = ψ :=
+  ⟨fun h => ext h.semiconj, fun h => h.recOn ⟨continuous_id, surjective_id, fun _ => .id_left⟩⟩
+
+/-- A flow `ψ` is called a *factor* of `ϕ` if there exists a semiconjugacy from `ϕ` to `ψ`. -/
+def IsFactorOf (ψ : Flow τ β) (ϕ : Flow τ α) : Prop := ∃ π : α → β, IsSemiconjugacy π ϕ ψ
+
+theorem IsSemiconjugacy.isFactorOf {π : α → β} (h : IsSemiconjugacy π ϕ ψ) : IsFactorOf ψ ϕ :=
+  ⟨π, h⟩
+
+/-- Transitivity of factors of flows. -/
+theorem IsFactorOf.trans (h₁ : IsFactorOf ϕ ψ) (h₂ : IsFactorOf ψ χ) : IsFactorOf ϕ χ :=
+  h₁.elim fun π hπ => h₂.elim fun ρ hρ => ⟨π ∘ ρ, hρ.comp χ ψ ϕ hπ⟩
+
+/-- Every flow is a factor of itself. -/
+theorem IsFactorOf.self : IsFactorOf ϕ ϕ := ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr (by rfl)⟩
+
 end Flow
 
 namespace Flow

Mathlib/Dynamics/Minimal.lean

@@ -100,4 +100,4 @@ theorem isMinimal_iff_isClosed_smul_invariant [ContinuousConstSMul M α] :
     exact eq_empty_or_univ_of_smul_invariant_closed M
   refine fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ ?_ ?_).resolve_left ?_⟩
   exacts [isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _,
-    (orbit_nonempty _).closure.ne_empty]
+    (nonempty_orbit _).closure.ne_empty]

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -87,7 +87,7 @@ theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
     a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by
   simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff,
     Fintype.card_le_one_iff_subsingleton, Nat.add_one_le_iff, Fintype.card_pos_iff,
-    Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, orbit_nonempty, implies_true]
+    Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, nonempty_orbit, implies_true]
 
 @[to_additive instDecidablePredMemSetFixedByAddOfDecidableEq]
 instance (m : M) [DecidableEq β] :

Mathlib/GroupTheory/GroupAction/Blocks.lean

@@ -78,7 +78,7 @@ theorem IsPartition.of_orbits :
   · intro x
     exact ⟨_, ⟨x, rfl⟩, mem_orbit_self x⟩
   · rintro ⟨a, ha : orbit G a = ∅⟩
-    exact (MulAction.orbit_nonempty a).ne_empty ha
+    exact (MulAction.nonempty_orbit a).ne_empty ha
 
 end orbits
 

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -65,9 +65,11 @@ theorem mem_orbit_self (a : α) : a ∈ orbit M a :=
   ⟨1, by simp⟩
 
 @[to_additive]
-theorem orbit_nonempty (a : α) : Set.Nonempty (orbit M a) :=
+theorem nonempty_orbit (a : α) : Set.Nonempty (orbit M a) :=
   Set.range_nonempty _
 
+@[deprecated (since := "2025-09-25")] alias orbit_nonempty := nonempty_orbit
+
 @[to_additive]
 theorem mapsTo_smul_orbit (m : M) (a : α) : Set.MapsTo (m • ·) (orbit M a) (orbit M a) :=
   Set.range_subset_iff.2 fun m' => ⟨m * m', mul_smul _ _ _⟩
@@ -388,10 +390,13 @@ lemma orbitRel.quotient_eq_of_quotient_subgroup_eq' {H : Subgroup G} {a b : α}
   orbitRel.quotient_eq_of_quotient_subgroup_eq h
 
 @[to_additive]
-nonrec lemma orbitRel.Quotient.orbit_nonempty (x : orbitRel.Quotient G α) :
+nonrec lemma orbitRel.Quotient.nonempty_orbit (x : orbitRel.Quotient G α) :
     Set.Nonempty x.orbit := by
   rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
-  exact orbit_nonempty _
+  exact nonempty_orbit _
+
+@[deprecated (since := "2025-09-25")]
+alias orbitRel.Quotient.orbit_nonempty := orbitRel.Quotient.nonempty_orbit
 
 @[to_additive]
 nonrec lemma orbitRel.Quotient.mapsTo_smul_orbit (g : G) (x : orbitRel.Quotient G α) :