Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii

gaxiiiiiiiiiiii/Krull.lean

Created December 8, 2025 22:31
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save gaxiiiiiiiiiiii/7ad9c6209e79cab13532c19b7bc4c6a3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save gaxiiiiiiiiiiii/7ad9c6209e79cab13532c19b7bc4c6a3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Krull.lean
import Mathlib
open Order
instance Ideal.isCoatomic (B : Type _) [BooleanAlgebra B] :
IsCoatomic (Ideal B)
:= {
eq_top_or_exists_le_coatom I := by
rw [or_iff_not_imp_left]; intro HI
let 𝓙 := {J : Ideal B | J.IsProper ∧ I ≀ J}
set 𝓙' := (LowerSet.carrier ∘ Ideal.toLowerSet) '' 𝓙
have H𝓙' : (βˆ€ c βŠ† 𝓙', IsChain (fun x1 x2 => x1 βŠ† x2) c β†’ c.Nonempty β†’ βˆƒ ub ∈ 𝓙', βˆ€ s ∈ c, s βŠ† ub) := by {
intro 𝓒 𝓒𝓙 H𝓒 H𝓒'
unfold IsChain at H𝓒; simp at H𝓒
let J : Ideal B := {
carrier := ⋃₀ 𝓒
lower' := by
intro x y yx Hx; simp at *
rcases Hx with ⟨C, HC, Cx⟩
have := 𝓒𝓙 HC; simp [𝓙', 𝓙] at this
rcases this with ⟨J, ⟨HJ, IJ⟩, E⟩
use C, HC
subst C
apply J.lower yx Cx
nonempty' := by
use βŠ₯; simp
rcases H𝓒' with ⟨c, Hc⟩
use c, Hc
apply 𝓒𝓙 at Hc; simp [𝓙', 𝓙] at Hc
rcases Hc with ⟨J, ⟨HJ, IJ⟩, E⟩; subst c
apply J.bot_mem
directed' := by
intro x Hx y Hy; simp at Hx Hy; simp
rcases Hx with ⟨X, HX, Xx⟩
rcases Hy with ⟨Y, HY, Yy⟩
have ⟨X', ⟨HX', IX'⟩, EX⟩:= 𝓒𝓙 HX; simp at EX
have ⟨Y', ⟨HY', IY'⟩, EY⟩:= 𝓒𝓙 HY; simp at EY
have := H𝓒 HX HY; simp at this
by_cases HXY : X = Y
Β· subst Y X
simp at HXY; subst Y'
have ⟨z, Hz, H1, H2⟩ := X'.directed _ Xx _ Yy
simp at H1 H2
use z, ⟨X', HX, Hz⟩, H1, H2
Β· rcases this HXY with XY | YX
Β· apply XY at Xx
subst Y
have ⟨z, Hz, H1, H2⟩:= Y'.directed _ Xx _ Yy
simp at H1 H2
use z, ⟨Y', HY, Hz⟩, H1, H2
Β· apply YX at Yy
subst X
have ⟨z, Hz, H1, H2⟩:= X'.directed _ Xx _ Yy
simp at H1 H2
use z, ⟨X', HX, Hz⟩, H1, H2
}
use J; constructor
Β· simp [𝓙', 𝓙]; constructor
Β· constructor
intro F
have : (⊀ : B) ∈ Set.univ := by simp
rw [<- F] at this
change ⊀ ∈ ⋃₀ 𝓒 at this
simp at this
rcases this with ⟨C, HC, Ct⟩
apply 𝓒𝓙 at HC; simp [𝓙', 𝓙] at HC
rcases HC with ⟨C', ⟨HC', IC'⟩, E⟩
apply HC'.ne_univ; ext x; simp; subst C
apply C'.lower (by simp) Ct
Β· intro x Hx
change x ∈ ⋃₀ 𝓒; simp
by_contra F; simp at F
have ⟨C, HC⟩ := H𝓒'
have FC := F C HC
apply 𝓒𝓙 at HC; simp [𝓙', 𝓙] at HC
rcases HC with ⟨C', ⟨HC', IC'⟩, E⟩
subst C
apply FC; apply IC' Hx
Β· intro C HC c Hc
change c ∈ ⋃₀ 𝓒; simp
use C
}
have I𝓙' : I.carrier ∈ 𝓙' := by {
simp [𝓙', 𝓙]
apply I.isProper_of_ne_top HI
}
have ⟨J, IJ, J𝓙', HJ⟩ := zorn_subset_nonempty _ H𝓙' _ I𝓙'
simp at *
simp [𝓙', 𝓙] at J𝓙'
rcases J𝓙' with ⟨J', ⟨HJ', IJ'⟩, E⟩
subst J; simp at *
use J', ?_, IJ'
constructor
Β· exact HJ'.ne_top
Β· intro K JK
by_contra F
rw [lt_iff_le_not_ge] at JK
rcases JK with ⟨JK, KJ⟩
apply KJ; clear KJ
apply HJ ?_ JK
simp [𝓙', 𝓙]; constructor
Β· apply K.isProper_of_ne_top F
Β· apply le_trans IJ JK
}
noncomputable def Order.Ideal.maximal [BooleanAlgebra B] (I : Ideal B) [HI : I.IsProper] :
Ideal B
:= by
have H := or_iff_not_imp_left.mp ((Ideal.isCoatomic B).eq_top_or_exists_le_coatom I) HI.ne_top
exact H.choose
lemma Order.Ideal.maximal_isMaximal [BooleanAlgebra B] (I : Ideal B) [HI : I.IsProper] :
(I.maximal).IsMaximal
:= by
have H := or_iff_not_imp_left.mp ((Ideal.isCoatomic B).eq_top_or_exists_le_coatom I) HI.ne_top
rw [Ideal.isMaximal_iff_isCoatom]
exact H.choose_spec.1
lemma Order.Ideal.le_maximal [BooleanAlgebra B] (I : Ideal B) [HI : I.IsProper] :
I ≀ I.maximal
:= by
have H := or_iff_not_imp_left.mp ((Ideal.isCoatomic B).eq_top_or_exists_le_coatom I) HI.ne_top
exact H.choose_spec.2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment