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

• SupHom: Maps which preserve ⊔.
• InfHom: Maps which preserve ⊓.
• SupBotHom: Finitary supremum homomorphisms. Maps which preserve ⊔ and ⊥.
• InfTopHom: Finitary infimum homomorphisms. Maps which preserve ⊓ and ⊤.
• LatticeHom: Lattice homomorphisms. Maps which preserve ⊔ and ⊓.
• BoundedLatticeHom: Bounded lattice homomorphisms. Maps which preserve ⊤, ⊥, ⊔ and ⊓.

Typeclasses

• SupHomClass
• InfHomClass
• SupBotHomClass
• InfTopHomClass
• LatticeHomClass
• BoundedLatticeHomClass

TODO

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

structure SupHom (α : Type u_7) (β : Type u_8) [Sup α] [Sup β] : Type (max u_7 u_8)

The type of ⊔-preserving functions from α to β.

• toFun : α → β

  The underlying function of a SupHom

• map_sup' : ∀ (a b : α), self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b

  A SupHom preserves suprema.

theorem SupHom.map_sup' {α : Type u_7} {β : Type u_8} [Sup α] [Sup β] (self : SupHom α β) (a : α) (b : α) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b

A SupHom preserves suprema.

structure InfHom (α : Type u_7) (β : Type u_8) [Inf α] [Inf β] : Type (max u_7 u_8)

The type of ⊓-preserving functions from α to β.

• toFun : α → β

  The underlying function of an InfHom

• map_inf' : ∀ (a b : α), self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b

  An InfHom preserves infima.

theorem InfHom.map_inf' {α : Type u_7} {β : Type u_8} [Inf α] [Inf β] (self : InfHom α β) (a : α) (b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b

An InfHom preserves infima.

structure SupBotHom (α : Type u_7) (β : Type u_8) [Sup α] [Sup β] [Bot α] [Bot β] extends SupHom : Type (max u_7 u_8)

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.

theorem SupBotHom.map_bot' {α : Type u_7} {β : Type u_8} [Sup α] [Sup β] [Bot α] [Bot β] (self : SupBotHom α β) : self.toFun ⊥ = ⊥

A SupBotHom preserves the bottom element.

structure InfTopHom (α : Type u_7) (β : Type u_8) [Inf α] [Inf β] [Top α] [Top β] extends InfHom : Type (max u_7 u_8)

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.

theorem InfTopHom.map_top' {α : Type u_7} {β : Type u_8} [Inf α] [Inf β] [Top α] [Top β] (self : InfTopHom α β) : self.toFun ⊤ = ⊤

An InfTopHom preserves the top element.

structure LatticeHom (α : Type u_7) (β : Type u_8) [Lattice α] [Lattice β] extends SupHom : Type (max u_7 u_8)

The type of 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

  A LatticeHom preserves infima.

theorem LatticeHom.map_inf' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] (self : LatticeHom α β) (a : α) (b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b

A LatticeHom preserves infima.

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

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.

• map_bot' : self.toFun ⊥ = ⊥

  A BoundedLatticeHom preserves the bottom element.

theorem BoundedLatticeHom.map_top' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (self : BoundedLatticeHom α β) : self.toFun ⊤ = ⊤

A BoundedLatticeHom preserves the top element.

theorem BoundedLatticeHom.map_bot' {α : Type u_7} {β : Type u_8} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (self : BoundedLatticeHom α β) : self.toFun ⊥ = ⊥

A BoundedLatticeHom preserves the bottom element.

class SupHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Sup α] [Sup β] [FunLike F α β] : Prop

SupHomClass F α β states that F is a type of ⊔-preserving morphisms.

You should extend this class when you extend SupHom.

• map_sup : ∀ (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b

  A SupHomClass morphism preserves suprema.

@[simp]

theorem SupHomClass.map_sup {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Sup α} {inst_1 : Sup β} {inst_2 : FunLike F α β} [self : SupHomClass F α β] (f : F) (a b : α), f (a ⊔ b) = f a ⊔ f b

A SupHomClass morphism preserves suprema.

class InfHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Inf α] [Inf β] [FunLike F α β] : Prop

InfHomClass F α β states that F is a type of ⊓-preserving morphisms.

You should extend this class when you extend InfHom.

• map_inf : ∀ (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b

  An InfHomClass morphism preserves infima.

@[simp]

theorem InfHomClass.map_inf {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Inf α} {inst_1 : Inf β} {inst_2 : FunLike F α β} [self : InfHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b

An InfHomClass morphism preserves infima.

class SupBotHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Sup α] [Sup β] [Bot α] [Bot β] [FunLike F α β] extends SupHomClass : 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.

theorem SupBotHomClass.map_bot {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Sup α} {inst_1 : Sup β} {inst_2 : Bot α} {inst_3 : Bot β} {inst_4 : FunLike F α β} [self : SupBotHomClass F α β] (f : F), f ⊥ = ⊥

A SupBotHomClass morphism preserves the bottom element.

class InfTopHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Inf α] [Inf β] [Top α] [Top β] [FunLike F α β] extends InfHomClass : 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.

theorem InfTopHomClass.map_top {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Inf α} {inst_1 : Inf β} {inst_2 : Top α} {inst_3 : Top β} {inst_4 : FunLike F α β} [self : InfTopHomClass F α β] (f : F), f ⊤ = ⊤

An InfTopHomClass morphism preserves the top element.

class LatticeHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Lattice α] [Lattice β] [FunLike F α β] extends SupHomClass : Prop

LatticeHomClass F α β states that F is a type of lattice morphisms.

You should extend this class when you extend LatticeHom.

• 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

  A LatticeHomClass morphism preserves infima.

theorem LatticeHomClass.map_inf {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : FunLike F α β} [self : LatticeHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b

A LatticeHomClass morphism preserves infima.

class BoundedLatticeHomClass (F : Type u_7) (α : Type u_8) (β : Type u_9) [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [FunLike F α β] extends LatticeHomClass : 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.

theorem BoundedLatticeHomClass.map_top {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f ⊤ = ⊤

A BoundedLatticeHomClass morphism preserves the top element.

theorem BoundedLatticeHomClass.map_bot {F : Type u_7} {α : Type u_8} {β : Type u_9} : ∀ {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α} {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β] (f : F), f ⊥ = ⊥

A BoundedLatticeHomClass morphism preserves the bottom element.

@[instance 100]

instance SupHomClass.toOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] : OrderHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance InfHomClass.toOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] : OrderHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance SupBotHomClass.toBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Sup α] [Sup β] [Bot α] [Bot β] [SupBotHomClass F α β] : BotHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance InfTopHomClass.toTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Inf α] [Inf β] [Top α] [Top β] [InfTopHomClass F α β] : TopHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance LatticeHomClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] : InfHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance BoundedLatticeHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : SupBotHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance BoundedLatticeHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : InfTopHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance BoundedLatticeHomClass.toBoundedOrderHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [BoundedLatticeHomClass F α β] : BoundedOrderHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toSupHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeSup α] [SemilatticeSup β] [OrderIsoClass F α β] : SupHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeInf α] [SemilatticeInf β] [OrderIsoClass F α β] : InfHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toSupBotHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [OrderIsoClass F α β] : SupBotHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toInfTopHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [OrderIsoClass F α β] : InfTopHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [Lattice α] [Lattice β] [OrderIsoClass F α β] : LatticeHomClass F α β

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderIsoClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [EquivLike F α β] [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] [OrderIsoClass F α β] : BoundedLatticeHomClass F α β

Equations

• ⋯ = ⋯

@[simp]

theorem orderEmbeddingOfInjective_apply {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Function.Injective ⇑f) (a : α) : (orderEmbeddingOfInjective f hf) a = f a

def orderEmbeddingOfInjective {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Function.Injective ⇑f) : α ↪o β

We can regard an injective map preserving binary infima as an order embedding.

Equations

• orderEmbeddingOfInjective f hf = OrderEmbedding.ofMapLEIff ⇑f ⋯

theorem Disjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : Disjoint a b) : Disjoint (f a) (f b)

theorem Codisjoint.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : Codisjoint a b) : Codisjoint (f a) (f b)

theorem IsCompl.map {F : Type u_1} {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) {a : α} {b : α} (h : IsCompl a b) : IsCompl (f a) (f b)

theorem map_compl' {F : Type u_1} {α : Type u_3} {β : Type u_4} [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_3} {β : Type u_4} [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_3} {β : Type u_4} [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 instCoeTCSupHomOfSupHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Sup α] [Sup β] [SupHomClass F α β] : CoeTC F (SupHom α β)

Equations

• instCoeTCSupHomOfSupHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sup' := ⋯ } }

instance instCoeTCInfHomOfInfHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Inf α] [Inf β] [InfHomClass F α β] : CoeTC F (InfHom α β)

Equations

• instCoeTCInfHomOfInfHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_inf' := ⋯ } }

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

Equations

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

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

Equations

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

instance instCoeTCLatticeHomOfLatticeHomClass {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [Lattice α] [Lattice β] [LatticeHomClass F α β] : CoeTC F (LatticeHom α β)

Equations

• instCoeTCLatticeHomOfLatticeHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } }

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

Equations

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

Supremum homomorphisms

instance SupHom.instFunLike {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] : FunLike (SupHom α β) α β

Equations

• SupHom.instFunLike = { coe := SupHom.toFun, coe_injective' := ⋯ }

instance SupHom.instSupHomClass {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] : SupHomClass (SupHom α β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem SupHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) : f.toFun = ⇑f

@[simp]

theorem SupHom.coe_mk {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : α → β) (hf : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) : ⇑{ toFun := f, map_sup' := hf } = f

theorem SupHom.ext_iff {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] {f : SupHom α β} {g : SupHom α β} : f = g ↔ ∀ (a : α), f a = g a

theorem SupHom.ext {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] {f : SupHom α β} {g : SupHom α β} (h : ∀ (a : α), f a = g a) : f = g

def SupHom.copy {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f) : SupHom α β

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

Equations

• f.copy f' h = { toFun := f', map_sup' := ⋯ }

@[simp]

theorem SupHom.coe_copy {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem SupHom.copy_eq {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def SupHom.id (α : Type u_3) [Sup α] : SupHom α α

id as a SupHom.

Equations

• SupHom.id α = { toFun := id, map_sup' := ⋯ }

instance SupHom.instInhabited (α : Type u_3) [Sup α] : Inhabited (SupHom α α)

Equations

• SupHom.instInhabited α = { default := SupHom.id α }

@[simp]

theorem SupHom.coe_id (α : Type u_3) [Sup α] : ⇑(SupHom.id α) = id

@[simp]

theorem SupHom.id_apply {α : Type u_3} [Sup α] (a : α) : (SupHom.id α) a = a

def SupHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (f : SupHom β γ) (g : SupHom α β) : SupHom α γ

Composition of SupHoms as a SupHom.

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ }

@[simp]

theorem SupHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (f : SupHom β γ) (g : SupHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem SupHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (f : SupHom β γ) (g : SupHom α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem SupHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Sup α] [Sup β] [Sup γ] [Sup δ] (f : SupHom γ δ) (g : SupHom β γ) (h : SupHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem SupHom.comp_id {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) : f.comp (SupHom.id α) = f

@[simp]

theorem SupHom.id_comp {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) : (SupHom.id β).comp f = f

@[simp]

theorem SupHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] {g₁ : SupHom β γ} {g₂ : SupHom β γ} {f : SupHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem SupHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] {g : SupHom β γ} {f₁ : SupHom α β} {f₂ : SupHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

def SupHom.const (α : Type u_3) {β : Type u_4} [Sup α] [SemilatticeSup β] (b : β) : SupHom α β

The constant function as a SupHom.

Equations

• SupHom.const α b = { toFun := fun (x : α) => b, map_sup' := ⋯ }

@[simp]

theorem SupHom.coe_const (α : Type u_3) {β : Type u_4} [Sup α] [SemilatticeSup β] (b : β) : ⇑(SupHom.const α b) = Function.const α b

@[simp]

theorem SupHom.const_apply (α : Type u_3) {β : Type u_4} [Sup α] [SemilatticeSup β] (b : β) (a : α) : (SupHom.const α b) a = b

instance SupHom.instSup {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] : Sup (SupHom α β)

Equations

• SupHom.instSup = { sup := fun (f g : SupHom α β) => { toFun := ⇑f ⊔ ⇑g, map_sup' := ⋯ } }

instance SupHom.instSemilatticeSup {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] : SemilatticeSup (SupHom α β)

Equations

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

instance SupHom.instBot {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Bot β] : Bot (SupHom α β)

Equations

• SupHom.instBot = { bot := SupHom.const α ⊥ }

instance SupHom.instTop {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Top β] : Top (SupHom α β)

Equations

• SupHom.instTop = { top := SupHom.const α ⊤ }

instance SupHom.instOrderBot {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [OrderBot β] : OrderBot (SupHom α β)

Equations

• SupHom.instOrderBot = OrderBot.lift DFunLike.coe ⋯ ⋯

instance SupHom.instOrderTop {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [OrderTop β] : OrderTop (SupHom α β)

Equations

• SupHom.instOrderTop = OrderTop.lift DFunLike.coe ⋯ ⋯

instance SupHom.instBoundedOrder {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [BoundedOrder β] : BoundedOrder (SupHom α β)

Equations

• SupHom.instBoundedOrder = BoundedOrder.lift DFunLike.coe ⋯ ⋯ ⋯

@[simp]

theorem SupHom.coe_sup {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] (f : SupHom α β) (g : SupHom α β) : ⇑(f ⊔ g) = ⇑(f ⊔ g)

@[simp]

theorem SupHom.coe_bot {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Bot β] : ⇑⊥ = ⊥

@[simp]

theorem SupHom.coe_top {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Top β] : ⇑⊤ = ⊤

@[simp]

theorem SupHom.sup_apply {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] (f : SupHom α β) (g : SupHom α β) (a : α) : (f ⊔ g) a = f a ⊔ g a

@[simp]

theorem SupHom.bot_apply {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Bot β] (a : α) : ⊥ a = ⊥

@[simp]

theorem SupHom.top_apply {α : Type u_3} {β : Type u_4} [Sup α] [SemilatticeSup β] [Top β] (a : α) : ⊤ a = ⊤

def SupHom.subtypeVal {β : Type u_4} [SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) : SupHom { x : β // P x } β

Subtype.val as a SupHom.

Equations

• SupHom.subtypeVal Psup = { toFun := Subtype.val, map_sup' := ⋯ }

@[simp]

theorem SupHom.subtypeVal_apply {β : Type u_4} [SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : { x : β // P x }) : (SupHom.subtypeVal Psup) x = ↑x

@[simp]

theorem SupHom.subtypeVal_coe {β : Type u_4} [SemilatticeSup β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) : ⇑(SupHom.subtypeVal Psup) = Subtype.val

Infimum homomorphisms

instance InfHom.instFunLike {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] : FunLike (InfHom α β) α β

Equations

• InfHom.instFunLike = { coe := InfHom.toFun, coe_injective' := ⋯ }

instance InfHom.instInfHomClass {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] : InfHomClass (InfHom α β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem InfHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) : f.toFun = ⇑f

@[simp]

theorem InfHom.coe_mk {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : α → β) (hf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) : ⇑{ toFun := f, map_inf' := hf } = f

theorem InfHom.ext_iff {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] {f : InfHom α β} {g : InfHom α β} : f = g ↔ ∀ (a : α), f a = g a

theorem InfHom.ext {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] {f : InfHom α β} {g : InfHom α β} (h : ∀ (a : α), f a = g a) : f = g

def InfHom.copy {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f) : InfHom α β

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

Equations

• f.copy f' h = { toFun := f', map_inf' := ⋯ }

@[simp]

theorem InfHom.coe_copy {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem InfHom.copy_eq {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def InfHom.id (α : Type u_3) [Inf α] : InfHom α α

id as an InfHom.

Equations

• InfHom.id α = { toFun := id, map_inf' := ⋯ }

instance InfHom.instInhabited (α : Type u_3) [Inf α] : Inhabited (InfHom α α)

Equations

• InfHom.instInhabited α = { default := InfHom.id α }

@[simp]

theorem InfHom.coe_id (α : Type u_3) [Inf α] : ⇑(InfHom.id α) = id

@[simp]

theorem InfHom.id_apply {α : Type u_3} [Inf α] (a : α) : (InfHom.id α) a = a

def InfHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (f : InfHom β γ) (g : InfHom α β) : InfHom α γ

Composition of InfHoms as an InfHom.

Equations

• f.comp g = { toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ }

@[simp]

theorem InfHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (f : InfHom β γ) (g : InfHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem InfHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (f : InfHom β γ) (g : InfHom α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem InfHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Inf α] [Inf β] [Inf γ] [Inf δ] (f : InfHom γ δ) (g : InfHom β γ) (h : InfHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem InfHom.comp_id {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) : f.comp (InfHom.id α) = f

@[simp]

theorem InfHom.id_comp {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) : (InfHom.id β).comp f = f

@[simp]

theorem InfHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] {g₁ : InfHom β γ} {g₂ : InfHom β γ} {f : InfHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem InfHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] {g : InfHom β γ} {f₁ : InfHom α β} {f₂ : InfHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

def InfHom.const (α : Type u_3) {β : Type u_4} [Inf α] [SemilatticeInf β] (b : β) : InfHom α β

The constant function as an InfHom.

Equations

• InfHom.const α b = { toFun := fun (x : α) => b, map_inf' := ⋯ }

@[simp]

theorem InfHom.coe_const (α : Type u_3) {β : Type u_4} [Inf α] [SemilatticeInf β] (b : β) : ⇑(InfHom.const α b) = Function.const α b

@[simp]

theorem InfHom.const_apply (α : Type u_3) {β : Type u_4} [Inf α] [SemilatticeInf β] (b : β) (a : α) : (InfHom.const α b) a = b

instance InfHom.instInf {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] : Inf (InfHom α β)

Equations

• InfHom.instInf = { inf := fun (f g : InfHom α β) => { toFun := ⇑f ⊓ ⇑g, map_inf' := ⋯ } }

instance InfHom.instSemilatticeInf {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] : SemilatticeInf (InfHom α β)

Equations

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

instance InfHom.instBot {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Bot β] : Bot (InfHom α β)

Equations

• InfHom.instBot = { bot := InfHom.const α ⊥ }

instance InfHom.instTop {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Top β] : Top (InfHom α β)

Equations

• InfHom.instTop = { top := InfHom.const α ⊤ }

instance InfHom.instOrderBot {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [OrderBot β] : OrderBot (InfHom α β)

Equations

• InfHom.instOrderBot = OrderBot.lift DFunLike.coe ⋯ ⋯

instance InfHom.instOrderTop {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [OrderTop β] : OrderTop (InfHom α β)

Equations

• InfHom.instOrderTop = OrderTop.lift DFunLike.coe ⋯ ⋯

instance InfHom.instBoundedOrder {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [BoundedOrder β] : BoundedOrder (InfHom α β)

Equations

• InfHom.instBoundedOrder = BoundedOrder.lift DFunLike.coe ⋯ ⋯ ⋯

@[simp]

theorem InfHom.coe_inf {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] (f : InfHom α β) (g : InfHom α β) : ⇑(f ⊓ g) = ⇑(f ⊓ g)

@[simp]

theorem InfHom.coe_bot {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Bot β] : ⇑⊥ = ⊥

@[simp]

theorem InfHom.coe_top {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Top β] : ⇑⊤ = ⊤

@[simp]

theorem InfHom.inf_apply {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] (f : InfHom α β) (g : InfHom α β) (a : α) : (f ⊓ g) a = f a ⊓ g a

@[simp]

theorem InfHom.bot_apply {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Bot β] (a : α) : ⊥ a = ⊥

@[simp]

theorem InfHom.top_apply {α : Type u_3} {β : Type u_4} [Inf α] [SemilatticeInf β] [Top β] (a : α) : ⊤ a = ⊤

def InfHom.subtypeVal {β : Type u_4} [SemilatticeInf β] {P : β → Prop} (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) : InfHom { x : β // P x } β

Subtype.val as an InfHom.

Equations

• InfHom.subtypeVal Pinf = { toFun := Subtype.val, map_inf' := ⋯ }

@[simp]

theorem InfHom.subtypeVal_apply {β : Type u_4} [SemilatticeInf β] {P : β → Prop} (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) : (InfHom.subtypeVal Pinf) x = ↑x

@[simp]

theorem InfHom.subtypeVal_coe {β : Type u_4} [SemilatticeInf β] {P : β → Prop} (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) : ⇑(InfHom.subtypeVal Pinf) = Subtype.val

Finitary supremum homomorphisms

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

Reinterpret a SupBotHom as a BotHom.

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

@[simp]

theorem SupBotHom.coe_mk {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : SupHom α β) (hf : f.toFun ⊥ = ⊥) : ⇑{ toSupHom := f, map_bot' := hf } = ⇑f

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

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

def SupBotHom.copy {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [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' := ⋯ }

@[simp]

theorem SupBotHom.coe_copy {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : SupBotHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem SupBotHom.copy_eq {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [Bot β] (f : SupBotHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

@[simp]

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

def SupBotHom.id (α : Type u_3) [Sup α] [Bot α] : SupBotHom α α

id as a SupBotHom.

Equations

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

instance SupBotHom.instInhabited (α : Type u_3) [Sup α] [Bot α] : Inhabited (SupBotHom α α)

Equations

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

@[simp]

theorem SupBotHom.coe_id (α : Type u_3) [Sup α] [Bot α] : ⇑(SupBotHom.id α) = id

@[simp]

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

def SupBotHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) : SupBotHom α γ

Composition of SupBotHoms as a SupBotHom.

Equations

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

@[simp]

theorem SupBotHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem SupBotHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (f : SupBotHom β γ) (g : SupBotHom α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem SupBotHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] [Sup δ] [Bot δ] (f : SupBotHom γ δ) (g : SupBotHom β γ) (h : SupBotHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

theorem SupBotHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] {g₁ : SupBotHom β γ} {g₂ : SupBotHom β γ} {f : SupBotHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem SupBotHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] {g : SupBotHom β γ} {f₁ : SupBotHom α β} {f₂ : SupBotHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance SupBotHom.instSup {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [SemilatticeSup β] [OrderBot β] : Sup (SupBotHom α β)

Equations

• SupBotHom.instSup = { sup := fun (f g : SupBotHom α β) => let __src := f.toBotHom ⊔ g.toBotHom; { toSupHom := f.toSupHom ⊔ g.toSupHom, map_bot' := ⋯ } }

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

Equations

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

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

Equations

• SupBotHom.instOrderBot = OrderBot.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem SupBotHom.sup_apply {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [SemilatticeSup β] [OrderBot β] (f : SupBotHom α β) (g : SupBotHom α β) (a : α) : (f ⊔ g) a = f a ⊔ g a

@[simp]

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

def SupBotHom.subtypeVal {β : Type u_4} [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' := ⋯ }

@[simp]

theorem SupBotHom.subtypeVal_apply {β : Type u_4} [SemilatticeSup β] [OrderBot β] {P : β → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (x : { x : β // P x }) : (SupBotHom.subtypeVal Pbot Psup) x = ↑x

@[simp]

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

Finitary infimum homomorphisms

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

Reinterpret an InfTopHom as a TopHom.

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

@[simp]

theorem InfTopHom.coe_mk {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : InfHom α β) (hf : f.toFun ⊤ = ⊤) : ⇑{ toInfHom := f, map_top' := hf } = ⇑f

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

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

def InfTopHom.copy {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [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' := ⋯ }

@[simp]

theorem InfTopHom.coe_copy {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : InfTopHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem InfTopHom.copy_eq {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : InfTopHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

@[simp]

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

def InfTopHom.id (α : Type u_3) [Inf α] [Top α] : InfTopHom α α

id as an InfTopHom.

Equations

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

instance InfTopHom.instInhabited (α : Type u_3) [Inf α] [Top α] : Inhabited (InfTopHom α α)

Equations

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

@[simp]

theorem InfTopHom.coe_id (α : Type u_3) [Inf α] [Top α] : ⇑(InfTopHom.id α) = id

@[simp]

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

def InfTopHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) : InfTopHom α γ

Composition of InfTopHoms as an InfTopHom.

Equations

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

@[simp]

theorem InfTopHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem InfTopHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (f : InfTopHom β γ) (g : InfTopHom α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem InfTopHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] [Inf δ] [Top δ] (f : InfTopHom γ δ) (g : InfTopHom β γ) (h : InfTopHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

theorem InfTopHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] {g₁ : InfTopHom β γ} {g₂ : InfTopHom β γ} {f : InfTopHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem InfTopHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] {g : InfTopHom β γ} {f₁ : InfTopHom α β} {f₂ : InfTopHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance InfTopHom.instInf {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [SemilatticeInf β] [OrderTop β] : Inf (InfTopHom α β)

Equations

• InfTopHom.instInf = { inf := fun (f g : InfTopHom α β) => let __src := f.toTopHom ⊓ g.toTopHom; { toInfHom := f.toInfHom ⊓ g.toInfHom, map_top' := ⋯ } }

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

Equations

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

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

Equations

• InfTopHom.instOrderTop = OrderTop.mk ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem InfTopHom.inf_apply {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [SemilatticeInf β] [OrderTop β] (f : InfTopHom α β) (g : InfTopHom α β) (a : α) : (f ⊓ g) a = f a ⊓ g a

@[simp]

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

def InfTopHom.subtypeVal {β : Type u_4} [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' := ⋯ }

@[simp]

theorem InfTopHom.subtypeVal_apply {β : Type u_4} [SemilatticeInf β] [OrderTop β] {P : β → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) : (InfTopHom.subtypeVal Ptop Pinf) x = ↑x

@[simp]

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

Lattice homomorphisms

def LatticeHom.toInfHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : InfHom α β

Reinterpret a LatticeHom as an InfHom.

Equations

• f.toInfHom = { toFun := f.toFun, map_inf' := ⋯ }

instance LatticeHom.instFunLike {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : FunLike (LatticeHom α β) α β

Equations

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

instance LatticeHom.instLatticeHomClass {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : LatticeHomClass (LatticeHom α β) α β

Equations

• ⋯ = ⋯

theorem LatticeHom.toFun_eq_coe {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : f.toFun = ⇑f

@[simp]

theorem LatticeHom.coe_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.toSupHom = ⇑f

@[simp]

theorem LatticeHom.coe_toInfHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.toInfHom = ⇑f

@[simp]

theorem LatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : SupHom α β) (hf : ∀ (a b : α), f.toFun (a ⊓ b) = f.toFun a ⊓ f.toFun b) : ⇑{ toSupHom := f, map_inf' := hf } = ⇑f

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

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

def LatticeHom.copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : α → β) (h : f' = ⇑f) : LatticeHom α β

Copy of a LatticeHom 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_inf' := ⋯ }

@[simp]

theorem LatticeHom.coe_copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem LatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

def LatticeHom.id (α : Type u_3) [Lattice α] : LatticeHom α α

id as a LatticeHom.

Equations

• LatticeHom.id α = { toFun := id, map_sup' := ⋯, map_inf' := ⋯ }

instance LatticeHom.instInhabited (α : Type u_3) [Lattice α] : Inhabited (LatticeHom α α)

Equations

• LatticeHom.instInhabited α = { default := LatticeHom.id α }

@[simp]

theorem LatticeHom.coe_id (α : Type u_3) [Lattice α] : ⇑(LatticeHom.id α) = id

@[simp]

theorem LatticeHom.id_apply {α : Type u_3} [Lattice α] (a : α) : (LatticeHom.id α) a = a

def LatticeHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : LatticeHom α γ

Composition of LatticeHoms as a LatticeHom.

Equations

• f.comp g = { toSupHom := f.comp g.toSupHom, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem LatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) (a : α) : (f.comp g) a = f (g a)

@[simp]

theorem LatticeHom.coe_comp_sup_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : { toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }

theorem LatticeHom.coe_comp_sup_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : { toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }

@[simp]

theorem LatticeHom.coe_comp_inf_hom' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : { toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }

theorem LatticeHom.coe_comp_inf_hom {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : { toFun := ⇑(f.comp g), map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.comp_assoc {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [Lattice α] [Lattice β] [Lattice γ] [Lattice δ] (f : LatticeHom γ δ) (g : LatticeHom β γ) (h : LatticeHom α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem LatticeHom.comp_id {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : f.comp (LatticeHom.id α) = f

@[simp]

theorem LatticeHom.id_comp {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : (LatticeHom.id β).comp f = f

@[simp]

theorem LatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] {g₁ : LatticeHom β γ} {g₂ : LatticeHom β γ} {f : LatticeHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem LatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] {g : LatticeHom β γ} {f₁ : LatticeHom α β} {f₂ : LatticeHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

def LatticeHom.subtypeVal {β : Type u_4} [Lattice β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) : LatticeHom { x : β // P x } β

Subtype.val as a LatticeHom.

Equations

• LatticeHom.subtypeVal Psup Pinf = { toSupHom := SupHom.subtypeVal Psup, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.subtypeVal_apply {β : Type u_4} [Lattice β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) (x : { x : β // P x }) : (LatticeHom.subtypeVal Psup Pinf) x = ↑x

@[simp]

theorem LatticeHom.subtypeVal_coe {β : Type u_4} [Lattice β] {P : β → Prop} (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) : ⇑(LatticeHom.subtypeVal Psup Pinf) = Subtype.val

@[instance 100]

instance OrderHomClass.toLatticeHomClass {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] : LatticeHomClass F α β

An order homomorphism from a linear order is a lattice homomorphism.

Equations

• ⋯ = ⋯

def OrderHomClass.toLatticeHom {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) : LatticeHom α β

Reinterpret an order homomorphism to a linear order as a LatticeHom.

Equations

• OrderHomClass.toLatticeHom α β f = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem OrderHomClass.coe_to_lattice_hom {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) : ⇑(OrderHomClass.toLatticeHom α β f) = ⇑f

@[simp]

theorem OrderHomClass.to_lattice_hom_apply {F : Type u_1} (α : Type u_3) (β : Type u_4) [FunLike F α β] [LinearOrder α] [Lattice β] [OrderHomClass F α β] (f : F) (a : α) : (OrderHomClass.toLatticeHom α β f) a = f a

Bounded lattice homomorphisms

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

Reinterpret a BoundedLatticeHom as a SupBotHom.

Equations

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

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

Reinterpret a BoundedLatticeHom as an InfTopHom.

Equations

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

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

Reinterpret a BoundedLatticeHom as a BoundedOrderHom.

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BoundedLatticeHom.coe_mk {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : LatticeHom α β) (hf : f.toFun ⊤ = ⊤) (hf' : f.toFun ⊥ = ⊥) : ⇑{ toLatticeHom := f, map_top' := hf, map_bot' := hf' } = ⇑f

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

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

def BoundedLatticeHom.copy {α : Type u_3} {β : Type u_4} [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' := ⋯ }

@[simp]

theorem BoundedLatticeHom.coe_copy {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

theorem BoundedLatticeHom.copy_eq {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) (f' : α → β) (h : f' = ⇑f) : f.copy f' h = f

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

id as a BoundedLatticeHom.

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

def BoundedLatticeHom.comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : BoundedLatticeHom α γ

Composition of BoundedLatticeHoms as a BoundedLatticeHom.

Equations

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

@[simp]

theorem BoundedLatticeHom.coe_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] (f : BoundedLatticeHom β γ) (g : BoundedLatticeHom α β) : ⇑(f.comp g) = ⇑f ∘ ⇑g

@[simp]

theorem BoundedLatticeHom.comp_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} [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_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [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_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder α] [BoundedOrder β] (f : BoundedLatticeHom α β) : f.comp (BoundedLatticeHom.id α) = f

@[simp]

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

@[simp]

theorem BoundedLatticeHom.cancel_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g₁ : BoundedLatticeHom β γ} {g₂ : BoundedLatticeHom β γ} {f : BoundedLatticeHom α β} (hf : Function.Surjective ⇑f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem BoundedLatticeHom.cancel_left {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] [BoundedOrder α] [BoundedOrder β] [BoundedOrder γ] {g : BoundedLatticeHom β γ} {f₁ : BoundedLatticeHom α β} {f₂ : BoundedLatticeHom α β} (hg : Function.Injective ⇑g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

def BoundedLatticeHom.subtypeVal {β : Type u_4} [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' := ⋯ }

@[simp]

theorem BoundedLatticeHom.subtypeVal_apply {β : Type u_4} [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 }) : (BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf) x = ↑x

@[simp]

theorem BoundedLatticeHom.subtypeVal_coe {β : Type u_4} [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.subtypeVal Pbot Ptop Psup Pinf) = Subtype.val

Dual homs

@[simp]

theorem SupHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : InfHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) : (SupHom.dual.symm f) a = f a

@[simp]

theorem SupHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] (f : SupHom α β) (a : α) : (SupHom.dual f) a = f a

def SupHom.dual {α : Type u_3} {β : Type u_4} [Sup α] [Sup β] : SupHom α β ≃ InfHom αᵒᵈ βᵒᵈ

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

Equations

• SupHom.dual = { toFun := fun (f : SupHom α β) => { toFun := ⇑f, map_inf' := ⋯ }, invFun := fun (f : InfHom αᵒᵈ βᵒᵈ) => { toFun := ⇑f, map_sup' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SupHom.dual_id {α : Type u_3} [Sup α] : SupHom.dual (SupHom.id α) = InfHom.id αᵒᵈ

@[simp]

theorem SupHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (g : SupHom β γ) (f : SupHom α β) : SupHom.dual (g.comp f) = (SupHom.dual g).comp (SupHom.dual f)

@[simp]

theorem SupHom.symm_dual_id {α : Type u_3} [Sup α] : SupHom.dual.symm (InfHom.id αᵒᵈ) = SupHom.id α

@[simp]

theorem SupHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Sup β] [Sup γ] (g : InfHom βᵒᵈ γᵒᵈ) (f : InfHom αᵒᵈ βᵒᵈ) : SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f)

@[simp]

theorem InfHom.dual_apply_toFun {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : InfHom α β) (a : α) : (InfHom.dual f) a = f a

@[simp]

theorem InfHom.dual_symm_apply_toFun {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] (f : SupHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ) : (InfHom.dual.symm f) a = f a

def InfHom.dual {α : Type u_3} {β : Type u_4} [Inf α] [Inf β] : InfHom α β ≃ SupHom αᵒᵈ βᵒᵈ

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

Equations

• InfHom.dual = { toFun := fun (f : InfHom α β) => { toFun := ⇑f, map_sup' := ⋯ }, invFun := fun (f : SupHom αᵒᵈ βᵒᵈ) => { toFun := ⇑f, map_inf' := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem InfHom.dual_id {α : Type u_3} [Inf α] : InfHom.dual (InfHom.id α) = SupHom.id αᵒᵈ

@[simp]

theorem InfHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (g : InfHom β γ) (f : InfHom α β) : InfHom.dual (g.comp f) = (InfHom.dual g).comp (InfHom.dual f)

@[simp]

theorem InfHom.symm_dual_id {α : Type u_3} [Inf α] : InfHom.dual.symm (SupHom.id αᵒᵈ) = InfHom.id α

@[simp]

theorem InfHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Inf β] [Inf γ] (g : SupHom βᵒᵈ γᵒᵈ) (f : SupHom αᵒᵈ βᵒᵈ) : InfHom.dual.symm (g.comp f) = (InfHom.dual.symm g).comp (InfHom.dual.symm f)

def SupBotHom.dual {α : Type u_3} {β : Type u_4} [Sup α] [Bot α] [Sup β] [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.

@[simp]

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

@[simp]

theorem SupBotHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (g : SupBotHom β γ) (f : SupBotHom α β) : SupBotHom.dual (g.comp f) = (SupBotHom.dual g).comp (SupBotHom.dual f)

@[simp]

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

@[simp]

theorem SupBotHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Sup α] [Bot α] [Sup β] [Bot β] [Sup γ] [Bot γ] (g : InfTopHom βᵒᵈ γᵒᵈ) (f : InfTopHom αᵒᵈ βᵒᵈ) : SupBotHom.dual.symm (g.comp f) = (SupBotHom.dual.symm g).comp (SupBotHom.dual.symm f)

@[simp]

theorem InfTopHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : InfTopHom α β) : (InfTopHom.dual f).toSupHom = InfHom.dual f.toInfHom

@[simp]

theorem InfTopHom.dual_symm_apply_toInfHom {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [Top β] (f : SupBotHom αᵒᵈ βᵒᵈ) : (InfTopHom.dual.symm f).toInfHom = InfHom.dual.symm f.toSupHom

def InfTopHom.dual {α : Type u_3} {β : Type u_4} [Inf α] [Top α] [Inf β] [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.

@[simp]

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

@[simp]

theorem InfTopHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [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_3} [Inf α] [Top α] : InfTopHom.dual.symm (SupBotHom.id αᵒᵈ) = InfTopHom.id α

@[simp]

theorem InfTopHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Inf α] [Top α] [Inf β] [Top β] [Inf γ] [Top γ] (g : SupBotHom βᵒᵈ γᵒᵈ) (f : SupBotHom αᵒᵈ βᵒᵈ) : InfTopHom.dual.symm (g.comp f) = (InfTopHom.dual.symm g).comp (InfTopHom.dual.symm f)

@[simp]

theorem LatticeHom.dual_symm_apply_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom αᵒᵈ βᵒᵈ) : (LatticeHom.dual.symm f).toSupHom = SupHom.dual.symm f.toInfHom

@[simp]

theorem LatticeHom.dual_apply_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : (LatticeHom.dual f).toSupHom = InfHom.dual f.toInfHom

def LatticeHom.dual {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : LatticeHom α β ≃ LatticeHom αᵒᵈ βᵒᵈ

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

Equations

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

@[simp]

theorem LatticeHom.dual_id {α : Type u_3} [Lattice α] : LatticeHom.dual (LatticeHom.id α) = LatticeHom.id αᵒᵈ

@[simp]

theorem LatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (g : LatticeHom β γ) (f : LatticeHom α β) : LatticeHom.dual (g.comp f) = (LatticeHom.dual g).comp (LatticeHom.dual f)

@[simp]

theorem LatticeHom.symm_dual_id {α : Type u_3} [Lattice α] : LatticeHom.dual.symm (LatticeHom.id αᵒᵈ) = LatticeHom.id α

@[simp]

theorem LatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (g : LatticeHom βᵒᵈ γᵒᵈ) (f : LatticeHom αᵒᵈ βᵒᵈ) : LatticeHom.dual.symm (g.comp f) = (LatticeHom.dual.symm g).comp (LatticeHom.dual.symm f)

@[simp]

theorem BoundedLatticeHom.dual_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom α β) : (BoundedLatticeHom.dual f).toLatticeHom = LatticeHom.dual f.toLatticeHom

@[simp]

theorem BoundedLatticeHom.dual_symm_apply_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : BoundedLatticeHom αᵒᵈ βᵒᵈ) : (BoundedLatticeHom.dual.symm f).toLatticeHom = LatticeHom.dual.symm f.toLatticeHom

def BoundedLatticeHom.dual {α : Type u_3} {β : Type u_4} [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.

@[simp]

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

@[simp]

theorem BoundedLatticeHom.dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [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_3} [Lattice α] [BoundedOrder α] : BoundedLatticeHom.dual.symm (BoundedLatticeHom.id αᵒᵈ) = BoundedLatticeHom.id α

@[simp]

theorem BoundedLatticeHom.symm_dual_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [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)

Prod

def LatticeHom.fst {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : LatticeHom (α × β) α

Natural projection homomorphism from α × β to α.

Equations

• LatticeHom.fst = { toFun := Prod.fst, map_sup' := ⋯, map_inf' := ⋯ }

def LatticeHom.snd {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : LatticeHom (α × β) β

Natural projection homomorphism from α × β to β.

Equations

• LatticeHom.snd = { toFun := Prod.snd, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.coe_fst {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : ⇑LatticeHom.fst = Prod.fst

@[simp]

theorem LatticeHom.coe_snd {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] : ⇑LatticeHom.snd = Prod.snd

theorem LatticeHom.fst_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (x : α × β) : LatticeHom.fst x = x.1

theorem LatticeHom.snd_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (x : α × β) : LatticeHom.snd x = x.2

Pi

def Pi.evalLatticeHom {ι : Type u_7} {α : ι → Type u_8} [(i : ι) → Lattice (α i)] (i : ι) : LatticeHom ((i : ι) → α i) (α i)

Evaluation as a lattice homomorphism.

Equations

• Pi.evalLatticeHom i = { toFun := Function.eval i, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem Pi.coe_evalLatticeHom {ι : Type u_7} {α : ι → Type u_8} [(i : ι) → Lattice (α i)] (i : ι) : ⇑(Pi.evalLatticeHom i) = Function.eval i

theorem Pi.evalLatticeHom_apply {ι : Type u_7} {α : ι → Type u_8} [(i : ι) → Lattice (α i)] (i : ι) (f : (i : ι) → α i) : (Pi.evalLatticeHom i) f = f i

WithTop, WithBot

@[simp]

theorem SupHom.withTop_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : ∀ (a : WithTop α), f.withTop a = WithTop.map (⇑f) a

def SupHom.withTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : SupHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of a SupHom.

Equations

• f.withTop = { toFun := WithTop.map ⇑f, map_sup' := ⋯ }

@[simp]

theorem SupHom.withTop_id {α : Type u_3} [SemilatticeSup α] : (SupHom.id α).withTop = SupHom.id (WithTop α)

@[simp]

theorem SupHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

@[simp]

theorem SupHom.withBot_toSupHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : ∀ (a : Option α), f.withBot.toSupHom a = Option.map (⇑f) a

def SupHom.withBot {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : SupBotHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of a SupHom.

Equations

• f.withBot = { toFun := Option.map ⇑f, map_sup' := ⋯, map_bot' := ⋯ }

@[simp]

theorem SupHom.withBot_id {α : Type u_3} [SemilatticeSup α] : (SupHom.id α).withBot = SupBotHom.id (WithBot α)

@[simp]

theorem SupHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

@[simp]

theorem SupHom.withTop'_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) (a : WithTop α) : f.withTop' a = Option.elim a ⊤ ⇑f

def SupHom.withTop' {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) : SupHom (WithTop α) β

Adjoins a ⊤ to the codomain of a SupHom.

Equations

• f.withTop' = { toFun := fun (a : WithTop α) => Option.elim a ⊤ ⇑f, map_sup' := ⋯ }

@[simp]

theorem SupHom.withBot'_toSupHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) (a : WithBot α) : f.withBot'.toSupHom a = Option.elim a ⊥ ⇑f

def SupHom.withBot' {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) : SupBotHom (WithBot α) β

Adjoins a ⊥ to the domain of a SupHom.

Equations

• f.withBot' = { toFun := fun (a : WithBot α) => Option.elim a ⊥ ⇑f, map_sup' := ⋯, map_bot' := ⋯ }

@[simp]

theorem InfHom.withTop_toInfHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : ∀ (a : Option α), f.withTop.toInfHom a = Option.map (⇑f) a

def InfHom.withTop {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : InfTopHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of an InfHom.

Equations

• f.withTop = { toFun := Option.map ⇑f, map_inf' := ⋯, map_top' := ⋯ }

@[simp]

theorem InfHom.withTop_id {α : Type u_3} [SemilatticeInf α] : (InfHom.id α).withTop = InfTopHom.id (WithTop α)

@[simp]

theorem InfHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

@[simp]

theorem InfHom.withBot_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : ∀ (a : Option α), f.withBot a = Option.map (⇑f) a

def InfHom.withBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : InfHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of an InfHom.

Equations

• f.withBot = { toFun := Option.map ⇑f, map_inf' := ⋯ }

@[simp]

theorem InfHom.withBot_id {α : Type u_3} [SemilatticeInf α] : (InfHom.id α).withBot = InfHom.id (WithBot α)

@[simp]

theorem InfHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

@[simp]

theorem InfHom.withTop'_toInfHom_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) (a : WithTop α) : f.withTop'.toInfHom a = Option.elim a ⊤ ⇑f

def InfHom.withTop' {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) : InfTopHom (WithTop α) β

Adjoins a ⊤ to the codomain of an InfHom.

Equations

• f.withTop' = { toFun := fun (a : WithTop α) => Option.elim a ⊤ ⇑f, map_inf' := ⋯, map_top' := ⋯ }

@[simp]

theorem InfHom.withBot'_toFun {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) (a : WithBot α) : f.withBot' a = Option.elim a ⊥ ⇑f

def InfHom.withBot' {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) : InfHom (WithBot α) β

Adjoins a ⊥ to the codomain of an InfHom.

Equations

• f.withBot' = { toFun := fun (a : WithBot α) => Option.elim a ⊥ ⇑f, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.withTop_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : f.withTop.toSupHom = f.withTop

def LatticeHom.withTop {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : LatticeHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of a LatticeHom.

Equations

• f.withTop = { toSupHom := f.withTop, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.coe_withTop {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withTop = WithTop.map ⇑f

theorem LatticeHom.withTop_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop α) : f.withTop a = WithTop.map (⇑f) a

@[simp]

theorem LatticeHom.withTop_id {α : Type u_3} [Lattice α] : (LatticeHom.id α).withTop = LatticeHom.id (WithTop α)

@[simp]

theorem LatticeHom.withTop_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

@[simp]

theorem LatticeHom.withBot_toSupHom_toFun {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) : f.withBot.toSupHom a = f.withBot a

def LatticeHom.withBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : LatticeHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of a LatticeHom.

Equations

• f.withBot = { toFun := ⇑f.withBot, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.coe_withBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withBot = Option.map ⇑f

theorem LatticeHom.withBot_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) : f.withBot a = WithBot.map (⇑f) a

@[simp]

theorem LatticeHom.withBot_id {α : Type u_3} [Lattice α] : (LatticeHom.id α).withBot = LatticeHom.id (WithBot α)

@[simp]

theorem LatticeHom.withBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

@[simp]

theorem LatticeHom.withTopWithBot_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : f.withTopWithBot.toLatticeHom = f.withBot.withTop

def LatticeHom.withTopWithBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : BoundedLatticeHom (WithTop (WithBot α)) (WithTop (WithBot β))

Adjoins a ⊤ and ⊥ to the domain and codomain of a LatticeHom.

Equations

• f.withTopWithBot = { toLatticeHom := f.withBot.withTop, map_top' := ⋯, map_bot' := ⋯ }

@[simp]

theorem LatticeHom.coe_withTopWithBot {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withTopWithBot = Option.map (Option.map ⇑f)

theorem LatticeHom.withTopWithBot_apply {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop (WithBot α)) : f.withTopWithBot a = WithTop.map (Option.map ⇑f) a

@[simp]

theorem LatticeHom.withTopWithBot_id {α : Type u_3} [Lattice α] : (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id (WithTop (WithBot α))

@[simp]

theorem LatticeHom.withTopWithBot_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

@[simp]

theorem LatticeHom.withTop'_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) : f.withTop'.toSupHom = f.withTop'

def LatticeHom.withTop' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) : LatticeHom (WithTop α) β

Adjoins a ⊥ to the codomain of a LatticeHom.

Equations

• f.withTop' = { toSupHom := f.withTop', map_inf' := ⋯ }

@[simp]

theorem LatticeHom.withBot'_toSupHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) : f.withBot'.toSupHom = f.withBot'.toSupHom

def LatticeHom.withBot' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) : LatticeHom (WithBot α) β

Adjoins a ⊥ to the domain and codomain of a LatticeHom.

Equations

• f.withBot' = { toSupHom := f.withBot'.toSupHom, map_inf' := ⋯ }

@[simp]

theorem LatticeHom.withTopWithBot'_toLatticeHom {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) : f.withTopWithBot'.toLatticeHom = f.withBot'.withTop'

def LatticeHom.withTopWithBot' {α : Type u_3} {β : Type u_4} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) : BoundedLatticeHom (WithTop (WithBot α)) β

Adjoins a ⊤ and ⊥ to the codomain of a LatticeHom.

Equations

• f.withTopWithBot' = { toLatticeHom := f.withBot'.withTop', map_top' := ⋯, map_bot' := ⋯ }