Unbounded lattice homomorphisms

This file defines unbounded lattice homomorphisms. Bounded lattice homomorphisms are defined in Mathlib/Order/Hom/BoundedLattice.lean.

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 ⊓.
• LatticeHom: Lattice homomorphisms. Maps which preserve ⊔ and ⊓.

Typeclasses

• SupHomClass
• InfHomClass
• LatticeHomClass

structure SupHom (α : Type u_6) (β : Type u_7) [Max α] [Max β] : Type (max u_6 u_7)

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

• toFun : α → β

  The underlying function of a SupHom.

  Do not use this function directly. Instead use the coercion coming from the FunLike instance.

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

  A SupHom preserves suprema.

  Do not use this directly. Use map_sup instead.

structure InfHom (α : Type u_6) (β : Type u_7) [Min α] [Min β] : Type (max u_6 u_7)

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

• toFun : α → β

  The underlying function of an InfHom.

  Do not use this function directly. Instead use the coercion coming from the FunLike instance.

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

  An InfHom preserves infima.

  Do not use this directly. Use map_inf instead.

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

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.

  Do not use this directly. Use map_inf instead.

class SupHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Max α] [Max β] [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.

class InfHomClass (F : Type u_6) (α : Type u_7) (β : Type u_8) [Min α] [Min β] [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.

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

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

@[simp]

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

instance instCoeTCSupHomOfSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Max α] [Max β] [SupHomClass F α β] : CoeTC F (SupHom α β)

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

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

Supremum homomorphisms

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

id as a SupHom.

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

@[simp]

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

@[simp]

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

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

Composition of SupHoms as a SupHom.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The constant function as a SupHom.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem SupHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Max α] [SemilatticeSup β] (toFun₁ toFun₂ : α → β) (map_sup₁ : ∀ (a b : α), toFun₁ (a ⊔ b) = toFun₁ a ⊔ toFun₁ b) (map_sup₂ : ∀ (a b : α), toFun₂ (a ⊔ b) = toFun₂ a ⊔ toFun₂ b) : { toFun := toFun₁, map_sup' := map_sup₁ } ≤ { toFun := toFun₂, map_sup' := map_sup₂ } ↔ toFun₁ ≤ toFun₂

theorem GCongr.SupHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Max α] [SemilatticeSup β] (toFun₁ toFun₂ : α → β) (map_sup₁ : ∀ (a b : α), toFun₁ (a ⊔ b) = toFun₁ a ⊔ toFun₁ b) (map_sup₂ : ∀ (a b : α), toFun₂ (a ⊔ b) = toFun₂ a ⊔ toFun₂ b) : toFun₁ ≤ toFun₂ → { toFun := toFun₁, map_sup' := map_sup₁ } ≤ { toFun := toFun₂, map_sup' := map_sup₂ }

Alias of the reverse direction of SupHom.mk_le_mk.

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

Subtype.val as a SupHom.

@[simp]

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

@[simp]

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

Infimum homomorphisms

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

id as an InfHom.

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

@[simp]

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

@[simp]

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

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

Composition of InfHoms as an InfHom.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The constant function as an InfHom.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem InfHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Min α] [SemilatticeInf β] (toFun₁ toFun₂ : α → β) (map_inf₁ : ∀ (a b : α), toFun₁ (a ⊓ b) = toFun₁ a ⊓ toFun₁ b) (map_inf₂ : ∀ (a b : α), toFun₂ (a ⊓ b) = toFun₂ a ⊓ toFun₂ b) : { toFun := toFun₁, map_inf' := map_inf₁ } ≤ { toFun := toFun₂, map_inf' := map_inf₂ } ↔ toFun₁ ≤ toFun₂

theorem GCongr.InfHom.mk_le_mk {α : Type u_2} {β : Type u_3} [Min α] [SemilatticeInf β] (toFun₁ toFun₂ : α → β) (map_inf₁ : ∀ (a b : α), toFun₁ (a ⊓ b) = toFun₁ a ⊓ toFun₁ b) (map_inf₂ : ∀ (a b : α), toFun₂ (a ⊓ b) = toFun₂ a ⊓ toFun₂ b) : toFun₁ ≤ toFun₂ → { toFun := toFun₁, map_inf' := map_inf₁ } ≤ { toFun := toFun₂, map_inf' := map_inf₂ }

Alias of the reverse direction of InfHom.mk_le_mk.

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

Subtype.val as an InfHom.

@[simp]

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

@[simp]

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

Lattice homomorphisms

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

Reinterpret a LatticeHom as an InfHom.

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LatticeHom.coe_mk {α : Type u_2} {β : Type u_3} [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 {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f g : LatticeHom α β} (h : ∀ (a : α), f a = g a) : f = g

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

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

@[simp]

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

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

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

id as a LatticeHom.

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

@[simp]

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

@[simp]

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

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

Composition of LatticeHoms as a LatticeHom.

@[simp]

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

@[simp]

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

@[simp]

theorem LatticeHom.coe_comp_sup_hom' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} [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_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [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_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : f.comp (LatticeHom.id α) = f

@[simp]

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

@[simp]

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

@[simp]

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

def LatticeHom.subtypeVal {β : Type u_3} [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.

@[simp]

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

@[simp]

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

@[instance 100]

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

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

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

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

@[simp]

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

@[simp]

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

Dual homs

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Prod

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

Natural projection homomorphism from α × β to α.

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

Natural projection homomorphism from α × β to β.

@[simp]

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

@[simp]

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

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

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

Pi

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

Evaluation as a lattice homomorphism.

@[simp]

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

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