mathlib3 documentation

order.semiconj_Sup

Semiconjugate by Sup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove two facts about semiconjugate (families of) functions.

First, if an order isomorphism fa : α → α is semiconjugate to an order embedding fb : β → β by g : α → β, then fb is semiconjugate to fa by y ↦ Sup {x | g x ≤ y}, see semiconj.symm_adjoint.

Second, 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', see function.Sup_div_semiconj. In the case of a conditionally complete lattice, a similar statement holds true under an additional assumption that each set {(f₁ g)⁻¹ (f₂ g x) | g : G} is bounded above, see function.cSup_div_semiconj.

The lemmas come from Étienne Ghys, Groupes d'homeomorphismes du cercle et cohomologie bornee, Proposition 2.1 and 5.4 respectively. In the paper they are formulated for homeomorphisms of the circle, so in order to apply results from this file one has to lift these homeomorphisms to the real line first.

source
def is_order_right_adjoint {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α → β) (g : β → α) :
Prop

We say that g : β → α is an order right adjoint function for f : α → β if it sends each y to a least upper bound for {x | f x ≤ y}. If α is a partial order, and f : α → β has a right adjoint, then this right adjoint is unique.

Equations
source
theorem is_order_right_adjoint_Sup {α : Type u_1} {β : Type u_2} [complete_lattice α] [preorder β] (f : α → β) :
is_order_right_adjoint f (λ (y : β), has_Sup.Sup {x : α | f x ≤ y})
source
theorem is_order_right_adjoint_cSup {α : Type u_1} {β : Type u_2} [conditionally_complete_lattice α] [preorder β] (f : α → β) (hne : ∀ (y : β), ∃ (x : α), f x ≤ y) (hbdd : ∀ (y : β), bdd_above {x : α | f x ≤ y}) :
is_order_right_adjoint f (λ (y : β), has_Sup.Sup {x : α | f x ≤ y})
source
@[protected]
theorem is_order_right_adjoint.unique {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {f : α → β} {g₁ g₂ : β → α} (h₁ : is_order_right_adjoint f g₁) (h₂ : is_order_right_adjoint f g₂) :
g₁ = g₂
source
theorem is_order_right_adjoint.right_mono {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {f : α → β} {g : β → α} (h : is_order_right_adjoint f g) :
monotone g
source
theorem is_order_right_adjoint.order_iso_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {f : α → β} {g : β → α} (h : is_order_right_adjoint f g) (e : β ≃o γ) :
is_order_right_adjoint (⇑e ∘ f) (g ∘ ⇑(e.symm))
source
theorem is_order_right_adjoint.comp_order_iso {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] {f : α → β} {g : β → α} (h : is_order_right_adjoint f g) (e : γ ≃o α) :
is_order_right_adjoint (f ∘ ⇑e) (⇑(e.symm) ∘ g)
source
theorem function.semiconj.symm_adjoint {α : Type u_1} {β : Type u_2} [partial_order α] [preorder β] {fa : α ≃o α} {fb : β ↪o β} {g : α → β} (h : function.semiconj g ⇑fa ⇑fb) {g' : β → α} (hg' : is_order_right_adjoint g g') :
function.semiconj g' ⇑fb ⇑fa

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 = Sup {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'homeomorphismes du cercle et cohomologie bornee.

source
theorem function.semiconj_of_is_lub {α : Type u_1} {G : Type u_4} [partial_order α] [group G] (f₁ f₂ : G →* α ≃o α) {h : α → α} (H : ∀ (x : α), is_lub (set.range (λ (g' : G), ⇑(⇑f₁ g')⁻¹ (⇑(⇑f₂ g') x))) (h x)) (g : G) :
function.semiconj h ⇑(⇑f₂ g) ⇑(⇑f₁ g)
source
theorem function.Sup_div_semiconj {α : Type u_1} {G : Type u_4} [complete_lattice α] [group G] (f₁ f₂ : G →* α ≃o α) (g : G) :
function.semiconj (λ (x : α), ⨆ (g' : G), ⇑(⇑f₁ g')⁻¹ (⇑(⇑f₂ g') x)) ⇑(⇑f₂ g) ⇑(⇑f₁ g)

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'homeomorphismes du cercle et cohomologie bornee.

source
theorem function.cSup_div_semiconj {α : Type u_1} {G : Type u_4} [conditionally_complete_lattice α] [group G] (f₁ f₂ : G →* α ≃o α) (hbdd : ∀ (x : α), bdd_above (set.range (λ (g : G), ⇑(⇑f₁ g)⁻¹ (⇑(⇑f₂ g) x)))) (g : G) :
function.semiconj (λ (x : α), ⨆ (g' : G), ⇑(⇑f₁ g')⁻¹ (⇑(⇑f₂ g') x)) ⇑(⇑f₂ g) ⇑(⇑f₁ g)

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 ↦ Sup s(x) semiconjugates each f₁ g' to f₂ g'.

This is a version of Proposition 5.4 from Étienne Ghys, Groupes d'homeomorphismes du cercle et cohomologie bornee.