English
A constructive corollary that from a disjoint filter-ideal pair one can obtain a prime ideal J with the stated order and disjointness properties.
Русский
Следствие о существовании простого идеала J из пары рассечения и сохраняющейся разобщённости.
LaTeX
$$$\\exists J \\; (J.IsPrime) \\wedge (I ≤ J) \\wedge Disjoint (F) J$$$
Lean4
theorem prime_ideal_of_disjoint_filter_ideal (hFI : Disjoint (F : Set α) (I : Set α)) :
∃ J : Ideal α, (IsPrime J) ∧ I ≤ J ∧ Disjoint (F : Set α) J := by
-- Let S be the set of ideals containing I and disjoint from F.
set S : Set (Set α) :=
{J : Set α | IsIdeal J ∧ I ≤ J ∧ Disjoint (F : Set α) J}
-- Then I is in S...
have IinS : ↑I ∈ S := by
refine
⟨Order.Ideal.isIdeal I, by trivial⟩
-- ...and S contains upper bounds for any non-empty chains.
have chainub : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub :=
by
intro c hcS hcC hcNe
use sUnion c
refine ⟨?_, fun s hs ↦ le_sSup hs⟩
simp only [le_eq_subset, mem_setOf_eq, disjoint_sUnion_right, S]
let ⟨J, hJ⟩ := hcNe
refine
⟨Order.isIdeal_sUnion_of_isChain (fun _ hJ ↦ (hcS hJ).1) hcC hcNe,
⟨le_trans (hcS hJ).2.1 (le_sSup hJ), fun J hJ ↦ (hcS hJ).2.2⟩⟩
-- Thus, by Zorn's lemma, we can pick a maximal ideal J in S.
obtain ⟨Jset, _, hmax⟩ := zorn_subset_nonempty S chainub I IinS
obtain ⟨Jidl, IJ, JF⟩ := hmax.prop
set J := IsIdeal.toIdeal Jidl
use J
have IJ' : I ≤ J := IJ
clear chainub IinS
refine
⟨?_, ⟨IJ, JF⟩⟩
-- First note that J is proper: ⊤ ∈ F so ⊤ ∉ J because F and J are disjoint.
have Jpr : IsProper J :=
isProper_of_notMem
(Set.disjoint_left.1 JF F.top_mem)
-- Suppose that a₁ ∉ J, a₂ ∉ J. We need to prove that a₁ ⊔ a₂ ∉ J.
rw [isPrime_iff_mem_or_mem]
intro a₁ a₂
contrapose!
intro
⟨ha₁, ha₂⟩
-- Consider the ideals J₁, J₂ generated by J ∪ {a₁} and J ∪ {a₂}, respectively.
let J₁ := J ⊔ principal a₁
let J₂ := J ⊔ principal a₂
have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
have J₁J : ↑J₁ ≠ Jset := ne_of_mem_of_not_mem' a₁J₁ ha₁
have J₂J : ↑J₂ ≠ Jset := ne_of_mem_of_not_mem' a₂J₂ ha₂
have J₁S : ↑J₁ ∉ S := fun h => J₁J (hmax.eq_of_le h (le_sup_left : J ≤ J₁)).symm
have J₂S : ↑J₂ ∉ S := fun h => J₂J (hmax.eq_of_le h (le_sup_left : J ≤ J₂)).symm
have J₁F : ¬(Disjoint (F : Set α) J₁) := by
intro hdis
apply J₁S
simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
exact ⟨J₁.isIdeal, le_trans IJ' le_sup_left, hdis⟩
have J₂F : ¬(Disjoint (F : Set α) J₂) := by
intro hdis
apply J₂S
simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
exact
⟨J₂.isIdeal, le_trans IJ' le_sup_left, hdis⟩
-- Thus, pick cᵢ ∈ F ∩ Jᵢ.
let ⟨c₁, ⟨c₁F, c₁J₁⟩⟩ := Set.not_disjoint_iff.1 J₁F
let ⟨c₂, ⟨c₂F, c₂J₂⟩⟩ := Set.not_disjoint_iff.1 J₂F
let ⟨b₁, ⟨b₁J, cba₁⟩⟩ := (mem_ideal_sup_principal a₁ c₁ J).1 c₁J₁
let ⟨b₂, ⟨b₂J, cba₂⟩⟩ := (mem_ideal_sup_principal a₂ c₂ J).1 c₂J₂
let b := b₁ ⊔ b₂
have bJ : b ∈ J := sup_mem b₁J b₂J
have ineq : c₁ ⊓ c₂ ≤ b ⊔ (a₁ ⊓ a₂) :=
calc
c₁ ⊓ c₂ ≤ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) := inf_le_inf cba₁ cba₂
_ ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂) := by gcongr; exacts [le_sup_left, le_sup_right]
_ = b ⊔ (a₁ ⊓ a₂) := (sup_inf_left b a₁ a₂).symm
have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F :=
PFilter.mem_of_le ineq
(PFilter.inf_mem c₁F c₂F)
-- Now, if we would have a₁ ⊓ a₂ ∈ J, then, since J is an ideal and b ∈ J, we would also get
-- b ⊔ (a₁ ⊓ a₂) ∈ J. But this contradicts that J is disjoint from F.
contrapose! JF with ha₁a₂
rw [Set.not_disjoint_iff]
use b ⊔ (a₁ ⊓ a₂)
exact
⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩
-- TODO: Define prime filters in Mathlib so that the following corollary can be stated and proved.
-- theorem prime_filter_of_disjoint_filter_ideal (hFI : Disjoint (F : Set α) (I : Set α)) :
-- ∃ G : PFilter α, (IsPrime G) ∧ F ≤ G ∧ Disjoint (G : Set α) I := by sorry
