English
An order isomorphism f: α ≃o γ and g: β ≃o δ induces an order isomorphism between the function prosets (α →o β) and (γ →o δ) by conjugation: p ↦ g ∘ p ∘ f^{-1}.
Русский
Однообразие порядка между проулю-объектами порождается конгруацией функций: p ↦ g ∘ p ∘ f^{-1}.
LaTeX
$$$\text{arrowCongr}(f,g) : (\alpha \to_o \beta) \simeq_o (\gamma \to_o \delta),\quad (\text{toFun})(p) = g \circ p \circ f^{-1}$$$
Lean4
/-- An order isomorphism between the domains and codomains of two prosets of
order homomorphisms gives an order isomorphism between the two function prosets. -/
@[simps apply symm_apply]
def arrowCongr {α β γ δ} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α ≃o γ) (g : β ≃o δ) :
(α →o β) ≃o (γ →o δ) where
toFun p := .comp g <| .comp p f.symm
invFun p := .comp g.symm <| .comp p f
left_inv
p :=
DFunLike.coe_injective <| by
change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p
simp only [← OrderIso.coe_trans, Function.id_comp, OrderIso.self_trans_symm, OrderIso.coe_refl, Function.comp_id]
right_inv
p :=
DFunLike.coe_injective <| by
change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
simp only [← OrderIso.coe_trans, Function.id_comp, OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]
map_rel_iff'
{p
q} :=
by
simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe, OrderHomClass.coe_coe, Function.comp_apply,
map_le_map_iff]
exact Iff.symm f.forall_congr_left
