Complete lattice homomorphisms

This file defines frame homomorphisms and complete 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

• 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)

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

• toFun : α → β

  The underlying function of a sSupHom.

• map_sSup' (s : Set α) : self.toFun (sSup s) = sSup (self.toFun '' s)

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

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

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

• toFun : α → β

  The underlying function of an sInfHom.

• map_sInf' (s : Set α) : self.toFun (sInf s) = sInf (self.toFun '' s)

  The proposition that a sInfHom commutes with arbitrary infima/meets

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

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

• toFun : α → β
• map_inf' (a b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
• map_top' : self.toFun ⊤ = ⊤
• map_sSup' (s : Set α) : self.toFun (sSup s) = sSup (self.toFun '' s)

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

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

The type of complete lattice homomorphisms from α to β.

• toFun : α → β
• map_sInf' (s : Set α) : self.toFun (sInf s) = sInf (self.toFun '' s)
• map_sSup' (s : Set α) : self.toFun (sSup s) = sSup (self.toFun '' s)

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

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

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

You should extend this class when you extend sSupHom.

• map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (⇑f '' s)

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

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

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

You should extend this class when you extend sInfHom.

• map_sInf (f : F) (s : Set α) : f (sInf s) = sInf (⇑f '' s)

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

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

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

You should extend this class when you extend FrameHom.

• map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
• map_top (f : F) : f ⊤ = ⊤
• map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (⇑f '' s)

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

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

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

You should extend this class when you extend CompleteLatticeHom.

• map_sInf (f : F) (s : Set α) : f (sInf s) = sInf (⇑f '' s)
• map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (⇑f '' s)

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

@[simp]

theorem map_iSup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [FunLike F α β] [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} [FunLike F α β] [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : (i : ι) → κ i → α) : f (⨆ (i : ι), ⨆ (j : κ i), g i j) = ⨆ (i : ι), ⨆ (j : κ i), f (g i j)

@[simp]

theorem map_iInf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Sort u_6} [FunLike F α β] [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} [FunLike F α β] [InfSet α] [InfSet β] [sInfHomClass F α β] (f : F) (g : (i : ι) → κ i → α) : f (⨅ (i : ι), ⨅ (j : κ i), g i j) = ⨅ (i : ι), ⨅ (j : κ i), f (g i j)

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

def OrderIso.toCompleteLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) : CompleteLatticeHom α β

Reinterpret an order isomorphism as a morphism of complete lattices.

Equations

• f.toCompleteLatticeHom = { toFun := ⇑f, map_sInf' := ⋯, map_sSup' := ⋯ }

@[simp]

theorem OrderIso.toCompleteLatticeHom_toFun {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (a : α) : f.toCompleteLatticeHom.toFun a = f a

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass = { coe := fun (f : F) => { toFun := ⇑f, map_sInf' := ⋯, map_sSup' := ⋯ } }

Supremum homomorphisms

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

Equations

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

instance sSupHom.instSSupHomClass {α : 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

@[simp]

theorem sSupHom.coe_mk {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : α → β) (hf : ∀ (s : Set α), f (sSup s) = sSup (f '' s)) : ⇑{ toFun := f, map_sSup' := hf } = f

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

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

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.

Equations

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

@[simp]

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

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

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

id as a sSupHom.

Equations

• sSupHom.id α = { toFun := id, map_sSup' := ⋯ }

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

Equations

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

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

Equations

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

@[simp]

theorem sSupHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SupSet α] [SupSet β] [SupSet γ] (f : sSupHom β γ) (g : sSupHom α β) : ⇑(f.comp 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 : α) : (f.comp 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 α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• sSupHom.instPartialOrder = PartialOrder.lift (fun (f : sSupHom α β) => ⇑f) ⋯

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

Equations

• sSupHom.instBot = { bot := { toFun := fun (x : α) => ⊥, map_sSup' := ⋯ } }

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

Equations

• sSupHom.instOrderBot = { toBot := sSupHom.instBot, bot_le := ⋯ }

@[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.instFunLike {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] : FunLike (sInfHom α β) α β

Equations

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

instance sInfHom.instSInfHomClass {α : 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

@[simp]

theorem sInfHom.coe_mk {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : α → β) (hf : ∀ (s : Set α), f (sInf s) = sInf (f '' s)) : ⇑{ toFun := f, map_sInf' := hf } = f

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

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

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.

Equations

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

@[simp]

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

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

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

id as an sInfHom.

Equations

• sInfHom.id α = { toFun := id, map_sInf' := ⋯ }

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

Equations

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

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

Equations

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

@[simp]

theorem sInfHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [InfSet α] [InfSet β] [InfSet γ] (f : sInfHom β γ) (g : sInfHom α β) : ⇑(f.comp 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 : α) : (f.comp 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 α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• sInfHom.instPartialOrder = PartialOrder.lift (fun (f : sInfHom α β) => ⇑f) ⋯

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

Equations

• sInfHom.instTop = { top := { toFun := fun (x : α) => ⊤, map_sInf' := ⋯ } }

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

Equations

• sInfHom.instOrderTop = { toTop := sInfHom.instTop, le_top := ⋯ }

@[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.instFunLike {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] : FunLike (FrameHom α β) α β

Equations

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

instance FrameHom.instFrameHomClass {α : 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.

Equations

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

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

@[simp]

theorem FrameHom.coe_toInfTopHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) : ⇑f.toInfTopHom = ⇑f

@[simp]

theorem FrameHom.coe_toLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : FrameHom α β) : ⇑f.toLatticeHom = ⇑f

@[simp]

theorem FrameHom.coe_mk {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : InfTopHom α β) (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)) : ⇑{ toInfTopHom := f, map_sSup' := hf } = ⇑f

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

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

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.

Equations

• f.copy f' h = { toInfTopHom := f.copy f' h, map_sSup' := ⋯ }

@[simp]

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

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

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

id as a FrameHom.

Equations

• FrameHom.id α = { toInfTopHom := InfTopHom.id α, map_sSup' := ⋯ }

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

Equations

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

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

Equations

• f.comp g = { toInfTopHom := f.comp g.toInfTopHom, map_sSup' := ⋯ }

@[simp]

theorem FrameHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β) : ⇑(f.comp 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 : α) : (f.comp 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 α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• FrameHom.instPartialOrder = PartialOrder.lift (fun (f : FrameHom α β) => ⇑f) ⋯

Complete lattice homomorphisms

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

Equations

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

instance CompleteLatticeHom.instCompleteLatticeHomClass {α : 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.

Equations

• f.tosSupHom = { toFun := ⇑f, map_sSup' := ⋯ }

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

Reinterpret a CompleteLatticeHom as a BoundedLatticeHom.

Equations

• f.toBoundedLatticeHom = { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }

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

@[simp]

theorem CompleteLatticeHom.coe_tosInfHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : ⇑f.tosInfHom = ⇑f

@[simp]

theorem CompleteLatticeHom.coe_tosSupHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : ⇑f.tosSupHom = ⇑f

@[simp]

theorem CompleteLatticeHom.coe_toBoundedLatticeHom {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) : ⇑f.toBoundedLatticeHom = ⇑f

@[simp]

theorem CompleteLatticeHom.coe_mk {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (f : sInfHom α β) (hf : ∀ (s : Set α), f.toFun (sSup s) = sSup (f.toFun '' s)) : ⇑{ tosInfHom := f, map_sSup' := hf } = ⇑f

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

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

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.

Equations

• f.copy f' h = { tosInfHom := f.copy f' h, map_sSup' := ⋯ }

@[simp]

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

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

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

id as a CompleteLatticeHom.

Equations

• CompleteLatticeHom.id α = { toFun := id, map_sInf' := ⋯, map_sSup' := ⋯ }

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

Equations

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

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

Equations

• f.comp g = { tosInfHom := f.comp g.tosInfHom, map_sSup' := ⋯ }

@[simp]

theorem CompleteLatticeHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] (f : CompleteLatticeHom β γ) (g : CompleteLatticeHom α β) : ⇑(f.comp 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 : α) : (f.comp 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 α β) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Dual homs

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

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

Equations

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

@[simp]

theorem sSupHom.dual_apply_toFun {α : Type u_2} {β : Type u_3} [SupSet α] [SupSet β] (f : sSupHom α β) (a✝ : αᵒᵈ) : (sSupHom.dual f).toFun 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✝

@[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 (g.comp f) = (sSupHom.dual g).comp (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 (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)

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

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

Equations

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

@[simp]

theorem sInfHom.dual_symm_apply_toFun {α : Type u_2} {β : Type u_3} [InfSet α] [InfSet β] (f : sSupHom αᵒᵈ βᵒᵈ) (a✝ : α) : (sInfHom.dual.symm f).toFun 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✝

@[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 (g.comp f) = (sInfHom.dual g).comp (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 (g.comp f) = (sInfHom.dual.symm g).comp (sInfHom.dual.symm f)

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.

Equations

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

@[simp]

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

@[simp]

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

@[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 (g.comp f) = (CompleteLatticeHom.dual g).comp (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 (g.comp f) = (CompleteLatticeHom.dual.symm g).comp (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.

Equations

• CompleteLatticeHom.setPreimage f = { toFun := Set.preimage f, map_sInf' := ⋯, map_sSup' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Set.image_sSup {α : Type u_2} {β : Type u_3} {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (image 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.

Equations

• sSupHom.setImage f = { toFun := Set.image f, map_sSup' := ⋯ }

@[simp]

theorem sSupHom.setImage_toFun {α : Type u_2} {β : Type u_3} (f : α → β) (s : Set α) : (setImage f) s = f '' 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.

Equations

• e.toOrderIsoSet = { toFun := fun (s : Set α) => ⇑e '' s, invFun := fun (s : Set β) => ⇑e.symm '' s, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• supsSupHom = { toFun := fun (x : α × α) => x.1 ⊔ x.2, map_sSup' := ⋯ }

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

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

Equations

• infsInfHom = { toFun := fun (x : α × α) => x.1 ⊓ x.2, map_sInf' := ⋯ }

@[simp]

theorem supsSupHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) : supsSupHom x = x.1 ⊔ x.2

@[simp]

theorem infsInfHom_apply {α : Type u_2} [CompleteLattice α] (x : α × α) : infsInfHom x = x.1 ⊓ x.2