order.hom.lattice - mathlib docs

structure bounded_lattice_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [lattice α] [lattice β] [bounded_order α] [bounded_order β] :

Type (max u_6 u_7 u_8)

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.

Instances

source

@[protected, instance]

def sup_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [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 := _}

source

@[protected, instance]

def inf_hom_class.to_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [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 := _}

source

@[protected, instance]

def lattice_hom_class.to_inf_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [lattice_hom_class F α β] :

inf_hom_class F α β

Equations

lattice_hom_class.to_inf_hom_class = {to_fun_like := sup_hom_class.to_fun_like lattice_hom_class.to_sup_hom_class, map_inf := _}

source

@[protected, instance]

def bounded_lattice_hom_class.to_bounded_order_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] [bounded_lattice_hom_class F α β] :

bounded_order_hom_class F α β

Equations

bounded_lattice_hom_class.to_bounded_order_hom_class = {to_rel_hom_class := inf_hom_class.to_order_hom_class lattice_hom_class.to_inf_hom_class, map_top := _, map_bot := _}

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 lattice_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [lattice_hom_class F α β] :

has_coe_t F (lattice_hom α β)

Equations

lattice_hom.has_coe_t = {coe := λ (f : F), {to_sup_hom := {to_fun := ⇑f, map_sup' := _}, map_inf' := _}}

source

@[protected, instance]

def bounded_lattice_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [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' := _}}

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 = {coe := λ (f : sup_hom α β), f.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.has_sup {α : Type u_2} {β : Type u_3} [has_sup α] [semilattice_sup β] :

has_sup (sup_hom α β)

Equations

sup_hom.has_sup = {sup := λ (f g : sup_hom α β), {to_fun := ⇑f ⊔ ⇑g, map_sup' := _}}

source

@[protected, instance]

def sup_hom.semilattice_sup {α : Type u_2} {β : Type u_3} [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

source

@[simp]

theorem sup_hom.coe_sup {α : Type u_2} {β : Type u_3} [has_sup α] [semilattice_sup β] (f g : sup_hom α β) :

⇑(f ⊔ g) = ⇑f ⊔ ⇑g

source

@[simp]

theorem sup_hom.sup_apply {α : Type u_2} {β : Type u_3} [has_sup α] [semilattice_sup β] (f g : sup_hom α β) (a : α) :

⇑(f ⊔ g) a = ⇑f a ⊔ ⇑g a

source

def sup_hom.const (α : Type u_2) {β : Type u_3} [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' := _}

source

@[simp]

theorem sup_hom.coe_const (α : Type u_2) {β : Type u_3} [has_sup α] [semilattice_sup β] (b : β) :

⇑(sup_hom.const α b) = function.const α b

source

@[simp]

theorem sup_hom.const_apply (α : Type u_2) {β : Type u_3} [has_sup α] [semilattice_sup β] (b : β) (a : α) :

⇑(sup_hom.const α b) a = b

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 = {coe := λ (f : inf_hom α β), f.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.has_inf {α : Type u_2} {β : Type u_3} [has_inf α] [semilattice_inf β] :

has_inf (inf_hom α β)

Equations

inf_hom.has_inf = {inf := λ (f g : inf_hom α β), {to_fun := ⇑f ⊓ ⇑g, map_inf' := _}}

source

@[protected, instance]

def inf_hom.semilattice_inf {α : Type u_2} {β : Type u_3} [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

source

@[simp]

theorem inf_hom.coe_inf {α : Type u_2} {β : Type u_3} [has_inf α] [semilattice_inf β] (f g : inf_hom α β) :

⇑(f ⊓ g) = ⇑f ⊓ ⇑g

source

@[simp]

theorem inf_hom.inf_apply {α : Type u_2} {β : Type u_3} [has_inf α] [semilattice_inf β] (f g : inf_hom α β) (a : α) :

⇑(f ⊓ g) a = ⇑f a ⊓ ⇑g a

source

def inf_hom.const (α : Type u_2) {β : Type u_3} [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' := _}

source

@[simp]

theorem inf_hom.coe_const (α : Type u_2) {β : Type u_3} [has_inf α] [semilattice_inf β] (b : β) :

⇑(inf_hom.const α b) = function.const α b

source

@[simp]

theorem inf_hom.const_apply (α : Type u_2) {β : Type u_3} [has_inf α] [semilattice_inf β] (b : β) (a : α) :

⇑(inf_hom.const α b) a = b

source

def lattice_hom.to_inf_hom {α : Type u_2} {β : Type u_3} [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' := _}

source

@[protected, instance]

def lattice_hom.lattice_hom_class {α : Type u_2} {β : Type u_3} [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 := _}

source

@[protected, instance]

def lattice_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [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}

source

@[simp]

theorem lattice_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] {f : lattice_hom α β} :

f.to_sup_hom.to_fun = ⇑f

source

@[ext]

theorem lattice_hom.ext {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] {f g : lattice_hom α β} (h : ∀ (a : α), ⇑f a = ⇑g a) :

f = g

source

@[protected]

def lattice_hom.copy {α : Type u_2} {β : Type u_3} [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.

Equations

f.copy f' h = {to_sup_hom := {to_fun := (f.to_sup_hom.copy f' h).to_fun, map_sup' := _}, map_inf' := _}

source

@[protected]

def lattice_hom.id (α : Type u_2) [lattice α] :

lattice_hom α α

id as a lattice_hom.

Equations

lattice_hom.id α = {to_sup_hom := {to_fun := id α, map_sup' := _}, map_inf' := _}

source

@[protected, instance]

def lattice_hom.inhabited (α : Type u_2) [lattice α] :

inhabited (lattice_hom α α)

Equations

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

source

@[simp]

theorem lattice_hom.coe_id (α : Type u_2) [lattice α] :

⇑(lattice_hom.id α) = id

source

@[simp]

theorem lattice_hom.id_apply {α : Type u_2} [lattice α] (a : α) :

⇑(lattice_hom.id α) a = a

source

def lattice_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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' := _}

source

@[simp]

theorem lattice_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem lattice_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) (a : α) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

@[simp]

theorem lattice_hom.coe_comp_sup_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem lattice_hom.coe_comp_inf_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] (f : lattice_hom β γ) (g : lattice_hom α β) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem lattice_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [lattice α] [lattice β] [lattice γ] [lattice δ] (f : lattice_hom γ δ) (g : lattice_hom β γ) (h : lattice_hom α β) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

theorem lattice_hom.comp_id {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : lattice_hom α β) :

f.comp (lattice_hom.id α) = f

source

@[simp]

theorem lattice_hom.id_comp {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] (f : lattice_hom α β) :

(lattice_hom.id β).comp f = f

source

theorem lattice_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] {g₁ g₂ : lattice_hom β γ} {f : lattice_hom α β} (hf : function.surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

source

theorem lattice_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] {g : lattice_hom β γ} {f₁ f₂ : lattice_hom α β} (hg : function.injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

source

def order_hom_class.to_lattice_hom_class {F : Type u_1} (α : Type u_2) (β : Type u_3) [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 := _}

source

def order_hom_class.to_lattice_hom {F : Type u_1} (α : Type u_2) (β : Type u_3) [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

source

@[simp]

theorem order_hom_class.coe_to_lattice_hom {F : Type u_1} (α : Type u_2) (β : Type u_3) [linear_order α] [lattice β] [order_hom_class F α β] (f : F) :

⇑(order_hom_class.to_lattice_hom α β f) = ⇑f

source

@[simp]

theorem order_hom_class.to_lattice_hom_apply {F : Type u_1} (α : Type u_2) (β : Type u_3) [linear_order α] [lattice β] [order_hom_class F α β] (f : F) (a : α) :

⇑(order_hom_class.to_lattice_hom α β f) a = ⇑f a

source

def bounded_lattice_hom.to_bounded_order_hom {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :

bounded_order_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' := _}

source

@[protected, instance]

def bounded_lattice_hom.bounded_lattice_hom_class {α : Type u_2} {β : Type u_3} [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 := _}

source

@[protected, instance]

def bounded_lattice_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [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}

source

@[simp]

theorem bounded_lattice_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] {f : bounded_lattice_hom α β} :

f.to_lattice_hom.to_sup_hom.to_fun = ⇑f

source

@[ext]

theorem bounded_lattice_hom.ext {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] {f g : bounded_lattice_hom α β} (h : ∀ (a : α), ⇑f a = ⇑g a) :

f = g

source

@[protected]

def bounded_lattice_hom.copy {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) (f' : α → β) (h : f' = ⇑f) :

bounded_lattice_hom α β

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' := _}

source

@[protected]

def bounded_lattice_hom.id (α : Type u_2) [lattice α] [bounded_order α] :

bounded_lattice_hom α α

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' := _}

source

@[protected, instance]

def bounded_lattice_hom.inhabited (α : Type u_2) [lattice α] [bounded_order α] :

inhabited (bounded_lattice_hom α α)

Equations

bounded_lattice_hom.inhabited α = {default := bounded_lattice_hom.id α _inst_5}

source

@[simp]

theorem bounded_lattice_hom.coe_id (α : Type u_2) [lattice α] [bounded_order α] :

⇑(bounded_lattice_hom.id α) = id

source

@[simp]

theorem bounded_lattice_hom.id_apply {α : Type u_2} [lattice α] [bounded_order α] (a : α) :

⇑(bounded_lattice_hom.id α) a = a

source

def bounded_lattice_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

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' := _}

source

@[simp]

theorem bounded_lattice_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem bounded_lattice_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) (a : α) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

@[simp]

theorem bounded_lattice_hom.coe_comp_lattice_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem bounded_lattice_hom.coe_comp_sup_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem bounded_lattice_hom.coe_comp_inf_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] (f : bounded_lattice_hom β γ) (g : bounded_lattice_hom α β) :

↑(f.comp g) = ↑f.comp ↑g

source

@[simp]

theorem bounded_lattice_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [lattice α] [lattice β] [lattice γ] [lattice δ] [bounded_order α] [bounded_order β] [bounded_order γ] [bounded_order δ] (f : bounded_lattice_hom γ δ) (g : bounded_lattice_hom β γ) (h : bounded_lattice_hom α β) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

theorem bounded_lattice_hom.comp_id {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :

f.comp (bounded_lattice_hom.id α) = f

source

@[simp]

theorem bounded_lattice_hom.id_comp {α : Type u_2} {β : Type u_3} [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : bounded_lattice_hom α β) :

(bounded_lattice_hom.id β).comp f = f

source

theorem bounded_lattice_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g₁ g₂ : bounded_lattice_hom β γ} {f : bounded_lattice_hom α β} (hf : function.surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

source

theorem bounded_lattice_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [lattice α] [lattice β] [lattice γ] [bounded_order α] [bounded_order β] [bounded_order γ] {g : bounded_lattice_hom β γ} {f₁ f₂ : bounded_lattice_hom α β} (hg : function.injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

mathlib documentation

Lattice homomorphisms #

Types of morphisms #

Typeclasses #

TODO #

Supremum homomorphisms #

Infimum homomorphisms #

Lattice homomorphisms #

Bounded lattice homomorphisms #