```
{-# 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 {!!})))))
-}
```