From f7905f0c0d78512557662f1a80bed2dd9c25c753 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 22 Mar 2022 20:22:09 +0000
Subject: [PATCH] feat(order/concept): Concept lattices (#12286)

Define `concept`, the type of concepts of a relation, and prove it forms a complete lattice.
---
 docs/references.bib    |  15 +++
 src/order/concept.lean | 265 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 280 insertions(+)
 create mode 100644 src/order/concept.lean

diff --git a/docs/references.bib b/docs/references.bib
index 2268b0097ef7e..a6a20e37d8797 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -392,6 +392,21 @@ @Book{            conway2001
   mrnumber      = {1803095}
 }
 
+@Book{            davey_priestley,
+  author        = {Davey, B. A. and Priestley, H. A.},
+  title         = {Introduction to lattices and order},
+  edition       = {Second},
+  publisher     = {Cambridge University Press, New York},
+  year          = {2002},
+  pages         = {xii+298},
+  isbn          = {0-521-78451-4},
+  MRCLASS       = {06-01 (68Q55)},
+  mrclass       = {1902334},
+  mrreviewer    = {T. S. Blyth},
+  doi           = {10.1017/CBO9780511809088},
+  url           = {https://doi.org/10.1017/CBO9780511809088},
+}
+
 @InProceedings{   deligne_formulaire,
   author        = {Deligne, P.},
   title         = {Courbes elliptiques: formulaire d'apr\`es {J}. {T}ate},
diff --git a/src/order/concept.lean b/src/order/concept.lean
new file mode 100644
index 0000000000000..c8d112fc01e15
--- /dev/null
+++ b/src/order/concept.lean
@@ -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