mathlib3 documentation

order.hom.bounded

Bounded order homomorphisms #

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

This file defines (bounded) order homomorphisms.

We use the fun_like design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

Typeclasses #

source
structure top_hom (α : Type u_6) (β : Type u_7) [has_top α] [has_top β] :
Type (max u_6 u_7)

The type of ⊤-preserving functions from α to β.

Instances for top_hom
source
structure bot_hom (α : Type u_6) (β : Type u_7) [has_bot α] [has_bot β] :
Type (max u_6 u_7)

The type of ⊥-preserving functions from α to β.

Instances for bot_hom
source
structure bounded_order_hom (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] [bounded_order α] [bounded_order β] :
Type (max u_6 u_7)

The type of bounded order homomorphisms from α to β.

Instances for bounded_order_hom
source
@[class]
structure top_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_top α] [has_top β] :
Type (max u_6 u_7 u_8)

top_hom_class F α β states that F is a type of ⊤-preserving morphisms.

You should extend this class when you extend top_hom.

Instances of this typeclass
Instances of other typeclasses for top_hom_class
  • top_hom_class.has_sizeof_inst
source
@[instance]
def top_hom_class.to_fun_like (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_top α] [has_top β] [self : top_hom_class F α β] :
fun_like F α (λ (_x : α), β)
source
@[class]
structure bot_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_bot α] [has_bot β] :
Type (max u_6 u_7 u_8)

bot_hom_class F α β states that F is a type of ⊥-preserving morphisms.

You should extend this class when you extend bot_hom.

Instances of this typeclass
Instances of other typeclasses for bot_hom_class
  • bot_hom_class.has_sizeof_inst
source
@[instance]
def bot_hom_class.to_fun_like (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_bot α] [has_bot β] [self : bot_hom_class F α β] :
fun_like F α (λ (_x : α), β)
source
@[class]
structure bounded_order_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_le α] [has_le β] [bounded_order α] [bounded_order β] :
Type (max u_6 u_7 u_8)

bounded_order_hom_class F α β states that F is a type of bounded order morphisms.

You should extend this class when you extend bounded_order_hom.

Instances of this typeclass
Instances of other typeclasses for bounded_order_hom_class
  • bounded_order_hom_class.has_sizeof_inst
source
@[instance]
def bounded_order_hom_class.to_rel_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [has_le α] [has_le β] [bounded_order α] [bounded_order β] [self : bounded_order_hom_class F α β] :
rel_hom_class F has_le.le has_le.le
source
@[protected, instance]
def bounded_order_hom_class.to_top_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [bounded_order α] [bounded_order β] [bounded_order_hom_class F α β] :
top_hom_class F α β
Equations
source
@[protected, instance]
def bounded_order_hom_class.to_bot_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [has_le β] [bounded_order α] [bounded_order β] [bounded_order_hom_class F α β] :
bot_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_top_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [partial_order β] [order_top β] [order_iso_class F α β] :
top_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_bot_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [partial_order β] [order_bot β] [order_iso_class F α β] :
bot_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_bounded_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [bounded_order α] [partial_order β] [bounded_order β] [order_iso_class F α β] :
bounded_order_hom_class F α β
Equations
source
@[simp]
theorem map_eq_top_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [partial_order β] [order_top β] [order_iso_class F α β] (f : F) {a : α} :
⇑f a = ⊤ ↔ a = ⊤
source
@[simp]
theorem map_eq_bot_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [partial_order β] [order_bot β] [order_iso_class F α β] (f : F) {a : α} :
⇑f a = ⊥ ↔ a = ⊥
source
@[protected, instance]
def top_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] [top_hom_class F α β] :
has_coe_t F (top_hom α β)
Equations
source
@[protected, instance]
def bot_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] [bot_hom_class F α β] :
has_coe_t F (bot_hom α β)
Equations
source
@[protected, instance]
def bounded_order_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] [bounded_order_hom_class F α β] :
has_coe_t F (bounded_order_hom α β)
Equations

Top homomorphisms #

source
@[protected, instance]
def top_hom.top_hom_class {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] :
top_hom_class (top_hom α β) α β
Equations
source
@[protected, instance]
def top_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] :
has_coe_to_fun (top_hom α β) (λ (_x : top_hom α β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[simp]
theorem top_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] {f : top_hom α β} :
f.to_fun = ⇑f
source
@[ext]
theorem top_hom.ext {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] {f g : top_hom α β} (h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
source
@[protected]
def top_hom.copy {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] (f : top_hom α β) (f' : α → β) (h : f' = ⇑f) :
top_hom α β

Copy of a top_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[simp]
theorem top_hom.coe_copy {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] (f : top_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem top_hom.copy_eq {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] (f : top_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected, instance]
def top_hom.inhabited {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] :
inhabited (top_hom α β)
Equations
source
@[protected]
def top_hom.id (α : Type u_2) [has_top α] :
top_hom α α

id as a top_hom.

Equations
source
@[simp]
theorem top_hom.coe_id (α : Type u_2) [has_top α] :
⇑(top_hom.id α) = id
source
@[simp]
theorem top_hom.id_apply {α : Type u_2} [has_top α] (a : α) :
⇑(top_hom.id α) a = a
source
def top_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_top α] [has_top β] [has_top γ] (f : top_hom β γ) (g : top_hom α β) :
top_hom α γ

Composition of top_homs as a top_hom.

Equations
source
@[simp]
theorem top_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_top α] [has_top β] [has_top γ] (f : top_hom β γ) (g : top_hom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem top_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_top α] [has_top β] [has_top γ] (f : top_hom β γ) (g : top_hom α β) (a : α) :
⇑(f.comp g) a = ⇑f (⇑g a)
source
@[simp]
theorem top_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [has_top α] [has_top β] [has_top γ] [has_top δ] (f : top_hom γ δ) (g : top_hom β γ) (h : top_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem top_hom.comp_id {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] (f : top_hom α β) :
f.comp (top_hom.id α) = f
source
@[simp]
theorem top_hom.id_comp {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] (f : top_hom α β) :
(top_hom.id β).comp f = f
source
theorem top_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_top α] [has_top β] [has_top γ] {g₁ g₂ : top_hom β γ} {f : top_hom α β} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
theorem top_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_top α] [has_top β] [has_top γ] {g : top_hom β γ} {f₁ f₂ : top_hom α β} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
@[protected, instance]
def top_hom.preorder {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [has_top β] :
preorder (top_hom α β)
Equations
source
@[protected, instance]
def top_hom.partial_order {α : Type u_2} {β : Type u_3} [has_top α] [partial_order β] [has_top β] :
partial_order (top_hom α β)
Equations
source
@[protected, instance]
def top_hom.order_top {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] :
order_top (top_hom α β)
Equations
source
@[simp]
theorem top_hom.coe_top {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] :
⇑⊤ = ⊤
source
@[simp]
theorem top_hom.top_apply {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] (a : α) :
⇑⊤ a = ⊤
source
@[protected, instance]
def top_hom.has_inf {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] :
has_inf (top_hom α β)
Equations
source
@[protected, instance]
def top_hom.semilattice_inf {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] :
semilattice_inf (top_hom α β)
Equations
source
@[simp]
theorem top_hom.coe_inf {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] (f g : top_hom α β) :
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
source
@[simp]
theorem top_hom.inf_apply {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] (f g : top_hom α β) (a : α) :
⇑(f ⊓ g) a = ⇑f a ⊓ ⇑g a
source
@[protected, instance]
def top_hom.has_sup {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] :
has_sup (top_hom α β)
Equations
source
@[protected, instance]
def top_hom.semilattice_sup {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] :
semilattice_sup (top_hom α β)
Equations
source
@[simp]
theorem top_hom.coe_sup {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] (f g : top_hom α β) :
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
source
@[simp]
theorem top_hom.sup_apply {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] (f g : top_hom α β) (a : α) :
⇑(f ⊔ g) a = ⇑f a ⊔ ⇑g a
source
@[protected, instance]
def top_hom.lattice {α : Type u_2} {β : Type u_3} [has_top α] [lattice β] [order_top β] :
lattice (top_hom α β)
Equations
source
@[protected, instance]
def top_hom.distrib_lattice {α : Type u_2} {β : Type u_3} [has_top α] [distrib_lattice β] [order_top β] :
distrib_lattice (top_hom α β)
Equations

Bot homomorphisms #

source
@[protected, instance]
def bot_hom.bot_hom_class {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] :
bot_hom_class (bot_hom α β) α β
Equations
source
@[protected, instance]
def bot_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] :
has_coe_to_fun (bot_hom α β) (λ (_x : bot_hom α β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[simp]
theorem bot_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] {f : bot_hom α β} :
f.to_fun = ⇑f
source
@[ext]
theorem bot_hom.ext {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] {f g : bot_hom α β} (h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
source
@[protected]
def bot_hom.copy {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] (f : bot_hom α β) (f' : α → β) (h : f' = ⇑f) :
bot_hom α β

Copy of a bot_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[simp]
theorem bot_hom.coe_copy {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] (f : bot_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem bot_hom.copy_eq {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] (f : bot_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected, instance]
def bot_hom.inhabited {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] :
inhabited (bot_hom α β)
Equations
source
@[protected]
def bot_hom.id (α : Type u_2) [has_bot α] :
bot_hom α α

id as a bot_hom.

Equations
source
@[simp]
theorem bot_hom.coe_id (α : Type u_2) [has_bot α] :
⇑(bot_hom.id α) = id
source
@[simp]
theorem bot_hom.id_apply {α : Type u_2} [has_bot α] (a : α) :
⇑(bot_hom.id α) a = a
source
def bot_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_bot α] [has_bot β] [has_bot γ] (f : bot_hom β γ) (g : bot_hom α β) :
bot_hom α γ

Composition of bot_homs as a bot_hom.

Equations
source
@[simp]
theorem bot_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_bot α] [has_bot β] [has_bot γ] (f : bot_hom β γ) (g : bot_hom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem bot_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_bot α] [has_bot β] [has_bot γ] (f : bot_hom β γ) (g : bot_hom α β) (a : α) :
⇑(f.comp g) a = ⇑f (⇑g a)
source
@[simp]
theorem bot_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [has_bot α] [has_bot β] [has_bot γ] [has_bot δ] (f : bot_hom γ δ) (g : bot_hom β γ) (h : bot_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem bot_hom.comp_id {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] (f : bot_hom α β) :
f.comp (bot_hom.id α) = f
source
@[simp]
theorem bot_hom.id_comp {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] (f : bot_hom α β) :
(bot_hom.id β).comp f = f
source
theorem bot_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_bot α] [has_bot β] [has_bot γ] {g₁ g₂ : bot_hom β γ} {f : bot_hom α β} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
theorem bot_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_bot α] [has_bot β] [has_bot γ] {g : bot_hom β γ} {f₁ f₂ : bot_hom α β} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
@[protected, instance]
def bot_hom.preorder {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [has_bot β] :
preorder (bot_hom α β)
Equations
source
@[protected, instance]
def bot_hom.partial_order {α : Type u_2} {β : Type u_3} [has_bot α] [partial_order β] [has_bot β] :
partial_order (bot_hom α β)
Equations
source
@[protected, instance]
def bot_hom.order_bot {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] :
order_bot (bot_hom α β)
Equations
source
@[simp]
theorem bot_hom.coe_bot {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] :
⇑⊥ = ⊥
source
@[simp]
theorem bot_hom.bot_apply {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] (a : α) :
⇑⊥ a = ⊥
source
@[protected, instance]
def bot_hom.has_inf {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] :
has_inf (bot_hom α β)
Equations
source
@[protected, instance]
def bot_hom.semilattice_inf {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] :
semilattice_inf (bot_hom α β)
Equations
source
@[simp]
theorem bot_hom.coe_inf {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] (f g : bot_hom α β) :
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
source
@[simp]
theorem bot_hom.inf_apply {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] (f g : bot_hom α β) (a : α) :
⇑(f ⊓ g) a = ⇑f a ⊓ ⇑g a
source
@[protected, instance]
def bot_hom.has_sup {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] :
has_sup (bot_hom α β)
Equations
source
@[protected, instance]
def bot_hom.semilattice_sup {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] :
semilattice_sup (bot_hom α β)
Equations
source
@[simp]
theorem bot_hom.coe_sup {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] (f g : bot_hom α β) :
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
source
@[simp]
theorem bot_hom.sup_apply {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] (f g : bot_hom α β) (a : α) :
⇑(f ⊔ g) a = ⇑f a ⊔ ⇑g a
source
@[protected, instance]
def bot_hom.lattice {α : Type u_2} {β : Type u_3} [has_bot α] [lattice β] [order_bot β] :
lattice (bot_hom α β)
Equations
source
@[protected, instance]
def bot_hom.distrib_lattice {α : Type u_2} {β : Type u_3} [has_bot α] [distrib_lattice β] [order_bot β] :
distrib_lattice (bot_hom α β)
Equations

Bounded order homomorphisms #

source
def bounded_order_hom.to_top_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
top_hom α β

Reinterpret a bounded_order_hom as a top_hom.

Equations
source
def bounded_order_hom.to_bot_hom {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
bot_hom α β

Reinterpret a bounded_order_hom as a bot_hom.

Equations
source
@[protected, instance]
def bounded_order_hom.bounded_order_hom_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] :
bounded_order_hom_class (bounded_order_hom α β) α β
Equations
source
@[protected, instance]
def bounded_order_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] :
has_coe_to_fun (bounded_order_hom α β) (λ (_x : bounded_order_hom α β), α → β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[simp]
theorem bounded_order_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] {f : bounded_order_hom α β} :
f.to_order_hom.to_fun = ⇑f
source
@[ext]
theorem bounded_order_hom.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] {f g : bounded_order_hom α β} (h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
source
@[protected]
def bounded_order_hom.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) (f' : α → β) (h : f' = ⇑f) :
bounded_order_hom α β

Copy of a bounded_order_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
source
@[simp]
theorem bounded_order_hom.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem bounded_order_hom.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def bounded_order_hom.id (α : Type u_2) [preorder α] [bounded_order α] :
bounded_order_hom α α

id as a bounded_order_hom.

Equations
source
@[protected, instance]
def bounded_order_hom.inhabited (α : Type u_2) [preorder α] [bounded_order α] :
inhabited (bounded_order_hom α α)
Equations
source
@[simp]
theorem bounded_order_hom.coe_id (α : Type u_2) [preorder α] [bounded_order α] :
⇑(bounded_order_hom.id α) = id
source
@[simp]
theorem bounded_order_hom.id_apply {α : Type u_2} [preorder α] [bounded_order α] (a : α) :
⇑(bounded_order_hom.id α) a = a
source
def bounded_order_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) :
bounded_order_hom α γ

Composition of bounded_order_homs as a bounded_order_hom.

Equations
source
@[simp]
theorem bounded_order_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem bounded_order_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) (a : α) :
⇑(f.comp g) a = ⇑f (⇑g a)
source
@[simp]
theorem bounded_order_hom.coe_comp_order_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) :
↑(f.comp g) = ↑f.comp ↑g
source
@[simp]
theorem bounded_order_hom.coe_comp_top_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) :
↑(f.comp g) = ↑f.comp ↑g
source
@[simp]
theorem bounded_order_hom.coe_comp_bot_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_order_hom β γ) (g : bounded_order_hom α β) :
↑(f.comp g) = ↑f.comp ↑g
source
@[simp]
theorem bounded_order_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] [bounded_order α] [bounded_order β] [bounded_order γ] [bounded_order δ] (f : bounded_order_hom γ δ) (g : bounded_order_hom β γ) (h : bounded_order_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem bounded_order_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
f.comp (bounded_order_hom.id α) = f
source
@[simp]
theorem bounded_order_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
(bounded_order_hom.id β).comp f = f
source
theorem bounded_order_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g₁ g₂ : bounded_order_hom β γ} {f : bounded_order_hom α β} (hf : function.surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
theorem bounded_order_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g : bounded_order_hom β γ} {f₁ f₂ : bounded_order_hom α β} (hg : function.injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Dual homs #

source
@[simp]
theorem top_hom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [has_le β] [order_top β] (f : bot_hom αᵒᵈ βᵒᵈ) (ᾰ : αᵒᵈ) :
⇑(⇑(top_hom.dual.symm) f) ᾰ = ⇑f ᾰ
source
@[protected]
def top_hom.dual {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [has_le β] [order_top β] :
top_hom α β ≃ bot_hom αᵒᵈ βᵒᵈ

Reinterpret a top homomorphism as a bot homomorphism between the dual lattices.

Equations
source
@[simp]
theorem top_hom.dual_apply_apply {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [has_le β] [order_top β] (f : top_hom α β) (ᾰ : α) :
⇑(⇑top_hom.dual f) ᾰ = ⇑f ᾰ
source
@[simp]
theorem top_hom.dual_id {α : Type u_2} [has_le α] [order_top α] :
⇑top_hom.dual (top_hom.id α) = bot_hom.id αᵒᵈ
source
@[simp]
theorem top_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [order_top α] [has_le β] [order_top β] [has_le γ] [order_top γ] (g : top_hom β γ) (f : top_hom α β) :
⇑top_hom.dual (g.comp f) = (⇑top_hom.dual g).comp (⇑top_hom.dual f)
source
@[simp]
theorem top_hom.symm_dual_id {α : Type u_2} [has_le α] [order_top α] :
⇑(top_hom.dual.symm) (bot_hom.id αᵒᵈ) = top_hom.id α
source
@[simp]
theorem top_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [order_top α] [has_le β] [order_top β] [has_le γ] [order_top γ] (g : bot_hom βᵒᵈ γᵒᵈ) (f : bot_hom αᵒᵈ βᵒᵈ) :
⇑(top_hom.dual.symm) (g.comp f) = (⇑(top_hom.dual.symm) g).comp (⇑(top_hom.dual.symm) f)
source
@[simp]
theorem bot_hom.dual_apply_apply {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [has_le β] [order_bot β] (f : bot_hom α β) (ᾰ : α) :
⇑(⇑bot_hom.dual f) ᾰ = ⇑f ᾰ
source
@[simp]
theorem bot_hom.dual_symm_apply_apply {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [has_le β] [order_bot β] (f : top_hom αᵒᵈ βᵒᵈ) (ᾰ : αᵒᵈ) :
⇑(⇑(bot_hom.dual.symm) f) ᾰ = ⇑f ᾰ
source
@[protected]
def bot_hom.dual {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [has_le β] [order_bot β] :
bot_hom α β ≃ top_hom αᵒᵈ βᵒᵈ

Reinterpret a bot homomorphism as a top homomorphism between the dual lattices.

Equations
source
@[simp]
theorem bot_hom.dual_id {α : Type u_2} [has_le α] [order_bot α] :
⇑bot_hom.dual (bot_hom.id α) = top_hom.id αᵒᵈ
source
@[simp]
theorem bot_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [order_bot α] [has_le β] [order_bot β] [has_le γ] [order_bot γ] (g : bot_hom β γ) (f : bot_hom α β) :
⇑bot_hom.dual (g.comp f) = (⇑bot_hom.dual g).comp (⇑bot_hom.dual f)
source
@[simp]
theorem bot_hom.symm_dual_id {α : Type u_2} [has_le α] [order_bot α] :
⇑(bot_hom.dual.symm) (top_hom.id αᵒᵈ) = bot_hom.id α
source
@[simp]
theorem bot_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_le α] [order_bot α] [has_le β] [order_bot β] [has_le γ] [order_bot γ] (g : top_hom βᵒᵈ γᵒᵈ) (f : top_hom αᵒᵈ βᵒᵈ) :
⇑(bot_hom.dual.symm) (g.comp f) = (⇑(bot_hom.dual.symm) g).comp (⇑(bot_hom.dual.symm) f)
source
@[simp]
theorem bounded_order_hom.dual_apply_to_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [bounded_order α] [preorder β] [bounded_order β] (f : bounded_order_hom α β) :
(⇑bounded_order_hom.dual f).to_order_hom = ⇑order_hom.dual f.to_order_hom
source
@[protected]
def bounded_order_hom.dual {α : Type u_2} {β : Type u_3} [preorder α] [bounded_order α] [preorder β] [bounded_order β] :
bounded_order_hom α β ≃ bounded_order_hom αᵒᵈ βᵒᵈ

Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.

Equations
source
@[simp]
theorem bounded_order_hom.dual_symm_apply_to_order_hom {α : Type u_2} {β : Type u_3} [preorder α] [bounded_order α] [preorder β] [bounded_order β] (f : bounded_order_hom αᵒᵈ βᵒᵈ) :
(⇑(bounded_order_hom.dual.symm) f).to_order_hom = ⇑(order_hom.dual.symm) f.to_order_hom
source
@[simp]
theorem bounded_order_hom.dual_id {α : Type u_2} [preorder α] [bounded_order α] :
⇑bounded_order_hom.dual (bounded_order_hom.id α) = bounded_order_hom.id αᵒᵈ
source
@[simp]
theorem bounded_order_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [bounded_order α] [preorder β] [bounded_order β] [preorder γ] [bounded_order γ] (g : bounded_order_hom β γ) (f : bounded_order_hom α β) :
⇑bounded_order_hom.dual (g.comp f) = (⇑bounded_order_hom.dual g).comp (⇑bounded_order_hom.dual f)
source
@[simp]
theorem bounded_order_hom.symm_dual_id {α : Type u_2} [preorder α] [bounded_order α] :
⇑(bounded_order_hom.dual.symm) (bounded_order_hom.id αᵒᵈ) = bounded_order_hom.id α
source
@[simp]
theorem bounded_order_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [bounded_order α] [preorder β] [bounded_order β] [preorder γ] [bounded_order γ] (g : bounded_order_hom βᵒᵈ γᵒᵈ) (f : bounded_order_hom αᵒᵈ βᵒᵈ) :
⇑(bounded_order_hom.dual.symm) (g.comp f) = (⇑(bounded_order_hom.dual.symm) g).comp (⇑(bounded_order_hom.dual.symm) f)