# The poset of radical ideals of a commutative ring

Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer and Gregor Perčič.

Created on 2023-06-08.

module commutative-algebra.poset-of-radical-ideals-commutative-rings where

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.poset-of-ideals-commutative-rings

open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.similarity-of-elements-large-posets


## Idea

The large poset of radical ideals in a commutative ring consists of radical ideals ordered by inclusion.

## Definition

### The ordering of radical ideals in a commutative ring

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

{l2 l3 : Level} →
radical-ideal-Commutative-Ring l3 A → Prop (l1 ⊔ l2 ⊔ l3)
leq-prop-ideal-Commutative-Ring A

{l2 l3 : Level} →
radical-ideal-Commutative-Ring l3 A → UU (l1 ⊔ l2 ⊔ l3)
leq-ideal-Commutative-Ring A

{l2 l3 : Level}
(J : radical-ideal-Commutative-Ring l3 A) →
is-prop-leq-ideal-Commutative-Ring A

{l2 : Level} (I : radical-ideal-Commutative-Ring l2 A) →
refl-leq-ideal-Commutative-Ring A

{l2 l3 l4 : Level}
(K : radical-ideal-Commutative-Ring l4 A) →
transitive-leq-ideal-Commutative-Ring A

{l2 : Level} (I J : radical-ideal-Commutative-Ring l2 A) →
leq-radical-ideal-Commutative-Ring J I → I ＝ J
antisymmetric-leq-radical-ideal-Commutative-Ring I J H K =
eq-type-subtype
( antisymmetric-leq-ideal-Commutative-Ring A
( H)
( K))


### The large preorder of radical ideals in a commutative ring

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

Large-Preorder (λ l1 → l ⊔ lsuc l1) (λ l1 l2 → l ⊔ l1 ⊔ l2)


### The large poset of radical ideals in a commutative ring

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

Large-Poset (λ l1 → l ⊔ lsuc l1) (λ l1 l2 → l ⊔ l1 ⊔ l2)


### Similarity of radical ideals in a commutative ring

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

sim-prop-radical-ideal-Commutative-Ring : Prop (l1 ⊔ l2 ⊔ l3)

sim-radical-ideal-Commutative-Ring : UU (l1 ⊔ l2 ⊔ l3)



### The inclusion of radical ideals into ideals of a commutative ring

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

{l1 l2 : Level}
(J : radical-ideal-Commutative-Ring l2 A) →
leq-ideal-Commutative-Ring A
preserves-order-ideal-radical-ideal-Commutative-Ring I J H = H