Complete lattice homomorphisms

This file defines frame homomorphisms and complete lattice homomorphisms.

We use the FunLike 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

• sSupHom: Maps which preserve ⨆.
• sInfHom: Maps which preserve ⨅.
• FrameHom: Frame homomorphisms. Maps which preserve ⨆, ⊓ and ⊤.
• CompleteLatticeHom: Complete lattice homomorphisms. Maps which preserve ⨆ and ⨅.

Typeclasses

• sSupHomClass
• sInfHomClass
• FrameHomClass
• CompleteLatticeHomClass

Concrete homs

• CompleteLatticeHom.setPreimage: Set.preimage as a complete lattice homomorphism.

TODO

Frame homs are Heyting homs.

structure sSupHom (α : Type u_8) (β : Type u_9) [SupSet α] [SupSet β] : Type (max u_8 u_9)

• toFun : α → β

  The underlying function of a sSupHom.

• map_sSup' : ∀ (s_1 : Set α), sSupHom.toFun s (sSup s_1) = sSup (s.toFun '' s_1)

  The proposition that a sSupHom commutes with arbitrary suprema/joins.

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

structure sInfHom (α : Type u_8) (β : Type u_9) [InfSet α] [InfSet β] : Type (max u_8 u_9)

• toFun : α → β

  The underlying function of an sInfHom.

• map_sInf' : ∀ (s_1 : Set α), sInfHom.toFun s (sInf s_1) = sInf (s.toFun '' s_1)

  The proposition that a sInfHom commutes with arbitrary infima/meets

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

structure FrameHom (α : Type u_8) (β : Type u_9) [CompleteLattice α] [CompleteLattice β] extends InfTopHom : Type (max u_8 u_9)

• toFun : α → β
• map_inf' : ∀ (a b : α), InfHom.toFun s.toInfHom (a ⊓ b) = InfHom.toFun s.toInfHom a ⊓ InfHom.toFun s.toInfHom b
• map_top' : InfHom.toFun s.toInfHom ⊤ = ⊤
• map_sSup' : ∀ (s_1 : Set α), InfHom.toFun s.toInfHom (sSup s_1) = sSup (s.toFun '' s_1)

  The proposition that frame homomorphisms commute with arbitrary suprema/joins.

The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.

structure CompleteLatticeHom (α : Type u_8) (β : Type u_9) [CompleteLattice α] [CompleteLattice β] extends sInfHom : Type (max u_8 u_9)

• toFun : α → β
• map_sInf' : ∀ (s_1 : Set α), sInfHom.toFun s.tosInfHom (sInf s_1) = sInf (s.toFun '' s_1)
• map_sSup' : ∀ (s_1 : Set α), sInfHom.toFun s.tosInfHom (sSup s_1) = sSup (s.toFun '' s_1)

  The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.

The type of complete lattice homomorphisms from α to β.

class sSupHomClass (F : Type u_8) (α : outParam (Type u_9)) (β : outParam (Type u_10)) [SupSet α] [SupSet β] extends FunLike : Type (max (max u_10 u_8) u_9)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_sSup : ∀ (f : F) (s_1 : Set α), ↑f (sSup s_1) = sSup (↑f '' s_1)

  The proposition that members of sSupHomClasss commute with arbitrary suprema/joins.

sSupHomClass F α β states that F is a type of ⨆-preserving morphisms.

You should extend this class when you extend sSupHom.

class sInfHomClass (F : Type u_8) (α : outParam (Type u_9)) (β : outParam (Type u_10)) [InfSet α] [InfSet β] extends FunLike : Type (max (max u_10 u_8) u_9)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_sInf : ∀ (f : F) (s_1 : Set α), ↑f (sInf s_1) = sInf (↑f '' s_1)

  The proposition that members of sInfHomClasss commute with arbitrary infima/meets.

sInfHomClass F α β states that F is a type of ⨅-preserving morphisms.

You should extend this class when you extend sInfHom.

class FrameHomClass (F : Type u_8) (α : outParam (Type u_9)) (β : outParam (Type u_10)) [CompleteLattice α] [CompleteLattice β] extends InfTopHomClass : Type (max (max u_10 u_8) u_9)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_inf : ∀ (f : F) (a b : α), ↑f (a ⊓ b) = ↑f a ⊓ ↑f b
• map_top : ∀ (f : F), ↑f ⊤ = ⊤
• map_sSup : ∀ (f : F) (s_1 : Set α), ↑f (sSup s_1) = sSup (↑f '' s_1)

  The proposition that members of FrameHomClass commute with arbitrary suprema/joins.

FrameHomClass F α β states that F is a type of frame morphisms. They preserve ⊓ and ⨆.

You should extend this class when you extend FrameHom.

class CompleteLatticeHomClass (F : Type u_8) (α : outParam (Type u_9)) (β : outParam (Type u_10)) [CompleteLattice α] [CompleteLattice β] extends sInfHomClass : Type (max (max u_10 u_8) u_9)

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• map_sInf : ∀ (f : F) (s_1 : Set α), ↑f (sInf s_1) = sInf (↑f '' s_1)
• map_sSup : ∀ (f : F) (s_1 : Set α), ↑f (sSup s_1) = sSup (↑f '' s_1)

  The proposition that members of CompleteLatticeHomClass commute with arbitrary suprema/joins.

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

You should extend this class when you extend CompleteLatticeHom.

theorem map_iSup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ι → α) : ↑f (⨆ (i : ι), g i) = ⨆ (i : ι), ↑f (g i)

theorem map_iSup₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι → Sort u_7} [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : (i : ι) → κ i → α) : ↑f (⨆ (i : ι) (j : κ i), g i j) = ⨆ (i : ι) (j : κ i), ↑f (g i j)

theorem map_iInf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : ι → α) : ↑f (⨅ (i : ι), g i) = ⨅ (i : ι), ↑f (g i)

theorem map_iInf₂ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} {κ : ι → Sort u_7} [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : (i : ι) → κ i → α) : ↑f (⨅ (i : ι) (j : κ i), g i j) = ⨅ (i : ι) (j : κ i), ↑f (g i j)

instance sSupHomClass.toSupBotHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] : SupBotHomClass F α β

instance sInfHomClass.toInfTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [sInfHomClass F α β] : InfTopHomClass F α β

instance FrameHomClass.tosSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : sSupHomClass F α β

instance FrameHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : BoundedLatticeHomClass F α β

instance CompleteLatticeHomClass.toFrameHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : FrameHomClass F α β

instance CompleteLatticeHomClass.toBoundedLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : BoundedLatticeHomClass F α β

instance OrderIsoClass.tosSupHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : sSupHomClass F α β

instance OrderIsoClass.tosInfHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : sInfHomClass F α β

instance OrderIsoClass.toCompleteLatticeHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [OrderIsoClass F α β] : CompleteLatticeHomClass F α β

instance instCoeTCSSupHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] [sSupHomClass F α β] : CoeTC F (sSupHom α β)

instance instCoeTCSInfHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] [sInfHomClass F α β] : CoeTC F (sInfHom α β)

instance instCoeTCFrameHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [FrameHomClass F α β] : CoeTC F (FrameHom α β)

instance instCoeTCCompleteLatticeHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] [CompleteLatticeHomClass F α β] : CoeTC F (CompleteLatticeHom α β)

Supremum homomorphisms

instance sSupHom.instSSupHomClassSSupHom {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] : sSupHomClass (sSupHom α β) α β

@[simp]

theorem sSupHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] {f : sSupHom α β} : f.toFun = ↑f

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

def sSupHom.copy {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ↑f) : sSupHom α β

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

@[simp]

theorem sSupHom.coe_copy {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ↑f) : ↑(sSupHom.copy f f' h) = f'

theorem sSupHom.copy_eq {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ↑f) : sSupHom.copy f f' h = f

def sSupHom.id (α : Type u_2) [SupSet α] : sSupHom α α

id as a sSupHom.

instance sSupHom.instInhabitedSSupHom (α : Type u_2) [SupSet α] : Inhabited (sSupHom α α)

@[simp]

theorem sSupHom.coe_id (α : Type u_2) [SupSet α] : ↑(sSupHom.id α) = id

@[simp]

theorem sSupHom.id_apply {α : Type u_2} [SupSet α] (a : α) : ↑(sSupHom.id α) a = a

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

Composition of sSupHoms as a sSupHom.

@[simp]

theorem sSupHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (f : sSupHom β γ) (g : sSupHom α β) : ↑(sSupHom.comp f g) = ↑f ∘ ↑g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance sSupHom.instPartialOrderSSupHomToSupSet {α : Type u_2} {β : Type u_3} [SupSet α] : {x : CompleteLattice β} → PartialOrder (sSupHom α β)

instance sSupHom.instBotSSupHomToSupSet {α : Type u_2} {β : Type u_3} [SupSet α] : {x : CompleteLattice β} → Bot (sSupHom α β)

instance sSupHom.instOrderBotSSupHomToSupSetToLEToPreorderInstPartialOrderSSupHomToSupSet {α : Type u_2} {β : Type u_3} [SupSet α] : {x : CompleteLattice β} → OrderBot (sSupHom α β)

@[simp]

theorem sSupHom.coe_bot {α : Type u_2} {β : Type u_3} [SupSet α] : ∀ {x : CompleteLattice β}, ↑⊥ = ⊥

@[simp]

theorem sSupHom.bot_apply {α : Type u_2} {β : Type u_3} [SupSet α] : ∀ {x : CompleteLattice β} (a : α), ↑⊥ a = ⊥

Infimum homomorphisms

instance sInfHom.instSInfHomClassSInfHom {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] : sInfHomClass (sInfHom α β) α β

@[simp]

theorem sInfHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] {f : sInfHom α β} : f.toFun = ↑f

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

def sInfHom.copy {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ↑f) : sInfHom α β

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

@[simp]

theorem sInfHom.coe_copy {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ↑f) : ↑(sInfHom.copy f f' h) = f'

theorem sInfHom.copy_eq {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ↑f) : sInfHom.copy f f' h = f

def sInfHom.id (α : Type u_2) [InfSet α] : sInfHom α α

id as an sInfHom.

instance sInfHom.instInhabitedSInfHom (α : Type u_2) [InfSet α] : Inhabited (sInfHom α α)

@[simp]

theorem sInfHom.coe_id (α : Type u_2) [InfSet α] : ↑(sInfHom.id α) = id

@[simp]

theorem sInfHom.id_apply {α : Type u_2} [InfSet α] (a : α) : ↑(sInfHom.id α) a = a

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

Composition of sInfHoms as a sInfHom.

@[simp]

theorem sInfHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (f : sInfHom β γ) (g : sInfHom α β) : ↑(sInfHom.comp f g) = ↑f ∘ ↑g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance sInfHom.instPartialOrderSInfHomToInfSet {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] : PartialOrder (sInfHom α β)

instance sInfHom.instTopSInfHomToInfSet {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] : Top (sInfHom α β)

instance sInfHom.instOrderTopSInfHomToInfSetToLEToPreorderInstPartialOrderSInfHomToInfSet {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] : OrderTop (sInfHom α β)

@[simp]

theorem sInfHom.coe_top {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] : ↑⊤ = ⊤

@[simp]

theorem sInfHom.top_apply {α : Type u_2} {β : Type u_3} [InfSet α] [CompleteLattice β] (a : α) : ↑⊤ a = ⊤

Frame homomorphisms

instance FrameHom.instFrameHomClassFrameHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] : FrameHomClass (FrameHom α β) α β

def FrameHom.toLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) : LatticeHom α β

Reinterpret a FrameHom as a LatticeHom.

theorem FrameHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : FrameHom α β} : f.toFun = ↑f

@[simp]

theorem FrameHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : FrameHom α β} : ↑f.toInfTopHom = ↑f

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

def FrameHom.copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : α → β) (h : f' = ↑f) : FrameHom α β

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

@[simp]

theorem FrameHom.coe_copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : α → β) (h : f' = ↑f) : ↑(FrameHom.copy f f' h) = f'

theorem FrameHom.copy_eq {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) (f' : α → β) (h : f' = ↑f) : FrameHom.copy f f' h = f

def FrameHom.id (α : Type u_2) [CompleteLattice α] : FrameHom α α

id as a FrameHom.

instance FrameHom.instInhabitedFrameHom (α : Type u_2) [CompleteLattice α] : Inhabited (FrameHom α α)

@[simp]

theorem FrameHom.coe_id (α : Type u_2) [CompleteLattice α] : ↑(FrameHom.id α) = id

@[simp]

theorem FrameHom.id_apply {α : Type u_2} [CompleteLattice α] (a : α) : ↑(FrameHom.id α) a = a

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

Composition of FrameHoms as a FrameHom.

@[simp]

theorem FrameHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) : ↑(FrameHom.comp f g) = ↑f ∘ ↑g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance FrameHom.instPartialOrderFrameHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] : PartialOrder (FrameHom α β)

Complete lattice homomorphisms

instance CompleteLatticeHom.instCompleteLatticeHomClassCompleteLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] : CompleteLatticeHomClass (CompleteLatticeHom α β) α β

def CompleteLatticeHom.tosSupHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : sSupHom α β

Reinterpret a CompleteLatticeHom as a sSupHom.

def CompleteLatticeHom.toBoundedLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : BoundedLatticeHom α β

Reinterpret a CompleteLatticeHom as a BoundedLatticeHom.

theorem CompleteLatticeHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : CompleteLatticeHom α β} : f.toFun = ↑f

@[simp]

theorem CompleteLatticeHom.toFun_eq_coe_aux {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] {f : CompleteLatticeHom α β} : ↑f.tosInfHom = ↑f

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

def CompleteLatticeHom.copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : α → β) (h : f' = ↑f) : CompleteLatticeHom α β

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

@[simp]

theorem CompleteLatticeHom.coe_copy {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : α → β) (h : f' = ↑f) : ↑(CompleteLatticeHom.copy f f' h) = f'

theorem CompleteLatticeHom.copy_eq {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (f' : α → β) (h : f' = ↑f) : CompleteLatticeHom.copy f f' h = f

def CompleteLatticeHom.id (α : Type u_2) [CompleteLattice α] : CompleteLatticeHom α α

id as a CompleteLatticeHom.

instance CompleteLatticeHom.instInhabitedCompleteLatticeHom (α : Type u_2) [CompleteLattice α] : Inhabited (CompleteLatticeHom α α)

@[simp]

theorem CompleteLatticeHom.coe_id (α : Type u_2) [CompleteLattice α] : ↑(CompleteLatticeHom.id α) = id

@[simp]

theorem CompleteLatticeHom.id_apply {α : Type u_2} [CompleteLattice α] (a : α) : ↑(CompleteLatticeHom.id α) a = a

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

Composition of CompleteLatticeHoms as a CompleteLatticeHom.

@[simp]

theorem CompleteLatticeHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) : ↑(CompleteLatticeHom.comp f g) = ↑f ∘ ↑g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Dual homs

@[simp]

theorem sSupHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) : ∀ (a : αᵒᵈ), ↑(↑sSupHom.dual f) a = (↑OrderDual.toDual ∘ ↑f ∘ ↑OrderDual.ofDual) a

@[simp]

theorem sSupHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sInfHom αᵒᵈ βᵒᵈ) : ∀ (a : α), ↑(↑sSupHom.dual.symm f) a = (↑OrderDual.ofDual ∘ ↑f ∘ ↑OrderDual.toDual) a

def sSupHom.dual {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] : sSupHom α β ≃ sInfHom αᵒᵈ βᵒᵈ

Reinterpret a ⨆-homomorphism as an ⨅-homomorphism between the dual orders.

@[simp]

theorem sSupHom.dual_id {α : Type u_2} [SupSet α] : ↑sSupHom.dual (sSupHom.id α) = sInfHom.id αᵒᵈ

@[simp]

theorem sSupHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (g : sSupHom β γ) (f : sSupHom α β) : ↑sSupHom.dual (sSupHom.comp g f) = sInfHom.comp (↑sSupHom.dual g) (↑sSupHom.dual f)

@[simp]

theorem sSupHom.symm_dual_id {α : Type u_2} [SupSet α] : ↑sSupHom.dual.symm (sInfHom.id αᵒᵈ) = sSupHom.id α

@[simp]

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

@[simp]

theorem sInfHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sSupHom αᵒᵈ βᵒᵈ) : ∀ (a : α), ↑(↑sInfHom.dual.symm f) a = (↑OrderDual.ofDual ∘ ↑f ∘ ↑OrderDual.toDual) a

@[simp]

theorem sInfHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sInfHom α β) : ∀ (a : αᵒᵈ), ↑(↑sInfHom.dual f) a = (↑OrderDual.toDual ∘ ↑f ∘ ↑OrderDual.ofDual) a

def sInfHom.dual {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] : sInfHom α β ≃ sSupHom αᵒᵈ βᵒᵈ

Reinterpret an ⨅-homomorphism as a ⨆-homomorphism between the dual orders.

@[simp]

theorem sInfHom.dual_id {α : Type u_2} [InfSet α] : ↑sInfHom.dual (sInfHom.id α) = sSupHom.id αᵒᵈ

@[simp]

theorem sInfHom.dual_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (g : sInfHom β γ) (f : sInfHom α β) : ↑sInfHom.dual (sInfHom.comp g f) = sSupHom.comp (↑sInfHom.dual g) (↑sInfHom.dual f)

@[simp]

theorem sInfHom.symm_dual_id {α : Type u_2} [InfSet α] : ↑sInfHom.dual.symm (sSupHom.id αᵒᵈ) = sInfHom.id α

@[simp]

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

@[simp]

theorem CompleteLatticeHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom αᵒᵈ βᵒᵈ) : ∀ (a : αᵒᵈᵒᵈ), ↑(↑CompleteLatticeHom.dual.symm f) a = ↑OrderDual.toDual (↑(CompleteLatticeHom.tosSupHom f) (↑OrderDual.ofDual a))

@[simp]

theorem CompleteLatticeHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : ∀ (a : αᵒᵈ), ↑(↑CompleteLatticeHom.dual f) a = ↑OrderDual.toDual (↑(CompleteLatticeHom.tosSupHom f) (↑OrderDual.ofDual a))

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

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

@[simp]

theorem CompleteLatticeHom.dual_id {α : Type u_2} [CompleteLattice α] : ↑CompleteLatticeHom.dual (CompleteLatticeHom.id α) = CompleteLatticeHom.id αᵒᵈ

@[simp]

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

@[simp]

theorem CompleteLatticeHom.symm_dual_id {α : Type u_2} [CompleteLattice α] : ↑CompleteLatticeHom.dual.symm (CompleteLatticeHom.id αᵒᵈ) = CompleteLatticeHom.id α

@[simp]

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

Concrete homs

def CompleteLatticeHom.setPreimage {α : Type u_2} {β : Type u_3} (f : α → β) : CompleteLatticeHom (Set β) (Set α)

Set.preimage as a complete lattice homomorphism.

See also sSupHom.setImage.

@[simp]

theorem CompleteLatticeHom.coe_setPreimage {α : Type u_2} {β : Type u_3} (f : α → β) : ↑(CompleteLatticeHom.setPreimage f) = Set.preimage f

@[simp]

theorem CompleteLatticeHom.setPreimage_apply {α : Type u_2} {β : Type u_3} (f : α → β) (s : Set β) : ↑(CompleteLatticeHom.setPreimage f) s = f ⁻¹' s

@[simp]

theorem CompleteLatticeHom.setPreimage_id {α : Type u_2} : CompleteLatticeHom.setPreimage id = CompleteLatticeHom.id (Set α)

theorem CompleteLatticeHom.setPreimage_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β → γ) (f : α → β) : CompleteLatticeHom.setPreimage (g ∘ f) = CompleteLatticeHom.comp (CompleteLatticeHom.setPreimage f) (CompleteLatticeHom.setPreimage g)

theorem Set.image_sSup {α : Type u_2} {β : Type u_3} {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (Set.image f '' s)

@[simp]

theorem sSupHom.setImage_toFun {α : Type u_2} {β : Type u_3} (f : α → β) (s : Set α) : ↑(sSupHom.setImage f) s = f '' s

def sSupHom.setImage {α : Type u_2} {β : Type u_3} (f : α → β) : sSupHom (Set α) (Set β)

Using Set.image, a function between types yields a sSupHom between their lattices of subsets.

See also CompleteLatticeHom.setPreimage.

@[simp]

theorem Equiv.toOrderIsoSet_symm_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : Set β) : ↑(RelIso.symm (Equiv.toOrderIsoSet e)) s = ↑e.symm '' s

@[simp]

theorem Equiv.toOrderIsoSet_apply {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : Set α) : ↑(Equiv.toOrderIsoSet e) s = ↑e '' s

def Equiv.toOrderIsoSet {α : Type u_2} {β : Type u_3} (e : α ≃ β) : Set α ≃o Set β

An equivalence of types yields an order isomorphism between their lattices of subsets.

def supsSupHom {α : Type u_2} [CompleteLattice α] : sSupHom (α × α) α

The map (a, b) ↦ a ⊔ b as a sSupHom.

def infsInfHom {α : Type u_2} [CompleteLattice α] : sInfHom (α × α) α

The map (a, b) ↦ a ⊓ b as an sInfHom.

@[simp]

theorem supsSupHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) : ↑supsSupHom x = x.fst ⊔ x.snd

@[simp]

theorem infsInfHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) : ↑infsInfHom x = x.fst ⊓ x.snd