```
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Algebra.Bundles
open import Data.Nat hiding (_*_)
```


┌────────────────────────────────────────────────────┐
|            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 over A
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        = ∅
  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        = ∅
  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.
  -- (Sometimes "Eventually P σ" is spelt "∇ P σ".)
  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 ⟩) ｝)

  -- In this incarnation, the maximal ideal is a stage-dependent subset of A:
  -- On a stage σ, a ring element x is contained in the maximal ideal iff
  -- eventually it will belong to one of the G n.
  𝔪 : List A → Pred A
  𝔪 σ x = Eventually (λ σ → x ∈ ⋃[ n ∶ ℕ ] G n σ) σ

  is-proper : (σ : List A) → ¬ 1# ∈ 𝔪 σ
  is-proper σ = {!!}

  -- The maximal ideal is indeed maximal: If the maximal ideals remains
  -- proper (even over time) when adding x, then x is already included in the maximal ideal.
  theorem
    : (x : A) (σ : List A)
    → (∀ τ → ¬ 1# ∈ ⟨ 𝔪 (σ ++ τ) , x ⟩)
    → x ∈ 𝔪 σ
  theorem x σ p = {!!}

  -- If a 2x1 matrix [a; b] is surjective (expressed by the existence of u, v
  -- such that u [a; b] = [1; 0] and v [a; b] = [0; 1]), then ⊥ (which is defined
  -- to mean 1 = 0 in A).
  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 = {!!}
```