refactor(Order/CompleteBooleanAlgebra): a complete lattice which is a…

… Heyting algebra is automatically a frame (#21391)

Every complete lattice that is a heyting algebra is also a frame. This is because the Heyting implication is the right adjoint to `⊓`, which means that `⊓` now preserves infinite suprema (because it is a left adjoint).

Mathlib/Data/Fintype/Order.lean

@@ -125,6 +125,8 @@ noncomputable abbrev toCompleteLinearOrder
 noncomputable abbrev toCompleteBooleanAlgebra [BooleanAlgebra α] : CompleteBooleanAlgebra α where
   __ := ‹BooleanAlgebra α›
   __ := Fintype.toCompleteDistribLattice α
+  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
+  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
 
 -- See note [reducible non-instances]
 /-- A finite boolean algebra is complete and atomic. -/

Mathlib/Order/CompleteBooleanAlgebra.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Yaël Dillies
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.Directed
 import Mathlib.Logic.Equiv.Set
+import Mathlib.Order.GaloisConnection.Basic
 
 /-!
 # Frames, completely distributive lattices and complete Boolean algebras
@@ -72,14 +73,20 @@ class Order.Coframe.MinimalAxioms (α : Type u) extends CompleteLattice α where
 
 /-- A frame, aka complete Heyting algebra, is a complete lattice whose `⊓` distributes over `⨆`. -/
 class Order.Frame (α : Type*) extends CompleteLattice α, HeytingAlgebra α where
-  /-- `⊓` distributes over `⨆`. -/
-  inf_sSup_le_iSup_inf (a : α) (s : Set α) : a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
+
+/-- `⊓` distributes over `⨆`. -/
+theorem inf_sSup_eq {α : Type*} [Order.Frame α] {s : Set α} {a : α} :
+    a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
+  gc_inf_himp.l_sSup
 
 /-- A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
 whose `⊔` distributes over `⨅`. -/
 class Order.Coframe (α : Type*) extends CompleteLattice α, CoheytingAlgebra α where
-  /-- `⊔` distributes over `⨅`. -/
-  iInf_sup_le_sup_sInf (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
+
+/-- `⊔` distributes over `⨅`. -/
+theorem sup_sInf_eq {α : Type*} [Order.Coframe α] {s : Set α} {a : α} :
+    a ⊔ sInf s  = ⨅ b ∈ s, a ⊔ b:=
+  gc_sdiff_sup.u_sInf
 
 open Order
 
@@ -100,9 +107,6 @@ attribute [nolint docBlame] CompleteDistribLattice.MinimalAxioms.toMinimalAxioms
 distribute over `⨅` and `⨆`. -/
 class CompleteDistribLattice (α : Type*) extends Frame α, Coframe α, BiheytingAlgebra α
 
-/-- In a complete distributive lattice, `⊔` distributes over `⨅`. -/
-add_decl_doc CompleteDistribLattice.iInf_sup_le_sup_sInf
-
 /-- Structure containing the minimal axioms required to check that an order is a completely
 distributive. Do NOT use, except for implementing `CompletelyDistribLattice` via
 `CompletelyDistribLattice.ofMinimalAxioms`.
@@ -146,7 +150,9 @@ lemma inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f
   simp only [inf_iSup_eq]
 
 /-- The `Order.Frame.MinimalAxioms` element corresponding to a frame. -/
-def of [Frame α] : MinimalAxioms α := { ‹Frame α› with }
+def of [Frame α] : MinimalAxioms α where
+  __ :=  ‹Frame α›
+  inf_sSup_le_iSup_inf a s := _root_.inf_sSup_eq.le
 
 end MinimalAxioms
 
@@ -182,7 +188,9 @@ lemma sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f
   simp only [sup_iInf_eq]
 
 /-- The `Order.Coframe.MinimalAxioms` element corresponding to a frame. -/
-def of [Coframe α] : MinimalAxioms α := { ‹Coframe α› with }
+def of [Coframe α] : MinimalAxioms α where
+  __ := ‹Coframe α›
+  iInf_sup_le_sup_sInf a s := _root_.sup_sInf_eq.ge
 
 end MinimalAxioms
 
@@ -204,7 +212,10 @@ variable (minAx : MinimalAxioms α)
 
 /-- The `CompleteDistribLattice.MinimalAxioms` element corresponding to a complete distrib lattice.
 -/
-def of [CompleteDistribLattice α] : MinimalAxioms α := { ‹CompleteDistribLattice α› with }
+def of [CompleteDistribLattice α] : MinimalAxioms α where
+  __ := ‹CompleteDistribLattice α›
+  inf_sSup_le_iSup_inf a s:= inf_sSup_eq.le
+  iInf_sup_le_sup_sInf a s:= sup_sInf_eq.ge
 
 /-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Frame`. -/
 abbrev toFrame : Frame.MinimalAxioms α := minAx.toMinimalAxioms
@@ -311,7 +322,6 @@ theorem iSup_iInf_eq [CompletelyDistribLattice α] {f : ∀ a, κ a → α} :
 instance (priority := 100) CompletelyDistribLattice.toCompleteDistribLattice
     [CompletelyDistribLattice α] : CompleteDistribLattice α where
   __ := ‹CompletelyDistribLattice α›
-  __ := CompleteDistribLattice.ofMinimalAxioms MinimalAxioms.of.toCompleteDistribLattice
 
 -- See note [lower instance priority]
 instance (priority := 100) CompleteLinearOrder.toCompletelyDistribLattice [CompleteLinearOrder α] :
@@ -349,10 +359,6 @@ variable [Frame α] {s t : Set α} {a b : α}
 instance OrderDual.instCoframe : Coframe αᵒᵈ where
   __ := instCompleteLattice
   __ := instCoheytingAlgebra
-  iInf_sup_le_sup_sInf := @Frame.inf_sSup_le_iSup_inf α _
-
-theorem inf_sSup_eq : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
-  (Frame.inf_sSup_le_iSup_inf _ _).antisymm iSup_inf_le_inf_sSup
 
 theorem sSup_inf_eq : sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b := by
   simpa only [inf_comm] using @inf_sSup_eq α _ s b
@@ -429,14 +435,10 @@ instance (priority := 100) Frame.toDistribLattice : DistribLattice α :=
 instance Prod.instFrame [Frame α] [Frame β] : Frame (α × β) where
   __ := instCompleteLattice
   __ := instHeytingAlgebra
-  inf_sSup_le_iSup_inf a s := by
-    simp [Prod.le_def, sSup_eq_iSup, fst_iSup, snd_iSup, fst_iInf, snd_iInf, inf_iSup_eq]
 
 instance Pi.instFrame {ι : Type*} {π : ι → Type*} [∀ i, Frame (π i)] : Frame (∀ i, π i) where
   __ := instCompleteLattice
   __ := instHeytingAlgebra
-  inf_sSup_le_iSup_inf a s i := by
-    simp only [sSup_apply, iSup_apply, inf_apply, inf_iSup_eq, ← iSup_subtype'']; rfl
 
 end Frame
 
@@ -447,10 +449,6 @@ variable [Coframe α] {s t : Set α} {a b : α}
 instance OrderDual.instFrame : Frame αᵒᵈ where
   __ := instCompleteLattice
   __ := instHeytingAlgebra
-  inf_sSup_le_iSup_inf := @Coframe.iInf_sup_le_sup_sInf α _
-
-theorem sup_sInf_eq : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b :=
-  @inf_sSup_eq αᵒᵈ _ _ _
 
 theorem sInf_sup_eq : sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b :=
   @sSup_inf_eq αᵒᵈ _ _ _
@@ -501,14 +499,10 @@ instance (priority := 100) Coframe.toDistribLattice : DistribLattice α where
 instance Prod.instCoframe [Coframe β] : Coframe (α × β) where
   __ := instCompleteLattice
   __ := instCoheytingAlgebra
-  iInf_sup_le_sup_sInf a s := by
-    simp [Prod.le_def, sInf_eq_iInf, fst_iSup, snd_iSup, fst_iInf, snd_iInf, sup_iInf_eq]
 
 instance Pi.instCoframe {ι : Type*} {π : ι → Type*} [∀ i, Coframe (π i)] : Coframe (∀ i, π i) where
   __ := instCompleteLattice
   __ := instCoheytingAlgebra
-  iInf_sup_le_sup_sInf a s i := by
-    simp only [sInf_apply, iInf_apply, sup_apply, sup_iInf_eq, ← iInf_subtype'']; rfl
 
 end Coframe
 
@@ -577,16 +571,22 @@ instance Prod.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] [CompleteBo
     CompleteBooleanAlgebra (α × β) where
   __ := instBooleanAlgebra
   __ := instCompleteDistribLattice
+  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
+  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
 
 instance Pi.instCompleteBooleanAlgebra {ι : Type*} {π : ι → Type*}
     [∀ i, CompleteBooleanAlgebra (π i)] : CompleteBooleanAlgebra (∀ i, π i) where
   __ := instBooleanAlgebra
   __ := instCompleteDistribLattice
+  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
+  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
 
 instance OrderDual.instCompleteBooleanAlgebra [CompleteBooleanAlgebra α] :
     CompleteBooleanAlgebra αᵒᵈ where
   __ := instBooleanAlgebra
   __ := instCompleteDistribLattice
+  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
+  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
 
 section CompleteBooleanAlgebra
 
@@ -650,8 +650,10 @@ instance (priority := 100) CompleteAtomicBooleanAlgebra.toCompletelyDistribLatti
 -- See note [lower instance priority]
 instance (priority := 100) CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra
     [CompleteAtomicBooleanAlgebra α] : CompleteBooleanAlgebra α where
-  __ := ‹CompleteAtomicBooleanAlgebra α›
   __ := CompletelyDistribLattice.toCompleteDistribLattice
+  __ := ‹CompleteAtomicBooleanAlgebra α›
+  inf_sSup_le_iSup_inf _ _ := inf_sSup_eq.le
+  iInf_sup_le_sup_sInf _ _ := sup_sInf_eq.ge
 
 instance Prod.instCompleteAtomicBooleanAlgebra [CompleteAtomicBooleanAlgebra α]
     [CompleteAtomicBooleanAlgebra β] : CompleteAtomicBooleanAlgebra (α × β) where

Mathlib/Order/Copy.lean

@@ -194,8 +194,6 @@ def Frame.copy (c : Frame α) (le : α → α → Prop) (eq_le : le = (by infer_
     (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Frame α where
   toCompleteLattice := CompleteLattice.copy (@Frame.toCompleteLattice α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf
-  inf_sSup_le_iSup_inf := fun a s => by
-    simp [eq_le, eq_sup, eq_inf, eq_sSup, @Order.Frame.inf_sSup_le_iSup_inf α _ a s]
   __ := HeytingAlgebra.copy (@Frame.toHeytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl
 
@@ -212,8 +210,6 @@ def Coframe.copy (c : Coframe α) (le : α → α → Prop) (eq_le : le = (by in
     (sInf : Set α → α) (eq_sInf : sInf = (by infer_instance : InfSet α).sInf) : Coframe α where
   toCompleteLattice := CompleteLattice.copy (@Coframe.toCompleteLattice α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf
-  iInf_sup_le_sup_sInf := fun a s => by
-    simp [eq_le, eq_sup, eq_inf, eq_sInf, @Order.Coframe.iInf_sup_le_sup_sInf α _ a s]
   __ := CoheytingAlgebra.copy (@Coframe.toCoheytingAlgebra α c)
     le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot
 

Mathlib/Order/Heyting/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.PropInstances
+import Mathlib.Order.GaloisConnection.Defs
 
 /-!
 # Heyting algebras
@@ -350,6 +351,9 @@ theorem himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c := by
 theorem himp_inf_himp_cancel (hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c :=
   (himp_triangle _ _ _).antisymm <| le_inf (himp_le_himp_left hcb) (himp_le_himp_right hba)
 
+theorem gc_inf_himp : GaloisConnection (a ⊓ ·) (a ⇨ ·) :=
+  fun _ _ ↦ Iff.symm le_himp_iff'
+
 -- See note [lower instance priority]
 instance (priority := 100) GeneralizedHeytingAlgebra.toDistribLattice : DistribLattice α :=
   DistribLattice.ofInfSupLe fun a b c => by
@@ -567,6 +571,9 @@ theorem inf_sdiff_sup_left : a \ c ⊓ (a ⊔ b) = a \ c :=
 theorem inf_sdiff_sup_right : a \ c ⊓ (b ⊔ a) = a \ c :=
   inf_of_le_left <| sdiff_le.trans le_sup_right
 
+theorem gc_sdiff_sup : GaloisConnection (· \ a) (a ⊔ ·) :=
+  fun _ _ ↦ sdiff_le_iff
+
 -- See note [lower instance priority]
 instance (priority := 100) GeneralizedCoheytingAlgebra.toDistribLattice : DistribLattice α :=
   { ‹GeneralizedCoheytingAlgebra α› with