The Zariski locale

Content created by Fredrik Bakke, Egbert Rijke and Maša Žaucer.

Created on 2023-06-08.
Last modified on 2023-06-09.

module commutative-algebra.zariski-locale where
open import commutative-algebra.commutative-rings
open import commutative-algebra.intersections-radical-ideals-commutative-rings
open import commutative-algebra.joins-radical-ideals-commutative-rings
open import commutative-algebra.poset-of-radical-ideals-commutative-rings

open import foundation.universe-levels

open import order-theory.large-frames
open import order-theory.large-locales


The Zariski locale of a commutative ring A is the large locale consisting of radical ideals of A. Our proof of the fact that meets distribute over arbitrary joins uses the fact that the intersection I ∩ J of radical ideals is equivalently described as the radical ideal √ IJ of the product ideal.


The Zariski frame

module _
  {l1 : Level} (A : Commutative-Ring l1)

  zariski-frame-Commutative-Ring :
    Large-Frame  l2  l1  lsuc l2)  l2 l3  l1  l2  l3) l1
    zariski-frame-Commutative-Ring =
    radical-ideal-Commutative-Ring-Large-Poset A
    zariski-frame-Commutative-Ring =
    is-large-meet-semilattice-radical-ideal-Commutative-Ring A
  is-large-suplattice-Large-Frame zariski-frame-Commutative-Ring =
    is-large-suplattice-radical-ideal-Commutative-Ring A
  distributive-meet-sup-Large-Frame zariski-frame-Commutative-Ring =
    distributive-intersection-join-family-of-radical-ideals-Commutative-Ring A

The Zariski locale

module _
  {l1 : Level} (A : Commutative-Ring l1)

  zariski-locale-Commutative-Ring :
    Large-Locale  l2  l1  lsuc l2)  l2 l3  l1  l2  l3) l1
  zariski-locale-Commutative-Ring = zariski-frame-Commutative-Ring A

Recent changes