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 #

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
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
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
@[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
@[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 : α), β)
@[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
@[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 : α), β)
@[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
@[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 α β] :
Equations
@[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 α β] :
Equations
@[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 α β] :
Equations
@[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 α β] :
Equations
@[protected, instance]
Equations
@[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 =
@[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 =
@[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
@[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
@[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 α β] :
Equations

Top homomorphisms #

@[protected, instance]
def top_hom.top_hom_class {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] :
top_hom_class (top_hom α β) α β
Equations
@[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
@[simp]
theorem top_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] {f : top_hom α β} :
@[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
@[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
@[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'
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
@[protected, instance]
def top_hom.inhabited {α : Type u_2} {β : Type u_3} [has_top α] [has_top β] :
Equations
@[protected]
def top_hom.id (α : Type u_2) [has_top α] :
top_hom α α

id as a top_hom.

Equations
@[simp]
theorem top_hom.coe_id (α : Type u_2) [has_top α] :
@[simp]
theorem top_hom.id_apply {α : Type u_2} [has_top α] (a : α) :
(top_hom.id α) a = a
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
@[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
@[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)
@[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)
@[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
@[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
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₂
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₂
@[protected, instance]
def top_hom.preorder {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [has_top β] :
Equations
@[protected, instance]
def top_hom.partial_order {α : Type u_2} {β : Type u_3} [has_top α] [partial_order β] [has_top β] :
Equations
@[protected, instance]
def top_hom.order_top {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] :
Equations
@[simp]
theorem top_hom.coe_top {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] :
@[simp]
theorem top_hom.top_apply {α : Type u_2} {β : Type u_3} [has_top α] [preorder β] [order_top β] (a : α) :
@[protected, instance]
def top_hom.has_inf {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] :
Equations
@[protected, instance]
def top_hom.semilattice_inf {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_inf β] [order_top β] :
Equations
@[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
@[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
@[protected, instance]
def top_hom.has_sup {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] :
Equations
@[protected, instance]
def top_hom.semilattice_sup {α : Type u_2} {β : Type u_3} [has_top α] [semilattice_sup β] [order_top β] :
Equations
@[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
@[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
@[protected, instance]
def top_hom.lattice {α : Type u_2} {β : Type u_3} [has_top α] [lattice β] [order_top β] :
Equations
@[protected, instance]
def top_hom.distrib_lattice {α : Type u_2} {β : Type u_3} [has_top α] [distrib_lattice β] [order_top β] :
Equations

Bot homomorphisms #

@[protected, instance]
def bot_hom.bot_hom_class {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] :
bot_hom_class (bot_hom α β) α β
Equations
@[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
@[simp]
theorem bot_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] {f : bot_hom α β} :
@[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
@[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
@[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'
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
@[protected, instance]
def bot_hom.inhabited {α : Type u_2} {β : Type u_3} [has_bot α] [has_bot β] :
Equations
@[protected]
def bot_hom.id (α : Type u_2) [has_bot α] :
bot_hom α α

id as a bot_hom.

Equations
@[simp]
theorem bot_hom.coe_id (α : Type u_2) [has_bot α] :
@[simp]
theorem bot_hom.id_apply {α : Type u_2} [has_bot α] (a : α) :
(bot_hom.id α) a = a
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
@[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
@[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)
@[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)
@[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
@[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
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₂
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₂
@[protected, instance]
def bot_hom.preorder {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [has_bot β] :
Equations
@[protected, instance]
def bot_hom.partial_order {α : Type u_2} {β : Type u_3} [has_bot α] [partial_order β] [has_bot β] :
Equations
@[protected, instance]
def bot_hom.order_bot {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] :
Equations
@[simp]
theorem bot_hom.coe_bot {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] :
@[simp]
theorem bot_hom.bot_apply {α : Type u_2} {β : Type u_3} [has_bot α] [preorder β] [order_bot β] (a : α) :
@[protected, instance]
def bot_hom.has_inf {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] :
Equations
@[protected, instance]
def bot_hom.semilattice_inf {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_inf β] [order_bot β] :
Equations
@[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
@[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
@[protected, instance]
def bot_hom.has_sup {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] :
Equations
@[protected, instance]
def bot_hom.semilattice_sup {α : Type u_2} {β : Type u_3} [has_bot α] [semilattice_sup β] [order_bot β] :
Equations
@[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
@[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
@[protected, instance]
def bot_hom.lattice {α : Type u_2} {β : Type u_3} [has_bot α] [lattice β] [order_bot β] :
Equations
@[protected, instance]
def bot_hom.distrib_lattice {α : Type u_2} {β : Type u_3} [has_bot α] [distrib_lattice β] [order_bot β] :
Equations

Bounded order homomorphisms #

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
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
@[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
@[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 α β} :
@[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
@[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) :

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

Equations
@[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'
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
@[protected, instance]
Equations
@[simp]
@[simp]
theorem bounded_order_hom.id_apply {α : Type u_2} [preorder α] [bounded_order α] (a : α) :
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 α β) :

Composition of bounded_order_homs as a bounded_order_hom.

Equations
@[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
@[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)
@[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
@[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
@[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
@[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)
@[simp]
theorem bounded_order_hom.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
@[simp]
theorem bounded_order_hom.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [bounded_order α] [bounded_order β] (f : bounded_order_hom α β) :
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₂
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 #

@[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 ᾰ
@[protected]
def top_hom.dual {α : Type u_2} {β : Type u_3} [has_le α] [order_top α] [has_le β] [order_top β] :

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

Equations
@[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 ᾰ
@[simp]
@[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 α β) :
@[simp]
@[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 αᵒᵈ βᵒᵈ) :
@[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 ᾰ
@[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 ᾰ
@[protected]
def bot_hom.dual {α : Type u_2} {β : Type u_3} [has_le α] [order_bot α] [has_le β] [order_bot β] :

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

Equations
@[simp]
@[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 α β) :
@[simp]
@[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 αᵒᵈ βᵒᵈ) :
@[protected]

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

Equations