Formal concepts: orthocomplements and attribute implication

[UPSTREAM] candidate for Mathlib/Order/Concept.lean.

The formal concepts of a symmetric, irreflexive relation r, an orthogonality relation, form an ortholattice. The lattice structure is mathlib's concept lattice; the new content is the orthocomplement Aᶜ = upperPolar r A = {x | ∀ y ∈ A, r x y}, which for a symmetric relation is an order-reversing involution on extents.

For any relation, the attribute concept of b lies below that of a exactly when every object with b has a, the attribute implication from b to a. A preorder on the attributes reverses along the attribute concepts exactly when each object's attributes form a lower set of it.

Main definitions

• Concept.instCompl: the orthocomplement of a concept, whose extent is the concept's intent.
• Concept.instSetLike: a concept of a single-sorted relation is determined by its extent.

Main results

• Concept.instInvolutiveCompl: for a symmetric relation the orthocomplement is an involution.
• Concept.instIsOrtholattice: for a symmetric, irreflexive relation the concepts form an ortholattice.
• Concept.ofAttribute_le_ofAttribute_iff: attribute concepts are ordered by attribute implication.
• Concept.antitone_ofAttribute_iff: the attribute concepts reverse a preorder exactly when every object's attributes form a lower set.

References

• [HM24]

theorem Order.upperPolar_eq_lowerPolar {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (s : Set S) : upperPolar r s = lowerPolar r s

For a symmetric relation the upper and lower polars coincide.

theorem Order.isExtent_upperPolar {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (s : Set S) : IsExtent r (upperPolar r s)

For a symmetric relation the upper polar of any set is an extent.

@[instance_reducible]

instance Concept.instCompl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] : Compl (Concept S S r)

The orthocomplement of a concept is the concept whose extent is its intent, well defined because r is symmetric.

Equations

• Concept.instCompl r = { compl := fun (c : Concept S S r) => Concept.ofIsExtent r c.intent ⋯ }

@[simp]

theorem Concept.extent_compl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (c : Concept S S r) : cᶜ.extent = c.intent

@[simp]

theorem Concept.intent_compl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] (c : Concept S S r) : cᶜ.intent = upperPolar r c.intent

@[instance_reducible]

instance Concept.instSetLike {S : Type u_1} {r : S → S → Prop} : SetLike (Concept S S r) S

A concept of a single-sorted relation is determined by its extent, so concepts form a SetLike family with ↑c = c.extent. (No PartialOrder diamond: SetLike supplies only Membership/coercions, and Concept's order is already extent-lifted.)

Equations

• Concept.instSetLike = { coe := fun (c : Concept S S r) => c.extent, coe_injective := ⋯ }

theorem Concept.extent_bot_eq_empty {S : Type u_1} (r : S → S → Prop) [Std.Irrefl r] : ⊥.extent = ∅

For an irreflexive relation the bottom concept has empty extent (no point is orthogonal to everything, including itself).

@[instance_reducible]

instance Concept.instInvolutiveCompl {S : Type u_1} (r : S → S → Prop) [Std.Symm r] : InvolutiveCompl (Concept S S r)

For a symmetric relation the orthocomplement is an involution of the concept lattice ([HM24] Proposition 4.8).

Equations

• Concept.instInvolutiveCompl r = { toCompl := Concept.instCompl r, compl_compl := ⋯, compl_le_compl := ⋯ }

instance Concept.instIsOrtholattice {S : Type u_1} (r : S → S → Prop) [Std.Symm r] [Std.Irrefl r] : IsOrtholattice (Concept S S r)

The concepts of a symmetric, irreflexive relation form an orthocomplemented lattice ([HM24] Proposition 4.8). The lattice structure is mathlib's concept lattice; only the orthocomplement and its axioms are new.

Attribute implication

theorem Concept.ofAttribute_le_ofAttribute_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {a b : β} : ofAttribute r b ≤ ofAttribute r a ↔ ∀ ⦃x : α⦄, r x b → r x a

The attribute concept of b lies below that of a exactly when every object with b has a.

theorem Concept.antitone_ofAttribute_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} [Preorder β] : Antitone (ofAttribute r) ↔ ∀ (x : α), IsLowerSet {b : β | r x b}

The attribute concepts reverse a preorder on the attributes exactly when the attributes of every object form a lower set of it.