Formal concept analysis

This file defines concept lattices. A concept of a relation r : α → β → Prop is a pair of sets s : Set α and t : Set β such that s is the set of all a : α that are related to all elements of t, and t is the set of all b : β that are related to all elements of s.

Ordering the concepts of a relation r by inclusion on the first component gives rise to a concept lattice. Every concept lattice is complete and in fact every complete lattice arises as the concept lattice of its ≤.

Implementation notes

Concept lattices are usually defined from a context, that is the triple (α, β, r), but the type of r determines α and β already, so we do not define contexts as a separate object.

TODO

Prove the fundamental theorem of concept lattices.

References

• [Davey, Priestley Introduction to Lattices and Order][davey_priestley]
• [Birkhoff, Garrett Lattice Theory][birkhoff1940]

Tags

concept, formal concept analysis, intent, extend, attribute

Lower and upper polars

def upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : Set β

The upper polar of s : Set α along a relation r : α → β → Prop is the set of all elements which r relates to all elements of s.

def lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : Set α

The lower polar of t : Set β along a relation r : α → β → Prop is the set of all elements which r relates to all elements of t.

theorem subset_upperPolar_iff_subset_lowerPolar {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {s : Set α} {t : Set β} : t ⊆ upperPolar r s ↔ s ⊆ lowerPolar r t

theorem gc_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : GaloisConnection (⇑OrderDual.toDual ∘ upperPolar r) (lowerPolar r ∘ ⇑OrderDual.ofDual)

theorem upperPolar_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : upperPolar (Function.swap r) t = lowerPolar r t

theorem lowerPolar_swap {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : lowerPolar (Function.swap r) s = upperPolar r s

@[simp]

theorem upperPolar_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : upperPolar r ∅ = Set.univ

@[simp]

theorem lowerPolar_empty {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : lowerPolar r ∅ = Set.univ

@[simp]

theorem upperPolar_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s₁ s₂ : Set α) : upperPolar r (s₁ ∪ s₂) = upperPolar r s₁ ∩ upperPolar r s₂

@[simp]

theorem lowerPolar_union {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t₁ t₂ : Set β) : lowerPolar r (t₁ ∪ t₂) = lowerPolar r t₁ ∩ lowerPolar r t₂

@[simp]

theorem upperPolar_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set α) : upperPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), upperPolar r (f i)

@[simp]

theorem lowerPolar_iUnion {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set β) : lowerPolar r (⋃ (i : ι), f i) = ⋂ (i : ι), lowerPolar r (f i)

theorem upperPolar_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_4} (r : α → β → Prop) (f : (i : ι) → κ i → Set α) : upperPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), upperPolar r (f i j)

theorem lowerPolar_iUnion₂ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_4} (r : α → β → Prop) (f : (i : ι) → κ i → Set β) : lowerPolar r (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), lowerPolar r (f i j)

theorem subset_lowerPolar_upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : s ⊆ lowerPolar r (upperPolar r s)

theorem subset_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : t ⊆ upperPolar r (lowerPolar r t)

@[simp]

theorem upperPolar_lowerPolar_upperPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α) : upperPolar r (lowerPolar r (upperPolar r s)) = upperPolar r s

@[simp]

theorem lowerPolar_upperPolar_lowerPolar {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β) : lowerPolar r (upperPolar r (lowerPolar r t)) = lowerPolar r t

theorem upperPolar_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (upperPolar r)

theorem lowerPolar_anti {α : Type u_2} {β : Type u_3} (r : α → β → Prop) : Antitone (lowerPolar r)

Concepts

structure Concept (α : Type u_2) (β : Type u_3) (r : α → β → Prop) : Type (max u_2 u_3)

The formal concepts of a relation. A concept of r : α → β → Prop is a pair of sets s, t such that s is the set of all elements that are r-related to all of t and t is the set of all elements that are r-related to all of s.

• extent : Set α

  The extent of a concept.

• intent : Set β

  The intent of a concept.

• upperPolar_extent : upperPolar r self.extent = self.intent

  The intent consists of all elements related to all elements of the extent.

• lowerPolar_intent : lowerPolar r self.intent = self.extent

  The extent consists of all elements related to all elements of the intent.

theorem Concept.ext {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} (h : c.extent = d.extent) : c = d

theorem Concept.ext_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c = d ↔ c.extent = d.extent

theorem Concept.ext' {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} (h : c.intent = d.intent) : c = d

theorem Concept.extent_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective extent

theorem Concept.intent_injective {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Function.Injective intent

def Concept.copy {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : Concept α β r

Copy a concept, adjusting definitional equalities.

@[simp]

theorem Concept.copy_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : (c.copy e i he hi).intent = i

@[simp]

theorem Concept.copy_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : (c.copy e i he hi).extent = e

theorem Concept.copy_eq {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent) (hi : i = c.intent) : c.copy e i he hi = c

theorem Concept.rel_extent_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c : Concept α β r} {x : α} {y : β} (hx : x ∈ c.extent) (hy : y ∈ c.intent) : r x y

theorem Concept.disjoint_extent_intent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Irrefl r'] : Disjoint c'.extent c'.intent

Note that if r' is the ≤ relation, this theorem will often not be true!

theorem Concept.mem_extent_of_rel_extent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α} (hy : r' y x) (hx : x ∈ c'.extent) : y ∈ c'.extent

theorem Concept.mem_intent_of_intent_rel {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [IsTrans α r'] {x y : α} (hy : r' x y) (hx : x ∈ c'.intent) : y ∈ c'.intent

theorem Concept.codisjoint_extent_intent {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Trichotomous r'] [IsTrans α r'] : Codisjoint c'.extent c'.intent

theorem Concept.isCompl_extent_intent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : IsCompl c'.extent c'.intent

@[simp]

theorem Concept.compl_extent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : c'.extentᶜ = c'.intent

@[simp]

theorem Concept.compl_intent {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r') : c'.intentᶜ = c'.extent

instance Concept.instSupConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Max (Concept α β r)

instance Concept.instInfConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Min (Concept α β r)

instance Concept.instPartialOrder {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : PartialOrder (Concept α β r)

instance Concept.instSemilatticeInfConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SemilatticeInf (Concept α β r)

@[simp]

theorem Concept.extent_subset_extent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.extent ⊆ d.extent ↔ c ≤ d

@[simp]

theorem Concept.extent_ssubset_extent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.extent ⊂ d.extent ↔ c < d

@[simp]

theorem Concept.intent_subset_intent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.intent ⊆ d.intent ↔ d ≤ c

@[simp]

theorem Concept.intent_ssubset_intent_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.intent ⊂ d.intent ↔ d < c

theorem Concept.strictMono_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictMono extent

theorem Concept.strictAnti_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : StrictAnti intent

instance Concept.instLatticeConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Lattice (Concept α β r)

instance Concept.instBoundedOrderConcept {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : BoundedOrder (Concept α β r)

instance Concept.instSupSet {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : SupSet (Concept α β r)

instance Concept.instInfSet {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : InfSet (Concept α β r)

instance Concept.instCompleteLattice {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : CompleteLattice (Concept α β r)

@[simp]

theorem Concept.extent_top {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.extent = Set.univ

@[simp]

theorem Concept.intent_top {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊤.intent = upperPolar r Set.univ

@[simp]

theorem Concept.extent_bot {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.extent = lowerPolar r Set.univ

@[simp]

theorem Concept.intent_bot {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : ⊥.intent = Set.univ

@[simp]

theorem Concept.extent_sup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).extent = lowerPolar r (c.intent ∩ d.intent)

@[simp]

theorem Concept.intent_sup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊔ d).intent = c.intent ∩ d.intent

@[simp]

theorem Concept.extent_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).extent = c.extent ∩ d.extent

@[simp]

theorem Concept.intent_inf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c d : Concept α β r) : (c ⊓ d).intent = upperPolar r (c.extent ∩ d.extent)

@[simp]

theorem Concept.extent_sSup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).extent = lowerPolar r (⋂ c ∈ S, c.intent)

@[simp]

theorem Concept.intent_sSup {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sSup S).intent = ⋂ c ∈ S, c.intent

@[simp]

theorem Concept.extent_sInf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).extent = ⋂ c ∈ S, c.extent

@[simp]

theorem Concept.intent_sInf {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)) : (sInf S).intent = upperPolar r (⋂ c ∈ S, c.extent)

@[simp]

theorem Concept.extent_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨆ (i : ι), f i).extent = lowerPolar r (⋂ (i : ι), (f i).intent)

@[simp]

theorem Concept.intent_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨆ (i : ι), f i).intent = ⋂ (i : ι), (f i).intent

@[simp]

theorem Concept.extent_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨅ (i : ι), f i).extent = ⋂ (i : ι), (f i).extent

@[simp]

theorem Concept.intent_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (f : ι → Concept α β r) : (⨅ (i : ι), f i).intent = upperPolar r (⋂ (i : ι), (f i).extent)

instance Concept.instInhabited {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : Inhabited (Concept α β r)

def Concept.swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : Concept β α (Function.swap r)

Swap the sets of a concept to make it a concept of the dual context.

@[simp]

theorem Concept.swap_extent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.extent = c.intent

@[simp]

theorem Concept.swap_intent {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.intent = c.extent

@[simp]

theorem Concept.swap_swap {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) : c.swap.swap = c

@[simp]

theorem Concept.swap_le_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.swap ≤ d.swap ↔ d ≤ c

@[simp]

theorem Concept.swap_lt_swap_iff {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r} : c.swap < d.swap ↔ d < c

def Concept.swapEquiv {α : Type u_2} {β : Type u_3} {r : α → β → Prop} : (Concept α β r)ᵒᵈ ≃o Concept β α (Function.swap r)

The dual of a concept lattice is isomorphic to the concept lattice of the dual context.

@[simp]

theorem Concept.swapEquiv_symm_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a✝ : Concept β α (Function.swap r)) : (RelIso.symm swapEquiv) a✝ = (⇑OrderDual.toDual ∘ swap) a✝

@[simp]

theorem Concept.swapEquiv_apply {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (a✝ : (Concept α β r)ᵒᵈ) : swapEquiv a✝ = (swap ∘ ⇑OrderDual.ofDual) a✝