Supremum-preserving maps and their upper adjoints

The supremum-preserving maps of the lattice theory (the identity, pointwise lifts, the lattice meet on Prop, functions, pairs, PProd and Unit, and Prod.map), and the laws of their upper adjoints.

instance Lean.Order.instPreservesSupId {α : Type u} [CompleteLattice α] : PreservesSup id

instance Lean.Order.instPreservesSupForallComp {α : Type u} [CompleteLattice α] {ε : Type v} (f : α → α) [PreservesSup f] : PreservesSup (Function.comp f)

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)

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.

instance Lean.Order.instPreservesSupProdMap {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (f : α → α) (g : β → β) [PreservesSup f] [PreservesSup g] : PreservesSup (Prod.map f g)

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.

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.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.PreservesSup.upperAdjoint_id {α : Type u} [CompleteLattice α] (b : α) : upperAdjoint id b = b

theorem Lean.Order.PreservesSup.upperAdjoint_comp_apply {α : Type u} [CompleteLattice α] {ε : Type v} (f : α → α) [PreservesSup f] (X : ε → α) (e : ε) : upperAdjoint (Function.comp f) X e = upperAdjoint f (X e)

theorem Lean.Order.PreservesSup.upperAdjoint_prodMap_fst {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (f : α → α) (g : β → β) [PreservesSup f] [PreservesSup g] (E : α × β) : (upperAdjoint (Prod.map f g) E).fst = upperAdjoint f E.fst

theorem Lean.Order.PreservesSup.upperAdjoint_prodMap_snd {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (f : α → α) (g : β → β) [PreservesSup f] [PreservesSup g] (E : α × β) : (upperAdjoint (Prod.map f g) E).snd = upperAdjoint g E.snd

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.