Function.Semiconj.symm_adjoint
theorem Function.Semiconj.symm_adjoint :
∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {fa : α ≃o α} {fb : β ↪o β}
{g : α → β},
Function.Semiconj g ⇑fa ⇑fb → ∀ {g' : β → α}, IsOrderRightAdjoint g g' → Function.Semiconj g' ⇑fb ⇑fa
The theorem states that given an order automorphism `fa` on a type `α` and an order embedding `fb` on a type `β`, if `fa` semiconjugates to `fb` via a function `g` (i.e., the composition of `g` after `fa` equals to the composition of `fb` after `g`), and if there exists a function `g'` which is an order right adjoint of `g` (meaning it maps each `y` to a least upper bound for the set `{x | f x ≤ y}`), then `fb` semiconjugates to `fa` via `g'`. This theorem is a variant of Proposition 2.1 from Étienne Ghys's work on groups of circle homeomorphisms and bounded cohomology.
More concisely: If an order automorphism semiconjugates to an order embedding via a function with an order right adjoint, then the order embedding semiconjugates to the order automorphism via the order right adjoint function.
|
Function.sSup_div_semiconj
theorem Function.sSup_div_semiconj :
∀ {α : Type u_1} {G : Type u_4} [inst : CompleteLattice α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α) (g : G),
Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
This theorem states that, given two actions `f₁` and `f₂` of a group `G` on a complete lattice `α` through order isomorphisms, the function that maps each element `x` to the supremum over all `g'` in `G` of the inverse of `f₁ g'` applied to `f₂ g' x` semiconjugates each `f₁ g'` to `f₂ g'`. In other words, if we perform `f₁ g'` then the new function, and then undo `f₂ g'`, we get the same result as if we'd just performed `f₂ g'` in the first place. This is a version of Proposition 5.4 from Étienne Ghys's paper "Groupes d'homéomorphismes du cercle et cohomologie bornée".
More concisely: Given group actions `f₁` and `f₂` of a group `G` on a complete lattice `α` through order isomorphisms, the function that maps each `x` to the supremum over all `g'` in `G` of the inverse of `f₁ g'` applied to `f₂ g' x` semiconjugates each `f₁ g'` to `f₂ g'`, i.e., `f₁ g' ∘ f₂ g' = f₂ g' ∘ (supₗ (inv ∘ f₁) g' ∘ f₂ g')` for all `x` in `α`.
|
Function.csSup_div_semiconj
theorem Function.csSup_div_semiconj :
∀ {α : Type u_1} {G : Type u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Group G] (f₁ f₂ : G →* α ≃o α),
(∀ (x : α), BddAbove (Set.range fun g => (f₁ g)⁻¹ ((f₂ g) x))) →
∀ (g : G), Function.Semiconj (fun x => ⨆ g', (f₁ g')⁻¹ ((f₂ g') x)) ⇑(f₂ g) ⇑(f₁ g)
Consider two actions `f₁` and `f₂` of a group `G` on a conditionally complete lattice `α` by order isomorphisms. Suppose that for each element `x` in `α`, the set `s(x)` consisting of elements of the form `(f₁ g)⁻¹ (f₂ g) x` for `g` in `G` is bounded above. Then the theorem states that the function mapping each `x` to the supremum of `s(x)` semiconjugates each `f₁ g'` to `f₂ g'`.
This theorem is a version of Proposition 5.4 from Étienne Ghys' work, "Groupes d'homéomorphismes du cercle et cohomologie bornée". In mathematical terms, if we have two actions of a group on a lattice by order isomorphisms and each set of the form `(f₁ g)⁻¹ (f₂ g) x` for all `x` in the lattice is upper bounded, then the supremum function semiconjugates each `f₁ g'` to `f₂ g'`.
More concisely: Given two group actions by order isomorphisms on a conditionally complete lattice, if the set of inverses of the compositions is upper bounded for each lattice element, then the function mapping each element to its supremum in this set semiconjugates the actions.
|