wip

Author: iehality

Foundation/Vorspiel/Order/Heyting.lean

@@ -40,3 +40,11 @@ lemma himp_inf_himp_inf_sup_le (a b c : α) : (a ⇨ c) ⊓ (b ⇨ c) ⊓ (a ⊔
   simpa only [GeneralizedHeytingAlgebra.le_himp_iff, inf_comm (a ⊔ b)] using this
 
 end HeytingAlgebra
+
+namespace CompleteBooleanAlgebra
+
+variable {α : Type*} [CompleteBooleanAlgebra α]
+
+
+
+end CompleteBooleanAlgebra

Foundation/Vorspiel/Order/Ideal.lean

@@ -4,14 +4,19 @@ module
 public import Mathlib.Order.Ideal
 public import Mathlib.Order.PFilter
 public import Mathlib.Data.Finset.Lattice.Basic
+public import Mathlib.Order.PrimeIdeal
 
 @[expose] public section
 
 namespace Order
 
 namespace Ideal
 
-variable  {P : Type*} [SemilatticeSup P] [OrderBot P]
+variable {P : Type*}
+
+section semilatticeSup
+
+variable [SemilatticeSup P] [OrderBot P]
 
 lemma sSup_def (s : Set (Ideal P)) : sSup s = sInf (upperBounds s) := rfl
 
@@ -60,6 +65,145 @@ lemma mem_iSup_iff [DecidableEq ι] {I : ι → Ideal P} {x : P} :
     intro i x hx
     refine ⟨{i}, by simpa using hx⟩
 
+end semilatticeSup
+
+section completeSemilatticeSup
+
+variable [CompleteSemilatticeSup P]
+
+theorem sSup_mem {s : Set P} {I : Ideal P} :
+    sSup s ∈ I → ∀ x ∈ s, x ∈ I := fun h _ hx ↦
+  I.lower (le_sSup_iff.mpr fun _ a ↦ a hx) h
+
+end completeSemilatticeSup
+
 end Ideal
 
+namespace Ideal.IsProper
+
+variable {P : Type*} [SemilatticeSup P]
+
+lemma iff_top_not_mem [OrderTop P] {I : Ideal P} : I.IsProper ↔ ⊤ ∉ I := by
+  constructor
+  · intro h ht
+    have : (I : Set P) = Set.univ := by
+      ext x
+      suffices x ∈ I by simpa
+      exact I.lower (show x ≤ ⊤ by simp) ht
+    exact h.ne_univ this
+  · intro hn
+    refine ⟨?_⟩
+    intro e
+    have : ⊤ ∈ I :=
+      SetLike.mem_coe.mp <| by rw [e]; simp
+    contradiction
+
+@[simp] lemma top_not_mem [OrderTop P] (I : Ideal P) [I.IsProper] : ⊤ ∉ I :=
+  iff_top_not_mem.mp inferInstance
+
+end Ideal.IsProper
+
+namespace Ideal.PrimePair
+
+variable {P : Type*}
+
+open IsPrime
+
+section booleanAlgebra
+
+section basic
+
+variable [Preorder P] (IF : PrimePair P)
+
+lemma not_mem_F_iff_mem_I {x : P} :
+    x ∉ IF.F ↔ x ∈ IF.I := by
+  have : x ∈ IF.I ∨ x ∈ IF.F := by simpa using Set.ext_iff.mp IF.I_union_F x
+  have : x ∈ IF.I → x ∉ IF.F := @Set.disjoint_left.mp IF.disjoint x
+  tauto
+
+lemma not_mem_I_iff_mem_F {x : P} :
+    x ∉ IF.I ↔ x ∈ IF.F := by
+  have : x ∈ IF.I ∨ x ∈ IF.F := by simpa using Set.ext_iff.mp IF.I_union_F x
+  have : x ∈ IF.F → x ∉ IF.I := @Set.disjoint_right.mp IF.disjoint x
+  tauto
+
+abbrev IsProper : Prop := IF.I.IsProper
+
+instance i_isProper (IF : PrimePair P) [IF.IsProper] : IF.I.IsProper := inferInstance
+
+instance : IF.I.IsPrime := I_isPrime IF
+
+end basic
+
+variable [BooleanAlgebra P] {IF : PrimePair P}
+
+lemma mem_or_compl_mem_I (x : P) : x ∈ IF.I ∨ xᶜ ∈ IF.I :=
+  IF.I_isPrime.mem_or_compl_mem
+
+lemma mem_or_compl_mem_F (x : P) : x ∈ IF.F ∨ xᶜ ∈ IF.F := by
+  by_contra!
+  have hx : x ∈ IF.I := by simpa [not_mem_F_iff_mem_I] using this.1
+  have hxc : xᶜ ∈ IF.I := by simpa [not_mem_F_iff_mem_I] using this.2
+  have : ⊤ ∈ IF.I := by simpa using Order.Ideal.sup_mem hx hxc
+  have : ⊤ ∉ IF.I := Ideal.IsProper.top_not_mem IF.I
+  contradiction
+
+lemma compl_mem_I_iff_mem_F :
+    xᶜ ∈ IF.I ↔ x ∈ IF.F := by
+  constructor
+  · have : x ∈ IF.F ∨ xᶜ ∉ IF.I := by simpa [not_mem_I_iff_mem_F] using mem_or_compl_mem_F x
+    tauto
+  · have : x ∉ IF.F ∨ xᶜ ∈ IF.I := by simpa [not_mem_F_iff_mem_I] using mem_or_compl_mem_I x
+    tauto
+
+lemma compl_mem_F_iff_mem_I :
+    xᶜ ∈ IF.F ↔ x ∈ IF.I := by
+  simpa using (compl_mem_I_iff_mem_F (x := xᶜ)).symm
+
+@[simp] lemma inf_mem_I_iff {x y : P} :
+    x ⊓ y ∈ IF.I ↔ x ∈ IF.I ∨ y ∈ IF.I := by
+  constructor
+  · exact mem_or_mem (I_isPrime IF)
+  · rintro (h | h)
+    · exact IF.I.lower (by simp) h
+    · exact IF.I.lower (by simp) h
+
+@[simp] lemma sup_mem_F_iff {x y : P} :
+    x ⊔ y ∈ IF.F ↔ x ∈ IF.F ∨ y ∈ IF.F := by
+  simp [←compl_mem_I_iff_mem_F]
+
+@[simp] lemma himp_mem_F_iff {x y : P} :
+    x ⇨ y ∈ IF.F ↔ (x ∈ IF.F → y ∈ IF.F) := by
+  simp [himp_eq, compl_mem_F_iff_mem_I, ←not_mem_F_iff_mem_I]
+  tauto
+
+end booleanAlgebra
+
+section completeBooleanAlgebra
+
+variable [CompleteBooleanAlgebra P] {IF : PrimePair P}
+
+lemma iSup_mem_iff {f : ι → P} :
+    ⨆ i, f i ∈ IF.I ↔ ∀ i, f i ∈ IF.I := by
+  constructor
+  · intro h i
+    exact IF.I.lower (le_iSup f i) h
+  · intro h
+    by_contra! hf
+    
+
+lemma iInf_mem_iff {f : ι → P} :
+    ⨅ i, f i ∈ IF.I ↔ ∃ i, f i ∈ IF.I := by
+  constructor
+  · intro h
+    by_contra! hf
+
+
+end completeBooleanAlgebra
+
+end Ideal.IsPrime
+
+
+
+
 end Order