Complete lattice homomorphisms #
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 #
Sup_hom: Maps which preserve⨆.Inf_hom: Maps which preserve⨅.frame_hom: Frame homomorphisms. Maps which preserve⨆and⊓.complete_lattice_hom: Complete lattice homomorphisms. Maps which preserve⨆and⨅.
Typeclasses #
structure
frame_hom
(α : Type u_8)
(β : Type u_9)
[complete_lattice α]
[complete_lattice β] :
Type (max u_8 u_9)
- to_Sup_hom : Sup_hom α β
- map_inf' : ∀ (a b : α), self.to_Sup_hom.to_fun (a ⊓ b) = self.to_Sup_hom.to_fun a ⊓ self.to_Sup_hom.to_fun b
The type of frame homomorphisms from α to β. They preserve ⊓ and ⨆.
structure
complete_lattice_hom
(α : Type u_8)
(β : Type u_9)
[complete_lattice α]
[complete_lattice β] :
Type (max u_8 u_9)
- to_Sup_hom : Sup_hom α β
- map_Inf' : ∀ (s : set α), self.to_Sup_hom.to_fun (Inf s) = Inf (self.to_Sup_hom.to_fun '' s)
The type of complete lattice homomorphisms from α to β.
@[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.
@[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.
@[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.
@[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.
@[protected, instance]
def
Sup_hom_class.to_sup_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[Sup_hom_class F α β] :
sup_hom_class F α β
Equations
- Sup_hom_class.to_sup_hom_class = {to_fun_like := Sup_hom_class.to_fun_like _inst_3, map_sup := _}
@[protected, instance]
def
Sup_hom_class.to_bot_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[Sup_hom_class F α β] :
bot_hom_class F α β
Equations
- Sup_hom_class.to_bot_hom_class = {to_fun_like := Sup_hom_class.to_fun_like _inst_3, map_bot := _}
@[protected, instance]
def
Inf_hom_class.to_inf_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[Inf_hom_class F α β] :
inf_hom_class F α β
Equations
- Inf_hom_class.to_inf_hom_class = {to_fun_like := Inf_hom_class.to_fun_like _inst_3, map_inf := _}
@[protected, instance]
def
Inf_hom_class.to_top_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[Inf_hom_class F α β] :
top_hom_class F α β
Equations
- Inf_hom_class.to_top_hom_class = {to_fun_like := Inf_hom_class.to_fun_like _inst_3, map_top := _}
@[protected, instance]
def
frame_hom_class.to_lattice_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[frame_hom_class F α β] :
lattice_hom_class F α β
@[protected, instance]
def
complete_lattice_hom_class.to_Inf_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
[complete_lattice_hom_class F α β] :
Inf_hom_class F α β
@[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
@[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 α β] :
@[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 α β] :
@[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 α β] :
@[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 α β] :
@[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 α β)
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
- Sup_hom.Sup_hom_class = {to_fun_like := {coe := Sup_hom.to_fun _inst_2, coe_injective' := _}, map_Sup := _}
@[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.
@[protected, instance]
Equations
- Sup_hom.inhabited α = {default := Sup_hom.id α _inst_1}
@[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
@[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
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
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
- Inf_hom.Inf_hom_class = {to_fun_like := {coe := Inf_hom.to_fun _inst_2, coe_injective' := _}, map_Inf := _}
@[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.
@[protected, instance]
Equations
- Inf_hom.inhabited α = {default := Inf_hom.id α _inst_1}
@[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
@[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
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
Frame homomorphisms #
@[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_Sup_hom_class := {to_fun_like := {coe := λ (f : frame_hom α β), f.to_Sup_hom.to_fun, coe_injective' := _}, map_Sup := _}, map_inf := _}
@[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 = {coe := λ (f : frame_hom α β), f.to_Sup_hom.to_fun}
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 = {to_sup_hom := {to_fun := ⇑f, map_sup' := _}, map_inf' := _}
@[simp]
theorem
frame_hom.to_fun_eq_coe
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
{f : frame_hom α β} :
f.to_Sup_hom.to_fun = ⇑f
@[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.
@[protected]
Equations
- frame_hom.id α = {to_Sup_hom := {to_fun := (Sup_hom.id α).to_fun, map_Sup' := _}, map_inf' := _}
@[protected, instance]
Equations
- frame_hom.inhabited α = {default := frame_hom.id α _inst_1}
@[simp]
@[simp]
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_Sup_hom := {to_fun := (f.to_Sup_hom.comp g.to_Sup_hom).to_fun, map_Sup' := _}, map_inf' := _}
@[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 α β) :
@[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 : α) :
@[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 α β) :
@[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
@[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
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) :
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) :
@[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
@[protected, instance]
Equations
- frame_hom.has_bot = {bot := {to_Sup_hom := {to_fun := (inf_hom.const α ⊥).to_fun, map_Sup' := _}, map_inf' := _}}
@[protected, instance]
@[simp]
@[simp]
theorem
frame_hom.bot_apply
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
(a : α) :
Complete lattice homomorphisms #
def
complete_lattice_hom.to_Inf_hom
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β]
(f : complete_lattice_hom α β) :
Inf_hom α β
Reinterpret a complete_lattice_hom as an Inf_hom.
Equations
- f.to_Inf_hom = {to_fun := f.to_Sup_hom.to_fun, map_Inf' := _}
@[protected, instance]
def
complete_lattice_hom.complete_lattice_hom_class
{α : Type u_2}
{β : Type u_3}
[complete_lattice α]
[complete_lattice β] :
Equations
- complete_lattice_hom.complete_lattice_hom_class = {to_Sup_hom_class := {to_fun_like := {coe := λ (f : complete_lattice_hom α β), f.to_Sup_hom.to_fun, coe_injective' := _}, map_Sup := _}, map_Inf := _}
@[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 = {coe := λ (f : complete_lattice_hom α β), f.to_Sup_hom.to_fun}
@[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_Sup_hom.to_fun = ⇑f
@[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.
@[protected]
id as a complete_lattice_hom.
Equations
- complete_lattice_hom.id α = {to_Sup_hom := {to_fun := id α, map_Sup' := _}, map_Inf' := _}
@[protected, instance]
Equations
- complete_lattice_hom.inhabited α = {default := complete_lattice_hom.id α _inst_1}
@[simp]
@[simp]
theorem
complete_lattice_hom.id_apply
{α : Type u_2}
[complete_lattice α]
(a : α) :
⇑(complete_lattice_hom.id α) a = a
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 α β) :
Composition of complete_lattice_homs as a complete_lattice_hom.
Equations
- f.comp g = {to_Sup_hom := {to_fun := (f.to_Sup_hom.comp g.to_Sup_hom).to_fun, map_Sup' := _}, map_Inf' := _}
@[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 α β) :
@[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 : α) :
@[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 α β) :
@[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
@[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
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) :
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) :