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?

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.

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.

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.

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.

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.

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.

@[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 α β

@[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 α β

@[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 α β

@[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 α β

@[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 α β

@[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 α β

@[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 α β

@[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 α β

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)

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)

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)

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.

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.

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.

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

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

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

Finitary supremum homomorphisms

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

Reinterpret a SupBotHom as a BotHom.

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

instance SupBotHom.instSupBotHomClass {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] : SupBotHomClass (SupBotHom α β) α β

theorem SupBotHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) : f.toFun = ⇑f

@[simp]

theorem SupBotHom.coe_toSupHom {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) : ⇑f.toSupHom = ⇑f

@[simp]

theorem SupBotHom.coe_toBotHom {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) : ⇑f.toBotHom = ⇑f

@[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

theorem SupBotHom.ext {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] {f g : SupBotHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem SupBotHom.ext_iff {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] {f g : SupBotHom α β} : f = g ↔ ∀ (a : α), f a = g a

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.

@[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'

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

def SupBotHom.id (α : Type u_2) [Max α] [Bot α] : SupBotHom α α

id as a SupBotHom.

@[simp]

theorem SupBotHom.id_toSupHom (α : Type u_2) [Max α] [Bot α] : (SupBotHom.id α).toSupHom = SupHom.id α

instance SupBotHom.instInhabited (α : Type u_2) [Max α] [Bot α] : Inhabited (SupBotHom α α)

@[simp]

theorem SupBotHom.coe_id (α : Type u_2) [Max α] [Bot α] : ⇑(SupBotHom.id α) = id

@[simp]

theorem SupBotHom.id_apply {α : Type u_2} [Max α] [Bot α] (a : α) : (SupBotHom.id α) a = a

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 SupBotHoms as a SupBotHom.

@[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

@[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)

@[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)

@[simp]

theorem SupBotHom.comp_id {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) : f.comp (SupBotHom.id α) = f

@[simp]

theorem SupBotHom.id_comp {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [Max β] [Bot β] (f : SupBotHom α β) : (SupBotHom.id β).comp f = f

@[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₂

@[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₂

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

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

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

@[simp]

theorem SupBotHom.coe_sup {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (f g : SupBotHom α β) : ⇑(f ⊔ g) = ⇑(f ⊔ g)

@[simp]

theorem SupBotHom.coe_bot {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] : ⇑⊥ = ⊥

@[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

@[simp]

theorem SupBotHom.bot_apply {α : Type u_2} {β : Type u_3} [Max α] [Bot α] [SemilatticeSup β] [OrderBot β] (a : α) : ⊥ a = ⊥

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.

@[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

@[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

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

Reinterpret an InfTopHom as a TopHom.

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

instance InfTopHom.instInfTopHomClass {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] : InfTopHomClass (InfTopHom α β) α β

theorem InfTopHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) : f.toFun = ⇑f

@[simp]

theorem InfTopHom.coe_toInfHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) : ⇑f.toInfHom = ⇑f

@[simp]

theorem InfTopHom.coe_toTopHom {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) : ⇑f.toTopHom = ⇑f

@[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

theorem InfTopHom.ext {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] {f g : InfTopHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem InfTopHom.ext_iff {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] {f g : InfTopHom α β} : f = g ↔ ∀ (a : α), f a = g a

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.

@[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'

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

def InfTopHom.id (α : Type u_2) [Min α] [Top α] : InfTopHom α α

id as an InfTopHom.

@[simp]

theorem InfTopHom.id_toInfHom (α : Type u_2) [Min α] [Top α] : (InfTopHom.id α).toInfHom = InfHom.id α

instance InfTopHom.instInhabited (α : Type u_2) [Min α] [Top α] : Inhabited (InfTopHom α α)

@[simp]

theorem InfTopHom.coe_id (α : Type u_2) [Min α] [Top α] : ⇑(InfTopHom.id α) = id

@[simp]

theorem InfTopHom.id_apply {α : Type u_2} [Min α] [Top α] (a : α) : (InfTopHom.id α) a = a

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 InfTopHoms as an InfTopHom.

@[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

@[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)

@[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)

@[simp]

theorem InfTopHom.comp_id {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) : f.comp (InfTopHom.id α) = f

@[simp]

theorem InfTopHom.id_comp {α : Type u_2} {β : Type u_3} [Min α] [Top α] [Min β] [Top β] (f : InfTopHom α β) : (InfTopHom.id β).comp f = f

@[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₂

@[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₂

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

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

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

@[simp]

theorem InfTopHom.coe_inf {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (f g : InfTopHom α β) : ⇑(f ⊓ g) = ⇑(f ⊓ g)

@[simp]

theorem InfTopHom.coe_top {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] : ⇑⊤ = ⊤

@[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

@[simp]

theorem InfTopHom.top_apply {α : Type u_2} {β : Type u_3} [Min α] [Top α] [SemilatticeInf β] [OrderTop β] (a : α) : ⊤ a = ⊤

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.

@[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

@[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

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

Reinterpret a BoundedLatticeHom as a SupBotHom.

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

Reinterpret a BoundedLatticeHom as an InfTopHom.

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

Reinterpret a BoundedLatticeHom as a BoundedOrderHom.

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

instance BoundedLatticeHom.instBoundedLatticeHomClass {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] : BoundedLatticeHomClass (BoundedLatticeHom α β) α β

@[simp]

theorem BoundedLatticeHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : f.toFun = ⇑f

@[simp]

theorem BoundedLatticeHom.coe_toLatticeHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : ⇑f.toLatticeHom = ⇑f

@[simp]

theorem BoundedLatticeHom.coe_toSupBotHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : ⇑f.toSupBotHom = ⇑f

@[simp]

theorem BoundedLatticeHom.coe_toInfTopHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : ⇑f.toInfTopHom = ⇑f

@[simp]

theorem BoundedLatticeHom.coe_toBoundedOrderHom {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : ⇑f.toBoundedOrderHom = ⇑f

@[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

theorem BoundedLatticeHom.ext {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] {f g : BoundedLatticeHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem BoundedLatticeHom.ext_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] {f g : BoundedLatticeHom α β} : f = g ↔ ∀ (a : α), f a = g a

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.

@[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'

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

def BoundedLatticeHom.id (α : Type u_2) [Lattice α] [BoundedOrder α] : BoundedLatticeHom α α

id as a BoundedLatticeHom.

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

@[simp]

theorem BoundedLatticeHom.coe_id (α : Type u_2) [Lattice α] [BoundedOrder α] : ⇑(BoundedLatticeHom.id α) = id

@[simp]

theorem BoundedLatticeHom.id_apply {α : Type u_2} [Lattice α] [BoundedOrder α] (a : α) : (BoundedLatticeHom.id α) a = a

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 BoundedLatticeHoms as a BoundedLatticeHom.

@[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

@[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)

@[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' := ⋯ }

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

@[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' := ⋯ }

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

@[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' := ⋯ }

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

@[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)

@[simp]

theorem BoundedLatticeHom.comp_id {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : f.comp (BoundedLatticeHom.id α) = f

@[simp]

theorem BoundedLatticeHom.id_comp {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : (BoundedLatticeHom.id β).comp f = f

@[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₂

@[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₂

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.

@[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

@[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

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.

@[simp]

theorem SupBotHom.dual_id {α : Type u_2} [Max α] [Bot α] : dual (SupBotHom.id α) = InfTopHom.id αᵒᵈ

@[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)

@[simp]

theorem SupBotHom.symm_dual_id {α : Type u_2} [Max α] [Bot α] : dual.symm (InfTopHom.id αᵒᵈ) = SupBotHom.id α

@[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)

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.

@[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

@[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

@[simp]

theorem InfTopHom.dual_id {α : Type u_2} [Min α] [Top α] : InfTopHom.dual (InfTopHom.id α) = SupBotHom.id αᵒᵈ

@[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)

@[simp]

theorem InfTopHom.symm_dual_id {α : Type u_2} [Min α] [Top α] : InfTopHom.dual.symm (SupBotHom.id αᵒᵈ) = InfTopHom.id α

@[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)

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.

@[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

@[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

@[simp]

theorem BoundedLatticeHom.dual_id {α : Type u_2} [Lattice α] [BoundedOrder α] : BoundedLatticeHom.dual (BoundedLatticeHom.id α) = BoundedLatticeHom.id αᵒᵈ

@[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)

@[simp]

theorem BoundedLatticeHom.symm_dual_id {α : Type u_2} [Lattice α] [BoundedOrder α] : BoundedLatticeHom.dual.symm (BoundedLatticeHom.id αᵒᵈ) = BoundedLatticeHom.id α

@[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)