{-# 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

{-
   The image of an fg ideal under a surjection is an fg ideal generated by the
   images of the generators
-}
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