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.

source
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
source
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
source
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
source
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
source
@[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
source
@[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 : α), β)
source
@[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 : α), β)
source
@[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
source
@[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
source
@[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 α β] :
inf_top_hom_class F α β
source
@[instance]
def complete_lattice_hom_class.to_Inf_hom_class (F : Type u_8) (α : out_param (Type u_9)) (β : out_param (Type u_10)) [complete_lattice α] [complete_lattice β] [self : complete_lattice_hom_class F α β] :
Inf_hom_class F α β
source
@[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
source
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)
source
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)
source
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)
source
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)
source
@[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 α β] :
sup_bot_hom_class F α β
Equations
source
@[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 α β] :
inf_top_hom_class F α β
Equations
source
@[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 α β] :
Sup_hom_class F α β
Equations
source
@[protected, instance]
def frame_hom_class.to_bounded_lattice_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [frame_hom_class F α β] :
bounded_lattice_hom_class F α β
Equations
source
@[protected, instance]
def complete_lattice_hom_class.to_frame_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [complete_lattice_hom_class F α β] :
frame_hom_class F α β
Equations
source
@[protected, instance]
def complete_lattice_hom_class.to_bounded_lattice_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [complete_lattice_hom_class F α β] :
bounded_lattice_hom_class F α β
Equations
source
@[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 α β] :
Sup_hom_class F α β
Equations
source
@[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 α β] :
Inf_hom_class F α β
Equations
source
@[protected, instance]
def order_iso_class.to_complete_lattice_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [order_iso_class F α β] :
complete_lattice_hom_class F α β
Equations
source
@[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
source
@[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
source
@[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 α β] :
has_coe_t F (frame_hom α β)
Equations
source
@[protected, instance]
def complete_lattice_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] [complete_lattice_hom_class F α β] :
has_coe_t F (complete_lattice_hom α β)
Equations

Supremum homomorphisms #

source
@[protected, instance]
def Sup_hom.Sup_hom_class {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] :
Sup_hom_class (Sup_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem Sup_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] {f : Sup_hom α β} :
f.to_fun = ⇑f
source
@[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
source
@[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
source
@[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'
source
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
source
@[protected]
def Sup_hom.id (α : Type u_2) [has_Sup α] :
Sup_hom α α

id as a Sup_hom.

Equations
source
@[protected, instance]
def Sup_hom.inhabited (α : Type u_2) [has_Sup α] :
inhabited (Sup_hom α α)
Equations
source
@[simp]
theorem Sup_hom.coe_id (α : Type u_2) [has_Sup α] :
⇑(Sup_hom.id α) = id
source
@[simp]
theorem Sup_hom.id_apply {α : Type u_2} [has_Sup α] (a : α) :
⇑(Sup_hom.id α) a = a
source
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
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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₂
source
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₂
source
@[protected, instance]
def Sup_hom.partial_order {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
partial_order (Sup_hom α β)
Equations
source
@[protected, instance]
def Sup_hom.has_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
has_bot (Sup_hom α β)
Equations
source
@[protected, instance]
def Sup_hom.order_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
order_bot (Sup_hom α β)
Equations
source
@[simp]
theorem Sup_hom.coe_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :
⇑⊥ = ⊥
source
@[simp]
theorem Sup_hom.bot_apply {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] (a : α) :
⇑⊥ a = ⊥

Infimum homomorphisms #

source
@[protected, instance]
def Inf_hom.Inf_hom_class {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] :
Inf_hom_class (Inf_hom α β) α β
Equations
source
@[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
source
@[simp]
theorem Inf_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] {f : Inf_hom α β} :
f.to_fun = ⇑f
source
@[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
source
@[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
source
@[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'
source
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
source
@[protected]
def Inf_hom.id (α : Type u_2) [has_Inf α] :
Inf_hom α α

id as an Inf_hom.

Equations
source
@[protected, instance]
def Inf_hom.inhabited (α : Type u_2) [has_Inf α] :
inhabited (Inf_hom α α)
Equations
source
@[simp]
theorem Inf_hom.coe_id (α : Type u_2) [has_Inf α] :
⇑(Inf_hom.id α) = id
source
@[simp]
theorem Inf_hom.id_apply {α : Type u_2} [has_Inf α] (a : α) :
⇑(Inf_hom.id α) a = a
source
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
source
@[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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
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₂
source
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₂
source
@[protected, instance]
def Inf_hom.partial_order {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
partial_order (Inf_hom α β)
Equations
source
@[protected, instance]
def Inf_hom.has_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
has_top (Inf_hom α β)
Equations
source
@[protected, instance]
def Inf_hom.order_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
order_top (Inf_hom α β)
Equations
source
@[simp]
theorem Inf_hom.coe_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :
⇑⊤ = ⊤
source
@[simp]
theorem Inf_hom.top_apply {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] (a : α) :
⇑⊤ a = ⊤

Frame homomorphisms #

source
@[protected, instance]
def frame_hom.frame_hom_class {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
frame_hom_class (frame_hom α β) α β
Equations
source
@[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
source
def frame_hom.to_lattice_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :
lattice_hom α β

Reinterpret a frame_hom as a lattice_hom.

Equations
source
@[simp]
theorem frame_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] {f : frame_hom α β} :
f.to_inf_top_hom.to_inf_hom.to_fun = ⇑f
source
@[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
source
@[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
source
@[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'
source
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
source
@[protected]
def frame_hom.id (α : Type u_2) [complete_lattice α] :
frame_hom α α

id as a frame_hom.

Equations
source
@[protected, instance]
def frame_hom.inhabited (α : Type u_2) [complete_lattice α] :
inhabited (frame_hom α α)
Equations
source
@[simp]
theorem frame_hom.coe_id (α : Type u_2) [complete_lattice α] :
⇑(frame_hom.id α) = id
source
@[simp]
theorem frame_hom.id_apply {α : Type u_2} [complete_lattice α] (a : α) :
⇑(frame_hom.id α) a = a
source
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
source
@[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
source
@[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)
source
@[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)
source
@[simp]
theorem frame_hom.comp_id {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :
f.comp (frame_hom.id α) = f
source
@[simp]
theorem frame_hom.id_comp {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : frame_hom α β) :
(frame_hom.id β).comp f = f
source
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₂
source
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₂
source
@[protected, instance]
def frame_hom.partial_order {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
partial_order (frame_hom α β)
Equations

Complete lattice homomorphisms #

source
@[protected, instance]
def complete_lattice_hom.complete_lattice_hom_class {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
complete_lattice_hom_class (complete_lattice_hom α β) α β
Equations
source
def complete_lattice_hom.to_Sup_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) :
Sup_hom α β

Reinterpret a complete_lattice_hom as a Sup_hom.

Equations
source
def complete_lattice_hom.to_bounded_lattice_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) :
bounded_lattice_hom α β

Reinterpret a complete_lattice_hom as a bounded_lattice_hom.

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

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

Equations
source
@[simp]
theorem complete_lattice_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] {f : complete_lattice_hom α β} :
f.to_Inf_hom.to_fun = ⇑f
source
@[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
source
@[protected]
def complete_lattice_hom.copy {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) (f' : α → β) (h : f' = ⇑f) :
complete_lattice_hom α β

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

Equations
source
@[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'
source
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
source
@[protected]
def complete_lattice_hom.id (α : Type u_2) [complete_lattice α] :
complete_lattice_hom α α

id as a complete_lattice_hom.

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

Composition of complete_lattice_homs as a complete_lattice_hom.

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

source
@[simp]
theorem Sup_hom.dual_symm_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Inf_hom αᵒᵈ βᵒᵈ) (ᾰ : α) :
⇑(⇑(Sup_hom.dual.symm) f) ᾰ = (⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual) ᾰ
source
@[protected]
def Sup_hom.dual {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] :
Sup_hom α β ≃ Inf_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem Sup_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) (ᾰ : αᵒᵈ) :
⇑(⇑Sup_hom.dual f) ᾰ = (⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual) ᾰ
source
@[simp]
theorem Sup_hom.dual_id {α : Type u_2} [has_Sup α] :
⇑Sup_hom.dual (Sup_hom.id α) = Inf_hom.id αᵒᵈ
source
@[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 α β) :
⇑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_2} [has_Sup α] :
⇑(Sup_hom.dual.symm) (Inf_hom.id αᵒᵈ) = Sup_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(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_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Sup_hom αᵒᵈ βᵒᵈ) (ᾰ : α) :
⇑(⇑(Inf_hom.dual.symm) f) ᾰ = (⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual) ᾰ
source
@[protected]
def Inf_hom.dual {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] :
Inf_hom α β ≃ Sup_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem Inf_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (ᾰ : αᵒᵈ) :
⇑(⇑Inf_hom.dual f) ᾰ = (⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual) ᾰ
source
@[simp]
theorem Inf_hom.dual_id {α : Type u_2} [has_Inf α] :
⇑Inf_hom.dual (Inf_hom.id α) = Sup_hom.id αᵒᵈ
source
@[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 α β) :
⇑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_2} [has_Inf α] :
⇑(Inf_hom.dual.symm) (Sup_hom.id αᵒᵈ) = Inf_hom.id α
source
@[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 αᵒᵈ βᵒᵈ) :
⇑(Inf_hom.dual.symm) (g.comp f) = (⇑(Inf_hom.dual.symm) g).comp (⇑(Inf_hom.dual.symm) f)
source
@[simp]
theorem complete_lattice_hom.dual_symm_apply_to_Inf_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom αᵒᵈ βᵒᵈ) :
(⇑(complete_lattice_hom.dual.symm) f).to_Inf_hom = ⇑Sup_hom.dual f.to_Sup_hom
source
@[protected]
def complete_lattice_hom.dual {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] :
complete_lattice_hom α β ≃ complete_lattice_hom αᵒᵈ βᵒᵈ

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

Equations
source
@[simp]
theorem complete_lattice_hom.dual_apply_to_Inf_hom {α : Type u_2} {β : Type u_3} [complete_lattice α] [complete_lattice β] (f : complete_lattice_hom α β) :
(⇑complete_lattice_hom.dual f).to_Inf_hom = ⇑Sup_hom.dual f.to_Sup_hom
source
@[simp]
theorem complete_lattice_hom.dual_id {α : Type u_2} [complete_lattice α] :
⇑complete_lattice_hom.dual (complete_lattice_hom.id α) = complete_lattice_hom.id αᵒᵈ
source
@[simp]
theorem complete_lattice_hom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (g : complete_lattice_hom β γ) (f : complete_lattice_hom α β) :
⇑complete_lattice_hom.dual (g.comp f) = (⇑complete_lattice_hom.dual g).comp (⇑complete_lattice_hom.dual f)
source
@[simp]
theorem complete_lattice_hom.symm_dual_id {α : Type u_2} [complete_lattice α] :
⇑(complete_lattice_hom.dual.symm) (complete_lattice_hom.id αᵒᵈ) = complete_lattice_hom.id α
source
@[simp]
theorem complete_lattice_hom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [complete_lattice α] [complete_lattice β] [complete_lattice γ] (g : complete_lattice_hom βᵒᵈ γᵒᵈ) (f : complete_lattice_hom αᵒᵈ βᵒᵈ) :
⇑(complete_lattice_hom.dual.symm) (g.comp f) = (⇑(complete_lattice_hom.dual.symm) g).comp (⇑(complete_lattice_hom.dual.symm) f)

Concrete homs #

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

set.preimage as a complete lattice homomorphism.

See also Sup_hom.set_image.

Equations
source
@[simp]
theorem complete_lattice_hom.coe_set_preimage {α : Type u_2} {β : Type u_3} (f : α → β) :
⇑(complete_lattice_hom.set_preimage f) = set.preimage f
source
@[simp]
theorem complete_lattice_hom.set_preimage_apply {α : Type u_2} {β : Type u_3} (f : α → β) (s : set β) :
⇑(complete_lattice_hom.set_preimage f) s = f ⁻¹' s
source
@[simp]
theorem complete_lattice_hom.set_preimage_id {α : Type u_2} :
complete_lattice_hom.set_preimage id = complete_lattice_hom.id (set α)
source
theorem complete_lattice_hom.set_preimage_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β → γ) (f : α → β) :
complete_lattice_hom.set_preimage (g ∘ f) = (complete_lattice_hom.set_preimage f).comp (complete_lattice_hom.set_preimage g)
source
theorem set.image_Sup {α : Type u_2} {β : Type u_3} {f : α → β} (s : set (set α)) :
f '' has_Sup.Sup s = has_Sup.Sup (set.image f '' s)
source
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
source
@[simp]
theorem Sup_hom.set_image_to_fun {α : Type u_2} {β : Type u_3} (f : α → β) (s : set α) :
⇑(Sup_hom.set_image f) s = f '' s
source
@[simp]
theorem equiv.to_order_iso_set_symm_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : set β) :
⇑(rel_iso.symm e.to_order_iso_set) s = ⇑(e.symm) '' s
source
@[simp]
theorem equiv.to_order_iso_set_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : set α) :
⇑(e.to_order_iso_set) s = ⇑e '' s
source
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
source
def sup_Sup_hom {α : Type u_2} [complete_lattice α] :
Sup_hom (α × α) α

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

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

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

Equations
source
@[simp, norm_cast]
theorem sup_Sup_hom_apply {α : Type u_2} [complete_lattice α] (x : α × α) :
⇑sup_Sup_hom x = x.fst ⊔ x.snd
source
@[simp, norm_cast]
theorem inf_Inf_hom_apply {α : Type u_2} [complete_lattice α] (x : α × α) :
⇑inf_Inf_hom x = x.fst ⊓ x.snd