Examples of finite presentations of CommAlgebra's (#680)

* Generalize universe levels in CommAlgebraHom

* State the universal property of FreeCommAlgebra

* refactor

* Refactor

* define finite presentation, refactor

* Draw conclusion from the universal property of the initial algebra

* stuck - TC speed

* construct terminal algebra

* show universal property

* terminal ring for any universe level

* Refactor: Use UnitCommRing

* Rollback renaming (for now)

* try 'abstract'

* abstract works...

* Fix

* WIP: Use CommIdeal

* Use CommIdeal for CommRing-Quotients

* Use CommIdeal for FGIdeals

* Remove obsolete comment

* Fix usages in CommAlgebra

* Fix usages in CommAlgebra

* WIP: Use CommIdeal

* Use CommIdeal for CommRing-Quotients

* Use CommIdeal for FGIdeals

* Remove obsolete comment

* Fix usages in CommAlgebra

* Fix usages in CommAlgebra

* Remove obsolete comment

* Converts non-commutatitive ideals to commutative ideal in CommRings

* remove something strange

* start with kernels of CommAlgebraHoms

* brush up old kernel ideal

* Some helper functions for CommAlgebra

* Define kernel of algebra homorphism

* Some helper functions for CommAlgebra

* Fix standardized boilerplate

* refactor

* universal prop for quotients of CommAlgebras

* Zero ideal in an CommAlgebra

* one ideal in CommAlgebra

* compute trivial quotients

* compute trivial quotients

* split and move FreeCommAlgebra

* Fix standardized boilerplate

* Draw conclusion from the universal property of the initial algebra

* Add identity CAlgHom

* clean up

* show

* flatten the hierarchie

* remove obsolete

* clean up and comments

* deduplicate definition of 1-ideal and 0-ideal

* deduplicate definition of 1-ideal and 0-ideal

* deduplicate definition of 1-ideal and 0-ideal

* 0-Ideal in CommAlgebra is generated

* Convience functions for CommAlgebras

* new tc speed problem...

* WIP

* wip: try to avoid tc speed problem

* wip: universal property of multivariate polynomials

* fixes

* make checkable

* induced morphism by universal property of finitely presented algebra

* refactor, continue

* refactor

* lemma for set quotients

* injectivity of precomposition with quotient map

* generalize universe level

* uniqueness in the universal property of FP-algebras

* construct finite presentation of initial CommAlgebra

* whitespace

* more naturality lemmas

* lemma about free algebra

* prove that the given relations in a finitely presented algebra hold

* WIP: the terminal algebra is finitely presented

* WIP: construct finite presentation of terminal algebra

* use ring solver

* clean up

* remove wrong commenting

* use concise notation

* corrected a comment

* better name for a lemma

* inducedHom (in FPAlgebra.agda) should take the algebra explicitly

* missing part of universal property of FPAlgebra

* wip: polynomial algebras are finitely presented

* polynomial algebras are finitely presented

* Spec Iso in FPAlgebra.agda

Isomorphism between spectrum (understood as zero locus of generators) and comm algebra homomorphisms.

* Update FPAlgebra.agda

Improve notation

* Update FPAlgebra.agda

eol

* minor conflict fix, indentation, notation

* Remove meaningless change

* state naming convetion

* replace occurences of the old style

* replace occurences of the old style

* Revert "state naming convetion"

This reverts commit befff8a.

* adapt to naming conventions

* minor beautification

* remove bad levels

Co-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>
Co-authored-by: arodrica43 <lexws33@gmail.com>

Cubical/Algebra/Algebra/Properties.agda

@@ -31,9 +31,6 @@ private
   variable
     ℓ ℓ' ℓ'' ℓ''' : Level
 
-
-
-
 module AlgebraTheory (R : Ring ℓ) (A : Algebra R ℓ') where
   open RingStr (snd R) renaming (_+_ to _+r_ ; _·_ to _·r_)
   open AlgebraStr (A .snd)
@@ -77,6 +74,11 @@ module AlgebraHoms {R : Ring ℓ} where
   compIsAlgebraHom {g = g} {f} gh fh .pres- x = cong g (fh .pres- x) ∙ gh .pres- (f x)
   compIsAlgebraHom {g = g} {f} gh fh .pres⋆ r x = cong g (fh .pres⋆ r x) ∙ gh .pres⋆ r (f x)
 
+  _∘≃a_ : {A B C : Algebra R ℓ'}
+         → AlgebraEquiv B C → AlgebraEquiv A B → AlgebraEquiv A C
+  _∘≃a_  g f .fst = compEquiv (fst f) (fst g)
+  _∘≃a_  g f .snd = compIsAlgebraHom (g .snd) (f .snd)
+
   compAlgebraHom : {A : Algebra R ℓ'} {B : Algebra R ℓ''} {C : Algebra R ℓ'''}
               → AlgebraHom A B → AlgebraHom B C → AlgebraHom A C
   compAlgebraHom f g .fst = g .fst ∘ f .fst

Cubical/Algebra/CommAlgebra/Base.agda

@@ -23,7 +23,7 @@ open import Cubical.Reflection.RecordEquiv
 
 private
   variable
-    ℓ ℓ' ℓ'' ℓ''' : Level
+    ℓ ℓ' ℓ'' : Level
 
 record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                      (0a : A) (1a : A)

Cubical/Algebra/CommAlgebra/FGIdeal.agda

@@ -1,22 +1,37 @@
 {-# OPTIONS --safe #-}
 module Cubical.Algebra.CommAlgebra.FGIdeal where
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.FinData
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Algebra.CommRing.FGIdeal renaming (generatedIdeal to generatedIdealCommRing)
+open import Cubical.Algebra.CommRing.FGIdeal using ()
+            renaming (generatedIdeal to generatedIdealCommRing;
+                      indInIdeal to ringIncInIdeal;
+                      0FGIdeal to 0FGIdealCommRing)
 open import Cubical.Algebra.CommAlgebra
 open import Cubical.Algebra.CommAlgebra.Ideal
 
 private
   variable
     ℓ : Level
+    R : CommRing ℓ
+
+generatedIdeal : {n : ℕ} (A : CommAlgebra R ℓ) → FinVec (fst A) n → IdealsIn A
+generatedIdeal A = generatedIdealCommRing (CommAlgebra→CommRing A)
+
+incInIdeal :   {n : ℕ} (A : CommAlgebra R ℓ)
+              (U : FinVec ⟨ A ⟩ n) (i : Fin n) → U i ∈ fst (generatedIdeal A U)
+incInIdeal A = ringIncInIdeal (CommAlgebra→CommRing A)
+
+syntax generatedIdeal A V = ⟨ V ⟩[ A ]
 
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   open CommAlgebraStr (snd A)
 
-  generatedIdeal : {n : ℕ} → FinVec (fst A) n → IdealsIn A
-  generatedIdeal = generatedIdealCommRing (CommAlgebra→CommRing A)
+  0FGIdeal : {n : ℕ} → ⟨ replicateFinVec n 0a ⟩[ A ] ≡ (0Ideal A)
+  0FGIdeal = 0FGIdealCommRing (CommAlgebra→CommRing A)