```
```
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Algebra.Bundles
open import Data.Nat
```

┌────────────────────────────────────────────────────┐
|            REIFYING DYNAMICAL ALGEBRA              |
│ maximal ideals for arbitrary rings, constructively │
└────────────────────────────────────────────────────┘

Ingo Blechschmidt

Proof and Computation
in Schlehdorf
June 2nd, 2022

honoring Helmut Schwichtenberg

# ..... IN THIS TALK .....

Explanations that ...

1. every set is countable.

2. every ring has a maximal ideal, constructively.

Checked in Agda. Both made possible by:

3. An intriguing fractal
(with lots of opens and no points).

4. Proofs with monadic side effects.

Thereby reifying dynamical algebra.

# ..... GROUNDING .....

Let A be a commutative ring with unit
(e.g. ℤ, ℤ[X], ℚ[X,Y,Z]/(Xⁿ+Yⁿ-Zⁿ), ...).

**THM.** Let M be a surjective matrix with more
rows than columns. Then 1 = 0 in A.

**PROOF.** [Assume not.]() Then there is a [maximal ideal]() 𝔪.
The matrix M is surjective over the [field]() A/𝔪.
This is a [contradiction]() to basic linear algebra.

# ..... A CONSTRUCTION OF [Krull 1929] .....

Let A be a **countable** commutative ring with unit.
Let f : ℕ ↠ A be an enumeration of A. Using **LEM**,
recursively define:

G₀   = ∅

Gₙ₊₁ = Gₙ,          if 1 ∈ ⟨Gₙ ∪ {f(n)}⟩
Gₙ ∪ {f(n)}, else.

Then 𝔪 ≔ ⋃ₙ Gₙ is a maximal ideal.
```

module _ (A… : CommutativeRing 0ℓ 0ℓ) where

open CommutativeRing A… renaming (Carrier to A)
open import SchlehdorfBasics (A…)

module Krull
(f : ℕ → A)
(p : (x : A) → Σ[ n ∈ ℕ ] x ≈ f n)
(oracle : ExcludedMiddle) where

{-
G₀   = ∅

Gₙ₊₁ = Gₙ,          if 1 ∈ ⟨Gₙ ∪ {f(n)}⟩
Gₙ ∪ {f(n)}, else.
-}
G : ℕ → Pred A
G 0       = ∅
G (suc n) with oracle (1# ∈ ⟨ G n ∪ ｛ f n ｝ ⟩)
... | yes _ = G n
... | no  _ = G n ∪ ｛ f n ｝

𝔪 : Pred A
𝔪 = ⋃[ n ∶ ℕ ] G n  -- = ⋃ₙ Gₙ

is-proper : ¬ 1# ∈ 𝔪
is-proper = {!!}

-- THM. For all x ∈ A, 1 ∈ ⟨𝔪,x⟩ or x ∈ 𝔪.
theorem : (x : A) → 1# ∈ ⟨ 𝔪 , x ⟩ ⊎ x ∈ 𝔪
theorem = {!!}

module Krivine
(f : ℕ → A)
(p : (x : A) → Σ[ n ∈ ℕ ] x ≈ f n)
where

{-
G₀   = ∅
Gₙ₊₁ = Gₙ ∪ { f(n) | 1 ∉ ⟨Gₙ, f(n)⟩ }
-}
G : ℕ → Pred A
G 0       = ∅
G (suc n) = G n ∪ ｛ f n ∥ ¬ 1# ∈ ⟨ G n , f n ⟩ ｝

𝔪 : Pred A
𝔪 = ⋃[ n ∶ ℕ ] G n  -- = ⋃ₙ Gₙ

is-proper : ¬ 1# ∈ 𝔪
is-proper = {!!}

-- THM. For all x, if not 1 ∈ ⟨𝔪,x⟩, then x ∈ 𝔪.
theorem : (x : A) → ¬ (1# ∈ ⟨ 𝔪 , x ⟩) → x ∈ 𝔪
theorem = {!!}

module Joyal–Tierney where
open import Data.List.Membership.Propositional renaming (_∈_ to _◂_)

-- Eventually P σ expresses that, no matter how the finite
-- approximation σ to the generic surjection ℕ ↠ A will develop
-- to a better approximation σ', eventually P σ' will hold.
data Eventually (P : List A → Set) : List A → Set where
Now          : ∀ {σ} → P σ → Eventually P σ
NeedValue    : ∀ {σ} → ((x : A) → Eventually P (σ ∷ʳ x)) → Eventually P σ
NeedPreimage : ∀ {σ} → {a : A} → ((τ : List A) → a ◂ (σ ++ τ) → Eventually P (σ ++ τ)) → Eventually P σ

conservative : {Q : Set} {σ : List A} → Eventually (λ _ → Q) σ → Q
conservative = {!!}

Eventually' : (List A → Pred A) → (List A → Pred A)
Eventually' M σ x = Eventually (λ τ → M τ x) σ

f : ℕ → List A → Pred A
f n σ = λ x → σ [ n ]≡ x

G : ℕ → List A → Pred A
G zero    σ = ∅
G (suc n) = Eventually'
(λ σ → G n σ ∪ ｛ x ∶ f n σ ∥ (∀ τ → ¬ 1# ∈ ⟨ G n (σ ++ τ) , x ⟩) ｝)

𝔪 : List A → Pred A
𝔪 σ x = Eventually (λ σ → x ∈ ⋃[ n ∶ ℕ ] G n σ) σ

theorem
: (x : A) (σ : List A)
→ (∀ τ → ¬ 1# ∈ ⟨ 𝔪 (σ ++ τ) , x ⟩)
→ x ∈ 𝔪 σ
theorem x σ p = {!!}

{-
NeedPreimage {a = x} h
where
open import Data.Product
open import Data.Fin

g : {α : List A} (q : x ◂ α) → x ∈ f (toℕ (index q)) α
g (here _≡_.refl) = _≡_.refl
g (there q)       = g q

--g' : {α : List A} (q : x ◂ α) → x ∈ f (toℕ (index q)) α

mon : {α : _} {n : ℕ} {a x : A} → a ∈ ⟨ (G n α) ~ x ⟩ → a ∈ ⟨ 𝔪 α ~ x ⟩
mon {α} {n} (Base (inj₁ x)) = Base (inj₁ (Now (n , x)))
mon {α} {n} (Base (inj₂ y)) = Base (inj₂ y)
mon {α} {n} (Add p q) = Add (mon {n = n} p) (mon {n = n} q)
mon {α} {n} (Mult p) = Mult (mon {n = n} p)
mon {α} {n} Zero = Zero
mon {α} {n} (Eq p q) = Eq p (mon {n = n} q)

h : (τ : List A) → x ◂ (τ ++ σ) → _
h τ q = Now (ℕ.suc (toℕ (index q)) , Now (inj₂ (g q , s)))
where
open import Data.List.Properties
z : ∀ {τ' τ σ x} → 1# ∈ ⟨ 𝔪 (τ' ++ τ ++ σ) ~ x ⟩ → 1# ∈ ⟨ 𝔪 ((τ' ++ τ) ++ σ) ~ x ⟩
z {τ'} {τ} {σ} {x} a rewrite ++-assoc τ' τ σ = a
s : (τ' : List A) → _ → _
s τ' r = p (τ' ++ τ) (z {τ'} {τ} {σ} {x} (mon {τ' ++ τ ++ σ} {toℕ (index q)} r))

example : (a b u v : A) → u * a ≈ 1# → u * b ≈ 0# → v * a ≈ 0# → v * b ≈ 1# → ⊥
example a b u v ua1 ub0 va0 vb1 =
is-proper (is-ideal (Eq ua1 (Mult (Base (theorem a {!!})))))
-}
```

```