Add Posetal Reflections

Cubical/Algebra/CommRing/Ideal/Base.agda

@@ -89,6 +89,12 @@ module CommIdeal (R' : CommRing ℓ) where
  ∑Closed I {n = zero} _ _ = I .snd .contains0
  ∑Closed I {n = suc n} V h = I .snd .+Closed (h zero) (∑Closed I (V ∘ suc) (h ∘ suc))
 
+ open Exponentiation R'
+
+ ^sucClosed : (I : CommIdeal) (x : R) {n : ℕ}
+            → x ∈ I → x ^ suc n ∈ I
+ ^sucClosed I x x∈I = subst-∈ I (·Comm _ x) (·Closed (snd I) _ x∈I)
+
  0Ideal : CommIdeal
  fst 0Ideal x = (x ≡ 0r) , is-set _ _
  +Closed (snd 0Ideal) x≡0 y≡0 = cong₂ (_+_) x≡0 y≡0 ∙ +IdR _

Cubical/Algebra/CommRing/Ideal/Sum.agda

@@ -156,6 +156,9 @@ module IdealSum (R' : CommRing ℓ) where
  ·iComm⊆ I J x = map λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
                       → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·Comm (α i) (β i)))
 
+ ·iRincl : ∀ (I J : CommIdeal) → (I ·i J) ⊆ J
+ ·iRincl I J x x∈IJ = ·iLincl J I x (·iComm⊆ I J x x∈IJ)
+
  ·iComm : ∀ (I J : CommIdeal) → I ·i J ≡ J ·i I
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)
 

Cubical/Algebra/CommRing/RadicalIdeal.agda

@@ -99,8 +99,12 @@ module RadicalIdeal (R' : CommRing ℓ) where
  1∈√→1∈ : ∀ (I : CommIdeal) → 1r ∈ √ I → 1r ∈ I
  1∈√→1∈ I = PT.rec (∈-isProp (fst I) _) λ (n , 1ⁿ∈I) → subst-∈ I (1ⁿ≡1 n) 1ⁿ∈I
 
+ √Resp⊆ : (I J : CommIdeal) → I ⊆ J → √ I ⊆ √ J
+ √Resp⊆ I J I⊆J x = map (map-snd λ {a} → I⊆J (x ^ a))
+
  -- important lemma for characterization of the Zariski lattice
  open KroneckerDelta (CommRing→Ring R')
+
  √FGIdealCharLImpl : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
          → √ ⟨ V ⟩[ R' ] ⊆ √ I → (∀ i → V i ∈ √ I)
  √FGIdealCharLImpl V I √⟨V⟩⊆√I i = √⟨V⟩⊆√I _ (∈→∈√ ⟨ V ⟩[ R' ] (V i)
@@ -234,3 +238,10 @@ module RadicalIdeal (R' : CommRing ℓ) where
 
  √·Absorb+ : ∀ (I J : CommIdeal) → √ (I ·i (I +i J)) ≡ √ I
  √·Absorb+ I J = CommIdeal≡Char (√·Absorb+LIncl I J) (√·Absorb+RIncl I J)
+
+ √·ContrLIncl : ∀ (I J : CommIdeal) → √ (√ I ·i √ J) ⊆ √ (I ·i J)
+ √·ContrLIncl I J x = √·RContrLIncl I J x ∘ subst (x ∈_) (√·LContr I (√ J))
+
+ √Pres·LIncl : ∀ (I J : CommIdeal) → (√ I ·i √ J) ⊆ √ (I ·i J)
+ √Pres·LIncl I J x = √·ContrLIncl I J x ∘ ∈→∈√ (√ I ·i √ J) x
+