English
Consider two actions f1, f2 : G →* α ≃o α of a group on a complete lattice α by order isomorphisms. Then the map h(x) = ⨆ g'∈G (f1 g')⁻¹ (f2 g' x) semiconjugates each f1 g' to f2 g'.
Русский
Рассмотрим две дествия f1, f2 : G →* α ≃o α группы на полной решётке α. Тогда отображение h(x) = ⨆ g'∈G (f1 g')⁻¹ (f2 g' x) полусопрязывает каждое f1 g' с f2 g'.
LaTeX
$$$h(x) = \bigvee_{g' \in G} (f_1 g')^{-1} (f_2 g' x) \quad \Rightarrow \quad \text{Semiconj } h \ (f_2 g) (f_1 g)$$$
Lean4
/-- Consider two actions `f₁ f₂ : G → α → α` of a group on a complete lattice by order
isomorphisms. Then the map `x ↦ ⨆ g : G, (f₁ g)⁻¹ (f₂ g 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 sSup_div_semiconj [CompleteLattice α] [Group G] (f₁ f₂ : G →* α ≃o α) (g : G) :
Function.Semiconj (fun x => ⨆ g' : G, (f₁ g')⁻¹ (f₂ g' x)) (f₂ g) (f₁ g) :=
semiconj_of_isLUB f₁ f₂ (fun _ => isLUB_iSup) _
