Fixed points of a self-map

We prove some simple lemmas about IsFixedPt and ∘, iterate, and Semiconj.

Tags

fixed point

theorem Function.IsFixedPt.comp {α : Type u_1} {f g : α → α} {x : α} (hf : IsFixedPt f x) (hg : IsFixedPt g x) : IsFixedPt (f ∘ g) x

If x is a fixed point of f and g, then it is a fixed point of f ∘ g.

theorem Function.IsFixedPt.iterate {α : Type u_1} {f : α → α} {x : α} (hf : IsFixedPt f x) (n : ℕ) : IsFixedPt f^[n] x

If x is a fixed point of f, then it is a fixed point of f^[n].

theorem Function.IsFixedPt.left_of_comp {α : Type u_1} {f g : α → α} {x : α} (hfg : IsFixedPt (f ∘ g) x) (hg : IsFixedPt g x) : IsFixedPt f x

If x is a fixed point of f ∘ g and g, then it is a fixed point of f.

theorem Function.IsFixedPt.to_leftInverse {α : Type u_1} {f g : α → α} {x : α} (hf : IsFixedPt f x) (h : LeftInverse g f) : IsFixedPt g x

If x is a fixed point of f and g is a left inverse of f, then x is a fixed point of g.

theorem Function.IsFixedPt.map {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) : IsFixedPt fb (g x)

If g (semi)conjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

theorem Function.IsFixedPt.apply {α : Type u_1} {f : α → α} {x : α} (hx : IsFixedPt f x) : IsFixedPt f (f x)

theorem Function.IsFixedPt.preimage_iterate {α : Type u_1} {f : α → α} {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) : IsFixedPt (Set.preimage f^[n]) s

theorem Function.IsFixedPt.image_iterate {α : Type u_1} {f : α → α} {s : Set α} (h : IsFixedPt (Set.image f) s) (n : ℕ) : IsFixedPt (Set.image f^[n]) s

theorem Function.IsFixedPt.equiv_symm {α : Type u_1} {x : α} {e : Equiv.Perm α} (h : IsFixedPt (⇑e) x) : IsFixedPt (⇑(Equiv.symm e)) x

theorem Function.IsFixedPt.perm_inv {α : Type u_1} {x : α} {e : Equiv.Perm α} (h : IsFixedPt (⇑e) x) : IsFixedPt (⇑e⁻¹) x

theorem Function.IsFixedPt.perm_pow {α : Type u_1} {x : α} {e : Equiv.Perm α} (h : IsFixedPt (⇑e) x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x

theorem Function.IsFixedPt.perm_zpow {α : Type u_1} {x : α} {e : Equiv.Perm α} (h : IsFixedPt (⇑e) x) (n : ℤ) : IsFixedPt (⇑(e ^ n)) x

@[simp]

theorem Function.Injective.isFixedPt_apply_iff {α : Type u_1} {f : α → α} (hf : Injective f) {x : α} : IsFixedPt f (f x) ↔ IsFixedPt f x

theorem Function.Semiconj.mapsTo_fixedPoints {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β} (h : Semiconj g fa fb) : Set.MapsTo g (fixedPoints fa) (fixedPoints fb)

If g semiconjugates fa to fb, then it sends fixed points of fa to fixed points of fb.

theorem Function.invOn_fixedPoints_comp {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (g ∘ f))

Any two maps f : α → β and g : β → α are inverse of each other on the sets of fixed points of f ∘ g and g ∘ f, respectively.

theorem Function.mapsTo_fixedPoints_comp {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Set.MapsTo f (fixedPoints (g ∘ f)) (fixedPoints (f ∘ g))

Any map f sends fixed points of g ∘ f to fixed points of f ∘ g.

theorem Function.bijOn_fixedPoints_comp {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) : Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (g ∘ f))

Given two maps f : α → β and g : β → α, g is a bijective map between the fixed points of f ∘ g and the fixed points of g ∘ f. The inverse map is f, see invOn_fixedPoints_comp.

theorem Function.Commute.invOn_fixedPoints_comp {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

If self-maps f and g commute, then they are inverse of each other on the set of fixed points of f ∘ g. This is a particular case of Function.invOn_fixedPoints_comp.

theorem Function.Commute.left_bijOn_fixedPoints_comp {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

If self-maps f and g commute, then f is bijective on the set of fixed points of f ∘ g. This is a particular case of Function.bijOn_fixedPoints_comp.

theorem Function.Commute.right_bijOn_fixedPoints_comp {α : Type u_1} {f g : α → α} (h : Function.Commute f g) : Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

If self-maps f and g commute, then g is bijective on the set of fixed points of f ∘ g. This is a particular case of Function.bijOn_fixedPoints_comp.