# Bounded lattice homomorphisms #

This file defines bounded lattice homomorphisms.

We use the `DFunLike` 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 #

- `SupBotHom`: Finitary supremum homomorphisms. Maps which preserve `⊔` and `⊥`.
- `InfTopHom`: Finitary infimum homomorphisms. Maps which preserve `⊓` and `⊤`.
- `BoundedLatticeHom`: Bounded lattice homomorphisms. Maps which preserve `⊤`, `⊥`, `⊔` and `⊓`.

## Typeclasses #

- `SupBotHomClass`
- `InfTopHomClass`
- `BoundedLatticeHomClass`

## TODO #

Do we need more intersections between `BotHom`, `TopHom` and lattice homomorphisms?

source
structure SupBotHom (α : Type u_6) (β : Type u_7) [Max α] [Max β] [Bot α] [Bot β] extends SupHom α β :
Type (max u_6 u_7)

The type of finitary supremum-preserving homomorphisms from `α` to `β`.

- toFun : α → β
- map_sup' (a b : α) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
- map_bot' : self.toFun ⊥ = ⊥

  A `SupBotHom` preserves the bottom element.

  Do not use this directly. Use `map_bot` instead.

Instances For

source
structure InfTopHom (α : Type u_6) (β : Type u_7) [Min α] [Min β] [Top α] [Top β] extends InfHom α β :
Type (max u_6 u_7)

The type of finitary infimum-preserving homomorphisms from `α` to `β`.

- toFun : α → β
- map_inf' (a b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
- map_top' : self.toFun ⊤ = ⊤

  An `InfTopHom` preserves the top element.

  Do not use this directly. Use `map_top` instead.

Instances For

source
structure BoundedLatticeHom (α : Type u_6) (β : Type u_7) [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] extends LatticeHom α β :
Type (max u_6 u_7)

The type of bounded lattice homomorphisms from `α` to `β`.

- toFun : α → β
- map_sup' (a b : α) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
- map_inf' (a b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
- map_top' : self.toFun ⊤ = ⊤

  A `BoundedLatticeHom` preserves the top element.

  Do not use this directly. Use `map_top` instead.

- map_bot' : self.toFun ⊥ = ⊥

  A `BoundedLatticeHom` preserves the bottom element.

  Do not use this directly. Use `map_bot` instead.

Instances For

source
class SupBotHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Max α] [Max β] [Bot α] [Bot β] [FunLike F α β] extends SupHomClass F α β :
Prop

`SupBotHomClass F α β` states that `F` is a type of finitary supremum-preserving morphisms.

You should extend this class when you extend `SupBotHom`.

- map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b
- map_bot (f : F) : f ⊥ = ⊥

  A `SupBotHomClass` morphism preserves the bottom element.

Instances

source
class InfTopHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Min α] [Min β] [Top α] [Top β] [FunLike F α β] extends InfHomClass F α β :
Prop

`InfTopHomClass F α β` states that `F` is a type of finitary infimum-preserving morphisms.

You should extend this class when you extend `SupBotHom`.

- map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
- map_top (f : F) : f ⊤ = ⊤

  An `InfTopHomClass` morphism preserves the top element.

Instances

source
class BoundedLatticeHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] extends LatticeHomClass F α β :
Prop

`BoundedLatticeHomClass F α β` states that `F` is a type of bounded lattice morphisms.

You should extend this class when you extend `BoundedLatticeHom`.

- map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b
- map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
- map_top (f : F) : f ⊤ = ⊤

  A `BoundedLatticeHomClass` morphism preserves the top element.

- map_bot (f : F) : f ⊥ = ⊥

  A `BoundedLatticeHomClass` morphism preserves the bottom element.

Instances

source
@[instance 100]
instance SupBotHomClass.toBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] :
BotHomClass F α β
source
@[instance 100]
instance InfTopHomClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] :
TopHomClass F α β
source
@[instance 100]
instance BoundedLatticeHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
SupBotHomClass F α β
source
@[instance 100]
instance BoundedLatticeHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
InfTopHomClass F α β
source
@[instance 100]
instance BoundedLatticeHomClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
BoundedOrderHomClass F α β
source
@[instance 100]
instance OrderIsoClass.toSupBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] :
SupBotHomClass F α β
source
@[instance 100]
instance OrderIsoClass.toInfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [OrderIsoClass F α β] :
InfTopHomClass F α β
source
@[instance 100]
instance OrderIsoClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [OrderIsoClass F α β] :
BoundedLatticeHomClass F α β
source
theorem Disjoint.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [FunLike F α β] [OrderBot α] [OrderBot β] [BotHomClass F α β] [InfHomClass F α β] {a b : α} (f : F) (h : Disjoint a b) :
Disjoint (f a) (f b)
source
theorem Codisjoint.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [FunLike F α β] [OrderTop α] [OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α} (f : F) (h : Codisjoint a b) :
Codisjoint (f a) (f b)
source
theorem IsCompl.map {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [FunLike F α β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] {a b : α} (f : F) (h : IsCompl a b) :
IsCompl (f a) (f b)
source
theorem map_compl' {F : Type u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a : α) :
f a ᶜ = (f a)ᶜ

Special case of `map_compl` for Boolean algebras.

source
theorem map_sdiff' {F : Type u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a b : α) :
f (a \ b) = f a \ f b

Special case of `map_sdiff` for Boolean algebras.

source
theorem map_symmDiff' {F : Type u_1} {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a b : α) :
f (symmDiff a b) = symmDiff (f a) (f b)

Special case of `map_symmDiff` for Boolean algebras.

source
instance instCoeTCSupBotHomOfSupBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Max α] [Max β] [Bot α] [Bot β] [SupBotHomClass F α β] :
CoeTC F (SupBotHom α β)
Equations

- instCoeTCSupBotHomOfSupBotHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sup' := ⋯, map_bot' := ⋯ } }

source
instance instCoeTCInfTopHomOfInfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Min α] [Min β] [Top α] [Top β] [InfTopHomClass F α β] :
CoeTC F (InfTopHom α β)
Equations

- instCoeTCInfTopHomOfInfTopHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_inf' := ⋯, map_top' := ⋯ } }

source
instance instCoeTCBoundedLatticeHomOfBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] :
CoeTC F (BoundedLatticeHom α β)
Equations

- One or more equations did not get rendered due to their size.

### Finitary supremum homomorphisms #

source
def SupBotHom.toBotHom {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
BotHom α β

Reinterpret a `SupBotHom` as a `BotHom`.

Equations

- f.toBotHom = { toFun := f.toFun, map_bot' := ⋯ }

Instances For

source
instance SupBotHom.instFunLike {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] :
FunLike (SupBotHom α β) α β
Equations

- SupBotHom.instFunLike = { coe := fun (f : SupBotHom α β) => f.toFun, coe_injective' := ⋯ }

source
instance SupBotHom.instSupBotHomClass {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] :
SupBotHomClass (SupBotHom α β) α β
source
theorem SupBotHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
f.toFun = ⇑f
source
@[simp]
theorem SupBotHom.coe_toSupHom {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
⇑f.toSupHom = ⇑f
source
@[simp]
theorem SupBotHom.coe_toBotHom {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
⇑f.toBotHom = ⇑f
source
@[simp]
theorem SupBotHom.coe_mk {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupHom α β) (hf : f.toFun ⊥ = ⊥) :
⇑{ toSupHom := f, map_bot' := hf } = ⇑f
source
theorem SupBotHom.ext {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] {f g : SupBotHom α β} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem SupBotHom.ext_iff {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] {f g : SupBotHom α β} :
f = g ↔ ∀ (a : α), f a = g a
source
def SupBotHom.copy {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : α → β) (h : f' = ⇑f) :
SupBotHom α β

Copy of a `SupBotHom` with a new `toFun` equal to the old one. Useful to fix definitional equalities.

Equations

- f.copy f' h = { toSupHom := f.copy f' h, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem SupBotHom.coe_copy {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem SupBotHom.copy_eq {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
def SupBotHom.id (α : Type u_2) [Max α] [Bot α] :
SupBotHom α α

`id` as a `SupBotHom`.

Equations

- SupBotHom.id α = { toSupHom := SupHom.id α, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem SupBotHom.id_toSupHom (α : Type u_2) [Max α] [Bot α] :
(SupBotHom.id α).toSupHom = SupHom.id α
source
instance SupBotHom.instInhabited (α : Type u_2) [Max α] [Bot α] :
Inhabited (SupBotHom α α)
Equations

- SupBotHom.instInhabited α = { default := SupBotHom.id α }

source
@[simp]
theorem SupBotHom.coe_id (α : Type u_2) [Max α] [Bot α] :
⇑(SupBotHom.id α) = id
source
@[simp]
theorem SupBotHom.id_apply {α : Type u_2} [Max α] [Bot α] (a : α) :
(SupBotHom.id α) a = a
source
def SupBotHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) :
SupBotHom α γ

Composition of `SupBotHom`s as a `SupBotHom`.

Equations

- f.comp g = { toSupHom := f.comp g.toSupHom, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem SupBotHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem SupBotHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) (a : α) :
(f.comp g) a = f (g a)
source
@[simp]
theorem SupBotHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] [Max δ] [Bot δ] (f : SupBotHom γ δ) (g : SupBotHom β γ) (h : SupBotHom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem SupBotHom.comp_id {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
f.comp (SupBotHom.id α) = f
source
@[simp]
theorem SupBotHom.id_comp {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) :
(SupBotHom.id β).comp f = f
source
@[simp]
theorem SupBotHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] {g₁ g₂ : SupBotHom β γ} {f : SupBotHom α β} (hf : Function.Surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
@[simp]
theorem SupBotHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] {g : SupBotHom β γ} {f₁ f₂ : SupBotHom α β} (hg : Function.Injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
instance SupBotHom.instMax {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
Max (SupBotHom α β)
Equations

- One or more equations did not get rendered due to their size.

source
instance SupBotHom.instSemilatticeSup {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
SemilatticeSup (SupBotHom α β)
Equations

- SupBotHom.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : SupBotHom α β) => ⇑f) ⋯ ⋯

source
instance SupBotHom.instOrderBot {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
OrderBot (SupBotHom α β)
Equations

- SupBotHom.instOrderBot = { bot := { toSupHom := ⊥, map_bot' := ⋯ }, bot_le := ⋯ }

source
@[simp]
theorem SupBotHom.coe_sup {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (f g : SupBotHom α β) :
⇑(f ⊔ g) = ⇑(f ⊔ g)
source
@[simp]
theorem SupBotHom.coe_bot {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] :
⇑⊥ = ⊥
source
@[simp]
theorem SupBotHom.sup_apply {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (f g : SupBotHom α β) (a : α) :
(f ⊔ g) a = f a ⊔ g a
source
@[simp]
theorem SupBotHom.bot_apply {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (a : α) :
⊥ a = ⊥
source
def SupBotHom.subtypeVal {β : Type u_3} [SemilatticeSup β] [OrderBot β] {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
SupBotHom { x : β // P x } β

`Subtype.val` as a `SupBotHom`.

Equations

- SupBotHom.subtypeVal Pbot Psup = { toSupHom := SupHom.subtypeVal Psup, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem SupBotHom.subtypeVal_apply {β : Type u_3} [SemilatticeSup β] [OrderBot β] {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : { x : β // P x }) :
(subtypeVal Pbot Psup) x = ↑x
source
@[simp]
theorem SupBotHom.subtypeVal_coe {β : Type u_3} [SemilatticeSup β] [OrderBot β] {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) :
⇑(subtypeVal Pbot Psup) = Subtype.val

### Finitary infimum homomorphisms #

source
def InfTopHom.toTopHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
TopHom α β

Reinterpret an `InfTopHom` as a `TopHom`.

Equations

- f.toTopHom = { toFun := f.toFun, map_top' := ⋯ }

Instances For

source
instance InfTopHom.instFunLike {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] :
FunLike (InfTopHom α β) α β
Equations

- InfTopHom.instFunLike = { coe := fun (f : InfTopHom α β) => f.toFun, coe_injective' := ⋯ }

source
instance InfTopHom.instInfTopHomClass {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] :
InfTopHomClass (InfTopHom α β) α β
source
theorem InfTopHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
f.toFun = ⇑f
source
@[simp]
theorem InfTopHom.coe_toInfHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
⇑f.toInfHom = ⇑f
source
@[simp]
theorem InfTopHom.coe_toTopHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
⇑f.toTopHom = ⇑f
source
@[simp]
theorem InfTopHom.coe_mk {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfHom α β) (hf : f.toFun ⊤ = ⊤) :
⇑{ toInfHom := f, map_top' := hf } = ⇑f
source
theorem InfTopHom.ext {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] {f g : InfTopHom α β} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem InfTopHom.ext_iff {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] {f g : InfTopHom α β} :
f = g ↔ ∀ (a : α), f a = g a
source
def InfTopHom.copy {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : α → β) (h : f' = ⇑f) :
InfTopHom α β

Copy of an `InfTopHom` with a new `toFun` equal to the old one. Useful to fix definitional equalities.

Equations

- f.copy f' h = { toInfHom := f.copy f' h, map_top' := ⋯ }

Instances For

source
@[simp]
theorem InfTopHom.coe_copy {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem InfTopHom.copy_eq {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
def InfTopHom.id (α : Type u_2) [Min α] [Top α] :
InfTopHom α α

`id` as an `InfTopHom`.

Equations

- InfTopHom.id α = { toInfHom := InfHom.id α, map_top' := ⋯ }

Instances For

source
@[simp]
theorem InfTopHom.id_toInfHom (α : Type u_2) [Min α] [Top α] :
(InfTopHom.id α).toInfHom = InfHom.id α
source
instance InfTopHom.instInhabited (α : Type u_2) [Min α] [Top α] :
Inhabited (InfTopHom α α)
Equations

- InfTopHom.instInhabited α = { default := InfTopHom.id α }

source
@[simp]
theorem InfTopHom.coe_id (α : Type u_2) [Min α] [Top α] :
⇑(InfTopHom.id α) = id
source
@[simp]
theorem InfTopHom.id_apply {α : Type u_2} [Min α] [Top α] (a : α) :
(InfTopHom.id α) a = a
source
def InfTopHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) :
InfTopHom α γ

Composition of `InfTopHom`s as an `InfTopHom`.

Equations

- f.comp g = { toInfHom := f.comp g.toInfHom, map_top' := ⋯ }

Instances For

source
@[simp]
theorem InfTopHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem InfTopHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) (a : α) :
(f.comp g) a = f (g a)
source
@[simp]
theorem InfTopHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] [Min δ] [Top δ] (f : InfTopHom γ δ) (g : InfTopHom β γ) (h : InfTopHom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem InfTopHom.comp_id {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
f.comp (InfTopHom.id α) = f
source
@[simp]
theorem InfTopHom.id_comp {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
(InfTopHom.id β).comp f = f
source
@[simp]
theorem InfTopHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] {g₁ g₂ : InfTopHom β γ} {f : InfTopHom α β} (hf : Function.Surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
@[simp]
theorem InfTopHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] {g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β} (hg : Function.Injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
instance InfTopHom.instMin {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
Min (InfTopHom α β)
Equations

- One or more equations did not get rendered due to their size.

source
instance InfTopHom.instSemilatticeInf {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
SemilatticeInf (InfTopHom α β)
Equations

- InfTopHom.instSemilatticeInf = Function.Injective.semilatticeInf (fun (f : InfTopHom α β) => ⇑f) ⋯ ⋯

source
instance InfTopHom.instOrderTop {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
OrderTop (InfTopHom α β)
Equations

- InfTopHom.instOrderTop = { top := { toInfHom := ⊤, map_top' := ⋯ }, le_top := ⋯ }

source
@[simp]
theorem InfTopHom.coe_inf {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (f g : InfTopHom α β) :
⇑(f ⊓ g) = ⇑(f ⊓ g)
source
@[simp]
theorem InfTopHom.coe_top {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] :
⇑⊤ = ⊤
source
@[simp]
theorem InfTopHom.inf_apply {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (f g : InfTopHom α β) (a : α) :
(f ⊓ g) a = f a ⊓ g a
source
@[simp]
theorem InfTopHom.top_apply {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (a : α) :
⊤ a = ⊤
source
def InfTopHom.subtypeVal {β : Type u_3} [SemilatticeInf β] [OrderTop β] {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
InfTopHom { x : β // P x } β

`Subtype.val` as an `InfTopHom`.

Equations

- InfTopHom.subtypeVal Ptop Pinf = { toInfHom := InfHom.subtypeVal Pinf, map_top' := ⋯ }

Instances For

source
@[simp]
theorem InfTopHom.subtypeVal_apply {β : Type u_3} [SemilatticeInf β] [OrderTop β] {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) :
(subtypeVal Ptop Pinf) x = ↑x
source
@[simp]
theorem InfTopHom.subtypeVal_coe {β : Type u_3} [SemilatticeInf β] [OrderTop β] {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
⇑(subtypeVal Ptop Pinf) = Subtype.val

### Bounded lattice homomorphisms #

source
def BoundedLatticeHom.toSupBotHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
SupBotHom α β

Reinterpret a `BoundedLatticeHom` as a `SupBotHom`.

Equations

- f.toSupBotHom = { toSupHom := f.toSupHom, map_bot' := ⋯ }

Instances For

source
def BoundedLatticeHom.toInfTopHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
InfTopHom α β

Reinterpret a `BoundedLatticeHom` as an `InfTopHom`.

Equations

- f.toInfTopHom = { toFun := f.toFun, map_inf' := ⋯, map_top' := ⋯ }

Instances For

source
def BoundedLatticeHom.toBoundedOrderHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
BoundedOrderHom α β

Reinterpret a `BoundedLatticeHom` as a `BoundedOrderHom`.

Equations

- f.toBoundedOrderHom = { toFun := f.toFun, monotone' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

Instances For

source
instance BoundedLatticeHom.instFunLike {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] :
FunLike (BoundedLatticeHom α β) α β
Equations

- BoundedLatticeHom.instFunLike = { coe := fun (f : BoundedLatticeHom α β) => f.toFun, coe_injective' := ⋯ }

source
instance BoundedLatticeHom.instBoundedLatticeHomClass {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] :
BoundedLatticeHomClass (BoundedLatticeHom α β) α β
source
@[simp]
theorem BoundedLatticeHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
f.toFun = ⇑f
source
@[simp]
theorem BoundedLatticeHom.coe_toLatticeHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
⇑f.toLatticeHom = ⇑f
source
@[simp]
theorem BoundedLatticeHom.coe_toSupBotHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
⇑f.toSupBotHom = ⇑f
source
@[simp]
theorem BoundedLatticeHom.coe_toInfTopHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
⇑f.toInfTopHom = ⇑f
source
@[simp]
theorem BoundedLatticeHom.coe_toBoundedOrderHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
⇑f.toBoundedOrderHom = ⇑f
source
@[simp]
theorem BoundedLatticeHom.coe_mk {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : LatticeHom α β) (hf : f.toFun ⊤ = ⊤) (hf' : f.toFun ⊥ = ⊥) :
⇑{ toLatticeHom := f, map_top' := hf, map_bot' := hf' } = ⇑f
source
theorem BoundedLatticeHom.ext {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] {f g : BoundedLatticeHom α β} (h : ∀ (a : α), f a = g a) :
f = g
source
theorem BoundedLatticeHom.ext_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] {f g : BoundedLatticeHom α β} :
f = g ↔ ∀ (a : α), f a = g a
source
def BoundedLatticeHom.copy {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f) :
BoundedLatticeHom α β

Copy of a `BoundedLatticeHom` with a new `toFun` equal to the old one. Useful to fix definitional equalities.

Equations

- f.copy f' h = { toLatticeHom := f.copy f' h, map_top' := ⋯, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem BoundedLatticeHom.coe_copy {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem BoundedLatticeHom.copy_eq {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f) :
f.copy f' h = f
source
def BoundedLatticeHom.id (α : Type u_2) [Lattice α] [BoundedOrder α] :
BoundedLatticeHom α α

`id` as a `BoundedLatticeHom`.

Equations

- BoundedLatticeHom.id α = { toLatticeHom := LatticeHom.id α, map_top' := ⋯, map_bot' := ⋯ }

Instances For

source
instance BoundedLatticeHom.instInhabited (α : Type u_2) [Lattice α] [BoundedOrder α] :
Inhabited (BoundedLatticeHom α α)
Equations

- BoundedLatticeHom.instInhabited α = { default := BoundedLatticeHom.id α }

source
@[simp]
theorem BoundedLatticeHom.coe_id (α : Type u_2) [Lattice α] [BoundedOrder α] :
⇑(BoundedLatticeHom.id α) = id
source
@[simp]
theorem BoundedLatticeHom.id_apply {α : Type u_2} [Lattice α] [BoundedOrder α] (a : α) :
(BoundedLatticeHom.id α) a = a
source
def BoundedLatticeHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
BoundedLatticeHom α γ

Composition of `BoundedLatticeHom`s as a `BoundedLatticeHom`.

Equations

- f.comp g = { toLatticeHom := f.comp g.toLatticeHom, map_top' := ⋯, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem BoundedLatticeHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem BoundedLatticeHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) (a : α) :
(f.comp g) a = f (g a)
source
@[simp]
theorem BoundedLatticeHom.coe_comp_lattice_hom' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toSupHom := { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }, map_inf' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
source
theorem BoundedLatticeHom.coe_comp_lattice_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toFun := ⇑(f.comp g), map_sup' := ⋯, map_inf' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
source
@[simp]
theorem BoundedLatticeHom.coe_comp_sup_hom' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
source
theorem BoundedLatticeHom.coe_comp_sup_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
source
@[simp]
theorem BoundedLatticeHom.coe_comp_inf_hom' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
source
theorem BoundedLatticeHom.coe_comp_inf_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) :
{ toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
source
@[simp]
theorem BoundedLatticeHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [Lattice δ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] [BoundedOrder δ] (f : BoundedLatticeHom γ δ) (g : BoundedLatticeHom β γ) (h : BoundedLatticeHom α β) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem BoundedLatticeHom.comp_id {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
f.comp (BoundedLatticeHom.id α) = f
source
@[simp]
theorem BoundedLatticeHom.id_comp {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) :
(BoundedLatticeHom.id β).comp f = f
source
@[simp]
theorem BoundedLatticeHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g₁ g₂ : BoundedLatticeHom β γ} {f : BoundedLatticeHom α β} (hf : Function.Surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
@[simp]
theorem BoundedLatticeHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g : BoundedLatticeHom β γ} {f₁ f₂ : BoundedLatticeHom α β} (hg : Function.Injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
def BoundedLatticeHom.subtypeVal {β : Type u_3} [Lattice β] [BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
BoundedLatticeHom { x : β // P x } β

`Subtype.val` as a `BoundedLatticeHom`.

Equations

- BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf = { toLatticeHom := LatticeHom.subtypeVal Psup Pinf, map_top' := ⋯, map_bot' := ⋯ }

Instances For

source
@[simp]
theorem BoundedLatticeHom.subtypeVal_apply {β : Type u_3} [Lattice β] [BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) :
(subtypeVal Pbot Ptop Psup Pinf) x = ↑x
source
@[simp]
theorem BoundedLatticeHom.subtypeVal_coe {β : Type u_3} [Lattice β] [BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) :
⇑(subtypeVal Pbot Ptop Psup Pinf) = Subtype.val

### Dual homs #

source
def SupBotHom.dual {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] :
SupBotHom α β ≃ InfTopHom α ᵒᵈ β ᵒᵈ

Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual lattices.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem SupBotHom.dual_id {α : Type u_2} [Max α] [Bot α] :
dual (SupBotHom.id α) = InfTopHom.id α ᵒᵈ
source
@[simp]
theorem SupBotHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (g : SupBotHom β γ) (f : SupBotHom α β) :
dual (g.comp f) = (dual g).comp (dual f)
source
@[simp]
theorem SupBotHom.symm_dual_id {α : Type u_2} [Max α] [Bot α] :
dual.symm (InfTopHom.id α ᵒᵈ) = SupBotHom.id α
source
@[simp]
theorem SupBotHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Max α] [Bot α] [Max β] [Bot β] [Max γ] [Bot γ] (g : InfTopHom β ᵒᵈ γ ᵒᵈ) (f : InfTopHom α ᵒᵈ β ᵒᵈ) :
dual.symm (g.comp f) = (dual.symm g).comp (dual.symm f)
source
def InfTopHom.dual {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] :
InfTopHom α β ≃ SupBotHom α ᵒᵈ β ᵒᵈ

Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual lattices.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem InfTopHom.dual_symm_apply_toInfHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : SupBotHom α ᵒᵈ β ᵒᵈ) :
(InfTopHom.dual.symm f).toInfHom = InfHom.dual.symm f.toSupHom
source
@[simp]
theorem InfTopHom.dual_apply_toSupHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) :
(InfTopHom.dual f).toSupHom = InfHom.dual f.toInfHom
source
@[simp]
theorem InfTopHom.dual_id {α : Type u_2} [Min α] [Top α] :
InfTopHom.dual (InfTopHom.id α) = SupBotHom.id α ᵒᵈ
source
@[simp]
theorem InfTopHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (g : InfTopHom β γ) (f : InfTopHom α β) :
InfTopHom.dual (g.comp f) = (InfTopHom.dual g).comp (InfTopHom.dual f)
source
@[simp]
theorem InfTopHom.symm_dual_id {α : Type u_2} [Min α] [Top α] :
InfTopHom.dual.symm (SupBotHom.id α ᵒᵈ) = InfTopHom.id α
source
@[simp]
theorem InfTopHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Min α] [Top α] [Min β] [Top β] [Min γ] [Top γ] (g : SupBotHom β ᵒᵈ γ ᵒᵈ) (f : SupBotHom α ᵒᵈ β ᵒᵈ) :
InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)
source
def BoundedLatticeHom.dual {α : Type u_2} {β : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] :
BoundedLatticeHom α β ≃ BoundedLatticeHom α ᵒᵈ β ᵒᵈ

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem BoundedLatticeHom.dual_apply_toLatticeHom {α : Type u_2} {β : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom α β) :
(BoundedLatticeHom.dual f).toLatticeHom = LatticeHom.dual f.toLatticeHom
source
@[simp]
theorem BoundedLatticeHom.dual_symm_apply_toLatticeHom {α : Type u_2} {β : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom α ᵒᵈ β ᵒᵈ) :
(BoundedLatticeHom.dual.symm f).toLatticeHom = LatticeHom.dual.symm f.toLatticeHom
source
@[simp]
theorem BoundedLatticeHom.dual_id {α : Type u_2} [Lattice α] [BoundedOrder α] :
BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id α ᵒᵈ
source
@[simp]
theorem BoundedLatticeHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β) :
BoundedLatticeHom.dual (g.comp f) = (BoundedLatticeHom.dual g).comp (BoundedLatticeHom.dual f)
source
@[simp]
theorem BoundedLatticeHom.symm_dual_id {α : Type u_2} [Lattice α] [BoundedOrder α] :
BoundedLatticeHom.dual.symm (BoundedLatticeHom.id α ᵒᵈ) = BoundedLatticeHom.id α
source
@[simp]
theorem BoundedLatticeHom.symm_dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (g : BoundedLatticeHom β ᵒᵈ γ ᵒᵈ) (f : BoundedLatticeHom α ᵒᵈ β ᵒᵈ) :
BoundedLatticeHom.dual.symm (g.comp f) = (BoundedLatticeHom.dual.symm g).comp (BoundedLatticeHom.dual.symm f)