{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.FGIdeal where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset
open import Cubical.Functions.Surjection
open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal.SurjectiveImage
import Cubical.Algebra.CommRing.Ideal as CommRing
import Cubical.Algebra.CommRing.FGIdeal as CommRing
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Ideal
private
variable
ℓ ℓ' ℓ'' : Level
R : CommRing ℓ
generatedIdeal : {n : ℕ} (A : CommAlgebra R ℓ') → FinVec ⟨ A ⟩ₐ n → IdealsIn R A
generatedIdeal A = CommRing.generatedIdeal (CommAlgebra→CommRing A)
incInIdeal : {n : ℕ} (A : CommAlgebra R ℓ')
(g : FinVec ⟨ A ⟩ₐ n) (i : Fin n) → g i ∈ fst (generatedIdeal A g)
incInIdeal A = CommRing.indInIdeal (CommAlgebra→CommRing A)
syntax generatedIdeal A V = ⟨ V ⟩[ A ]
module _ (A : CommAlgebra R ℓ') where
open CommRingStr (A .fst .snd)
opaque
0FGIdeal≡0Ideal : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩[ A ] ≡ (0Ideal R A)
0FGIdeal≡0Ideal = CommRing.0FGIdeal (CommAlgebra→CommRing A)
inclOfFGIdeal : {n : ℕ} (V : FinVec ⟨ A ⟩ₐ n) (I : IdealsIn R A)
→ (∀ i → V i ∈ fst I) → fst ⟨ V ⟩[ A ] ⊆ fst I
inclOfFGIdeal V I ∀i→Vi∈I = CommRing.inclOfFGIdeal (CommAlgebra→CommRing A) V I ∀i→Vi∈I
imageIdealIsImageFGIdeal :
{n : ℕ} (A : CommAlgebra R ℓ') (g : FinVec ⟨ A ⟩ₐ n) (B : CommAlgebra R ℓ')
(f : CommAlgebraHom A B) (surjective : isSurjection ⟨ f ⟩ₐ→)
→ imageIdeal (CommAlgebraHom→CommRingHom f) surjective ⟨ g ⟩[ A ] ≡ generatedIdeal B (⟨ f ⟩ₐ→ ∘ g)
imageIdealIsImageFGIdeal {n = n} A g B f surjective =
CommRing.CommIdeal.CommIdeal≡Char BasCR
(λ b b∈image →
PT.rec isPropPropTrunc
(λ (a , (a∈⟨g⟩ , fa≡b)) →
PT.rec isPropPropTrunc
(λ (v , a≡vg) →
∣ (⟨ f ⟩ₐ→ ∘ v ,
(b ≡⟨ sym fa≡b ⟩
fst f a ≡⟨ cong (fst f) a≡vg ⟩
fst f (linComb AasCR v g)
≡⟨ CommRing.presLinearCombination AasCR BasCR (CommAlgebraHom→CommRingHom f) _ v g ⟩
linComb BasCR (⟨ f ⟩ₐ→ ∘ v) (⟨ f ⟩ₐ→ ∘ g) ∎)) ∣₁)
a∈⟨g⟩)
b∈image)
(inclOfFGIdeal B (⟨ f ⟩ₐ→ ∘ g) image λ i → ∣ (g i) , incInIdeal A g i , refl ∣₁)
where image = imageIdeal (CommAlgebraHom→CommRingHom f) surjective ⟨ g ⟩[ A ]
linComb = CommRing.linearCombination
AasCR = CommAlgebra→CommRing A
BasCR = CommAlgebra→CommRing B