mathlib3 documentation

order.hom.lattice

Lattice homomorphisms #

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

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?

source
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
source
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
source
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
source
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
source
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
source
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
source
@[instance]
def sup_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_sup α] [has_sup β] [self : sup_hom_class F α β] :
fun_like F α (λ (_x : α), β)
source
@[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
source
@[instance]
def inf_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_inf α] [has_inf β] [self : inf_hom_class F α β] :
fun_like F α (λ (_x : α), β)
source
@[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
source
@[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
source
@[instance]
def sup_bot_hom_class.to_sup_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_sup α] [has_sup β] [has_bot α] [has_bot β] [self : sup_bot_hom_class F α β] :
sup_hom_class F α β
source
@[instance]
def inf_top_hom_class.to_inf_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_inf α] [has_inf β] [has_top α] [has_top β] [self : inf_top_hom_class F α β] :
inf_hom_class F α β
source
@[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
source
@[instance]
def lattice_hom_class.to_sup_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [lattice α] [lattice β] [self : lattice_hom_class F α β] :
sup_hom_class F α β
source
@[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
source
@[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
source
@[instance]
def bounded_lattice_hom_class.to_lattice_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [lattice α] [lattice β] [bounded_order α] [bounded_order β] [self : bounded_lattice_hom_class F α β] :
lattice_hom_class F α β
source
@[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 α β] :
order_hom_class F α β
Equations
source
@[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 α β] :
order_hom_class F α β
Equations
source
@[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 α β] :
bot_hom_class F α β
Equations
source
@[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 α β] :
top_hom_class F α β
Equations
source
@[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 α β] :
inf_hom_class F α β
Equations
source
@[protected, instance]
def bounded_lattice_hom_class.to_sup_bot_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [bounded_lattice_hom_class F α β] :
sup_bot_hom_class F α β
Equations
source
@[protected, instance]
def bounded_lattice_hom_class.to_inf_top_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [bounded_lattice_hom_class F α β] :
inf_top_hom_class F α β
Equations
source
@[protected, instance]
def bounded_lattice_hom_class.to_bounded_order_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [bounded_lattice_hom_class F α β] :
bounded_order_hom_class F α β
Equations
source
@[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 α β] :
sup_hom_class F α β
Equations
source
@[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 α β] :
inf_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_sup_bot_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_sup α] [order_bot α] [semilattice_sup β] [order_bot β] [order_iso_class F α β] :
sup_bot_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_inf_top_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [semilattice_inf α] [order_top α] [semilattice_inf β] [order_top β] [order_iso_class F α β] :
inf_top_hom_class F α β
Equations
source
@[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 α β] :
lattice_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_bounded_lattice_hom_class {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [order_iso_class F α β] :
bounded_lattice_hom_class F α β
Equations
source
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)
source
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)
source
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)
source
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)ᶜ

Special case of map_compl for boolean algebras.

source
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

Special case of map_sdiff for boolean algebras.

source
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

Special case of map_symm_diff for boolean algebras.

source
@[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
source
@[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
source
@[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 α β] :
has_coe_t F (sup_bot_hom α β)
Equations
source
@[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 α β] :
has_coe_t F (inf_top_hom α β)
Equations
source
@[protected, instance]
def lattice_hom.has_coe_t {F : Type u_1} {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [lattice_hom_class F α β] :
has_coe_t F (lattice_hom α β)
Equations
source
@[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 α β] :
has_coe_t F (bounded_lattice_hom α β)
Equations

Supremum homomorphisms #

source
@[protected, instance]
def sup_hom.sup_hom_class {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] :
sup_hom_class (sup_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem sup_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] {f : sup_hom α β} :
f.to_fun = ⇑f
source
@[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
source
@[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
source
@[simp]
theorem sup_hom.coe_copy {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem sup_hom.copy_eq {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] (f : sup_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def sup_hom.id (α : Type u_3) [has_sup α] :
sup_hom α α

id as a sup_hom.

Equations
source
@[protected, instance]
def sup_hom.inhabited (α : Type u_3) [has_sup α] :
inhabited (sup_hom α α)
Equations
source
@[simp]
theorem sup_hom.coe_id (α : Type u_3) [has_sup α] :
⇑(sup_hom.id α) = id
source
@[simp]
theorem sup_hom.id_apply {α : Type u_3} [has_sup α] (a : α) :
⇑(sup_hom.id α) a = a
source
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
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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₂
source
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₂
source
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
source
@[simp]
theorem sup_hom.coe_const (α : Type u_3) {β : Type u_4} [has_sup α] [semilattice_sup β] (b : β) :
⇑(sup_hom.const α b) = function.const α b
source
@[simp]
theorem sup_hom.const_apply (α : Type u_3) {β : Type u_4} [has_sup α] [semilattice_sup β] (b : β) (a : α) :
⇑(sup_hom.const α b) a = b
source
@[protected, instance]
def sup_hom.has_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] :
has_sup (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.semilattice_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] :
semilattice_sup (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.has_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] :
has_bot (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.has_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] :
has_top (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.order_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [order_bot β] :
order_bot (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.order_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [order_top β] :
order_top (sup_hom α β)
Equations
source
@[protected, instance]
def sup_hom.bounded_order {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [bounded_order β] :
bounded_order (sup_hom α β)
Equations
source
@[simp]
theorem sup_hom.coe_sup {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] (f g : sup_hom α β) :
⇑(f ⊔ g) = ⇑f ⊔ ⇑g
source
@[simp]
theorem sup_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] :
⇑⊥ = ⊥
source
@[simp]
theorem sup_hom.coe_top {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] :
⇑⊤ = ⊤
source
@[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
source
@[simp]
theorem sup_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_bot β] (a : α) :
⇑⊥ a = ⊥
source
@[simp]
theorem sup_hom.top_apply {α : Type u_3} {β : Type u_4} [has_sup α] [semilattice_sup β] [has_top β] (a : α) :
⇑⊤ a = ⊤

Infimum homomorphisms #

source
@[protected, instance]
def inf_hom.inf_hom_class {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] :
inf_hom_class (inf_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem inf_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] {f : inf_hom α β} :
f.to_fun = ⇑f
source
@[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
source
@[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
source
@[simp]
theorem inf_hom.coe_copy {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem inf_hom.copy_eq {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] (f : inf_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[protected]
def inf_hom.id (α : Type u_3) [has_inf α] :
inf_hom α α

id as an inf_hom.

Equations
source
@[protected, instance]
def inf_hom.inhabited (α : Type u_3) [has_inf α] :
inhabited (inf_hom α α)
Equations
source
@[simp]
theorem inf_hom.coe_id (α : Type u_3) [has_inf α] :
⇑(inf_hom.id α) = id
source
@[simp]
theorem inf_hom.id_apply {α : Type u_3} [has_inf α] (a : α) :
⇑(inf_hom.id α) a = a
source
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
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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₂
source
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₂
source
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
source
@[simp]
theorem inf_hom.coe_const (α : Type u_3) {β : Type u_4} [has_inf α] [semilattice_inf β] (b : β) :
⇑(inf_hom.const α b) = function.const α b
source
@[simp]
theorem inf_hom.const_apply (α : Type u_3) {β : Type u_4} [has_inf α] [semilattice_inf β] (b : β) (a : α) :
⇑(inf_hom.const α b) a = b
source
@[protected, instance]
def inf_hom.has_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] :
has_inf (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.semilattice_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] :
semilattice_inf (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.has_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] :
has_bot (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.has_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] :
has_top (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.order_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [order_bot β] :
order_bot (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.order_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [order_top β] :
order_top (inf_hom α β)
Equations
source
@[protected, instance]
def inf_hom.bounded_order {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [bounded_order β] :
bounded_order (inf_hom α β)
Equations
source
@[simp]
theorem inf_hom.coe_inf {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] (f g : inf_hom α β) :
⇑(f ⊓ g) = ⇑f ⊓ ⇑g
source
@[simp]
theorem inf_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] :
⇑⊥ = ⊥
source
@[simp]
theorem inf_hom.coe_top {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] :
⇑⊤ = ⊤
source
@[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
source
@[simp]
theorem inf_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_bot β] (a : α) :
⇑⊥ a = ⊥
source
@[simp]
theorem inf_hom.top_apply {α : Type u_3} {β : Type u_4} [has_inf α] [semilattice_inf β] [has_top β] (a : α) :
⇑⊤ a = ⊤

Finitary supremum homomorphisms #

source
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
source
@[protected, instance]
def sup_bot_hom.sup_bot_hom_class {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] :
sup_bot_hom_class (sup_bot_hom α β) α β
Equations
source
@[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
source
@[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 α β} :
f.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[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) :
sup_bot_hom α β

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

Equations
source
@[simp]
theorem sup_bot_hom.coe_copy {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem sup_bot_hom.copy_eq {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] (f : sup_bot_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[simp]
theorem sup_bot_hom.id_to_sup_hom (α : Type u_3) [has_sup α] [has_bot α] :
(sup_bot_hom.id α).to_sup_hom = sup_hom.id α
source
@[protected]
def sup_bot_hom.id (α : Type u_3) [has_sup α] [has_bot α] :
sup_bot_hom α α

id as a sup_bot_hom.

Equations
source
@[protected, instance]
def sup_bot_hom.inhabited (α : Type u_3) [has_sup α] [has_bot α] :
inhabited (sup_bot_hom α α)
Equations
source
@[simp]
theorem sup_bot_hom.coe_id (α : Type u_3) [has_sup α] [has_bot α] :
⇑(sup_bot_hom.id α) = id
source
@[simp]
theorem sup_bot_hom.id_apply {α : Type u_3} [has_sup α] [has_bot α] (a : α) :
⇑(sup_bot_hom.id α) a = a
source
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 α β) :
sup_bot_hom α γ

Composition of sup_bot_homs as a sup_bot_hom.

Equations
source
@[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
source
@[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)
source
@[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)
source
@[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 α β) :
f.comp (sup_bot_hom.id α) = f
source
@[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 α β) :
(sup_bot_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def sup_bot_hom.has_sup {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
has_sup (sup_bot_hom α β)
Equations
source
@[protected, instance]
def sup_bot_hom.semilattice_sup {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
semilattice_sup (sup_bot_hom α β)
Equations
source
@[protected, instance]
def sup_bot_hom.order_bot {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
order_bot (sup_bot_hom α β)
Equations
source
@[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
source
@[simp]
theorem sup_bot_hom.coe_bot {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] :
⇑⊥ = ⊥
source
@[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
source
@[simp]
theorem sup_bot_hom.bot_apply {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [semilattice_sup β] [order_bot β] (a : α) :
⇑⊥ a = ⊥

Finitary infimum homomorphisms #

source
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
source
@[protected, instance]
def inf_top_hom.inf_top_hom_class {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] :
inf_top_hom_class (inf_top_hom α β) α β
Equations
source
@[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
source
@[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 α β} :
f.to_inf_hom.to_fun = ⇑f
source
@[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
source
@[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) :
inf_top_hom α β

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

Equations
source
@[simp]
theorem inf_top_hom.coe_copy {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem inf_top_hom.copy_eq {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : inf_top_hom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
@[simp]
theorem inf_top_hom.id_to_inf_hom (α : Type u_3) [has_inf α] [has_top α] :
(inf_top_hom.id α).to_inf_hom = inf_hom.id α
source
@[protected]
def inf_top_hom.id (α : Type u_3) [has_inf α] [has_top α] :
inf_top_hom α α

id as an inf_top_hom.

Equations
source
@[protected, instance]
def inf_top_hom.inhabited (α : Type u_3) [has_inf α] [has_top α] :
inhabited (inf_top_hom α α)
Equations
source
@[simp]
theorem inf_top_hom.coe_id (α : Type u_3) [has_inf α] [has_top α] :
⇑(inf_top_hom.id α) = id
source
@[simp]
theorem inf_top_hom.id_apply {α : Type u_3} [has_inf α] [has_top α] (a : α) :
⇑(inf_top_hom.id α) a = a
source
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 α β) :
inf_top_hom α γ

Composition of inf_top_homs as an inf_top_hom.

Equations
source
@[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
source
@[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)
source
@[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)
source
@[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 α β) :
f.comp (inf_top_hom.id α) = f
source
@[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 α β) :
(inf_top_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def inf_top_hom.has_inf {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
has_inf (inf_top_hom α β)
Equations
source
@[protected, instance]
def inf_top_hom.semilattice_inf {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
semilattice_inf (inf_top_hom α β)
Equations
source
@[protected, instance]
def inf_top_hom.order_top {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
order_top (inf_top_hom α β)
Equations
source
@[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
source
@[simp]
theorem inf_top_hom.coe_top {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] :
⇑⊤ = ⊤
source
@[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
source
@[simp]
theorem inf_top_hom.top_apply {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [semilattice_inf β] [order_top β] (a : α) :
⇑⊤ a = ⊤

Lattice homomorphisms #

source
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
source
@[protected, instance]
def lattice_hom.lattice_hom_class {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] :
lattice_hom_class (lattice_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem lattice_hom.to_fun_eq_coe {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] {f : lattice_hom α β} :
f.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[protected]
def lattice_hom.copy {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) (f' : α → β) (h : f' = ⇑f) :
lattice_hom α β

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

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

id as a lattice_hom.

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

Composition of lattice_homs as a lattice_hom.

Equations
source
@[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
source
@[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)
source
@[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
source
@[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
source
@[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)
source
@[simp]
theorem lattice_hom.comp_id {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
f.comp (lattice_hom.id α) = f
source
@[simp]
theorem lattice_hom.id_comp {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
(lattice_hom.id β).comp f = f
source
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₂
source
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₂
source
@[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 α β] :
lattice_hom_class F α β

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

Equations
source
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) :
lattice_hom α β

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

Equations
source
@[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) :
⇑(order_hom_class.to_lattice_hom α β f) = ⇑f
source
@[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 : α) :
⇑(order_hom_class.to_lattice_hom α β f) a = ⇑f a

Bounded lattice homomorphisms #

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

Reinterpret a bounded_lattice_hom as a sup_bot_hom.

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

Reinterpret a bounded_lattice_hom as an inf_top_hom.

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

Reinterpret a bounded_lattice_hom as a bounded_order_hom.

Equations
source
@[protected, instance]
def bounded_lattice_hom.bounded_lattice_hom_class {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] :
bounded_lattice_hom_class (bounded_lattice_hom α β) α β
Equations
source
@[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
source
@[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 α β} :
f.to_lattice_hom.to_sup_hom.to_fun = ⇑f
source
@[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
source
@[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) :
bounded_lattice_hom α β

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

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

id as a bounded_lattice_hom.

Equations
source
@[protected, instance]
def bounded_lattice_hom.inhabited (α : Type u_3) [lattice α] [bounded_order α] :
inhabited (bounded_lattice_hom α α)
Equations
source
@[simp]
theorem bounded_lattice_hom.coe_id (α : Type u_3) [lattice α] [bounded_order α] :
⇑(bounded_lattice_hom.id α) = id
source
@[simp]
theorem bounded_lattice_hom.id_apply {α : Type u_3} [lattice α] [bounded_order α] (a : α) :
⇑(bounded_lattice_hom.id α) a = a
source
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 α β) :
bounded_lattice_hom α γ

Composition of bounded_lattice_homs as a bounded_lattice_hom.

Equations
source
@[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
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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)
source
@[simp]
theorem bounded_lattice_hom.comp_id {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :
f.comp (bounded_lattice_hom.id α) = f
source
@[simp]
theorem bounded_lattice_hom.id_comp {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :
(bounded_lattice_hom.id β).comp f = f
source
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₂
source
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 #

source
@[protected]
def sup_hom.dual {α : Type u_3} {β : Type u_4} [has_sup α] [has_sup β] :
sup_hom α β ≃ inf_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[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 ᾰ
source
@[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 ᾰ
source
@[simp]
theorem sup_hom.dual_id {α : Type u_3} [has_sup α] :
⇑sup_hom.dual (sup_hom.id α) = inf_hom.id αᵒᵈ
source
@[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 α β) :
⇑sup_hom.dual (g.comp f) = (⇑sup_hom.dual g).comp (⇑sup_hom.dual f)
source
@[simp]
theorem sup_hom.symm_dual_id {α : Type u_3} [has_sup α] :
⇑(sup_hom.dual.symm) (inf_hom.id αᵒᵈ) = sup_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(sup_hom.dual.symm) (g.comp f) = (⇑(sup_hom.dual.symm) g).comp (⇑(sup_hom.dual.symm) f)
source
@[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 ᾰ
source
@[protected]
def inf_hom.dual {α : Type u_3} {β : Type u_4} [has_inf α] [has_inf β] :
inf_hom α β ≃ sup_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[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 ᾰ
source
@[simp]
theorem inf_hom.dual_id {α : Type u_3} [has_inf α] :
⇑inf_hom.dual (inf_hom.id α) = sup_hom.id αᵒᵈ
source
@[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 α β) :
⇑inf_hom.dual (g.comp f) = (⇑inf_hom.dual g).comp (⇑inf_hom.dual f)
source
@[simp]
theorem inf_hom.symm_dual_id {α : Type u_3} [has_inf α] :
⇑(inf_hom.dual.symm) (sup_hom.id αᵒᵈ) = inf_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(inf_hom.dual.symm) (g.comp f) = (⇑(inf_hom.dual.symm) g).comp (⇑(inf_hom.dual.symm) f)
source
def sup_bot_hom.dual {α : Type u_3} {β : Type u_4} [has_sup α] [has_bot α] [has_sup β] [has_bot β] :
sup_bot_hom α β ≃ inf_top_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem sup_bot_hom.dual_id {α : Type u_3} [has_sup α] [has_bot α] :
⇑sup_bot_hom.dual (sup_bot_hom.id α) = inf_top_hom.id αᵒᵈ
source
@[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 α β) :
⇑sup_bot_hom.dual (g.comp f) = (⇑sup_bot_hom.dual g).comp (⇑sup_bot_hom.dual f)
source
@[simp]
theorem sup_bot_hom.symm_dual_id {α : Type u_3} [has_sup α] [has_bot α] :
⇑(sup_bot_hom.dual.symm) (inf_top_hom.id αᵒᵈ) = sup_bot_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(sup_bot_hom.dual.symm) (g.comp f) = (⇑(sup_bot_hom.dual.symm) g).comp (⇑(sup_bot_hom.dual.symm) f)
source
@[simp]
theorem inf_top_hom.dual_symm_apply_to_inf_hom {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] (f : sup_bot_hom αᵒᵈ βᵒᵈ) :
(⇑(inf_top_hom.dual.symm) f).to_inf_hom = ⇑(inf_hom.dual.symm) f.to_sup_hom
source
@[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 α β) :
(⇑inf_top_hom.dual f).to_sup_hom = ⇑inf_hom.dual f.to_inf_hom
source
@[protected]
def inf_top_hom.dual {α : Type u_3} {β : Type u_4} [has_inf α] [has_top α] [has_inf β] [has_top β] :
inf_top_hom α β ≃ sup_bot_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem inf_top_hom.dual_id {α : Type u_3} [has_inf α] [has_top α] :
⇑inf_top_hom.dual (inf_top_hom.id α) = sup_bot_hom.id αᵒᵈ
source
@[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 α β) :
⇑inf_top_hom.dual (g.comp f) = (⇑inf_top_hom.dual g).comp (⇑inf_top_hom.dual f)
source
@[simp]
theorem inf_top_hom.symm_dual_id {α : Type u_3} [has_inf α] [has_top α] :
⇑(inf_top_hom.dual.symm) (sup_bot_hom.id αᵒᵈ) = inf_top_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(inf_top_hom.dual.symm) (g.comp f) = (⇑(inf_top_hom.dual.symm) g).comp (⇑(inf_top_hom.dual.symm) f)
source
@[protected]
def lattice_hom.dual {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] :
lattice_hom α β ≃ lattice_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem lattice_hom.dual_apply_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
(⇑lattice_hom.dual f).to_sup_hom = ⇑inf_hom.dual f.to_inf_hom
source
@[simp]
theorem lattice_hom.dual_symm_apply_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom αᵒᵈ βᵒᵈ) :
(⇑(lattice_hom.dual.symm) f).to_sup_hom = ⇑inf_hom.dual f.to_inf_hom
source
@[simp]
theorem lattice_hom.dual_id {α : Type u_3} [lattice α] :
⇑lattice_hom.dual (lattice_hom.id α) = lattice_hom.id αᵒᵈ
source
@[simp]
theorem lattice_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (g : lattice_hom β γ) (f : lattice_hom α β) :
⇑lattice_hom.dual (g.comp f) = (⇑lattice_hom.dual g).comp (⇑lattice_hom.dual f)
source
@[simp]
theorem lattice_hom.symm_dual_id {α : Type u_3} [lattice α] :
⇑(lattice_hom.dual.symm) (lattice_hom.id αᵒᵈ) = lattice_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(lattice_hom.dual.symm) (g.comp f) = (⇑(lattice_hom.dual.symm) g).comp (⇑(lattice_hom.dual.symm) f)
source
@[simp]
theorem bounded_lattice_hom.dual_symm_apply_to_lattice_hom {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] (f : bounded_lattice_hom αᵒᵈ βᵒᵈ) :
(⇑(bounded_lattice_hom.dual.symm) f).to_lattice_hom = ⇑(lattice_hom.dual.symm) f.to_lattice_hom
source
@[simp]
theorem bounded_lattice_hom.dual_apply_to_lattice_hom {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] (f : bounded_lattice_hom α β) :
(⇑bounded_lattice_hom.dual f).to_lattice_hom = ⇑lattice_hom.dual f.to_lattice_hom
source
@[protected]
def bounded_lattice_hom.dual {α : Type u_3} {β : Type u_4} [lattice α] [bounded_order α] [lattice β] [bounded_order β] :
bounded_lattice_hom α β ≃ bounded_lattice_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem bounded_lattice_hom.dual_id {α : Type u_3} [lattice α] [bounded_order α] :
⇑bounded_lattice_hom.dual (bounded_lattice_hom.id α) = bounded_lattice_hom.id αᵒᵈ
source
@[simp]
theorem bounded_lattice_hom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [bounded_order α] [lattice β] [bounded_order β] [lattice γ] [bounded_order γ] (g : bounded_lattice_hom β γ) (f : bounded_lattice_hom α β) :
⇑bounded_lattice_hom.dual (g.comp f) = (⇑bounded_lattice_hom.dual g).comp (⇑bounded_lattice_hom.dual f)
source
@[simp]
theorem bounded_lattice_hom.symm_dual_id {α : Type u_3} [lattice α] [bounded_order α] :
⇑(bounded_lattice_hom.dual.symm) (bounded_lattice_hom.id αᵒᵈ) = bounded_lattice_hom.id α
source
@[simp]
theorem bounded_lattice_hom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [bounded_order α] [lattice β] [bounded_order β] [lattice γ] [bounded_order γ] (g : bounded_lattice_hom βᵒᵈ γᵒᵈ) (f : bounded_lattice_hom αᵒᵈ βᵒᵈ) :
⇑(bounded_lattice_hom.dual.symm) (g.comp f) = (⇑(bounded_lattice_hom.dual.symm) g).comp (⇑(bounded_lattice_hom.dual.symm) f)

with_top, with_bot #

source
@[protected]
def sup_hom.with_top {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] (f : sup_hom α β) :
sup_hom (with_top α) (with_top β)

Adjoins a ⊤ to the domain and codomain of a sup_hom.

Equations
source
@[simp]
theorem sup_hom.with_top_to_fun {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] (f : sup_hom α β) (o : option α) :
⇑(f.with_top) o = option.map ⇑f o
source
@[simp]
theorem sup_hom.with_top_id {α : Type u_3} [semilattice_sup α] :
(sup_hom.id α).with_top = sup_hom.id (with_top α)
source
@[simp]
theorem sup_hom.with_top_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_sup α] [semilattice_sup β] [semilattice_sup γ] (f : sup_hom β γ) (g : sup_hom α β) :
(f.comp g).with_top = f.with_top.comp g.with_top
source
@[protected]
def sup_hom.with_bot {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] (f : sup_hom α β) :
sup_bot_hom (with_bot α) (with_bot β)

Adjoins a ⊥ to the domain and codomain of a sup_hom.

Equations
source
@[simp]
theorem sup_hom.with_bot_to_sup_hom_to_fun {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] (f : sup_hom α β) (o : option α) :
⇑(f.with_bot.to_sup_hom) o = option.map ⇑f o
source
@[simp]
theorem sup_hom.with_bot_id {α : Type u_3} [semilattice_sup α] :
(sup_hom.id α).with_bot = sup_bot_hom.id (with_bot α)
source
@[simp]
theorem sup_hom.with_bot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_sup α] [semilattice_sup β] [semilattice_sup γ] (f : sup_hom β γ) (g : sup_hom α β) :
(f.comp g).with_bot = f.with_bot.comp g.with_bot
source
@[simp]
theorem sup_hom.with_top'_to_fun {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [order_top β] (f : sup_hom α β) (a : with_top α) :
⇑(f.with_top') a = option.elim ⊤ ⇑f a
source
def sup_hom.with_top' {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [order_top β] (f : sup_hom α β) :
sup_hom (with_top α) β

Adjoins a ⊤ to the codomain of a sup_hom.

Equations
source
def sup_hom.with_bot' {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [order_bot β] (f : sup_hom α β) :
sup_bot_hom (with_bot α) β

Adjoins a ⊥ to the domain of a sup_hom.

Equations
source
@[simp]
theorem sup_hom.with_bot'_to_sup_hom_to_fun {α : Type u_3} {β : Type u_4} [semilattice_sup α] [semilattice_sup β] [order_bot β] (f : sup_hom α β) (a : with_bot α) :
⇑(f.with_bot'.to_sup_hom) a = option.elim ⊥ ⇑f a
source
@[simp]
theorem inf_hom.with_top_to_inf_hom_to_fun {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] (f : inf_hom α β) (o : option α) :
⇑(f.with_top.to_inf_hom) o = option.map ⇑f o
source
@[protected]
def inf_hom.with_top {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] (f : inf_hom α β) :
inf_top_hom (with_top α) (with_top β)

Adjoins a ⊤ to the domain and codomain of an inf_hom.

Equations
source
@[simp]
theorem inf_hom.with_top_id {α : Type u_3} [semilattice_inf α] :
(inf_hom.id α).with_top = inf_top_hom.id (with_top α)
source
@[simp]
theorem inf_hom.with_top_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_inf α] [semilattice_inf β] [semilattice_inf γ] (f : inf_hom β γ) (g : inf_hom α β) :
(f.comp g).with_top = f.with_top.comp g.with_top
source
@[protected]
def inf_hom.with_bot {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] (f : inf_hom α β) :
inf_hom (with_bot α) (with_bot β)

Adjoins a ⊥ to the domain and codomain of aninf_hom`.

Equations
source
@[simp]
theorem inf_hom.with_bot_to_fun {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] (f : inf_hom α β) (o : option α) :
⇑(f.with_bot) o = option.map ⇑f o
source
@[simp]
theorem inf_hom.with_bot_id {α : Type u_3} [semilattice_inf α] :
(inf_hom.id α).with_bot = inf_hom.id (with_bot α)
source
@[simp]
theorem inf_hom.with_bot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [semilattice_inf α] [semilattice_inf β] [semilattice_inf γ] (f : inf_hom β γ) (g : inf_hom α β) :
(f.comp g).with_bot = f.with_bot.comp g.with_bot
source
@[simp]
theorem inf_hom.with_top'_to_inf_hom_to_fun {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [order_top β] (f : inf_hom α β) (a : with_top α) :
⇑(f.with_top'.to_inf_hom) a = option.elim ⊤ ⇑f a
source
def inf_hom.with_top' {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [order_top β] (f : inf_hom α β) :
inf_top_hom (with_top α) β

Adjoins a ⊤ to the codomain of an inf_hom.

Equations
source
@[simp]
theorem inf_hom.with_bot'_to_fun {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [order_bot β] (f : inf_hom α β) (a : with_bot α) :
⇑(f.with_bot') a = option.elim ⊥ ⇑f a
source
def inf_hom.with_bot' {α : Type u_3} {β : Type u_4} [semilattice_inf α] [semilattice_inf β] [order_bot β] (f : inf_hom α β) :
inf_hom (with_bot α) β

Adjoins a ⊥ to the codomain of an inf_hom.

Equations
source
@[protected]
def lattice_hom.with_top {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
lattice_hom (with_top α) (with_top β)

Adjoins a ⊤ to the domain and codomain of a lattice_hom.

Equations
source
@[simp]
theorem lattice_hom.with_top_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
f.with_top.to_sup_hom = f.to_sup_hom.with_top
source
@[simp]
theorem lattice_hom.with_top_id {α : Type u_3} [lattice α] :
(lattice_hom.id α).with_top = lattice_hom.id (with_top α)
source
@[simp]
theorem lattice_hom.with_top_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g).with_top = f.with_top.comp g.with_top
source
@[simp]
theorem lattice_hom.with_bot_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
f.with_bot.to_sup_hom = ↑(f.to_sup_hom.with_bot)
source
@[protected]
def lattice_hom.with_bot {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
lattice_hom (with_bot α) (with_bot β)

Adjoins a ⊥ to the domain and codomain of a lattice_hom.

Equations
source
@[simp]
theorem lattice_hom.with_bot_id {α : Type u_3} [lattice α] :
(lattice_hom.id α).with_bot = lattice_hom.id (with_bot α)
source
@[simp]
theorem lattice_hom.with_bot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g).with_bot = f.with_bot.comp g.with_bot
source
@[simp]
theorem lattice_hom.with_top_with_bot_to_lattice_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
f.with_top_with_bot.to_lattice_hom = f.with_bot.with_top
source
def lattice_hom.with_top_with_bot {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] (f : lattice_hom α β) :
bounded_lattice_hom (with_top (with_bot α)) (with_top (with_bot β))

Adjoins a ⊤ and ⊥ to the domain and codomain of a lattice_hom.

Equations
source
@[simp]
theorem lattice_hom.with_top_with_bot_id {α : Type u_3} [lattice α] :
(lattice_hom.id α).with_top_with_bot = bounded_lattice_hom.id (with_top (with_bot α))
source
@[simp]
theorem lattice_hom.with_top_with_bot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :
(f.comp g).with_top_with_bot = f.with_top_with_bot.comp g.with_top_with_bot
source
def lattice_hom.with_top' {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [order_top β] (f : lattice_hom α β) :
lattice_hom (with_top α) β

Adjoins a ⊥ to the codomain of a lattice_hom.

Equations
source
@[simp]
theorem lattice_hom.with_top'_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [order_top β] (f : lattice_hom α β) :
f.with_top'.to_sup_hom = f.to_sup_hom.with_top'
source
@[simp]
theorem lattice_hom.with_bot'_to_sup_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [order_bot β] (f : lattice_hom α β) :
f.with_bot'.to_sup_hom = f.to_sup_hom.with_bot'.to_sup_hom
source
def lattice_hom.with_bot' {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [order_bot β] (f : lattice_hom α β) :
lattice_hom (with_bot α) β

Adjoins a ⊥ to the domain and codomain of a lattice_hom.

Equations
source
def lattice_hom.with_top_with_bot' {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order β] (f : lattice_hom α β) :
bounded_lattice_hom (with_top (with_bot α)) β

Adjoins a ⊤ and ⊥ to the codomain of a lattice_hom.

Equations
source
@[simp]
theorem lattice_hom.with_top_with_bot'_to_lattice_hom {α : Type u_3} {β : Type u_4} [lattice α] [lattice β] [bounded_order β] (f : lattice_hom α β) :
f.with_top_with_bot'.to_lattice_hom = f.with_bot'.with_top'