English
Let α be a poset, β a preorder, fa an order automorphism of α, fb an order embedding of β, and g: α → β. If g semiconjugates fa to fb and g′ is an order right adjoint of g, then fb semiconjugates to fa via g′.
Русский
Пусть α — частично упорядоченное множество, β — предпроследование, fa — упорядоченный автоморфизм α, fb — вложение β в β, и g: α → β. Если g полусопряжает fa к fb и g′ является правым сопряжённым к g, тогда fb полусопряжает fa через g′.
LaTeX
$$$\\forall \\alpha, \\beta, (\\le_\\alpha) \\text{ частично упорядочено}, (\\le_\\beta) \\text{ preorder}, fa: \\alpha \\to \\alpha, fb: \\beta \\to \\beta, g: \\alpha \\to \\beta, g': \\beta \\to \\alpha, \\\\ g \\circ fa = fb \\circ g \\implies g' \\circ fb = fa \\circ g'$$$
Lean4
/-- If an order automorphism `fa` is semiconjugate to an order embedding `fb` by a function `g`
and `g'` is an order right adjoint of `g` (i.e. `g' y = sSup {x | f x ≤ y}`), then `fb` is
semiconjugate to `fa` by `g'`.
This is a version of Proposition 2.1 from [Étienne Ghys, Groupes d'homéomorphismes du cercle et
cohomologie bornée][ghys87:groupes]. -/
theorem symm_adjoint [PartialOrder α] [Preorder β] {fa : α ≃o α} {fb : β ↪o β} {g : α → β}
(h : Function.Semiconj g fa fb) {g' : β → α} (hg' : IsOrderRightAdjoint g g') : Function.Semiconj g' fb fa :=
by
refine fun y => (hg' _).unique ?_
rw [← fa.surjective.image_preimage {x | g x ≤ fb y}, preimage_setOf_eq]
simp only [h.eq, fb.le_iff_le, fa.leftOrdContinuous (hg' _)]
