Dedekind-MacNeille completion

The Dedekind-MacNeille completion of a partial order is the smallest complete lattice into which it embeds.

The theory of concept lattices allows for a simple construction. In fact, DedekindCut α is simply an abbreviation for Concept α α (· ≤ ·). This means we don't need to reprove that this is a complete lattice; instead, the file simply proves that any order embedding into another complete lattice factors through it.

Todo

• Build the order isomorphism DedekindCut ℚ ≃o EReal.

Tags

Dedekind completion, Dedekind cut

@[reducible, inline]

abbrev DedekindCut (α : Type u_1) [Preorder α] : Type u_1

The Dedekind-MacNeille completion of a partial order is the smallest complete lattice that contains it. We define here the type of Dedekind cuts of α as the Concept lattice of the ≤ relation of α.

For A : DedekindCut α, the sets A.left and A.right are related by upperBounds A.left = A.right and lowerBounds A.right = A.left.

The theorem DedekindCut.principalEmbedding_trans_factorEmbedding proves that if α is a partial order and β is a complete lattice, any embedding α ↪o β factors through DedekindCut α.

Equations

• DedekindCut α = Concept α α fun (x1 x2 : α) => x1 ≤ x2

@[reducible, inline]

abbrev DedekindCut.left {α : Type u_1} [Preorder α] (A : DedekindCut α) : Set α

The left set of a Dedekind cut. This is an alias for Concept.extent.

Equations

• A.left = A.extent

@[reducible, inline]

abbrev DedekindCut.right {α : Type u_1} [Preorder α] (A : DedekindCut α) : Set α

The right set of a Dedekind cut. This is an alias for Concept.intent.

Equations

• A.right = A.intent

theorem DedekindCut.ext {α : Type u_1} [Preorder α] {A B : DedekindCut α} (h : A.left = B.left) : A = B

See DedekindCut.ext' for a version using the right set instead.

theorem DedekindCut.ext_iff {α : Type u_1} [Preorder α] {A B : DedekindCut α} : A = B ↔ A.left = B.left

theorem DedekindCut.ext' {α : Type u_1} [Preorder α] {A B : DedekindCut α} (h : A.right = B.right) : A = B

See DedekindCut.ext for a version using the left set instead.

@[simp]

theorem DedekindCut.upperBounds_left {α : Type u_1} [Preorder α] (A : DedekindCut α) : upperBounds A.left = A.right

@[simp]

theorem DedekindCut.lowerBounds_right {α : Type u_1} [Preorder α] (A : DedekindCut α) : lowerBounds A.right = A.left

theorem DedekindCut.image_left_subset_lowerBounds {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (A : DedekindCut α) : f '' A.left ⊆ lowerBounds (f '' A.right)

theorem DedekindCut.image_right_subset_upperBounds {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (A : DedekindCut α) : f '' A.right ⊆ upperBounds (f '' A.left)

def DedekindCut.principal {α : Type u_1} [Preorder α] (a : α) : DedekindCut α

Convert an element into its Dedekind cut (Iic a, Ici a). This map is order-preserving, though it is injective only on partial orders.

Equations

• DedekindCut.principal a = (Concept.ofObject (fun (x1 x2 : α) => x1 ≤ x2) a).copy (Set.Iic a) (Set.Ici a) ⋯ ⋯

@[simp]

theorem DedekindCut.left_principal {α : Type u_1} [Preorder α] (a : α) : (principal a).left = Set.Iic a

@[simp]

theorem DedekindCut.right_principal {α : Type u_1} [Preorder α] (a : α) : (principal a).right = Set.Ici a

@[simp]

theorem DedekindCut.ofObject_eq_principal {α : Type u_1} [Preorder α] (a : α) : Concept.ofObject (fun (x1 x2 : α) => x1 ≤ x2) a = principal a

@[simp]

theorem DedekindCut.ofAttribute_eq_principal {α : Type u_1} [Preorder α] (a : α) : Concept.ofAttribute (fun (x1 x2 : α) => x1 ≤ x2) a = principal a

@[simp]

theorem DedekindCut.principal_le_principal {α : Type u_1} [Preorder α] {a b : α} : principal a ≤ principal b ↔ a ≤ b

@[simp]

theorem DedekindCut.principal_lt_principal {α : Type u_1} [Preorder α] {a b : α} : principal a < principal b ↔ a < b

@[implicit_reducible]

noncomputable instance DedekindCut.instDecidableLE {α : Type u_1} [Preorder α] : DecidableLE (DedekindCut α)

We can never have a computable decidable instance, for the same reason we can't on Set α.

Equations

• DedekindCut.instDecidableLE = Classical.decRel LE.le

@[simp]

theorem DedekindCut.principal_inj {α : Type u_1} [PartialOrder α] {a b : α} : principal a = principal b ↔ a = b

def DedekindCut.principalEmbedding {α : Type u_1} [PartialOrder α] : α ↪o DedekindCut α

DedekindCut.principal as an OrderEmbedding.

Equations

• DedekindCut.principalEmbedding = { toFun := DedekindCut.principal, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem DedekindCut.principalEmbedding_apply {α : Type u_1} [PartialOrder α] (a : α) : principalEmbedding a = principal a

@[simp]

theorem DedekindCut.coe_principalEmbedding {α : Type u_1} [PartialOrder α] : ⇑principalEmbedding = principal

@[simp]

theorem DedekindCut.principal_sSup_left {α : Type u_1} [CompleteLattice α] (A : DedekindCut α) : principal (sSup A.left) = A

@[simp]

theorem DedekindCut.principal_sInf_right {α : Type u_1} [CompleteLattice α] (A : DedekindCut α) : principal (sInf A.right) = A

def DedekindCut.factorEmbedding {α : Type u_1} {β : Type u_2} [CompleteLattice α] [PartialOrder β] (f : β ↪o α) : DedekindCut β ↪o α

Any order embedding β ↪o α into a complete lattice α factors through DedekindCut β.

This map is defined so that factorEmbedding f A = sSup (f '' A.left). Although the construction factorEmbedding f A = sInf (f '' A.right) would also work, these do not in general give equal embeddings.

Equations

• DedekindCut.factorEmbedding f = OrderEmbedding.ofMapLEIff (fun (A : DedekindCut β) => sSup (⇑f '' A.left)) ⋯

theorem DedekindCut.factorEmbedding_apply {α : Type u_1} {β : Type u_2} [CompleteLattice α] [PartialOrder β] (f : β ↪o α) (A : DedekindCut β) : (factorEmbedding f) A = sSup (⇑f '' A.left)

@[simp]

theorem DedekindCut.factorEmbedding_principal {α : Type u_1} {β : Type u_2} [CompleteLattice α] [PartialOrder β] (f : β ↪o α) (x : β) : (factorEmbedding f) (principal x) = f x

theorem DedekindCut.principalEmbedding_trans_factorEmbedding {α : Type u_1} {β : Type u_2} [CompleteLattice α] [PartialOrder β] (f : β ↪o α) : RelEmbedding.trans principalEmbedding (factorEmbedding f) = f

The Dedekind-MacNeille completion of a partial order is the smallest complete lattice containing it, in the sense that any embedding into any complete lattice factors through it.

def DedekindCut.principalIso {α : Type u_1} [CompleteLattice α] : α ≃o DedekindCut α

DedekindCut.principal as an OrderIso.

This provides the second half of the fundamental theorem of concept lattices: every complete lattice is isomorphic to a concept lattice (its own Dedekind completion).

See Concept.instCompleteLattice for the first half.

Equations

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

@[simp]

theorem DedekindCut.principalIso_apply {α : Type u_1} [CompleteLattice α] (a✝ : α) : principalIso a✝ = principal a✝

theorem DedekindCut.principalIso_symm_apply {α : Type u_1} [CompleteLattice α] (A : DedekindCut α) : principalIso.symm A = sSup A.left

instance DedekindCut.instTotalLe {α : Type u_1} [LinearOrder α] : Std.Total fun (x1 x2 : DedekindCut α) => x1 ≤ x2

@[implicit_reducible]

noncomputable instance DedekindCut.instLinearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (DedekindCut α)

Equations

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

@[implicit_reducible]

noncomputable instance DedekindCut.instCompleteLinearOrder {α : Type u_1} [LinearOrder α] : CompleteLinearOrder (DedekindCut α)

Equations

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