Lattice homomorphisms #
This file defines (bounded) lattice homomorphisms.
We use the fun_like design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
sup_hom: Maps which preserve⊔.inf_hom: Maps which preserve⊓.sup_bot_hom: Finitary supremum homomorphisms. Maps which preserve⊔and⊥.inf_top_hom: Finitary infimum homomorphisms. Maps which preserve⊓and⊤.lattice_hom: Lattice homomorphisms. Maps which preserve⊔and⊓.bounded_lattice_hom: Bounded lattice homomorphisms. Maps which preserve⊤,⊥,⊔and⊓.
Typeclasses #
sup_hom_classinf_hom_classsup_bot_hom_classinf_top_hom_classlattice_hom_classbounded_lattice_hom_class
TODO #
Do we need more intersections between bot_hom, top_hom and lattice homomorphisms?
- 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 lattice homomorphisms from α to β.
structure
bounded_lattice_hom
(α : Type u_7)
(β : Type u_8)
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β] :
Type (max u_7 u_8)
- to_lattice_hom : lattice_hom α β
- map_top' : self.to_lattice_hom.to_sup_hom.to_fun ⊤ = ⊤
- map_bot' : self.to_lattice_hom.to_sup_hom.to_fun ⊥ = ⊥
The type of bounded lattice homomorphisms from α to β.
@[class]
structure
sup_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[has_sup α]
[has_sup β] :
Type (max u_7 u_8 u_9)
sup_hom_class F α β states that F is a type of ⊔-preserving morphisms.
You should extend this class when you extend sup_hom.
@[class]
structure
inf_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[has_inf α]
[has_inf β] :
Type (max u_7 u_8 u_9)
inf_hom_class F α β states that F is a type of ⊓-preserving morphisms.
You should extend this class when you extend inf_hom.
@[class]
structure
sup_bot_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[has_sup α]
[has_sup β]
[has_bot α]
[has_bot β] :
Type (max u_7 u_8 u_9)
- to_sup_hom_class : sup_hom_class F α β
- map_bot : ∀ (f : F), ⇑f ⊥ = ⊥
sup_bot_hom_class F α β states that F is a type of finitary supremum-preserving morphisms.
You should extend this class when you extend sup_bot_hom.
@[class]
structure
inf_top_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[has_inf α]
[has_inf β]
[has_top α]
[has_top β] :
Type (max u_7 u_8 u_9)
- to_inf_hom_class : inf_hom_class F α β
- map_top : ∀ (f : F), ⇑f ⊤ = ⊤
inf_top_hom_class F α β states that F is a type of finitary infimum-preserving morphisms.
You should extend this class when you extend sup_bot_hom.
@[class]
structure
lattice_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[lattice α]
[lattice β] :
Type (max u_7 u_8 u_9)
lattice_hom_class F α β states that F is a type of lattice morphisms.
You should extend this class when you extend lattice_hom.
@[class]
structure
bounded_lattice_hom_class
(F : Type u_7)
(α : out_param (Type u_8))
(β : out_param (Type u_9))
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β] :
Type (max u_7 u_8 u_9)
- to_lattice_hom_class : lattice_hom_class F α β
- map_top : ∀ (f : F), ⇑f ⊤ = ⊤
- map_bot : ∀ (f : F), ⇑f ⊥ = ⊥
bounded_lattice_hom_class F α β states that F is a type of bounded lattice morphisms.
You should extend this class when you extend bounded_lattice_hom.
@[protected, instance]
def
sup_hom_class.to_order_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[semilattice_sup β]
[sup_hom_class F α β] :
order_hom_class F α β
Equations
- sup_hom_class.to_order_hom_class = {to_fun_like := sup_hom_class.to_fun_like _inst_3, map_rel := _}
@[protected, instance]
def
inf_hom_class.to_order_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[semilattice_inf β]
[inf_hom_class F α β] :
order_hom_class F α β
Equations
- inf_hom_class.to_order_hom_class = {to_fun_like := inf_hom_class.to_fun_like _inst_3, map_rel := _}
@[protected, instance]
def
sup_bot_hom_class.to_bot_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
[has_bot α]
[has_bot β]
[sup_bot_hom_class F α β] :
bot_hom_class F α β
@[protected, instance]
def
inf_top_hom_class.to_top_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
[has_top α]
[has_top β]
[inf_top_hom_class F α β] :
top_hom_class F α β
@[protected, instance]
def
lattice_hom_class.to_inf_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[lattice_hom_class F α β] :
inf_hom_class F α β
@[protected, instance]
def
bounded_lattice_hom_class.to_sup_bot_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
[bounded_lattice_hom_class F α β] :
sup_bot_hom_class F α β
@[protected, instance]
def
bounded_lattice_hom_class.to_inf_top_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
[bounded_lattice_hom_class F α β] :
inf_top_hom_class F α β
@[protected, instance]
def
bounded_lattice_hom_class.to_bounded_order_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
[bounded_lattice_hom_class F α β] :
bounded_order_hom_class F α β
@[protected, instance]
def
order_iso_class.to_sup_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[semilattice_sup β]
[order_iso_class F α β] :
sup_hom_class F α β
@[protected, instance]
def
order_iso_class.to_inf_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[semilattice_inf β]
[order_iso_class F α β] :
inf_hom_class F α β
@[protected, instance]
def
order_iso_class.to_sup_bot_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[order_bot α]
[semilattice_sup β]
[order_bot β]
[order_iso_class F α β] :
sup_bot_hom_class F α β
Equations
@[protected, instance]
def
order_iso_class.to_inf_top_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[order_top α]
[semilattice_inf β]
[order_top β]
[order_iso_class F α β] :
inf_top_hom_class F α β
Equations
@[protected, instance]
def
order_iso_class.to_lattice_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[order_iso_class F α β] :
lattice_hom_class F α β
Equations
@[protected, instance]
def
order_iso_class.to_bounded_lattice_hom_class
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
[order_iso_class F α β] :
Equations
@[simp]
theorem
map_finset_sup
{F : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[semilattice_sup α]
[order_bot α]
[semilattice_sup β]
[order_bot β]
[sup_bot_hom_class F α β]
(f : F)
(s : finset ι)
(g : ι → α) :
@[simp]
theorem
map_finset_inf
{F : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[semilattice_inf α]
[order_top α]
[semilattice_inf β]
[order_top β]
[inf_top_hom_class F α β]
(f : F)
(s : finset ι)
(g : ι → α) :
theorem
disjoint.map
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
[bounded_lattice_hom_class F α β]
(f : F)
{a b : α}
(h : disjoint a b) :
theorem
is_compl.map
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
[bounded_lattice_hom_class F α β]
(f : F)
{a b : α}
(h : is_compl a b) :
theorem
map_compl
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[boolean_algebra α]
[boolean_algebra β]
[bounded_lattice_hom_class F α β]
(f : F)
(a : α) :
theorem
map_sdiff
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[boolean_algebra α]
[boolean_algebra β]
[bounded_lattice_hom_class F α β]
(f : F)
(a b : α) :
theorem
map_symm_diff
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[boolean_algebra α]
[boolean_algebra β]
[bounded_lattice_hom_class F α β]
(f : F)
(a b : α) :
@[protected, instance]
def
sup_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
[sup_hom_class F α β] :
@[protected, instance]
def
inf_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
[inf_hom_class F α β] :
@[protected, instance]
def
sup_bot_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
[has_bot α]
[has_bot β]
[sup_bot_hom_class F α β] :
has_coe_t F (sup_bot_hom α β)
Equations
- sup_bot_hom.has_coe_t = {coe := λ (f : F), {to_sup_hom := ↑f, map_bot' := _}}
@[protected, instance]
def
inf_top_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
[has_top α]
[has_top β]
[inf_top_hom_class F α β] :
has_coe_t F (inf_top_hom α β)
Equations
- inf_top_hom.has_coe_t = {coe := λ (f : F), {to_inf_hom := ↑f, map_top' := _}}
@[protected, instance]
def
lattice_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[lattice_hom_class F α β] :
has_coe_t F (lattice_hom α β)
@[protected, instance]
def
bounded_lattice_hom.has_coe_t
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
[bounded_lattice_hom_class F α β] :
has_coe_t F (bounded_lattice_hom α β)
Equations
- bounded_lattice_hom.has_coe_t = {coe := λ (f : F), {to_lattice_hom := {to_sup_hom := {to_fun := ⇑f, map_sup' := _}, map_inf' := _}, map_top' := _, map_bot' := _}}
Supremum homomorphisms #
@[protected, instance]
def
sup_hom.sup_hom_class
{α : Type u_3}
{β : Type u_4}
[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_3}
{β : Type u_4}
[has_sup α]
[has_sup β] :
has_coe_to_fun (sup_hom α β) (λ (_x : sup_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[protected, instance]
Equations
- sup_hom.inhabited α = {default := sup_hom.id α _inst_1}
@[simp]
theorem
sup_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
(f : sup_hom α β) :
f.comp (sup_hom.id α) = f
@[simp]
theorem
sup_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
(f : sup_hom α β) :
(sup_hom.id β).comp f = f
def
sup_hom.const
(α : Type u_3)
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
(b : β) :
sup_hom α β
The constant function as a sup_hom.
Equations
- sup_hom.const α b = {to_fun := λ (_x : α), b, map_sup' := _}
@[simp]
theorem
sup_hom.coe_const
(α : Type u_3)
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
(b : β) :
⇑(sup_hom.const α b) = function.const α b
@[simp]
theorem
sup_hom.const_apply
(α : Type u_3)
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
(b : β)
(a : α) :
⇑(sup_hom.const α b) a = b
@[protected, instance]
def
sup_hom.semilattice_sup
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[semilattice_sup β] :
semilattice_sup (sup_hom α β)
Equations
- sup_hom.semilattice_sup = function.injective.semilattice_sup coe_fn sup_hom.semilattice_sup._proof_1 sup_hom.semilattice_sup._proof_2
@[protected, instance]
Equations
- sup_hom.has_bot = {bot := sup_hom.const α ⊥}
@[protected, instance]
Equations
- sup_hom.has_top = {top := sup_hom.const α ⊤}
@[protected, instance]
Equations
- sup_hom.order_bot = order_bot.lift coe_fn sup_hom.order_bot._proof_5 sup_hom.order_bot._proof_6
@[protected, instance]
Equations
- sup_hom.order_top = order_top.lift coe_fn sup_hom.order_top._proof_5 sup_hom.order_top._proof_6
@[protected, instance]
def
sup_hom.bounded_order
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
[bounded_order β] :
bounded_order (sup_hom α β)
Equations
- sup_hom.bounded_order = bounded_order.lift coe_fn sup_hom.bounded_order._proof_5 sup_hom.bounded_order._proof_6 sup_hom.bounded_order._proof_7
@[simp]
@[simp]
@[simp]
theorem
sup_hom.bot_apply
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
[has_bot β]
(a : α) :
@[simp]
theorem
sup_hom.top_apply
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[semilattice_sup β]
[has_top β]
(a : α) :
Infimum homomorphisms #
@[protected, instance]
def
inf_hom.inf_hom_class
{α : Type u_3}
{β : Type u_4}
[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_3}
{β : Type u_4}
[has_inf α]
[has_inf β] :
has_coe_to_fun (inf_hom α β) (λ (_x : inf_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[protected, instance]
Equations
- inf_hom.inhabited α = {default := inf_hom.id α _inst_1}
@[simp]
theorem
inf_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
(f : inf_hom α β) :
f.comp (inf_hom.id α) = f
@[simp]
theorem
inf_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
(f : inf_hom α β) :
(inf_hom.id β).comp f = f
def
inf_hom.const
(α : Type u_3)
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
(b : β) :
inf_hom α β
The constant function as an inf_hom.
Equations
- inf_hom.const α b = {to_fun := λ (_x : α), b, map_inf' := _}
@[simp]
theorem
inf_hom.coe_const
(α : Type u_3)
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
(b : β) :
⇑(inf_hom.const α b) = function.const α b
@[simp]
theorem
inf_hom.const_apply
(α : Type u_3)
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
(b : β)
(a : α) :
⇑(inf_hom.const α b) a = b
@[protected, instance]
def
inf_hom.semilattice_inf
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[semilattice_inf β] :
semilattice_inf (inf_hom α β)
Equations
- inf_hom.semilattice_inf = function.injective.semilattice_inf coe_fn inf_hom.semilattice_inf._proof_1 inf_hom.semilattice_inf._proof_2
@[protected, instance]
Equations
- inf_hom.has_bot = {bot := inf_hom.const α ⊥}
@[protected, instance]
Equations
- inf_hom.has_top = {top := inf_hom.const α ⊤}
@[protected, instance]
Equations
- inf_hom.order_bot = order_bot.lift coe_fn inf_hom.order_bot._proof_5 inf_hom.order_bot._proof_6
@[protected, instance]
Equations
- inf_hom.order_top = order_top.lift coe_fn inf_hom.order_top._proof_5 inf_hom.order_top._proof_6
@[protected, instance]
def
inf_hom.bounded_order
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
[bounded_order β] :
bounded_order (inf_hom α β)
Equations
- inf_hom.bounded_order = bounded_order.lift coe_fn inf_hom.bounded_order._proof_5 inf_hom.bounded_order._proof_6 inf_hom.bounded_order._proof_7
@[simp]
@[simp]
@[simp]
theorem
inf_hom.bot_apply
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
[has_bot β]
(a : α) :
@[simp]
theorem
inf_hom.top_apply
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[semilattice_inf β]
[has_top β]
(a : α) :
Finitary supremum homomorphisms #
def
sup_bot_hom.to_bot_hom
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
(f : sup_bot_hom α β) :
bot_hom α β
Reinterpret a sup_bot_hom as a bot_hom.
Equations
- f.to_bot_hom = {to_fun := f.to_sup_hom.to_fun, map_bot' := _}
@[protected, instance]
def
sup_bot_hom.sup_bot_hom_class
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β] :
sup_bot_hom_class (sup_bot_hom α β) α β
Equations
- sup_bot_hom.sup_bot_hom_class = {to_sup_hom_class := {to_fun_like := {coe := λ (f : sup_bot_hom α β), f.to_sup_hom.to_fun, coe_injective' := _}, map_sup := _}, map_bot := _}
@[protected, instance]
def
sup_bot_hom.has_coe_to_fun
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β] :
has_coe_to_fun (sup_bot_hom α β) (λ (_x : sup_bot_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
sup_bot_hom.to_fun_eq_coe
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
{f : sup_bot_hom α β} :
f.to_sup_hom.to_fun = ⇑f
@[protected]
def
sup_bot_hom.copy
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
(f : sup_bot_hom α β)
(f' : α → β)
(h : f' = ⇑f) :
sup_bot_hom α β
Copy of a sup_bot_hom with a new to_fun equal to the old one. Useful to fix definitional
equalities.
Equations
- f.copy f' h = {to_sup_hom := f.to_sup_hom.copy f' h, map_bot' := _}
@[simp]
theorem
sup_bot_hom.id_to_sup_hom
(α : Type u_3)
[has_sup α]
[has_bot α] :
(sup_bot_hom.id α).to_sup_hom = sup_hom.id α
@[protected]
id as a sup_bot_hom.
Equations
- sup_bot_hom.id α = {to_sup_hom := sup_hom.id α _inst_1, map_bot' := _}
@[protected, instance]
Equations
- sup_bot_hom.inhabited α = {default := sup_bot_hom.id α _inst_2}
@[simp]
@[simp]
theorem
sup_bot_hom.id_apply
{α : Type u_3}
[has_sup α]
[has_bot α]
(a : α) :
⇑(sup_bot_hom.id α) a = a
def
sup_bot_hom.comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
(f : sup_bot_hom β γ)
(g : sup_bot_hom α β) :
sup_bot_hom α γ
Composition of sup_bot_homs as a sup_bot_hom.
Equations
- f.comp g = {to_sup_hom := {to_fun := (f.to_sup_hom.comp g.to_sup_hom).to_fun, map_sup' := _}, map_bot' := _}
@[simp]
theorem
sup_bot_hom.comp_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
(f : sup_bot_hom β γ)
(g : sup_bot_hom α β)
(a : α) :
@[simp]
theorem
sup_bot_hom.comp_assoc
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
[has_sup δ]
[has_bot δ]
(f : sup_bot_hom γ δ)
(g : sup_bot_hom β γ)
(h : sup_bot_hom α β) :
@[simp]
theorem
sup_bot_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
(f : sup_bot_hom α β) :
f.comp (sup_bot_hom.id α) = f
@[simp]
theorem
sup_bot_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
(f : sup_bot_hom α β) :
(sup_bot_hom.id β).comp f = f
theorem
sup_bot_hom.cancel_right
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
{g₁ g₂ : sup_bot_hom β γ}
{f : sup_bot_hom α β}
(hf : function.surjective ⇑f) :
theorem
sup_bot_hom.cancel_left
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
{g : sup_bot_hom β γ}
{f₁ f₂ : sup_bot_hom α β}
(hg : function.injective ⇑g) :
@[protected, instance]
def
sup_bot_hom.has_sup
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β] :
has_sup (sup_bot_hom α β)
Equations
- sup_bot_hom.has_sup = {sup := λ (f g : sup_bot_hom α β), {to_sup_hom := f.to_sup_hom ⊔ g.to_sup_hom, map_bot' := _}}
@[protected, instance]
def
sup_bot_hom.semilattice_sup
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β] :
semilattice_sup (sup_bot_hom α β)
Equations
- sup_bot_hom.semilattice_sup = function.injective.semilattice_sup coe_fn sup_bot_hom.semilattice_sup._proof_1 sup_bot_hom.semilattice_sup._proof_2
@[protected, instance]
def
sup_bot_hom.order_bot
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β] :
order_bot (sup_bot_hom α β)
Equations
- sup_bot_hom.order_bot = {bot := {to_sup_hom := ⊥, map_bot' := _}, bot_le := _}
@[simp]
theorem
sup_bot_hom.coe_sup
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β]
(f g : sup_bot_hom α β) :
@[simp]
theorem
sup_bot_hom.coe_bot
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β] :
@[simp]
theorem
sup_bot_hom.sup_apply
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β]
(f g : sup_bot_hom α β)
(a : α) :
@[simp]
theorem
sup_bot_hom.bot_apply
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[semilattice_sup β]
[order_bot β]
(a : α) :
Finitary infimum homomorphisms #
def
inf_top_hom.to_top_hom
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : inf_top_hom α β) :
top_hom α β
Reinterpret an inf_top_hom as a top_hom.
Equations
- f.to_top_hom = {to_fun := f.to_inf_hom.to_fun, map_top' := _}
@[protected, instance]
def
inf_top_hom.inf_top_hom_class
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β] :
inf_top_hom_class (inf_top_hom α β) α β
Equations
- inf_top_hom.inf_top_hom_class = {to_inf_hom_class := {to_fun_like := {coe := λ (f : inf_top_hom α β), f.to_inf_hom.to_fun, coe_injective' := _}, map_inf := _}, map_top := _}
@[protected, instance]
def
inf_top_hom.has_coe_to_fun
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β] :
has_coe_to_fun (inf_top_hom α β) (λ (_x : inf_top_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
inf_top_hom.to_fun_eq_coe
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
{f : inf_top_hom α β} :
f.to_inf_hom.to_fun = ⇑f
@[protected]
def
inf_top_hom.copy
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : inf_top_hom α β)
(f' : α → β)
(h : f' = ⇑f) :
inf_top_hom α β
Copy of an inf_top_hom with a new to_fun equal to the old one. Useful to fix definitional
equalities.
Equations
- f.copy f' h = {to_inf_hom := f.to_inf_hom.copy f' h, map_top' := _}
@[simp]
theorem
inf_top_hom.id_to_inf_hom
(α : Type u_3)
[has_inf α]
[has_top α] :
(inf_top_hom.id α).to_inf_hom = inf_hom.id α
@[protected]
id as an inf_top_hom.
Equations
- inf_top_hom.id α = {to_inf_hom := inf_hom.id α _inst_1, map_top' := _}
@[protected, instance]
Equations
- inf_top_hom.inhabited α = {default := inf_top_hom.id α _inst_2}
@[simp]
@[simp]
theorem
inf_top_hom.id_apply
{α : Type u_3}
[has_inf α]
[has_top α]
(a : α) :
⇑(inf_top_hom.id α) a = a
def
inf_top_hom.comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
(f : inf_top_hom β γ)
(g : inf_top_hom α β) :
inf_top_hom α γ
Composition of inf_top_homs as an inf_top_hom.
Equations
- f.comp g = {to_inf_hom := {to_fun := (f.to_inf_hom.comp g.to_inf_hom).to_fun, map_inf' := _}, map_top' := _}
@[simp]
theorem
inf_top_hom.comp_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
(f : inf_top_hom β γ)
(g : inf_top_hom α β)
(a : α) :
@[simp]
theorem
inf_top_hom.comp_assoc
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
[has_inf δ]
[has_top δ]
(f : inf_top_hom γ δ)
(g : inf_top_hom β γ)
(h : inf_top_hom α β) :
@[simp]
theorem
inf_top_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : inf_top_hom α β) :
f.comp (inf_top_hom.id α) = f
@[simp]
theorem
inf_top_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : inf_top_hom α β) :
(inf_top_hom.id β).comp f = f
theorem
inf_top_hom.cancel_right
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
{g₁ g₂ : inf_top_hom β γ}
{f : inf_top_hom α β}
(hf : function.surjective ⇑f) :
theorem
inf_top_hom.cancel_left
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
{g : inf_top_hom β γ}
{f₁ f₂ : inf_top_hom α β}
(hg : function.injective ⇑g) :
@[protected, instance]
def
inf_top_hom.has_inf
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β] :
has_inf (inf_top_hom α β)
Equations
- inf_top_hom.has_inf = {inf := λ (f g : inf_top_hom α β), {to_inf_hom := f.to_inf_hom ⊓ g.to_inf_hom, map_top' := _}}
@[protected, instance]
def
inf_top_hom.semilattice_inf
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β] :
semilattice_inf (inf_top_hom α β)
Equations
- inf_top_hom.semilattice_inf = function.injective.semilattice_inf coe_fn inf_top_hom.semilattice_inf._proof_1 inf_top_hom.semilattice_inf._proof_2
@[protected, instance]
def
inf_top_hom.order_top
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β] :
order_top (inf_top_hom α β)
Equations
- inf_top_hom.order_top = {top := {to_inf_hom := ⊤, map_top' := _}, le_top := _}
@[simp]
theorem
inf_top_hom.coe_inf
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β]
(f g : inf_top_hom α β) :
@[simp]
theorem
inf_top_hom.coe_top
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β] :
@[simp]
theorem
inf_top_hom.inf_apply
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β]
(f g : inf_top_hom α β)
(a : α) :
@[simp]
theorem
inf_top_hom.top_apply
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[semilattice_inf β]
[order_top β]
(a : α) :
Lattice homomorphisms #
def
lattice_hom.to_inf_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom α β) :
inf_hom α β
Reinterpret a lattice_hom as an inf_hom.
Equations
- f.to_inf_hom = {to_fun := f.to_sup_hom.to_fun, map_inf' := _}
@[protected, instance]
def
lattice_hom.lattice_hom_class
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β] :
lattice_hom_class (lattice_hom α β) α β
Equations
- lattice_hom.lattice_hom_class = {to_sup_hom_class := {to_fun_like := {coe := λ (f : lattice_hom α β), f.to_sup_hom.to_fun, coe_injective' := _}, map_sup := _}, map_inf := _}
@[protected, instance]
def
lattice_hom.has_coe_to_fun
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β] :
has_coe_to_fun (lattice_hom α β) (λ (_x : lattice_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
- lattice_hom.has_coe_to_fun = {coe := λ (f : lattice_hom α β), f.to_sup_hom.to_fun}
@[simp]
theorem
lattice_hom.to_fun_eq_coe
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
{f : lattice_hom α β} :
f.to_sup_hom.to_fun = ⇑f
@[ext]
theorem
lattice_hom.ext
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
{f g : lattice_hom α β}
(h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
@[protected]
def
lattice_hom.copy
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom α β)
(f' : α → β)
(h : f' = ⇑f) :
lattice_hom α β
Copy of a lattice_hom with a new to_fun equal to the old one. Useful to fix definitional
equalities.
@[protected]
id as a lattice_hom.
Equations
- lattice_hom.id α = {to_sup_hom := {to_fun := id α, map_sup' := _}, map_inf' := _}
@[protected, instance]
Equations
- lattice_hom.inhabited α = {default := lattice_hom.id α _inst_1}
@[simp]
def
lattice_hom.comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(f : lattice_hom β γ)
(g : lattice_hom α β) :
lattice_hom α γ
Composition of lattice_homs as a lattice_hom.
Equations
- 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
lattice_hom.coe_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(f : lattice_hom β γ)
(g : lattice_hom α β) :
@[simp]
theorem
lattice_hom.comp_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(f : lattice_hom β γ)
(g : lattice_hom α β)
(a : α) :
@[simp]
theorem
lattice_hom.coe_comp_sup_hom
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(f : lattice_hom β γ)
(g : lattice_hom α β) :
@[simp]
theorem
lattice_hom.coe_comp_inf_hom
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(f : lattice_hom β γ)
(g : lattice_hom α β) :
@[simp]
theorem
lattice_hom.comp_assoc
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[lattice α]
[lattice β]
[lattice γ]
[lattice δ]
(f : lattice_hom γ δ)
(g : lattice_hom β γ)
(h : lattice_hom α β) :
@[simp]
theorem
lattice_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom α β) :
f.comp (lattice_hom.id α) = f
@[simp]
theorem
lattice_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom α β) :
(lattice_hom.id β).comp f = f
theorem
lattice_hom.cancel_right
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
{g₁ g₂ : lattice_hom β γ}
{f : lattice_hom α β}
(hf : function.surjective ⇑f) :
theorem
lattice_hom.cancel_left
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
{g : lattice_hom β γ}
{f₁ f₂ : lattice_hom α β}
(hg : function.injective ⇑g) :
def
order_hom_class.to_lattice_hom_class
{F : Type u_1}
(α : Type u_3)
(β : Type u_4)
[linear_order α]
[lattice β]
[order_hom_class F α β] :
lattice_hom_class F α β
An order homomorphism from a linear order is a lattice homomorphism.
Equations
- order_hom_class.to_lattice_hom_class α β = {to_sup_hom_class := {to_fun_like := rel_hom_class.to_fun_like _inst_3, map_sup := _}, map_inf := _}
def
order_hom_class.to_lattice_hom
{F : Type u_1}
(α : Type u_3)
(β : Type u_4)
[linear_order α]
[lattice β]
[order_hom_class F α β]
(f : F) :
lattice_hom α β
Reinterpret an order homomorphism to a linear order as a lattice_hom.
Equations
- order_hom_class.to_lattice_hom α β f = ↑f
@[simp]
theorem
order_hom_class.coe_to_lattice_hom
{F : Type u_1}
(α : Type u_3)
(β : Type u_4)
[linear_order α]
[lattice β]
[order_hom_class F α β]
(f : F) :
⇑(order_hom_class.to_lattice_hom α β f) = ⇑f
@[simp]
theorem
order_hom_class.to_lattice_hom_apply
{F : Type u_1}
(α : Type u_3)
(β : Type u_4)
[linear_order α]
[lattice β]
[order_hom_class F α β]
(f : F)
(a : α) :
⇑(order_hom_class.to_lattice_hom α β f) a = ⇑f a
Bounded lattice homomorphisms #
def
bounded_lattice_hom.to_sup_bot_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β) :
sup_bot_hom α β
Reinterpret a bounded_lattice_hom as a sup_bot_hom.
Equations
- f.to_sup_bot_hom = {to_sup_hom := f.to_lattice_hom.to_sup_hom, map_bot' := _}
def
bounded_lattice_hom.to_inf_top_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β) :
inf_top_hom α β
Reinterpret a bounded_lattice_hom as an inf_top_hom.
Equations
- f.to_inf_top_hom = {to_inf_hom := {to_fun := f.to_lattice_hom.to_sup_hom.to_fun, map_inf' := _}, map_top' := _}
def
bounded_lattice_hom.to_bounded_order_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β) :
Reinterpret a bounded_lattice_hom as a bounded_order_hom.
Equations
- f.to_bounded_order_hom = {to_order_hom := {to_fun := f.to_lattice_hom.to_sup_hom.to_fun, monotone' := _}, map_top' := _, map_bot' := _}
@[protected, instance]
def
bounded_lattice_hom.bounded_lattice_hom_class
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β] :
bounded_lattice_hom_class (bounded_lattice_hom α β) α β
Equations
- bounded_lattice_hom.bounded_lattice_hom_class = {to_lattice_hom_class := {to_sup_hom_class := {to_fun_like := {coe := λ (f : bounded_lattice_hom α β), f.to_lattice_hom.to_sup_hom.to_fun, coe_injective' := _}, map_sup := _}, map_inf := _}, map_top := _, map_bot := _}
@[protected, instance]
def
bounded_lattice_hom.has_coe_to_fun
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β] :
has_coe_to_fun (bounded_lattice_hom α β) (λ (_x : bounded_lattice_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
- bounded_lattice_hom.has_coe_to_fun = {coe := λ (f : bounded_lattice_hom α β), f.to_lattice_hom.to_sup_hom.to_fun}
@[simp]
theorem
bounded_lattice_hom.to_fun_eq_coe
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
{f : bounded_lattice_hom α β} :
@[ext]
theorem
bounded_lattice_hom.ext
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
{f g : bounded_lattice_hom α β}
(h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
@[protected]
def
bounded_lattice_hom.copy
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β)
(f' : α → β)
(h : f' = ⇑f) :
Copy of a bounded_lattice_hom with a new to_fun equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_lattice_hom := {to_sup_hom := (f.to_lattice_hom.copy f' h).to_sup_hom, map_inf' := _}, map_top' := _, map_bot' := _}
@[protected]
id as a bounded_lattice_hom.
Equations
- bounded_lattice_hom.id α = {to_lattice_hom := {to_sup_hom := (lattice_hom.id α).to_sup_hom, map_inf' := _}, map_top' := _, map_bot' := _}
@[protected, instance]
def
bounded_lattice_hom.inhabited
(α : Type u_3)
[lattice α]
[bounded_order α] :
inhabited (bounded_lattice_hom α α)
Equations
- bounded_lattice_hom.inhabited α = {default := bounded_lattice_hom.id α _inst_5}
@[simp]
@[simp]
theorem
bounded_lattice_hom.id_apply
{α : Type u_3}
[lattice α]
[bounded_order α]
(a : α) :
⇑(bounded_lattice_hom.id α) a = a
def
bounded_lattice_hom.comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β) :
Composition of bounded_lattice_homs as a bounded_lattice_hom.
Equations
- f.comp g = {to_lattice_hom := {to_sup_hom := (f.to_lattice_hom.comp g.to_lattice_hom).to_sup_hom, map_inf' := _}, map_top' := _, map_bot' := _}
@[simp]
theorem
bounded_lattice_hom.coe_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β) :
@[simp]
theorem
bounded_lattice_hom.comp_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β)
(a : α) :
@[simp]
theorem
bounded_lattice_hom.coe_comp_lattice_hom
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β) :
@[simp]
theorem
bounded_lattice_hom.coe_comp_sup_hom
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β) :
@[simp]
theorem
bounded_lattice_hom.coe_comp_inf_hom
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_lattice_hom β γ)
(g : bounded_lattice_hom α β) :
@[simp]
theorem
bounded_lattice_hom.comp_assoc
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_6}
[lattice α]
[lattice β]
[lattice γ]
[lattice δ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
[bounded_order δ]
(f : bounded_lattice_hom γ δ)
(g : bounded_lattice_hom β γ)
(h : bounded_lattice_hom α β) :
@[simp]
theorem
bounded_lattice_hom.comp_id
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β) :
f.comp (bounded_lattice_hom.id α) = f
@[simp]
theorem
bounded_lattice_hom.id_comp
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
[bounded_order α]
[bounded_order β]
(f : bounded_lattice_hom α β) :
(bounded_lattice_hom.id β).comp f = f
theorem
bounded_lattice_hom.cancel_right
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
{g₁ g₂ : bounded_lattice_hom β γ}
{f : bounded_lattice_hom α β}
(hf : function.surjective ⇑f) :
theorem
bounded_lattice_hom.cancel_left
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
{g : bounded_lattice_hom β γ}
{f₁ f₂ : bounded_lattice_hom α β}
(hg : function.injective ⇑g) :
Dual homs #
@[protected]
def
sup_hom.dual
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β] :
sup_hom α β ≃ inf_hom (order_dual α) (order_dual β)
Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices.
@[simp]
theorem
sup_hom.dual_apply_to_fun
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
(f : sup_hom α β)
(ᾰ : α) :
⇑(⇑sup_hom.dual f) ᾰ = ⇑f ᾰ
@[simp]
theorem
sup_hom.dual_symm_apply_to_fun
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_sup β]
(f : inf_hom (order_dual α) (order_dual β))
(ᾰ : order_dual α) :
@[simp]
theorem
sup_hom.dual_id
{α : Type u_3}
[has_sup α] :
⇑sup_hom.dual (sup_hom.id α) = inf_hom.id (order_dual α)
@[simp]
theorem
sup_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_sup β]
[has_sup γ]
(g : sup_hom β γ)
(f : sup_hom α β) :
⇑sup_hom.dual (g.comp f) = (⇑sup_hom.dual g).comp (⇑sup_hom.dual f)
@[simp]
theorem
sup_hom.symm_dual_id
{α : Type u_3}
[has_sup α] :
⇑(sup_hom.dual.symm) (inf_hom.id (order_dual α)) = sup_hom.id α
@[simp]
theorem
sup_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_sup β]
[has_sup γ]
(g : inf_hom (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)
@[simp]
theorem
inf_hom.dual_symm_apply_to_fun
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
(f : sup_hom (order_dual α) (order_dual β))
(ᾰ : order_dual α) :
@[protected]
def
inf_hom.dual
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β] :
inf_hom α β ≃ sup_hom (order_dual α) (order_dual β)
Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices.
@[simp]
theorem
inf_hom.dual_apply_to_fun
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_inf β]
(f : inf_hom α β)
(ᾰ : α) :
⇑(⇑inf_hom.dual f) ᾰ = ⇑f ᾰ
@[simp]
theorem
inf_hom.dual_id
{α : Type u_3}
[has_inf α] :
⇑inf_hom.dual (inf_hom.id α) = sup_hom.id (order_dual α)
@[simp]
theorem
inf_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_inf β]
[has_inf γ]
(g : inf_hom β γ)
(f : inf_hom α β) :
⇑inf_hom.dual (g.comp f) = (⇑inf_hom.dual g).comp (⇑inf_hom.dual f)
@[simp]
theorem
inf_hom.symm_dual_id
{α : Type u_3}
[has_inf α] :
⇑(inf_hom.dual.symm) (sup_hom.id (order_dual α)) = inf_hom.id α
@[simp]
theorem
inf_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_inf β]
[has_inf γ]
(g : sup_hom (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)
def
sup_bot_hom.dual
{α : Type u_3}
{β : Type u_4}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β] :
sup_bot_hom α β ≃ inf_top_hom (order_dual α) (order_dual β)
Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual lattices.
Equations
- sup_bot_hom.dual = {to_fun := λ (f : sup_bot_hom α β), {to_inf_hom := ⇑sup_hom.dual f.to_sup_hom, map_top' := _}, inv_fun := λ (f : inf_top_hom (order_dual α) (order_dual β)), {to_sup_hom := ⇑(sup_hom.dual.symm) f.to_inf_hom, map_bot' := _}, left_inv := _, right_inv := _}
@[simp]
@[simp]
theorem
sup_bot_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
(g : sup_bot_hom β γ)
(f : sup_bot_hom α β) :
⇑sup_bot_hom.dual (g.comp f) = (⇑sup_bot_hom.dual g).comp (⇑sup_bot_hom.dual f)
@[simp]
theorem
sup_bot_hom.symm_dual_id
{α : Type u_3}
[has_sup α]
[has_bot α] :
⇑(sup_bot_hom.dual.symm) (inf_top_hom.id (order_dual α)) = sup_bot_hom.id α
@[simp]
theorem
sup_bot_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_sup α]
[has_bot α]
[has_sup β]
[has_bot β]
[has_sup γ]
[has_bot γ]
(g : inf_top_hom (order_dual β) (order_dual γ))
(f : inf_top_hom (order_dual α) (order_dual β)) :
⇑(sup_bot_hom.dual.symm) (g.comp f) = (⇑(sup_bot_hom.dual.symm) g).comp (⇑(sup_bot_hom.dual.symm) f)
@[simp]
theorem
inf_top_hom.dual_symm_apply_to_inf_hom
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : sup_bot_hom (order_dual α) (order_dual β)) :
(⇑(inf_top_hom.dual.symm) f).to_inf_hom = ⇑(inf_hom.dual.symm) f.to_sup_hom
@[simp]
theorem
inf_top_hom.dual_apply_to_sup_hom
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
(f : inf_top_hom α β) :
@[protected]
def
inf_top_hom.dual
{α : Type u_3}
{β : Type u_4}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β] :
inf_top_hom α β ≃ sup_bot_hom (order_dual α) (order_dual β)
Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual lattices.
Equations
- inf_top_hom.dual = {to_fun := λ (f : inf_top_hom α β), {to_sup_hom := ⇑inf_hom.dual f.to_inf_hom, map_bot' := _}, inv_fun := λ (f : sup_bot_hom (order_dual α) (order_dual β)), {to_inf_hom := ⇑(inf_hom.dual.symm) f.to_sup_hom, map_top' := _}, left_inv := _, right_inv := _}
@[simp]
@[simp]
theorem
inf_top_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
(g : inf_top_hom β γ)
(f : inf_top_hom α β) :
⇑inf_top_hom.dual (g.comp f) = (⇑inf_top_hom.dual g).comp (⇑inf_top_hom.dual f)
@[simp]
theorem
inf_top_hom.symm_dual_id
{α : Type u_3}
[has_inf α]
[has_top α] :
⇑(inf_top_hom.dual.symm) (sup_bot_hom.id (order_dual α)) = inf_top_hom.id α
@[simp]
theorem
inf_top_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[has_inf α]
[has_top α]
[has_inf β]
[has_top β]
[has_inf γ]
[has_top γ]
(g : sup_bot_hom (order_dual β) (order_dual γ))
(f : sup_bot_hom (order_dual α) (order_dual β)) :
⇑(inf_top_hom.dual.symm) (g.comp f) = (⇑(inf_top_hom.dual.symm) g).comp (⇑(inf_top_hom.dual.symm) f)
@[protected]
def
lattice_hom.dual
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β] :
lattice_hom α β ≃ lattice_hom (order_dual α) (order_dual β)
Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.
Equations
- lattice_hom.dual = {to_fun := λ (f : lattice_hom α β), {to_sup_hom := ⇑inf_hom.dual f.to_inf_hom, map_inf' := _}, inv_fun := λ (f : lattice_hom (order_dual α) (order_dual β)), {to_sup_hom := ⇑inf_hom.dual f.to_inf_hom, map_inf' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
lattice_hom.dual_apply_to_sup_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom α β) :
@[simp]
theorem
lattice_hom.dual_symm_apply_to_sup_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[lattice β]
(f : lattice_hom (order_dual α) (order_dual β)) :
@[simp]
@[simp]
theorem
lattice_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(g : lattice_hom β γ)
(f : lattice_hom α β) :
⇑lattice_hom.dual (g.comp f) = (⇑lattice_hom.dual g).comp (⇑lattice_hom.dual f)
@[simp]
theorem
lattice_hom.symm_dual_id
{α : Type u_3}
[lattice α] :
⇑(lattice_hom.dual.symm) (lattice_hom.id (order_dual α)) = lattice_hom.id α
@[simp]
theorem
lattice_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[lattice β]
[lattice γ]
(g : lattice_hom (order_dual β) (order_dual γ))
(f : lattice_hom (order_dual α) (order_dual β)) :
⇑(lattice_hom.dual.symm) (g.comp f) = (⇑(lattice_hom.dual.symm) g).comp (⇑(lattice_hom.dual.symm) f)
@[simp]
theorem
bounded_lattice_hom.dual_symm_apply_to_lattice_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
(f : bounded_lattice_hom (order_dual α) (order_dual β)) :
@[simp]
theorem
bounded_lattice_hom.dual_apply_to_lattice_hom
{α : Type u_3}
{β : Type u_4}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
(f : bounded_lattice_hom α β) :
@[protected]
def
bounded_lattice_hom.dual
{α : Type u_3}
{β : Type u_4}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β] :
bounded_lattice_hom α β ≃ bounded_lattice_hom (order_dual α) (order_dual β)
Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual bounded lattices.
Equations
- bounded_lattice_hom.dual = {to_fun := λ (f : bounded_lattice_hom α β), {to_lattice_hom := ⇑lattice_hom.dual f.to_lattice_hom, map_top' := _, map_bot' := _}, inv_fun := λ (f : bounded_lattice_hom (order_dual α) (order_dual β)), {to_lattice_hom := ⇑(lattice_hom.dual.symm) f.to_lattice_hom, map_top' := _, map_bot' := _}, left_inv := _, right_inv := _}
@[simp]
@[simp]
theorem
bounded_lattice_hom.dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
[lattice γ]
[bounded_order γ]
(g : bounded_lattice_hom β γ)
(f : bounded_lattice_hom α β) :
@[simp]
@[simp]
theorem
bounded_lattice_hom.symm_dual_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[lattice α]
[bounded_order α]
[lattice β]
[bounded_order β]
[lattice γ]
[bounded_order γ]
(g : bounded_lattice_hom (order_dual β) (order_dual γ))
(f : bounded_lattice_hom (order_dual α) (order_dual β)) :
⇑(bounded_lattice_hom.dual.symm) (g.comp f) = (⇑(bounded_lattice_hom.dual.symm) g).comp (⇑(bounded_lattice_hom.dual.symm) f)