mathlib3 documentation

order.hom.complete_lattice

Complete lattice homomorphisms #

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

This file defines frame homorphisms and complete 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 #

Concrete homs #

TODO #

Frame homs are Heyting homs.

structure Sup_hom (α : Type u_8) (β : Type u_9) [has_Sup α] [has_Sup β] :
Type (max u_8 u_9)

The type of -preserving functions from α to β.

Instances for Sup_hom
structure Inf_hom (α : Type u_8) (β : Type u_9) [has_Inf α] [has_Inf β] :
Type (max u_8 u_9)

The type of -preserving functions from α to β.

Instances for Inf_hom
structure frame_hom (α : Type u_8) (β : Type u_9) [complete_lattice α] [complete_lattice β] :
Type (max u_8 u_9)

The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.

Instances for frame_hom
structure complete_lattice_hom (α : Type u_8) (β : Type u_9) [complete_lattice α] [complete_lattice β] :
Type (max u_8 u_9)

The type of complete lattice homomorphisms from α to β.

Instances for complete_lattice_hom
@[class]
structure Sup_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [has_Sup α] [has_Sup β] :
Type (max u_10 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
@[instance]
def Sup_hom_class.to_fun_like (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [has_Sup α] [has_Sup β] [self : Sup_hom_class F α β] :
fun_like F α (λ (_x : α), β)
@[instance]
def Inf_hom_class.to_fun_like (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [has_Inf α] [has_Inf β] [self : Inf_hom_class F α β] :
fun_like F α (λ (_x : α), β)
@[class]
structure Inf_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [has_Inf α] [has_Inf β] :
Type (max u_10 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 frame_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [complete_lattice α] [complete_lattice β] :
Type (max u_10 u_8 u_9)

frame_hom_class F α β states that F is a type of frame morphisms. They preserve and .

You should extend this class when you extend frame_hom.

Instances of this typeclass
Instances of other typeclasses for frame_hom_class
  • frame_hom_class.has_sizeof_inst
@[instance]
def frame_hom_class.to_inf_top_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [complete_lattice α] [complete_lattice β] [self : frame_hom_class F α β] :
@[instance]
@[class]
structure complete_lattice_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [complete_lattice α] [complete_lattice β] :
Type (max u_10 u_8 u_9)

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

You should extend this class when you extend complete_lattice_hom.

Instances of this typeclass
Instances of other typeclasses for complete_lattice_hom_class
  • complete_lattice_hom_class.has_sizeof_inst
theorem map_supr {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [has_Sup α] [has_Sup β] [Sup_hom_class F α β] (f : F) (g : ι α) :
f ( (i : ι), g i) = (i : ι), f (g i)
theorem map_supr₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι Sort u_7} [has_Sup α] [has_Sup β] [Sup_hom_class F α β] (f : F) (g : Π (i : ι), κ i α) :
f ( (i : ι) (j : κ i), g i j) = (i : ι) (j : κ i), f (g i j)
theorem map_infi {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [has_Inf α] [has_Inf β] [Inf_hom_class F α β] (f : F) (g : ι α) :
f ( (i : ι), g i) = (i : ι), f (g i)
theorem map_infi₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι Sort u_7} [has_Inf α] [has_Inf β] [Inf_hom_class F α β] (f : F) (g : Π (i : ι), κ i α) :
f ( (i : ι) (j : κ i), g i j) = (i : ι) (j : κ i), f (g i j)
@[protected, instance]
def Sup_hom_class.to_sup_bot_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [Sup_hom_class F α β] :
Equations
@[protected, instance]
def Inf_hom_class.to_inf_top_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [Inf_hom_class F α β] :
Equations
@[protected, instance]
def frame_hom_class.to_Sup_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [frame_hom_class F α β] :
Equations
@[protected, instance]
def order_iso_class.to_Sup_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [order_iso_class F α β] :
Equations
@[protected, instance]
def order_iso_class.to_Inf_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [order_iso_class F α β] :
Equations
@[protected, instance]
def Sup_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [has_Inf α] [has_Inf β] [Inf_hom_class F α β] :
has_coe_t F (Inf_hom α β)
Equations
@[protected, instance]
def frame_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [frame_hom_class F α β] :
Equations
@[protected, instance]
Equations

Supremum homomorphisms #

@[protected, instance]
def Sup_hom.Sup_hom_class {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] :
Sup_hom_class (Sup_hom α β) α β
Equations
@[protected, instance]
def Sup_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [has_Sup α] [has_Sup β] {f : Sup_hom α β} :
@[ext]
theorem Sup_hom.ext {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] {f g : Sup_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def Sup_hom.copy {α : Type u_2} {β : Type u_3} [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
@[simp]
theorem Sup_hom.coe_copy {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem Sup_hom.copy_eq {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def Sup_hom.id (α : Type u_2) [has_Sup α] :
Sup_hom α α

id as a Sup_hom.

Equations
@[protected, instance]
def Sup_hom.inhabited (α : Type u_2) [has_Sup α] :
Equations
@[simp]
theorem Sup_hom.coe_id (α : Type u_2) [has_Sup α] :
@[simp]
theorem Sup_hom.id_apply {α : Type u_2} [has_Sup α] (a : α) :
(Sup_hom.id α) a = a
def Sup_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [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_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) :
f.comp (Sup_hom.id α) = f
@[simp]
theorem Sup_hom.id_comp {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) :
(Sup_hom.id β).comp f = f
theorem Sup_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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₂
@[protected, instance]
def Sup_hom.partial_order {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
Equations
@[protected, instance]
def Sup_hom.has_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
Equations
@[protected, instance]
def Sup_hom.order_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
Equations
@[simp]
theorem Sup_hom.coe_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
@[simp]
theorem Sup_hom.bot_apply {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] (a : α) :

Infimum homomorphisms #

@[protected, instance]
def Inf_hom.Inf_hom_class {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] :
Inf_hom_class (Inf_hom α β) α β
Equations
@[protected, instance]
def Inf_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [has_Inf α] [has_Inf β] {f : Inf_hom α β} :
@[ext]
theorem Inf_hom.ext {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] {f g : Inf_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def Inf_hom.copy {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (f' : α β) (h : f' = f) :
Inf_hom α β

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

Equations
@[simp]
theorem Inf_hom.coe_copy {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem Inf_hom.copy_eq {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def Inf_hom.id (α : Type u_2) [has_Inf α] :
Inf_hom α α

id as an Inf_hom.

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

Composition of Inf_homs as a Inf_hom.

Equations
@[simp]
theorem Inf_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [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_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) :
f.comp (Inf_hom.id α) = f
@[simp]
theorem Inf_hom.id_comp {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) :
(Inf_hom.id β).comp f = f
theorem Inf_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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₂
@[protected, instance]
def Inf_hom.partial_order {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
Equations
@[protected, instance]
def Inf_hom.has_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
Equations
@[protected, instance]
def Inf_hom.order_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
Equations
@[simp]
theorem Inf_hom.coe_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
@[simp]
theorem Inf_hom.top_apply {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] (a : α) :

Frame homomorphisms #

@[protected, instance]
def frame_hom.frame_hom_class {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
Equations
@[protected, instance]
def frame_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
has_coe_to_fun (frame_hom α β) (λ (_x : frame_hom α β), α β)

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

Equations
def frame_hom.to_lattice_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :

Reinterpret a frame_hom as a lattice_hom.

Equations
@[simp]
@[ext]
theorem frame_hom.ext {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] {f g : frame_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def frame_hom.copy {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) (f' : α β) (h : f' = f) :
frame_hom α β

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

Equations
@[simp]
theorem frame_hom.coe_copy {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem frame_hom.copy_eq {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected]
def frame_hom.id (α : Type u_2) [complete_lattice α] :
frame_hom α α

id as a frame_hom.

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

Composition of frame_homs as a frame_hom.

Equations
@[simp]
theorem frame_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (f : frame_hom β γ) (g : frame_hom α β) :
(f.comp g) = f g
@[simp]
theorem frame_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (f : frame_hom β γ) (g : frame_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem frame_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [complete_lattice α] [complete_lattice β] [complete_lattice γ] [complete_lattice δ] (f : frame_hom γ δ) (g : frame_hom β γ) (h : frame_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem frame_hom.comp_id {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :
@[simp]
theorem frame_hom.id_comp {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :
theorem frame_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {g₁ g₂ : frame_hom β γ} {f : frame_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem frame_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {g : frame_hom β γ} {f₁ f₂ : frame_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
Equations

Complete lattice homomorphisms #

Reinterpret a complete_lattice_hom as a Sup_hom.

Equations
@[protected, instance]

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

Equations
@[ext]
theorem complete_lattice_hom.ext {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] {f g : complete_lattice_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def complete_lattice_hom.copy {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) (f' : α β) (h : f' = f) :

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

Equations
@[simp]
theorem complete_lattice_hom.coe_copy {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem complete_lattice_hom.copy_eq {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[simp]
theorem complete_lattice_hom.id_apply {α : Type u_2} [complete_lattice α] (a : α) :
@[simp]
theorem complete_lattice_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (f : complete_lattice_hom β γ) (g : complete_lattice_hom α β) :
(f.comp g) = f g
@[simp]
theorem complete_lattice_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (f : complete_lattice_hom β γ) (g : complete_lattice_hom α β) (a : α) :
(f.comp g) a = f (g a)
@[simp]
theorem complete_lattice_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [complete_lattice α] [complete_lattice β] [complete_lattice γ] [complete_lattice δ] (f : complete_lattice_hom γ δ) (g : complete_lattice_hom β γ) (h : complete_lattice_hom α β) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
@[simp]
theorem complete_lattice_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {g₁ g₂ : complete_lattice_hom β γ} {f : complete_lattice_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem complete_lattice_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] {g : complete_lattice_hom β γ} {f₁ f₂ : complete_lattice_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂

Dual homs #

@[simp]
theorem Sup_hom.dual_symm_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Inf_hom αᵒᵈ βᵒᵈ) (ᾰ : α) :
@[protected]
def Sup_hom.dual {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] :

Reinterpret a -homomorphism as an -homomorphism between the dual orders.

Equations
@[simp]
theorem Sup_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) (ᾰ : αᵒᵈ) :
@[simp]
@[simp]
theorem Sup_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_Sup α] [has_Sup β] [has_Sup γ] (g : Sup_hom β γ) (f : Sup_hom α β) :
@[simp]
theorem Sup_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_Sup α] [has_Sup β] [has_Sup γ] (g : Inf_hom βᵒᵈ γᵒᵈ) (f : Inf_hom αᵒᵈ βᵒᵈ) :
@[simp]
theorem Inf_hom.dual_symm_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Sup_hom αᵒᵈ βᵒᵈ) (ᾰ : α) :
@[protected]
def Inf_hom.dual {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] :

Reinterpret an -homomorphism as a -homomorphism between the dual orders.

Equations
@[simp]
theorem Inf_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (ᾰ : αᵒᵈ) :
@[simp]
@[simp]
theorem Inf_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_Inf α] [has_Inf β] [has_Inf γ] (g : Inf_hom β γ) (f : Inf_hom α β) :
@[simp]
theorem Inf_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_Inf α] [has_Inf β] [has_Inf γ] (g : Sup_hom βᵒᵈ γᵒᵈ) (f : Sup_hom αᵒᵈ βᵒᵈ) :
@[protected]

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

Equations

Concrete homs #

def complete_lattice_hom.set_preimage {α : Type u_2} {β : Type u_3} (f : α β) :

set.preimage as a complete lattice homomorphism.

See also Sup_hom.set_image.

Equations
@[simp]
theorem complete_lattice_hom.set_preimage_apply {α : Type u_2} {β : Type u_3} (f : α β) (s : set β) :
theorem set.image_Sup {α : Type u_2} {β : Type u_3} {f : α β} (s : set (set α)) :
def Sup_hom.set_image {α : Type u_2} {β : Type u_3} (f : α β) :
Sup_hom (set α) (set β)

Using set.image, a function between types yields a Sup_hom between their lattices of subsets.

See also complete_lattice_hom.set_preimage.

Equations
@[simp]
theorem Sup_hom.set_image_to_fun {α : Type u_2} {β : Type u_3} (f : α β) (s : set α) :
@[simp]
theorem equiv.to_order_iso_set_symm_apply {α : Type u_2} {β : Type u_3} (e : α β) (s : set β) :
@[simp]
theorem equiv.to_order_iso_set_apply {α : Type u_2} {β : Type u_3} (e : α β) (s : set α) :
def equiv.to_order_iso_set {α : Type u_2} {β : Type u_3} (e : α β) :
set α ≃o set β

An equivalence of types yields an order isomorphism between their lattices of subsets.

Equations
def sup_Sup_hom {α : Type u_2} [complete_lattice α] :
Sup_hom × α) α

The map (a, b) ↦ a ⊔ b as a Sup_hom.

Equations
def inf_Inf_hom {α : Type u_2} [complete_lattice α] :
Inf_hom × α) α

The map (a, b) ↦ a ⊓ b as an Inf_hom.

Equations
@[simp, norm_cast]
theorem sup_Sup_hom_apply {α : Type u_2} [complete_lattice α] (x : α × α) :
@[simp, norm_cast]
theorem inf_Inf_hom_apply {α : Type u_2} [complete_lattice α] (x : α × α) :