English
Let α be a conditionally complete lattice and G a group. For two actions f1, f2 : G →* α ≃o α, define h(x) = ⨆ g'∈G (f1 g')⁻¹ (f2 g' x). Then h semiconjugates each f1 g' to f2 g'.
Русский
Пусть α — условно совершенная решётка, G — группа. Для двух действий f1, f2: G →* α ≃o α задаём h(x) = ⨆ g'∈G (f1 g')⁻¹ (f2 g' x). Тогда h полусопрязывает каждое f1 g' к f2 g'.
LaTeX
$$$h(x) = \bigvee_{g' \in G} (f_1 g')^{-1} (f_2 g' x) \implies \text{Semiconj } h \ (f_2 g) (f_1 g)$$$
Lean4
/-- Consider two actions `f₁ f₂ : G → α → α` of a group on a conditionally complete lattice by order
isomorphisms. Suppose that each set $s(x)=\{f_1(g)^{-1} (f_2(g)(x)) | g \in G\}$ is bounded above.
Then the map `x ↦ sSup s(x)` semiconjugates each `f₁ g'` to `f₂ g'`.
This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes]. -/
theorem csSup_div_semiconj [ConditionallyCompleteLattice α] [Group G] (f₁ f₂ : G →* α ≃o α)
(hbdd : ∀ x, BddAbove (range fun g => (f₁ g)⁻¹ (f₂ g x))) (g : G) :
Function.Semiconj (fun x => ⨆ g' : G, (f₁ g')⁻¹ (f₂ g' x)) (f₂ g) (f₁ g) :=
semiconj_of_isLUB f₁ f₂ (fun x => isLUB_csSup (range_nonempty _) (hbdd x)) _
