The Synthetic Spectrum

All the mathematics presented here, is from Ingo Blechschmidt’s thesis or unpublished work of David Jaz Myers. The formalization in Agda is due to Felix Cherubini.

In the following, we will use a fixed, commutative ring 𝔸. We are specifically interested in commutative algebras over that ring, so let us introduce a short name for those and let us use ‘𝔸’ to refer to the 𝔸-algebra 𝔸.

module SpecExamples (𝔸asRing : CommRing {ℓ}) where
  𝔸-Alg = CommAlgebra 𝔸asRing
  𝔸 = CommAlgebraExamples.initial 𝔸asRing

The synthetic spectrum of an 𝔸-algebra R, Spec R, is supposed to be a space such that the ring of functions on Spec R is R. Moreover, Spec R, should be so small and rigid, that the only homomorphisms R → 𝔸 are evaluations at points. The latter can be turned around to give a definition:

  Hom : 𝔸-Alg → 𝔸-Alg → Type ℓ
  Hom R S = CAlgHom R S

  Spec : 𝔸-Alg → Type ℓ
  Spec R = Hom R 𝔸

𝔸 is the initial 𝔸-algebra, so we know that its spectrum has to be equal to the point:

  point : Type ℓ
  point = Unit*

  _ : Spec 𝔸 ≡ point
  _ = CommAlgebraExamples.isInitial 𝔸asRing 𝔸

Note that in the Zariski topos based on affine k-schemes, Spec k would be the point as well. In general, 𝔸 behaves like the base field (or ring) when plugged into the Spec construction. Here is another instance of this phenomenon:

  𝔸[X] = 𝔸asRing [ Unit* ]
  𝔸′ = CommAlgebra.Carrier 𝔸              -- 𝔸′ is the underlying type of the algebra 𝔸

  _ : Spec 𝔸[X] ≡ 𝔸′
  _ = Spec 𝔸[X]        ≡⟨ refl ⟩
      Hom 𝔸[X] 𝔸      ≡⟨ homMapEq 𝔸 ⟩
      (Unit* → 𝔸′)     ≡⟨ isoToPath
                            (iso (λ f → f tt*) (λ a _ → a)
                                 (λ b i → b)
                                 λ a i x → a x) ⟩
      𝔸′ ∎

More generall, any type of the form ‘D → 𝔸’ is a ‘Spec’ of the 𝔸-algebra 𝔸[D]:

  module _ (D : Type ℓ) where
    𝔸[D] = 𝔸asRing [ D ]
    mappingSchemeEq : Spec 𝔸[D] ≡ (D → 𝔸′)
    mappingSchemeEq = Spec 𝔸[D]      ≡⟨ refl ⟩
                      Hom 𝔸[D] 𝔸    ≡⟨ homMapEq 𝔸 ⟩
                      (D → 𝔸′)       ∎

We can use the standard n-elment type ‘Fin n’ to define the affine n-dimensional standard space as a spectrum:

  𝔸″ : ℕ → Type ℓ
  𝔸″ n = Spec (𝔸asRing [ Lift (Fin n) ])

This space is equivalent to a mapping space as we showed above, which in turn is a cartesian product. For the n-fold cartesian product of 𝔸, we use the type ‘Vec 𝔸 n’:

  standardSpaceEq : ∀ (n : ℕ)
                  → 𝔸″ n ≡ Vec 𝔸′ n
  standardSpaceEq n = 𝔸″ n                ≡⟨ mappingSchemeEq _ ⟩
                      (Lift (Fin n) → 𝔸′) ≡⟨ lemma _ _ LiftEquiv ⟩
                      (Fin n → 𝔸′)        ≡⟨ FinVec≡Vec n ⟩
                      Vec 𝔸′ n ∎
    where lemma : (X : Type₀) (Y : Type ℓ) → (X ≃ Y) → (Y → 𝔸′) ≡ (X → 𝔸′)
          lemma X Y equiv =
            let open Iso (equivToIso equiv)
                  renaming (fun to e; inv to e⁻¹)
            in isoToPath
               (iso (λ f → λ x → f (e x))
                    (λ g → λ y → g (e⁻¹ y))
                    (λ f → λ i x →
                         (f (e⁻¹ (e x)) ≡⟨ cong f (leftInv x) ⟩
                         f x            ∎)
                      i)
                    λ g → λ i y →
                         (g (e (e⁻¹ y)) ≡⟨ cong g (rightInv y) ⟩
                         g y ∎)
                       i)

See how the story is supposed to continue with Synthetic Quasi Coherence.