Supremum-preserving maps and their upper adjoints

A supremum-preserving map on a complete lattice is a lower adjoint. Its upper adjoint is the implication belonging to it: Heyting ⇨ for the lattice meet, a magic wand for a separating conjunction.

class Lean.Order.PreservesSup {α : Type u} [CompleteLattice α] (f : α → α) : Prop

f : α → α preserves suprema if it distributes over arbitrary suprema: f (sup s) = sup { f x | x ∈ s }. Equivalently f is a lower adjoint, so it has an upper adjoint PreservesSup.upperAdjoint f.

A frame operator acts by a supremum-preserving map for each resource r: the lattice meet (a ⊓ ·), or a cost combinator (costConj r) for a counter resource. The upper adjoint is the corresponding implication: Heyting ⇨ for the meet, a magic wand for separating conjunction.

• map_sup (s : α → Prop) : f (CompleteLattice.sup s) = CompleteLattice.sup fun (y : α) => ∃ (x : α), s x ∧ y = f x

  f preserves joins.

instance Lean.Order.instPreservesSupMeet (a : Prop) : PreservesSup (meet a)

instance Lean.Order.instPreservesSupForallMeet {σ : Type v} {β : σ → Type u} [(s : σ) → CompleteLattice (β s)] [∀ (s : σ) (c : β s), PreservesSup (meet c)] (a : (s : σ) → β s) : PreservesSup (meet a)

theorem Lean.Order.PProd.mk_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α ×' β) : ⟨meet p.fst q.fst, meet p.snd q.snd⟩ = meet p q

mk of the componentwise meets is the meet on a product.

theorem Lean.Order.PProd.mk_sup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (c : α ×' β → Prop) : ⟨CompleteLattice.sup fun (a : α) => ∃ (b : β), c ⟨a, b⟩, CompleteLattice.sup fun (b : β) => ∃ (a : α), c ⟨a, b⟩⟩ = CompleteLattice.sup c

mk of the componentwise least upper bounds is the least upper bound on a product.

instance Lean.Order.instPreservesSupPProdMeet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] [∀ (a : α), PreservesSup (meet a)] [∀ (b : β), PreservesSup (meet b)] (p : α ×' β) : PreservesSup (meet p)

A product lattice preserves suprema componentwise: meets, least upper bounds and the order all act on the two components separately.

theorem Lean.Order.Prod.mk_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p.fst q.fst, meet p.snd q.snd) = meet p q

mk of the componentwise meets is the meet on a product.

@[simp]

theorem Lean.Order.Prod.fst_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p q).fst = meet p.fst q.fst

The first component of a meet is the meet of the first components.

@[simp]

theorem Lean.Order.Prod.snd_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p q).snd = meet p.snd q.snd

The second component of a meet is the meet of the second components.

theorem Lean.Order.Prod.fst_bot {α : Type u} {β : Type v} [CCPO α] [CCPO β] : bot.fst = bot

The first component of the bottom element is the bottom element. Propositional (not definitional), because ⊥ is csup ∅, not a constructor application.

theorem Lean.Order.Prod.snd_bot {α : Type u} {β : Type v} [CCPO α] [CCPO β] : bot.snd = bot

The second component of the bottom element is the bottom element. Propositional (not definitional), because ⊥ is csup ∅, not a constructor application.

theorem Lean.Order.Prod.fst_top {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] : top.fst = top

The first component of the top element is the top element. Propositional (not definitional), because ⊤ is a supremum, not a constructor application.

theorem Lean.Order.Prod.snd_top {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] : top.snd = top

The second component of the top element is the top element. Propositional (not definitional), because ⊤ is a supremum, not a constructor application.

instance Lean.Order.instPreservesSupProdMeet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] [∀ (a : α), PreservesSup (meet a)] [∀ (b : β), PreservesSup (meet b)] (p : α × β) : PreservesSup (meet p)

A product lattice preserves suprema at the two components.

instance Lean.Order.instPreservesSupUnitMeet (a : Unit) : PreservesSup (meet a)

Unit carries a single value, so every map on it preserves suprema.

noncomputable def Lean.Order.PreservesSup.upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : α

The upper adjoint of f: the join of all x with f x ⊑ b. For f = (a ⊓ ·) this is Heyting implication a ⇨ ·.

Equations

• Lean.Order.PreservesSup.upperAdjoint f b = Lean.Order.CompleteLattice.sup fun (x : α) => Lean.Order.PartialOrder.rel (f x) b

theorem Lean.Order.PreservesSup.upperAdjoint_spec {α : Type u} [CompleteLattice α] (f : α → α) (b : α) : is_sup (fun (x : α) => PartialOrder.rel (f x) b) (upperAdjoint f b)

upperAdjoint f b is the least upper bound of {x | f x ⊑ b} by definition.

theorem Lean.Order.PreservesSup.le_upperAdjoint {α : Type u} [CompleteLattice α] (f : α → α) {b x : α} (h : PartialOrder.rel (f x) b) : PartialOrder.rel x (upperAdjoint f b)

Unit, free from the definition of upperAdjoint: f x ⊑ b → x ⊑ upperAdjoint f b. Needs only CompleteLattice.

theorem Lean.Order.PreservesSup.upperAdjoint_le {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] (b : α) : PartialOrder.rel (f (upperAdjoint f b)) b

Counit (modus ponens), from supremum preservation: f (upperAdjoint f b) ⊑ b.

theorem Lean.Order.PreservesSup.map_mono {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] {b b' : α} (h : PartialOrder.rel b b') : PartialOrder.rel (f b) (f b')

Monotonicity of a supremum-preserving f, derived from supremum preservation.

theorem Lean.Order.PreservesSup.upperAdjoint_mono {α : Type u} [CompleteLattice α] (f : α → α) [PreservesSup f] {b b' : α} (h : PartialOrder.rel b b') : PartialOrder.rel (upperAdjoint f b) (upperAdjoint f b')

A right adjoint is monotone.

theorem Lean.Order.iSup_meet_le {α : Type u} [CompleteLattice α] {ι : Type v} {P R : α} {Φ : ι → α} [PreservesSup (meet P)] (h : ∀ (i : ι), PartialOrder.rel (meet (Φ i) P) R) : PartialOrder.rel (meet (iSup Φ) P) R

Frame elimination: a join on the left of a meet is eliminated pointwise.