mathlib documentation

order.hom.lattice

Lattice homomorphisms #

This file defines (bounded) lattice 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 #

TODO #

Do we need more intersections between bot_hom, top_hom and lattice homomorphisms?

structure sup_hom (α : Type u_7) (β : Type u_8) [has_sup α] [has_sup β] :
Type (max u_7 u_8)

The type of -preserving functions from α to β.

Instances for sup_hom
structure inf_hom (α : Type u_7) (β : Type u_8) [has_inf α] [has_inf β] :
Type (max u_7 u_8)

The type of -preserving functions from α to β.

Instances for inf_hom
structure sup_bot_hom (α : Type u_7) (β : Type u_8) [has_sup α] [has_sup β] [has_bot α] [has_bot β] :
Type (max u_7 u_8)

The type of finitary supremum-preserving homomorphisms from α to β.

Instances for sup_bot_hom
structure inf_top_hom (α : Type u_7) (β : Type u_8) [has_inf α] [has_inf β] [has_top α] [has_top β] :
Type (max u_7 u_8)

The type of finitary infimum-preserving homomorphisms from α to β.

Instances for inf_top_hom
structure lattice_hom (α : Type u_7) (β : Type u_8) [lattice α] [lattice β] :
Type (max u_7 u_8)

The type of lattice homomorphisms from α to β.

Instances for lattice_hom
structure bounded_lattice_hom (α : Type u_7) (β : Type u_8) [lattice α] [lattice β] [bounded_order α] [bounded_order β] :
Type (max u_7 u_8)

The type of bounded lattice homomorphisms from α to β.

Instances for bounded_lattice_hom
@[class]
structure sup_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_sup α] [has_sup β] :
Type (max u_7 u_8 u_9)

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

You should extend this class when you extend sup_hom.

Instances of this typeclass
Instances of other typeclasses for sup_hom_class
  • sup_hom_class.has_sizeof_inst
@[class]
structure inf_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_inf α] [has_inf β] :
Type (max u_7 u_8 u_9)

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

You should extend this class when you extend inf_hom.

Instances of this typeclass
Instances of other typeclasses for inf_hom_class
  • inf_hom_class.has_sizeof_inst
@[class]
structure sup_bot_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_sup α] [has_sup β] [has_bot α] [has_bot β] :
Type (max u_7 u_8 u_9)

sup_bot_hom_class F α β states that F is a type of finitary supremum-preserving morphisms.

You should extend this class when you extend sup_bot_hom.

Instances of this typeclass
Instances of other typeclasses for sup_bot_hom_class
  • sup_bot_hom_class.has_sizeof_inst
@[class]
structure inf_top_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_inf α] [has_inf β] [has_top α] [has_top β] :
Type (max u_7 u_8 u_9)

inf_top_hom_class F α β states that F is a type of finitary infimum-preserving morphisms.

You should extend this class when you extend sup_bot_hom.

Instances of this typeclass
Instances of other typeclasses for inf_top_hom_class
  • inf_top_hom_class.has_sizeof_inst
@[class]
structure lattice_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [lattice α] [lattice β] :
Type (max u_7 u_8 u_9)

lattice_hom_class F α β states that F is a type of lattice morphisms.

You should extend this class when you extend lattice_hom.

Instances of this typeclass
Instances of other typeclasses for lattice_hom_class
  • lattice_hom_class.has_sizeof_inst
@[class]
structure bounded_lattice_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [lattice α] [lattice β] [bounded_order α] [bounded_order β] :
Type (max u_7 u_8 u_9)

bounded_lattice_hom_class F α β states that F is a type of bounded lattice morphisms.

You should extend this class when you extend bounded_lattice_hom.

Instances of this typeclass
Instances of other typeclasses for bounded_lattice_hom_class
  • bounded_lattice_hom_class.has_sizeof_inst
@[protected, instance]
def sup_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [sup_hom_class F α β] :
Equations
@[protected, instance]
def inf_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [inf_hom_class F α β] :
Equations
@[protected, instance]
def sup_bot_hom_class.to_bot_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] [has_bot α] [has_bot β] [sup_bot_hom_class F α β] :
Equations
@[protected, instance]
def inf_top_hom_class.to_top_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] [has_top α] [has_top β] [inf_top_hom_class F α β] :
Equations
@[protected, instance]
def lattice_hom_class.to_inf_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [lattice_hom_class F α β] :
Equations
@[protected, instance]
def order_iso_class.to_sup_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [order_iso_class F α β] :
Equations
@[protected, instance]
def order_iso_class.to_inf_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [order_iso_class F α β] :
Equations
@[protected, instance]
def order_iso_class.to_lattice_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [order_iso_class F α β] :
Equations
@[simp]
theorem map_finset_sup {F : Type u_1} {ι : Type u_2} {α : Type u_3} {β : Type u_4} [semilattice_sup α] [order_bot α] [semilattice_sup β] [order_bot β] [sup_bot_hom_class F α β] (f : F) (s : finset ι) (g : ι → α) :
f (s.sup g) = s.sup (f g)
@[simp]
theorem map_finset_inf {F : Type u_1} {ι : Type u_2} {α : Type u_3} {β : Type u_4} [semilattice_inf α] [order_top α] [semilattice_inf β] [order_top β] [inf_top_hom_class F α β] (f : F) (s : finset ι) (g : ι → α) :
f (s.inf g) = s.inf (f g)
theorem disjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] [bounded_lattice_hom_class F α β] (f : F) {a b : α} (h : disjoint a b) :
disjoint (f a) (f b)
theorem codisjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] [bounded_lattice_hom_class F α β] (f : F) {a b : α} (h : codisjoint a b) :
codisjoint (f a) (f b)
theorem is_compl.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] [bounded_lattice_hom_class F α β] (f : F) {a b : α} (h : is_compl a b) :
is_compl (f a) (f b)
theorem map_compl {F : Type u_1} {α : Type u_3} {β : Type u_4} [boolean_algebra α] [boolean_algebra β] [bounded_lattice_hom_class F α β] (f : F) (a : α) :
f a = (f a)
theorem map_sdiff {F : Type u_1} {α : Type u_3} {β : Type u_4} [boolean_algebra α] [boolean_algebra β] [bounded_lattice_hom_class F α β] (f : F) (a b : α) :
f (a \ b) = f a \ f b
theorem map_symm_diff {F : Type u_1} {α : Type u_3} {β : Type u_4} [boolean_algebra α] [boolean_algebra β] [bounded_lattice_hom_class F α β] (f : F) (a b : α) :
f (a b) = f a f b
@[protected, instance]
def sup_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] [sup_hom_class F α β] :
has_coe_t F (sup_hom α β)
Equations
@[protected, instance]
def inf_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] [inf_hom_class F α β] :
has_coe_t F (inf_hom α β)
Equations
@[protected, instance]
def sup_bot_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] [has_bot α] [has_bot β] [sup_bot_hom_class F α β] :
Equations
@[protected, instance]
def inf_top_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] [has_top α] [has_top β] [inf_top_hom_class F α β] :
Equations
@[protected, instance]
def lattice_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [lattice_hom_class F α β] :
Equations
@[protected, instance]
def bounded_lattice_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [bounded_lattice_hom_class F α β] :
Equations

Supremum homomorphisms #

@[protected, instance]
def sup_hom.sup_hom_class {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] :
sup_hom_class (sup_hom α β) α β
Equations
@[protected, instance]
def sup_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] :
has_coe_to_fun (sup_hom α β) (λ (_x : sup_hom α β), α → β)

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

Equations
@[simp]
theorem sup_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] {f : sup_hom α β} :
@[ext]
theorem sup_hom.ext {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] {f g : sup_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def sup_hom.copy {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) (f' : α → β) (h : f' = f) :
sup_hom α β

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

Equations
@[protected]
def sup_hom.id (α : Type u_3) [has_sup α] :
sup_hom α α

id as a sup_hom.

Equations
@[protected, instance]
def sup_hom.inhabited (α : Type u_3) [has_sup α] :
Equations
@[simp]
theorem sup_hom.coe_id (α : Type u_3) [has_sup α] :
@[simp]
theorem sup_hom.id_apply {α : Type u_3} [has_sup α] (a : α) :
(sup_hom.id α) a = a
def sup_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] (f : sup_hom β γ) (g : sup_hom α β) :
sup_hom α γ

Composition of sup_homs as a sup_hom.

Equations
@[simp]
theorem sup_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] (f : sup_hom β γ) (g : sup_hom α β) :
(f.comp g) = f g
@[simp]
theorem sup_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] (f : sup_hom β γ) (g : sup_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem sup_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_sup α] [has_sup β] [has_sup γ] [has_sup δ] (f : sup_hom γ δ) (g : sup_hom β γ) (h : sup_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem sup_hom.comp_id {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) :
f.comp (sup_hom.id α) = f
@[simp]
theorem sup_hom.id_comp {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) :
(sup_hom.id β).comp f = f
theorem sup_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] {g₁ g₂ : sup_hom β γ} {f : sup_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem sup_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] {g : sup_hom β γ} {f₁ f₂ : sup_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def sup_hom.const (α : Type u_3) {β : Type u_4} [has_sup α] [semilattice_sup β] (b : β) :
sup_hom α β

The constant function as a sup_hom.

Equations
@[simp]
theorem sup_hom.coe_const (α : Type u_3) {β : Type u_4} [has_sup α] [semilattice_sup β] (b : β) :
@[simp]
theorem sup_hom.const_apply (α : Type u_3) {β : Type u_4} [has_sup α] [semilattice_sup β] (b : β) (a : α) :
(sup_hom.const α b) a = b
@[protected, instance]
def sup_hom.has_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] :
Equations
@[protected, instance]
def sup_hom.semilattice_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] :
Equations
@[protected, instance]
def sup_hom.has_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] :
Equations
@[protected, instance]
def sup_hom.has_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] :
Equations
@[protected, instance]
def sup_hom.order_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [order_bot β] :
Equations
@[protected, instance]
def sup_hom.order_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [order_top β] :
Equations
@[protected, instance]
def sup_hom.bounded_order {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [bounded_order β] :
Equations
@[simp]
theorem sup_hom.coe_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] (f g : sup_hom α β) :
(f g) = f g
@[simp]
theorem sup_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] :
@[simp]
theorem sup_hom.coe_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] :
@[simp]
theorem sup_hom.sup_apply {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] (f g : sup_hom α β) (a : α) :
(f g) a = f a g a
@[simp]
theorem sup_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] (a : α) :
@[simp]
theorem sup_hom.top_apply {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] (a : α) :

Infimum homomorphisms #

@[protected, instance]
def inf_hom.inf_hom_class {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] :
inf_hom_class (inf_hom α β) α β
Equations
@[protected, instance]
def inf_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] :
has_coe_to_fun (inf_hom α β) (λ (_x : inf_hom α β), α → β)

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

Equations
@[simp]
theorem inf_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] {f : inf_hom α β} :
@[ext]
theorem inf_hom.ext {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] {f g : inf_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def inf_hom.copy {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) (f' : α → β) (h : f' = f) :
inf_hom α β

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

Equations
@[protected]
def inf_hom.id (α : Type u_3) [has_inf α] :
inf_hom α α

id as an inf_hom.

Equations
@[protected, instance]
def inf_hom.inhabited (α : Type u_3) [has_inf α] :
Equations
@[simp]
theorem inf_hom.coe_id (α : Type u_3) [has_inf α] :
@[simp]
theorem inf_hom.id_apply {α : Type u_3} [has_inf α] (a : α) :
(inf_hom.id α) a = a
def inf_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] (f : inf_hom β γ) (g : inf_hom α β) :
inf_hom α γ

Composition of inf_homs as an inf_hom.

Equations
@[simp]
theorem inf_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] (f : inf_hom β γ) (g : inf_hom α β) :
(f.comp g) = f g
@[simp]
theorem inf_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] (f : inf_hom β γ) (g : inf_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem inf_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_inf α] [has_inf β] [has_inf γ] [has_inf δ] (f : inf_hom γ δ) (g : inf_hom β γ) (h : inf_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem inf_hom.comp_id {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) :
f.comp (inf_hom.id α) = f
@[simp]
theorem inf_hom.id_comp {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) :
(inf_hom.id β).comp f = f
theorem inf_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] {g₁ g₂ : inf_hom β γ} {f : inf_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem inf_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] {g : inf_hom β γ} {f₁ f₂ : inf_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
def inf_hom.const (α : Type u_3) {β : Type u_4} [has_inf α] [semilattice_inf β] (b : β) :
inf_hom α β

The constant function as an inf_hom.

Equations
@[simp]
theorem inf_hom.coe_const (α : Type u_3) {β : Type u_4} [has_inf α] [semilattice_inf β] (b : β) :
@[simp]
theorem inf_hom.const_apply (α : Type u_3) {β : Type u_4} [has_inf α] [semilattice_inf β] (b : β) (a : α) :
(inf_hom.const α b) a = b
@[protected, instance]
def inf_hom.has_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] :
Equations
@[protected, instance]
def inf_hom.semilattice_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] :
Equations
@[protected, instance]
def inf_hom.has_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] :
Equations
@[protected, instance]
def inf_hom.has_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] :
Equations
@[protected, instance]
def inf_hom.order_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [order_bot β] :
Equations
@[protected, instance]
def inf_hom.order_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [order_top β] :
Equations
@[protected, instance]
def inf_hom.bounded_order {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [bounded_order β] :
Equations
@[simp]
theorem inf_hom.coe_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] (f g : inf_hom α β) :
(f g) = f g
@[simp]
theorem inf_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] :
@[simp]
theorem inf_hom.coe_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] :
@[simp]
theorem inf_hom.inf_apply {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] (f g : inf_hom α β) (a : α) :
(f g) a = f a g a
@[simp]
theorem inf_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] (a : α) :
@[simp]
theorem inf_hom.top_apply {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] (a : α) :

Finitary supremum homomorphisms #

def sup_bot_hom.to_bot_hom {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) :
bot_hom α β

Reinterpret a sup_bot_hom as a bot_hom.

Equations
@[protected, instance]
def sup_bot_hom.sup_bot_hom_class {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] :
Equations
@[protected, instance]
def sup_bot_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] :
has_coe_to_fun (sup_bot_hom α β) (λ (_x : sup_bot_hom α β), α → β)

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

Equations
@[simp]
theorem sup_bot_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] {f : sup_bot_hom α β} :
@[ext]
theorem sup_bot_hom.ext {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] {f g : sup_bot_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def sup_bot_hom.copy {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) (f' : α → β) (h : f' = f) :

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

Equations
@[simp]
theorem sup_bot_hom.id_to_sup_hom (α : Type u_3) [has_sup α] [has_bot α] :
@[protected]
def sup_bot_hom.id (α : Type u_3) [has_sup α] [has_bot α] :

id as a sup_bot_hom.

Equations
@[protected, instance]
def sup_bot_hom.inhabited (α : Type u_3) [has_sup α] [has_bot α] :
Equations
@[simp]
theorem sup_bot_hom.coe_id (α : Type u_3) [has_sup α] [has_bot α] :
@[simp]
theorem sup_bot_hom.id_apply {α : Type u_3} [has_sup α] [has_bot α] (a : α) :
def sup_bot_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] (f : sup_bot_hom β γ) (g : sup_bot_hom α β) :

Composition of sup_bot_homs as a sup_bot_hom.

Equations
@[simp]
theorem sup_bot_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] (f : sup_bot_hom β γ) (g : sup_bot_hom α β) :
(f.comp g) = f g
@[simp]
theorem sup_bot_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] (f : sup_bot_hom β γ) (g : sup_bot_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem sup_bot_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] [has_sup δ] [has_bot δ] (f : sup_bot_hom γ δ) (g : sup_bot_hom β γ) (h : sup_bot_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem sup_bot_hom.comp_id {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) :
@[simp]
theorem sup_bot_hom.id_comp {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) :
theorem sup_bot_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] {g₁ g₂ : sup_bot_hom β γ} {f : sup_bot_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem sup_bot_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] {g : sup_bot_hom β γ} {f₁ f₂ : sup_bot_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def sup_bot_hom.has_sup {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
Equations
@[protected, instance]
def sup_bot_hom.semilattice_sup {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
Equations
@[protected, instance]
def sup_bot_hom.order_bot {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
Equations
@[simp]
theorem sup_bot_hom.coe_sup {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] (f g : sup_bot_hom α β) :
(f g) = f g
@[simp]
theorem sup_bot_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
@[simp]
theorem sup_bot_hom.sup_apply {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] (f g : sup_bot_hom α β) (a : α) :
(f g) a = f a g a
@[simp]
theorem sup_bot_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] (a : α) :

Finitary infimum homomorphisms #

def inf_top_hom.to_top_hom {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) :
top_hom α β

Reinterpret an inf_top_hom as a top_hom.

Equations
@[protected, instance]
def inf_top_hom.inf_top_hom_class {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] :
Equations
@[protected, instance]
def inf_top_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] :
has_coe_to_fun (inf_top_hom α β) (λ (_x : inf_top_hom α β), α → β)

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

Equations
@[simp]
theorem inf_top_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] {f : inf_top_hom α β} :
@[ext]
theorem inf_top_hom.ext {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] {f g : inf_top_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def inf_top_hom.copy {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) (f' : α → β) (h : f' = f) :

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

Equations
@[simp]
theorem inf_top_hom.id_to_inf_hom (α : Type u_3) [has_inf α] [has_top α] :
@[protected]
def inf_top_hom.id (α : Type u_3) [has_inf α] [has_top α] :

id as an inf_top_hom.

Equations
@[protected, instance]
def inf_top_hom.inhabited (α : Type u_3) [has_inf α] [has_top α] :
Equations
@[simp]
theorem inf_top_hom.coe_id (α : Type u_3) [has_inf α] [has_top α] :
@[simp]
theorem inf_top_hom.id_apply {α : Type u_3} [has_inf α] [has_top α] (a : α) :
def inf_top_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] (f : inf_top_hom β γ) (g : inf_top_hom α β) :

Composition of inf_top_homs as an inf_top_hom.

Equations
@[simp]
theorem inf_top_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] (f : inf_top_hom β γ) (g : inf_top_hom α β) :
(f.comp g) = f g
@[simp]
theorem inf_top_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] (f : inf_top_hom β γ) (g : inf_top_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem inf_top_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] [has_inf δ] [has_top δ] (f : inf_top_hom γ δ) (g : inf_top_hom β γ) (h : inf_top_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem inf_top_hom.comp_id {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) :
@[simp]
theorem inf_top_hom.id_comp {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) :
theorem inf_top_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] {g₁ g₂ : inf_top_hom β γ} {f : inf_top_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem inf_top_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] {g : inf_top_hom β γ} {f₁ f₂ : inf_top_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def inf_top_hom.has_inf {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
Equations
@[protected, instance]
def inf_top_hom.semilattice_inf {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
Equations
@[protected, instance]
def inf_top_hom.order_top {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
Equations
@[simp]
theorem inf_top_hom.coe_inf {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] (f g : inf_top_hom α β) :
(f g) = f g
@[simp]
theorem inf_top_hom.coe_top {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
@[simp]
theorem inf_top_hom.inf_apply {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] (f g : inf_top_hom α β) (a : α) :
(f g) a = f a g a
@[simp]
theorem inf_top_hom.top_apply {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] (a : α) :

Lattice homomorphisms #

def lattice_hom.to_inf_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
inf_hom α β

Reinterpret a lattice_hom as an inf_hom.

Equations
@[protected, instance]
def lattice_hom.lattice_hom_class {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] :
Equations
@[protected, instance]
def lattice_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] :
has_coe_to_fun (lattice_hom α β) (λ (_x : lattice_hom α β), α → β)

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

Equations
@[simp]
theorem lattice_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] {f : lattice_hom α β} :
@[ext]
theorem lattice_hom.ext {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] {f g : lattice_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def lattice_hom.copy {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) (f' : α → β) (h : f' = f) :

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

Equations
@[protected]
def lattice_hom.id (α : Type u_3) [lattice α] :

id as a lattice_hom.

Equations
@[protected, instance]
def lattice_hom.inhabited (α : Type u_3) [lattice α] :
Equations
@[simp]
theorem lattice_hom.coe_id (α : Type u_3) [lattice α] :
@[simp]
theorem lattice_hom.id_apply {α : Type u_3} [lattice α] (a : α) :
def lattice_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :

Composition of lattice_homs as a lattice_hom.

Equations
@[simp]
theorem lattice_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g) = f g
@[simp]
theorem lattice_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem lattice_hom.coe_comp_sup_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g) = f.comp g
@[simp]
theorem lattice_hom.coe_comp_inf_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g) = f.comp g
@[simp]
theorem lattice_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [lattice α] [lattice β] [lattice γ] [lattice δ] (f : lattice_hom γ δ) (g : lattice_hom β γ) (h : lattice_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem lattice_hom.comp_id {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
@[simp]
theorem lattice_hom.id_comp {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
theorem lattice_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] {g₁ g₂ : lattice_hom β γ} {f : lattice_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem lattice_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] {g : lattice_hom β γ} {f₁ f₂ : lattice_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[reducible]
def order_hom_class.to_lattice_hom_class {F : Type u_1} (α : Type u_3) (β : Type u_4) [linear_order α] [lattice β] [order_hom_class F α β] :

An order homomorphism from a linear order is a lattice homomorphism.

Equations
def order_hom_class.to_lattice_hom {F : Type u_1} (α : Type u_3) (β : Type u_4) [linear_order α] [lattice β] [order_hom_class F α β] (f : F) :

Reinterpret an order homomorphism to a linear order as a lattice_hom.

Equations
@[simp]
theorem order_hom_class.coe_to_lattice_hom {F : Type u_1} (α : Type u_3) (β : Type u_4) [linear_order α] [lattice β] [order_hom_class F α β] (f : F) :
@[simp]
theorem order_hom_class.to_lattice_hom_apply {F : Type u_1} (α : Type u_3) (β : Type u_4) [linear_order α] [lattice β] [order_hom_class F α β] (f : F) (a : α) :

Bounded lattice homomorphisms #

def bounded_lattice_hom.to_sup_bot_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :

Reinterpret a bounded_lattice_hom as a sup_bot_hom.

Equations
def bounded_lattice_hom.to_inf_top_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :

Reinterpret a bounded_lattice_hom as an inf_top_hom.

Equations
@[protected, instance]
def bounded_lattice_hom.has_coe_to_fun {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] :
has_coe_to_fun (bounded_lattice_hom α β) (λ (_x : bounded_lattice_hom α β), α → β)

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

Equations
@[simp]
theorem bounded_lattice_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] {f : bounded_lattice_hom α β} :
@[ext]
theorem bounded_lattice_hom.ext {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] {f g : bounded_lattice_hom α β} (h : ∀ (a : α), f a = g a) :
f = g
@[protected]
def bounded_lattice_hom.copy {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) (f' : α → β) (h : f' = f) :

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

Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem bounded_lattice_hom.id_apply {α : Type u_3} [lattice α] [bounded_order α] (a : α) :
def bounded_lattice_hom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

Composition of bounded_lattice_homs as a bounded_lattice_hom.

Equations
@[simp]
theorem bounded_lattice_hom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :
(f.comp g) = f g
@[simp]
theorem bounded_lattice_hom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem bounded_lattice_hom.coe_comp_lattice_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :
(f.comp g) = f.comp g
@[simp]
theorem bounded_lattice_hom.coe_comp_sup_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :
(f.comp g) = f.comp g
@[simp]
theorem bounded_lattice_hom.coe_comp_inf_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :
(f.comp g) = f.comp g
@[simp]
theorem bounded_lattice_hom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [lattice α] [lattice β] [lattice γ] [lattice δ] [bounded_order α] [bounded_order β] [bounded_order γ] [bounded_order δ] (f : bounded_lattice_hom γ δ) (g : bounded_lattice_hom β γ) (h : bounded_lattice_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem bounded_lattice_hom.comp_id {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :
@[simp]
theorem bounded_lattice_hom.id_comp {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :
theorem bounded_lattice_hom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g₁ g₂ : bounded_lattice_hom β γ} {f : bounded_lattice_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem bounded_lattice_hom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g : bounded_lattice_hom β γ} {f₁ f₂ : bounded_lattice_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂

Dual homs #

@[protected]
def sup_hom.dual {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] :

Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices.

Equations
@[simp]
theorem sup_hom.dual_apply_to_fun {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) (ᾰ : α) :
(sup_hom.dual f) = f ᾰ
@[simp]
theorem sup_hom.dual_symm_apply_to_fun {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : inf_hom αᵒᵈ βᵒᵈ) (ᾰ : αᵒᵈ) :
((sup_hom.dual.symm) f) = f ᾰ
@[simp]
theorem sup_hom.dual_id {α : Type u_3} [has_sup α] :
@[simp]
theorem sup_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] (g : sup_hom β γ) (f : sup_hom α β) :
@[simp]
theorem sup_hom.symm_dual_id {α : Type u_3} [has_sup α] :
@[simp]
theorem sup_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_sup β] [has_sup γ] (g : inf_hom βᵒᵈ γᵒᵈ) (f : inf_hom αᵒᵈ βᵒᵈ) :
@[simp]
theorem inf_hom.dual_symm_apply_to_fun {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : sup_hom αᵒᵈ βᵒᵈ) (ᾰ : αᵒᵈ) :
((inf_hom.dual.symm) f) = f ᾰ
@[protected]
def inf_hom.dual {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] :

Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices.

Equations
@[simp]
theorem inf_hom.dual_apply_to_fun {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) (ᾰ : α) :
(inf_hom.dual f) = f ᾰ
@[simp]
theorem inf_hom.dual_id {α : Type u_3} [has_inf α] :
@[simp]
theorem inf_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] (g : inf_hom β γ) (f : inf_hom α β) :
@[simp]
theorem inf_hom.symm_dual_id {α : Type u_3} [has_inf α] :
@[simp]
theorem inf_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_inf β] [has_inf γ] (g : sup_hom βᵒᵈ γᵒᵈ) (f : sup_hom αᵒᵈ βᵒᵈ) :
def sup_bot_hom.dual {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] :

Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual lattices.

Equations
@[simp]
@[simp]
theorem sup_bot_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] (g : sup_bot_hom β γ) (f : sup_bot_hom α β) :
@[simp]
theorem sup_bot_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ] (g : inf_top_hom βᵒᵈ γᵒᵈ) (f : inf_top_hom αᵒᵈ βᵒᵈ) :
@[simp]
@[simp]
theorem inf_top_hom.dual_apply_to_sup_hom {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) :
@[protected]
def inf_top_hom.dual {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] :

Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual lattices.

Equations
@[simp]
@[simp]
theorem inf_top_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] (g : inf_top_hom β γ) (f : inf_top_hom α β) :
@[simp]
theorem inf_top_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ] (g : sup_bot_hom βᵒᵈ γᵒᵈ) (f : sup_bot_hom αᵒᵈ βᵒᵈ) :
@[protected]
def lattice_hom.dual {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] :

Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.

Equations
@[simp]
theorem lattice_hom.dual_apply_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
@[simp]
theorem lattice_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (g : lattice_hom β γ) (f : lattice_hom α β) :
@[simp]
theorem lattice_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (g : lattice_hom βᵒᵈ γᵒᵈ) (f : lattice_hom αᵒᵈ βᵒᵈ) :
@[protected]
def bounded_lattice_hom.dual {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] :

Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual bounded lattices.

Equations
@[simp]