Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(order/concept): Concept lattices (#12286)
Define `concept`, the type of concepts of a relation, and prove it forms a complete lattice.
- Loading branch information
1 parent
b226b4b
commit f7905f0
Showing
2 changed files
with
280 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,265 @@ | ||
/- | ||
Copyright (c) 2022 Yaël Dillies. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yaël Dillies | ||
-/ | ||
import data.set.lattice | ||
|
||
/-! | ||
# 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] | ||
## Tags | ||
concept, formal concept analysis, intent, extend, attribute | ||
-/ | ||
|
||
open function order_dual set | ||
|
||
variables {ι : Sort*} {α β γ : Type*} {κ : ι → Sort*} (r : α → β → Prop) {s s₁ s₂ : set α} | ||
{t t₁ t₂ : set β} | ||
|
||
/-! ### Intent and extent -/ | ||
|
||
/-- The intent closure of `s : set α` along a relation `r : α → β → Prop` is the set of all elements | ||
which `r` relates to all elements of `s`. -/ | ||
def intent_closure (s : set α) : set β := {b | ∀ ⦃a⦄, a ∈ s → r a b} | ||
|
||
/-- The extent closure of `t : set β` along a relation `r : α → β → Prop` is the set of all elements | ||
which `r` relates to all elements of `t`. -/ | ||
def extent_closure (t : set β) : set α := {a | ∀ ⦃b⦄, b ∈ t → r a b} | ||
|
||
variables {r} | ||
|
||
lemma subset_intent_closure_iff_subset_extent_closure : | ||
t ⊆ intent_closure r s ↔ s ⊆ extent_closure r t := | ||
⟨λ h a ha b hb, h hb ha, λ h b hb a ha, h ha hb⟩ | ||
|
||
variables (r) | ||
|
||
lemma gc_intent_closure_extent_closure : | ||
galois_connection (to_dual ∘ intent_closure r) (extent_closure r ∘ of_dual) := | ||
λ s t, subset_intent_closure_iff_subset_extent_closure | ||
|
||
lemma intent_closure_swap (t : set β) : intent_closure (swap r) t = extent_closure r t := rfl | ||
lemma extent_closure_swap (s : set α) : extent_closure (swap r) s = intent_closure r s := rfl | ||
|
||
@[simp] lemma intent_closure_empty : intent_closure r ∅ = univ := | ||
eq_univ_of_forall $ λ _ _, false.elim | ||
|
||
@[simp] lemma extent_closure_empty : extent_closure r ∅ = univ := intent_closure_empty _ | ||
|
||
@[simp] lemma intent_closure_union (s₁ s₂ : set α) : | ||
intent_closure r (s₁ ∪ s₂) = intent_closure r s₁ ∩ intent_closure r s₂ := | ||
set.ext $ λ _, ball_or_left_distrib | ||
|
||
@[simp] lemma extent_closure_union (t₁ t₂ : set β) : | ||
extent_closure r (t₁ ∪ t₂) = extent_closure r t₁ ∩ extent_closure r t₂ := | ||
intent_closure_union _ _ _ | ||
|
||
@[simp] lemma intent_closure_Union (f : ι → set α) : | ||
intent_closure r (⋃ i, f i) = ⋂ i, intent_closure r (f i) := | ||
(gc_intent_closure_extent_closure r).l_supr | ||
|
||
@[simp] lemma extent_closure_Union (f : ι → set β) : | ||
extent_closure r (⋃ i, f i) = ⋂ i, extent_closure r (f i) := | ||
intent_closure_Union _ _ | ||
|
||
@[simp] lemma intent_closure_Union₂ (f : Π i, κ i → set α) : | ||
intent_closure r (⋃ i j, f i j) = ⋂ i j, intent_closure r (f i j) := | ||
(gc_intent_closure_extent_closure r).l_supr₂ | ||
|
||
@[simp] lemma extent_closure_Union₂ (f : Π i, κ i → set β) : | ||
extent_closure r (⋃ i j, f i j) = ⋂ i j, extent_closure r (f i j) := | ||
intent_closure_Union₂ _ _ | ||
|
||
lemma subset_extent_closure_intent_closure (s : set α) : | ||
s ⊆ extent_closure r (intent_closure r s) := | ||
(gc_intent_closure_extent_closure r).le_u_l _ | ||
|
||
lemma subset_intent_closure_extent_closure (t : set β) : | ||
t ⊆ intent_closure r (extent_closure r t) := | ||
subset_extent_closure_intent_closure _ t | ||
|
||
@[simp] lemma intent_closure_extent_closure_intent_closure (s : set α) : | ||
intent_closure r (extent_closure r $ intent_closure r s) = intent_closure r s := | ||
(gc_intent_closure_extent_closure r).l_u_l_eq_l _ | ||
|
||
@[simp] lemma extent_closure_intent_closure_extent_closure (t : set β) : | ||
extent_closure r (intent_closure r $ extent_closure r t) = extent_closure r t := | ||
intent_closure_extent_closure_intent_closure _ t | ||
|
||
lemma intent_closure_anti : antitone (intent_closure r) := | ||
(gc_intent_closure_extent_closure r).monotone_l | ||
|
||
lemma extent_closure_anti : antitone (extent_closure r) := intent_closure_anti _ | ||
|
||
/-! ### Concepts -/ | ||
|
||
variables (α β) | ||
|
||
/-- 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`. -/ | ||
structure concept extends set α × set β := | ||
(closure_fst : intent_closure r fst = snd) | ||
(closure_snd : extent_closure r snd = fst) | ||
|
||
namespace concept | ||
variables {r α β} {c d : concept α β r} | ||
|
||
attribute [simp] closure_fst closure_snd | ||
|
||
@[ext] lemma ext (h : c.fst = d.fst) : c = d := | ||
begin | ||
obtain ⟨⟨s₁, t₁⟩, h₁, _⟩ := c, | ||
obtain ⟨⟨s₂, t₂⟩, h₂, _⟩ := d, | ||
dsimp at h₁ h₂ h, | ||
subst h, | ||
subst h₁, | ||
subst h₂, | ||
end | ||
|
||
lemma ext' (h : c.snd = d.snd) : c = d := | ||
begin | ||
obtain ⟨⟨s₁, t₁⟩, _, h₁⟩ := c, | ||
obtain ⟨⟨s₂, t₂⟩, _, h₂⟩ := d, | ||
dsimp at h₁ h₂ h, | ||
subst h, | ||
subst h₁, | ||
subst h₂, | ||
end | ||
|
||
lemma fst_injective : injective (λ c : concept α β r, c.fst) := λ c d, ext | ||
lemma snd_injective : injective (λ c : concept α β r, c.snd) := λ c d, ext' | ||
|
||
instance : has_sup (concept α β r) := | ||
⟨λ c d, { fst := extent_closure r (c.snd ∩ d.snd), | ||
snd := c.snd ∩ d.snd, | ||
closure_fst := by rw [←c.closure_fst, ←d.closure_fst, ←intent_closure_union, | ||
intent_closure_extent_closure_intent_closure], | ||
closure_snd := rfl }⟩ | ||
|
||
instance : has_inf (concept α β r) := | ||
⟨λ c d, { fst := c.fst ∩ d.fst, | ||
snd := intent_closure r (c.fst ∩ d.fst), | ||
closure_fst := rfl, | ||
closure_snd := by rw [←c.closure_snd, ←d.closure_snd, ←extent_closure_union, | ||
extent_closure_intent_closure_extent_closure] }⟩ | ||
|
||
instance : semilattice_inf (concept α β r) := fst_injective.semilattice_inf _ $ λ _ _, rfl | ||
|
||
@[simp] lemma fst_subset_fst_iff : c.fst ⊆ d.fst ↔ c ≤ d := iff.rfl | ||
@[simp] lemma fst_ssubset_fst_iff : c.fst ⊂ d.fst ↔ c < d := iff.rfl | ||
|
||
@[simp] lemma snd_subset_snd_iff : c.snd ⊆ d.snd ↔ d ≤ c := | ||
begin | ||
refine ⟨λ h, _, λ h, _⟩, | ||
{ rw [←fst_subset_fst_iff, ←c.closure_snd, ←d.closure_snd], | ||
exact extent_closure_anti _ h }, | ||
{ rw [←c.closure_fst, ←d.closure_fst], | ||
exact intent_closure_anti _ h } | ||
end | ||
|
||
@[simp] lemma snd_ssubset_snd_iff : c.snd ⊂ d.snd ↔ d < c := | ||
by rw [ssubset_iff_subset_not_subset, lt_iff_le_not_le, snd_subset_snd_iff, snd_subset_snd_iff] | ||
|
||
lemma strict_mono_fst : strict_mono (prod.fst ∘ to_prod : concept α β r → set α) := | ||
λ c d, fst_ssubset_fst_iff.2 | ||
|
||
lemma strict_anti_snd : strict_anti (prod.snd ∘ to_prod : concept α β r → set β) := | ||
λ c d, snd_ssubset_snd_iff.2 | ||
|
||
instance : lattice (concept α β r) := | ||
{ sup := (⊔), | ||
le_sup_left := λ c d, snd_subset_snd_iff.1 $ inter_subset_left _ _, | ||
le_sup_right := λ c d, snd_subset_snd_iff.1 $ inter_subset_right _ _, | ||
sup_le := λ c d e, by { simp_rw ←snd_subset_snd_iff, exact subset_inter }, | ||
..concept.semilattice_inf } | ||
|
||
instance : bounded_order (concept α β r) := | ||
{ top := ⟨⟨univ, intent_closure r univ⟩, rfl, eq_univ_of_forall $ λ a b hb, hb trivial⟩, | ||
le_top := λ _, subset_univ _, | ||
bot := ⟨⟨extent_closure r univ, univ⟩, eq_univ_of_forall $ λ b a ha, ha trivial, rfl⟩, | ||
bot_le := λ _, snd_subset_snd_iff.1 $ subset_univ _ } | ||
|
||
instance : has_Sup (concept α β r) := | ||
⟨λ S, { fst := extent_closure r (⋂ c ∈ S, (c : concept _ _ _).snd), | ||
snd := ⋂ c ∈ S, (c : concept _ _ _).snd, | ||
closure_fst := by simp_rw [←closure_fst, ←intent_closure_Union₂, | ||
intent_closure_extent_closure_intent_closure], | ||
closure_snd := rfl }⟩ | ||
|
||
instance : has_Inf (concept α β r) := | ||
⟨λ S, { fst := ⋂ c ∈ S, (c : concept _ _ _).fst, | ||
snd := intent_closure r (⋂ c ∈ S, (c : concept _ _ _).fst), | ||
closure_fst := rfl, | ||
closure_snd := by simp_rw [←closure_snd, ←extent_closure_Union₂, | ||
extent_closure_intent_closure_extent_closure] }⟩ | ||
|
||
instance : complete_lattice (concept α β r) := | ||
{ Sup := Sup, | ||
le_Sup := λ S c hc, snd_subset_snd_iff.1 $ bInter_subset_of_mem hc, | ||
Sup_le := λ S c hc, snd_subset_snd_iff.1 $ subset_Inter₂ $ λ d hd, snd_subset_snd_iff.2 $ hc d hd, | ||
Inf := Inf, | ||
Inf_le := λ S c, bInter_subset_of_mem, | ||
le_Inf := λ S c, subset_Inter₂, | ||
..concept.lattice, ..concept.bounded_order } | ||
|
||
@[simp] lemma top_fst : (⊤ : concept α β r).fst = univ := rfl | ||
@[simp] lemma top_snd : (⊤ : concept α β r).snd = intent_closure r univ := rfl | ||
@[simp] lemma bot_fst : (⊥ : concept α β r).fst = extent_closure r univ := rfl | ||
@[simp] lemma bot_snd : (⊥ : concept α β r).snd = univ := rfl | ||
@[simp] lemma sup_fst (c d : concept α β r) : (c ⊔ d).fst = extent_closure r (c.snd ∩ d.snd) := rfl | ||
@[simp] lemma sup_snd (c d : concept α β r) : (c ⊔ d).snd = c.snd ∩ d.snd := rfl | ||
@[simp] lemma inf_fst (c d : concept α β r) : (c ⊓ d).fst = c.fst ∩ d.fst := rfl | ||
@[simp] lemma inf_snd (c d : concept α β r) : (c ⊓ d).snd = intent_closure r (c.fst ∩ d.fst) := rfl | ||
@[simp] lemma Sup_fst (S : set (concept α β r)) : | ||
(Sup S).fst = extent_closure r ⋂ c ∈ S, (c : concept _ _ _).snd := rfl | ||
@[simp] lemma Sup_snd (S : set (concept α β r)) : (Sup S).snd = ⋂ c ∈ S, (c : concept _ _ _).snd := | ||
rfl | ||
@[simp] lemma Inf_fst (S : set (concept α β r)) : (Inf S).fst = ⋂ c ∈ S, (c : concept _ _ _).fst := | ||
rfl | ||
@[simp] lemma Inf_snd (S : set (concept α β r)) : | ||
(Inf S).snd = intent_closure r ⋂ c ∈ S, (c : concept _ _ _).fst := rfl | ||
|
||
instance : inhabited (concept α β r) := ⟨⊥⟩ | ||
|
||
/-- Swap the sets of a concept to make it a concept of the dual context. -/ | ||
@[simps] def swap (c : concept α β r) : concept β α (swap r) := | ||
⟨c.to_prod.swap, c.closure_snd, c.closure_fst⟩ | ||
|
||
@[simp] lemma swap_swap (c : concept α β r) : c.swap.swap = c := ext rfl | ||
|
||
@[simp] lemma swap_le_swap_iff : c.swap ≤ d.swap ↔ d ≤ c := snd_subset_snd_iff | ||
@[simp] lemma swap_lt_swap_iff : c.swap < d.swap ↔ d < c := snd_ssubset_snd_iff | ||
|
||
/-- The dual of a concept lattice is isomorphic to the concept lattice of the dual context. -/ | ||
@[simps] def swap_equiv : order_dual (concept α β r) ≃o concept β α (function.swap r) := | ||
{ to_fun := swap ∘ of_dual, | ||
inv_fun := to_dual ∘ swap, | ||
left_inv := swap_swap, | ||
right_inv := swap_swap, | ||
map_rel_iff' := λ c d, swap_le_swap_iff } | ||
|
||
end concept |