comment

Author: felixwellen

Cubical/Algebra/CommAlgebra/FGIdeal.agda

@@ -45,6 +45,10 @@ module _ (A : CommAlgebra R ℓ') where
         → (∀ 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 ⟩ₐ→)