# The Zariski locale

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

Created on 2023-06-08.

module commutative-algebra.zariski-locale where
Imports
open import commutative-algebra.commutative-rings

open import foundation.universe-levels

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

## Idea

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.

## Definition

### The Zariski frame

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

zariski-frame-Commutative-Ring :
Large-Frame  l2  l1  lsuc l2)  l2 l3  l1  l2  l3) l1
large-poset-Large-Frame
zariski-frame-Commutative-Ring =
is-large-meet-semilattice-Large-Frame
zariski-frame-Commutative-Ring =
is-large-suplattice-Large-Frame zariski-frame-Commutative-Ring =
distributive-meet-sup-Large-Frame zariski-frame-Commutative-Ring =