{-
This module shows, that a couple of R-algebras are finitely presented.
So far, in all cases a finite presentation is constructed.
Here is a list of the fp-algebras in this file, with their presentations:
* R[X₁,...,Xₙ] = R[X₁,...,Xₙ]/⟨⟩ (ideal generated by zero elements)
* R = R[⊥]/⟨⟩
* R/⟨x₁,...,xₙ⟩ = R[⊥]/⟨x₁,...,xₙ⟩
* R/⟨x⟩ (as special case of the above)
-}
{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Algebra.CommAlgebra.FP.Instances where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal using (inclOfFGIdeal)
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Polynomials as Poly
open import Cubical.Algebra.CommAlgebra.Quotient as Quot
open import Cubical.Algebra.CommAlgebra.Ideal using (IdealsIn; 0Ideal)
open import Cubical.Algebra.CommAlgebra.FGIdeal
open import Cubical.Algebra.CommAlgebra.Instances.Initial
open import Cubical.Algebra.CommAlgebra.Instances.Terminal
open import Cubical.Algebra.CommAlgebra.Notation
open import Cubical.Algebra.CommAlgebra.FP as FP
private variable
ℓ ℓ' : Level
module _ (R : CommRing ℓ) where
open FinitePresentation
{- Every (multivariate) polynomial algebra is finitely presented -}
module _ (n : ℕ) where
private
opaque
p : 0Ideal R (Polynomials R n) ≡ ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]
p = sym $ 0FGIdeal≡0Ideal (Polynomials R n)
compute :
CommAlgebraEquiv (Polynomials R n)
((Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ])
compute =
transport (λ i → CommAlgebraEquiv (Polynomials R n) ((Polynomials R n) / (p i))) $
zeroIdealQuotient (Polynomials R n)
polynomialsFP : FinitePresentation R
polynomialsFP =
record {
n = n ;
m = 0 ;
relations = emptyFinVec ⟨ Polynomials R n ⟩ₐ
}
opaque
unfolding fpAlg fgIdeal
isFPPolynomials : isFP R (Polynomials R n)
isFPPolynomials = ∣ polynomialsFP , invCommAlgebraEquiv compute ∣₁
{- The initial R-algebra is finitely presented -}
private
R[⊥] : CommAlgebra R ℓ
R[⊥] = Polynomials R 0
emptyGen : FinVec ⟨ R[⊥] ⟩ₐ 0
emptyGen = λ ()
initialAlgFP : FinitePresentation R
initialAlgFP = record { n = 0 ; m = 0 ; relations = emptyGen }
R[⊥]/⟨0⟩ : CommAlgebra R ℓ
R[⊥]/⟨0⟩ = fpAlg initialAlgFP
R[⊥]/⟨0⟩IsInitial : (B : CommAlgebra R ℓ)
→ isContr (CommAlgebraHom R[⊥]/⟨0⟩ B)
R[⊥]/⟨0⟩IsInitial B = indHom , uniqueness
where
indHom : CommAlgebraHom R[⊥]/⟨0⟩ B
indHom = FP.inducedHom R initialAlgFP B (emptyFinVec ⟨ B ⟩ₐ) (λ ())
uniqueness : (f : CommAlgebraHom R[⊥]/⟨0⟩ B) →
indHom ≡ f
uniqueness f = FP.inducedHomUnique R initialAlgFP B (emptyFinVec ⟨ B ⟩ₐ) (λ ()) f (λ ())
initialCAlgIsFP : isFP R (initialCAlg R)
initialCAlgIsFP = ∣ (initialAlgFP , equivByInitiality R R[⊥]/⟨0⟩ R[⊥]/⟨0⟩IsInitial) ∣₁
{- The terminal R-algebra is finitely presented -}
private
unitGen : FinVec ⟨ R[⊥] ⟩ₐ 1
unitGen zero = 1r
where open InstancesForCAlg R[⊥]
terminalCAlgFP : FinitePresentation R
terminalCAlgFP = record { n = 0 ; m = 1 ; relations = unitGen }
R[⊥]/⟨1⟩ : CommAlgebra R ℓ
R[⊥]/⟨1⟩ = fpAlg terminalCAlgFP
opaque
unfolding fpAlg fgIdeal
terminalCAlgIsFP : isFP R (terminalCAlg R)
terminalCAlgIsFP = ∣ (terminalCAlgFP ,
(equivFrom1≡0 R R[⊥]/⟨1⟩
(1r ≡⟨ sym pres1 ⟩
(π terminalCAlgFP) $ca 1r ≡⟨ isZeroFromIdeal 1r (incInIdeal (Polynomials R 0) unitGen zero) ⟩
0r ∎))) ∣₁
where open InstancesForCAlg (fpAlg terminalCAlgFP)
open InstancesForCAlg (Polynomials R 0)
open IsCommAlgebraHom (π terminalCAlgFP .snd)
{-
{-
Quotients of the base ring by finitely generated ideals are finitely presented.
-}
module _ {m : ℕ} (xs : FinVec ⟨ R ⟩ m) where
⟨xs⟩ : IdealsIn (initialCAlg R)
⟨xs⟩ = generatedIdeal (initialCAlg R) xs
R/⟨xs⟩ = (initialCAlg R) / ⟨xs⟩
open CommAlgebraStr ⦃...⦄
private
rels : FinVec ⟨ Polynomials {R = R} 0 ⟩ m
rels = Construction.const ∘ xs
B = FPAlgebra 0 rels
π = quotientHom (initialCAlg R) ⟨xs⟩
instance
_ = snd R/⟨xs⟩
_ = snd (initialCAlg R)
_ = snd B
πxs≡0 : (i : Fin m) → π $a xs i ≡ 0a
πxs≡0 i = isZeroFromIdeal {A = initialCAlg R} {I = ⟨xs⟩} (xs i)
(incInIdeal (initialCAlg R) xs i)
R/⟨xs⟩FP : FinitePresentation R/⟨xs⟩
n R/⟨xs⟩FP = 0
FinitePresentation.m R/⟨xs⟩FP = m
relations R/⟨xs⟩FP = rels
equiv R/⟨xs⟩FP = (isoToEquiv (iso (fst toA) (fst fromA)
(λ a i → toFrom i $a a)
λ a i → fromTo i $a a))
, (snd toA)
where
toA : CommAlgebraHom B R/⟨xs⟩
toA = inducedHom 0 rels R/⟨xs⟩ (λ ()) relation-holds
where
vals : FinVec ⟨ R/⟨xs⟩ ⟩ 0
vals ()
vals' : FinVec ⟨ initialCAlg R ⟩ 0
vals' ()
relation-holds = λ i →
evPoly R/⟨xs⟩ (rels i) vals ≡⟨ sym
(evPolyHomomorphic
(initialCAlg R)
R/⟨xs⟩
π
(rels i)
vals') ⟩
π $a (evPoly (initialCAlg R)
(rels i)
vals') ≡⟨ cong (π $a_) (·IdR (xs i)) ⟩
π $a xs i ≡⟨ πxs≡0 i ⟩
0a ∎
{-
R ─→ R/⟨xs⟩
id↓ ↓ ∃!
R ─→ R[⊥]/⟨rels⟩
-}
fromA : CommAlgebraHom R/⟨xs⟩ B
fromA =
quotientInducedHom
(initialCAlg R)
⟨xs⟩
B
(initialMap R B)
(inclOfFGIdeal
(CommAlgebra→CommRing (initialCAlg R))
xs
(kernel (initialCAlg R) B (initialMap R B))
(relationsHold 0 rels))
open AlgebraHoms
fromTo : fromA ∘a toA ≡ idCAlgHom B
fromTo = cong fst
(isContr→isProp (universal 0 rels B (λ ()) (relationsHold 0 rels))
(fromA ∘a toA , (λ ()))
(idCAlgHom B , (λ ())))
toFrom : toA ∘a fromA ≡ idCAlgHom R/⟨xs⟩
toFrom = injectivePrecomp (initialCAlg R) ⟨xs⟩ R/⟨xs⟩ (toA ∘a fromA) (idCAlgHom R/⟨xs⟩)
(isContr→isProp (initialityContr R R/⟨xs⟩) _ _)
module _ {m : ℕ} (x : ⟨ R ⟩) where
R/⟨x⟩FP : FinitePresentation (initialCAlg R / generatedIdeal (initialCAlg R) (replicateFinVec 1 x))
R/⟨x⟩FP = R/⟨xs⟩FP (replicateFinVec 1 x)
-- -}