order.hom.complete_lattice

source

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

Type (max u_8 u_9)

to_fun : α → β
map_Sup' : ∀ (s : set α), self.to_fun (Sup s) = Sup (self.to_fun '' s)

The type of ⨆-preserving functions from α to β.

source

structure Inf_hom (α : Type u_8) (β : Type u_9) [has_Inf α] [has_Inf β] :

Type (max u_8 u_9)

to_fun : α → β
map_Inf' : ∀ (s : set α), self.to_fun (Inf s) = Inf (self.to_fun '' s)

The type of ⨅-preserving functions from α to β.

source

structure frame_hom (α : Type u_8) (β : Type u_9) [complete_lattice α] [complete_lattice β] :

Type (max u_8 u_9)

to_inf_top_hom : inf_top_hom α β
map_Sup' : ∀ (s : set α), self.to_inf_top_hom.to_inf_hom.to_fun (Sup s) = Sup (self.to_inf_top_hom.to_inf_hom.to_fun '' s)

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

source

structure complete_lattice_hom (α : Type u_8) (β : Type u_9) [complete_lattice α] [complete_lattice β] :

Type (max u_8 u_9)

to_Inf_hom : Inf_hom α β
map_Sup' : ∀ (s : set α), self.to_Inf_hom.to_fun (Sup s) = Sup (self.to_Inf_hom.to_fun '' s)

The type of complete lattice homomorphisms from α to β.

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)

to_fun_like : fun_like F α (λ (_x : α), β)
map_Sup : ∀ (f : F) (s : set α), ⇑f (Sup s) = Sup (⇑f '' s)

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

You should extend this class when you extend Sup_hom.

Instances

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)

to_fun_like : fun_like F α (λ (_x : α), β)
map_Inf : ∀ (f : F) (s : set α), ⇑f (Inf s) = Inf (⇑f '' s)

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

You should extend this class when you extend Inf_hom.

Instances

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)

to_inf_top_hom_class : inf_top_hom_class F α β
map_Sup : ∀ (f : F) (s : set α), ⇑f (Sup s) = Sup (⇑f '' s)

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

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)

to_Inf_hom_class : Inf_hom_class F α β
map_Sup : ∀ (f : F) (s : set α), ⇑f (Sup s) = Sup (⇑f '' s)

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

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

Sup_hom_class.to_sup_bot_hom_class = {to_sup_hom_class := {to_fun_like := Sup_hom_class.to_fun_like _inst_3, map_sup := _}, map_bot := _}

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

Inf_hom_class.to_inf_top_hom_class = {to_inf_hom_class := {to_fun_like := Inf_hom_class.to_fun_like _inst_3, map_inf := _}, map_top := _}

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

frame_hom_class.to_Sup_hom_class = {to_fun_like := inf_hom_class.to_fun_like inf_top_hom_class.to_inf_hom_class, map_Sup := _}

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

frame_hom_class.to_bounded_lattice_hom_class = {to_lattice_hom_class := {to_sup_hom_class := sup_bot_hom_class.to_sup_hom_class Sup_hom_class.to_sup_bot_hom_class, map_inf := _}, map_top := _, map_bot := _}

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

complete_lattice_hom_class.to_frame_hom_class = {to_inf_top_hom_class := {to_inf_hom_class := inf_top_hom_class.to_inf_hom_class Inf_hom_class.to_inf_top_hom_class, map_top := _}, map_Sup := _}

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

complete_lattice_hom_class.to_bounded_lattice_hom_class = {to_lattice_hom_class := {to_sup_hom_class := sup_bot_hom_class.to_sup_hom_class Sup_hom_class.to_sup_bot_hom_class, map_inf := _}, map_top := _, map_bot := _}

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

order_iso_class.to_Sup_hom_class = {to_fun_like := inf_hom_class.to_fun_like order_iso_class.to_inf_hom_class, map_Sup := _}

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

order_iso_class.to_Inf_hom_class = {to_fun_like := Sup_hom_class.to_fun_like order_iso_class.to_Sup_hom_class, map_Inf := _}

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

order_iso_class.to_complete_lattice_hom_class = {to_Inf_hom_class := order_iso_class.to_Inf_hom_class _inst_3, map_Sup := _}

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

Sup_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_Sup' := _}}

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

Inf_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_Inf' := _}}

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

frame_hom.has_coe_t = {coe := λ (f : F), {to_inf_top_hom := ↑f, map_Sup' := _}}

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

complete_lattice_hom.has_coe_t = {coe := λ (f : F), {to_Inf_hom := ↑f, map_Sup' := _}}

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

Sup_hom.Sup_hom_class = {to_fun_like := {coe := Sup_hom.to_fun _inst_2, coe_injective' := _}, map_Sup := _}

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

Sup_hom.has_coe_to_fun = fun_like.has_coe_to_fun

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

f.copy f' h = {to_fun := f', map_Sup' := _}

source

@[protected]

def Sup_hom.id (α : Type u_2) [has_Sup α] :

Sup_hom α α

id as a Sup_hom.

Equations

Sup_hom.id α = {to_fun := id α, map_Sup' := _}

source

@[protected, instance]

def Sup_hom.inhabited (α : Type u_2) [has_Sup α] :

inhabited (Sup_hom α α)

Equations

Sup_hom.inhabited α = {default := Sup_hom.id α _inst_1}

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

f.comp g = {to_fun := ⇑f ∘ ⇑g, map_Sup' := _}

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

Sup_hom.partial_order = partial_order.lift coe_fn Sup_hom.partial_order._proof_1

source

@[protected, instance]

def Sup_hom.has_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :

has_bot (Sup_hom α β)

Equations

Sup_hom.has_bot = {bot := {to_fun := λ (_x : α), ⊥, map_Sup' := _}}

source

@[protected, instance]

def Sup_hom.order_bot {α : Type u_2} {β : Type u_3} [has_Sup α] [complete_lattice β] :

order_bot (Sup_hom α β)

Equations

Sup_hom.order_bot = {bot := ⊥, bot_le := _}

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 = ⊥

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

Inf_hom.Inf_hom_class = {to_fun_like := {coe := Inf_hom.to_fun _inst_2, coe_injective' := _}, map_Inf := _}

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

Inf_hom.has_coe_to_fun = fun_like.has_coe_to_fun

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

f.copy f' h = {to_fun := f', map_Inf' := _}

source

@[protected]

def Inf_hom.id (α : Type u_2) [has_Inf α] :

Inf_hom α α

id as an Inf_hom.

Equations

Inf_hom.id α = {to_fun := id α, map_Inf' := _}

source

@[protected, instance]

def Inf_hom.inhabited (α : Type u_2) [has_Inf α] :

inhabited (Inf_hom α α)

Equations

Inf_hom.inhabited α = {default := Inf_hom.id α _inst_1}

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

f.comp g = {to_fun := ⇑f ∘ ⇑g, map_Inf' := _}

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

Inf_hom.partial_order = partial_order.lift coe_fn Inf_hom.partial_order._proof_1

source

@[protected, instance]

def Inf_hom.has_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :

has_top (Inf_hom α β)

Equations

Inf_hom.has_top = {top := {to_fun := λ (_x : α), ⊤, map_Inf' := _}}

source

@[protected, instance]

def Inf_hom.order_top {α : Type u_2} {β : Type u_3} [has_Inf α] [complete_lattice β] :

order_top (Inf_hom α β)

Equations

Inf_hom.order_top = {top := ⊤, le_top := _}

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 = ⊤

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

frame_hom.frame_hom_class = {to_inf_top_hom_class := {to_inf_hom_class := {to_fun_like := {coe := λ (f : frame_hom α β), f.to_inf_top_hom.to_inf_hom.to_fun, coe_injective' := _}, map_inf := _}, map_top := _}, map_Sup := _}

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

frame_hom.has_coe_to_fun = fun_like.has_coe_to_fun

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

f.to_lattice_hom = ↑f

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

f.copy f' h = {to_inf_top_hom := f.to_inf_top_hom.copy f' h, map_Sup' := _}

source

@[protected]

def frame_hom.id (α : Type u_2) [complete_lattice α] :

frame_hom α α

id as a frame_hom.

Equations

frame_hom.id α = {to_inf_top_hom := inf_top_hom.id α (complete_lattice.to_has_top α), map_Sup' := _}

source

@[protected, instance]

def frame_hom.inhabited (α : Type u_2) [complete_lattice α] :

inhabited (frame_hom α α)

Equations

frame_hom.inhabited α = {default := frame_hom.id α _inst_1}

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

f.comp g = {to_inf_top_hom := f.to_inf_top_hom.comp g.to_inf_top_hom, map_Sup' := _}

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

frame_hom.partial_order = partial_order.lift coe_fn frame_hom.partial_order._proof_1

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

complete_lattice_hom.complete_lattice_hom_class = {to_Inf_hom_class := {to_fun_like := {coe := λ (f : complete_lattice_hom α β), f.to_Inf_hom.to_fun, coe_injective' := _}, map_Inf := _}, map_Sup := _}

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

f.to_Sup_hom = ↑f

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

f.to_bounded_lattice_hom = ↑f

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

complete_lattice_hom.has_coe_to_fun = fun_like.has_coe_to_fun

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

f.copy f' h = {to_Inf_hom := f.to_Inf_hom.copy f' h, map_Sup' := _}

source

@[protected]

def complete_lattice_hom.id (α : Type u_2) [complete_lattice α] :

complete_lattice_hom α α

id as a complete_lattice_hom.

Equations

complete_lattice_hom.id α = {to_Inf_hom := {to_fun := id α, map_Inf' := _}, map_Sup' := _}

source

@[protected, instance]

def complete_lattice_hom.inhabited (α : Type u_2) [complete_lattice α] :

inhabited (complete_lattice_hom α α)

Equations

complete_lattice_hom.inhabited α = {default := complete_lattice_hom.id α _inst_1}

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

f.comp g = {to_Inf_hom := f.to_Inf_hom.comp g.to_Inf_hom, map_Sup' := _}

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₂

source

@[simp]

theorem Sup_hom.dual_symm_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Inf_hom (order_dual α) (order_dual β)) (ᾰ : α) :

⇑(⇑(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 (order_dual α) (order_dual β)

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

Equations

Sup_hom.dual = {to_fun := λ (f : Sup_hom α β), {to_fun := ⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual, map_Inf' := _}, inv_fun := λ (f : Inf_hom (order_dual α) (order_dual β)), {to_fun := ⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual, map_Sup' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem Sup_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Sup α] [has_Sup β] (f : Sup_hom α β) (ᾰ : order_dual α) :

⇑(⇑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 (order_dual α)

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 (order_dual α)) = 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 (order_dual β) (order_dual γ)) (f : Inf_hom (order_dual α) (order_dual β)) :

⇑(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 (order_dual α) (order_dual β)) (ᾰ : α) :

⇑(⇑(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 (order_dual α) (order_dual β)

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

Equations

Inf_hom.dual = {to_fun := λ (f : Inf_hom α β), {to_fun := ⇑order_dual.to_dual ∘ ⇑f ∘ ⇑order_dual.of_dual, map_Sup' := _}, inv_fun := λ (f : Sup_hom (order_dual α) (order_dual β)), {to_fun := ⇑order_dual.of_dual ∘ ⇑f ∘ ⇑order_dual.to_dual, map_Inf' := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem Inf_hom.dual_apply_to_fun {α : Type u_2} {β : Type u_3} [has_Inf α] [has_Inf β] (f : Inf_hom α β) (ᾰ : order_dual α) :

⇑(⇑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 (order_dual α)

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 (order_dual α)) = 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 (order_dual β) (order_dual γ)) (f : Sup_hom (order_dual α) (order_dual β)) :

⇑(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 (order_dual α) (order_dual β)) :

(⇑(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 (order_dual α) (order_dual β)

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

Equations

complete_lattice_hom.dual = {to_fun := λ (f : complete_lattice_hom α β), {to_Inf_hom := ⇑Sup_hom.dual f.to_Sup_hom, map_Sup' := _}, inv_fun := λ (f : complete_lattice_hom (order_dual α) (order_dual β)), {to_Inf_hom := ⇑Sup_hom.dual f.to_Sup_hom, map_Sup' := _}, left_inv := _, right_inv := _}

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 (order_dual α)

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 (order_dual α)) = 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 (order_dual β) (order_dual γ)) (f : complete_lattice_hom (order_dual α) (order_dual β)) :

⇑(complete_lattice_hom.dual.symm) (g.comp f) = (⇑(complete_lattice_hom.dual.symm) g).comp (⇑(complete_lattice_hom.dual.symm) f)

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.

Equations

complete_lattice_hom.set_preimage f = {to_Inf_hom := {to_fun := set.preimage f, map_Inf' := _}, map_Sup' := _}

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)

mathlib documentation

Complete lattice homomorphisms #

Types of morphisms #

Typeclasses #

Concrete homs #

Supremum homomorphisms #

Infimum homomorphisms #

Frame homomorphisms #

Complete lattice homomorphisms #

Dual homs #

Concrete homs #