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