Presentations of algebras

A presentation of an R-algebra S is a distinguished family of generators and relations.

Main definition

• Algebra.Presentation: A presentation of an R-algebra S is a family of generators with
  1. rels: The type of relations.
  2. relation : relations → MvPolynomial vars R: The assignment of each relation to a polynomial in the generators.
• Algebra.Presentation.IsFinite: A presentation is called finite if both variables and relations are finite.
• Algebra.Presentation.dimension: The dimension of a presentation is the number of generators minus the number of relations.

We also give constructors for localization, base change and composition.

TODO

• Define Homs of presentations.

Notes

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

structure Algebra.Presentation (R : Type u) (S : Type v) (ι : Type w) (σ : Type t) [CommRing R] [CommRing S] [Algebra R S] extends Algebra.Generators R S ι : Type (max (max (max t u) v) w)

A presentation of an R-algebra S is a family of generators with σ → MvPolynomial ι R: The assignment of each relation to a polynomial in the generators.

• val : ι → S
• σ' : S → MvPolynomial ι R
• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s
• algebra : Algebra (MvPolynomial ι R) S
• algebraMap_eq : algebraMap (MvPolynomial ι R) S = ↑(MvPolynomial.aeval self.val)
• relation : σ → self.Ring

  The assignment of each relation to a polynomial in the generators.

• span_range_relation_eq_ker : Ideal.span (Set.range self.relation) = self.ker

  The relations span the kernel of the canonical map.

@[simp]

theorem Algebra.Presentation.aeval_val_relation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (i : σ) : (MvPolynomial.aeval P.val) (P.relation i) = 0

theorem Algebra.Presentation.relation_mem_ker {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (i : σ) : P.relation i ∈ P.ker

@[reducible, inline]

abbrev Algebra.Presentation.Quotient {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : Type (max w u)

The polynomial algebra w.r.t. a family of generators modulo a family of relations.

def Algebra.Presentation.quotientEquiv {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : P.Quotient ≃ₐ[P.Ring] S

P.Quotient is P.Ring-isomorphic to S and in particular R-isomorphic to S.

@[simp]

theorem Algebra.Presentation.quotientEquiv_mk {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (p : P.Ring) : P.quotientEquiv ((Ideal.Quotient.mk P.ker) p) = (algebraMap P.Ring S) p

@[simp]

theorem Algebra.Presentation.quotientEquiv_symm {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) (x : S) : P.quotientEquiv.symm x = (Ideal.Quotient.mk P.ker) (P.σ x)

noncomputable def Algebra.Presentation.dimension {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) : ℕ

Dimension of a presentation defined as the cardinality of the generators minus the cardinality of the relations.

Note: this definition is completely non-sensical for non-finite presentations and even then for this to make sense, you should assume that the presentation is a complete intersection.

theorem Algebra.Presentation.fg_ker {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) [Finite σ] : P.ker.FG

instance Algebra.Presentation.instFinitePresentationQuotientOfFinite {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) [Finite σ] [Finite ι] : FinitePresentation R P.Quotient

If a presentation is finite, the corresponding quotient is of finite presentation.

theorem Algebra.Presentation.finitePresentation_of_isFinite {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] [Finite ι] (P : Presentation R S ι σ) : FinitePresentation R S

theorem Algebra.Presentation.exists_presentation_fin (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : ∃ (n : ℕ) (m : ℕ), Nonempty (Presentation R S (Fin n) (Fin m))

noncomputable def Algebra.Presentation.ofFinitePresentationVars (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : ℕ

The index of generators to ofFinitePresentation.

noncomputable def Algebra.Presentation.ofFinitePresentationRels (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : ℕ

The index of relations to ofFinitePresentation.

noncomputable def Algebra.Presentation.ofFinitePresentation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : Presentation R S (Fin (ofFinitePresentationVars R S)) (Fin (ofFinitePresentationRels R S))

An arbitrary choice of a finite presentation of a finitely presented algebra.

def Algebra.Presentation.ofAlgEquiv {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) : Presentation R T ι σ

Transport a presentation along an algebra isomorphism.

@[simp]

theorem Algebra.Presentation.ofAlgEquiv_relation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) (i : σ) : (P.ofAlgEquiv e).relation i = P.relation i

@[simp]

theorem Algebra.Presentation.ofAlgEquiv_toGenerators {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) : (P.ofAlgEquiv e).toGenerators = P.ofAlgEquiv e

@[simp]

theorem Algebra.Presentation.dimension_ofAlgEquiv {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {T : Type u_1} [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) : (P.ofAlgEquiv e).dimension = P.dimension

noncomputable def Algebra.Presentation.ofBijectiveAlgebraMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : Presentation R S PEmpty.{w + 1} PEmpty.{t + 1}

If algebraMap R S is bijective, the empty generators are a presentation with no relations.

theorem Algebra.Presentation.ofBijectiveAlgebraMap_dimension {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : (ofBijectiveAlgebraMap h).dimension = 0

noncomputable def Algebra.Presentation.id (R : Type u) [CommRing R] : Presentation R R PEmpty.{w + 1} PEmpty.{t + 1}

The canonical R-presentation of R with no generators and no relations.

theorem Algebra.Presentation.id_dimension {R : Type u} [CommRing R] : (id R).dimension = 0

theorem Algebra.Generators.ker_localizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (localizationAway S r).ker = Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1}

noncomputable def Algebra.Presentation.localizationAway {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Presentation R S Unit Unit

If S is the localization of R away from r, we can construct a natural presentation of S as R-algebra with a single generator X and the relation r * X - 1 = 0.

@[simp]

theorem Algebra.Presentation.localizationAway_relation {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x✝ : Unit) : (localizationAway S r).relation x✝ = MvPolynomial.C r * MvPolynomial.X () - 1

@[simp]

theorem Algebra.Presentation.localizationAway_dimension_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (localizationAway S r).dimension = 0

theorem Algebra.Generators.C_mul_X_sub_one_mem_ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : MvPolynomial.C r * MvPolynomial.X () - 1 ∈ (localizationAway S r).ker

noncomputable def Algebra.Presentation.baseChange {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Presentation R S ι σ) : Presentation T (TensorProduct R T S) ι σ

If P is a presentation of S over R and T is an R-algebra, we obtain a natural presentation of T ⊗[R] S over T.

@[simp]

theorem Algebra.Presentation.baseChange_relation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Presentation R S ι σ) (i : σ) : (baseChange T P).relation i = (MvPolynomial.map (algebraMap R T)) (P.relation i)

theorem Algebra.Presentation.baseChange_toGenerators {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Presentation R S ι σ) : (baseChange T P).toGenerators = Generators.baseChange T P.toGenerators

Composition of presentations

Let S be an R-algebra with presentation P and T be an S-algebra with presentation Q. In this section we construct a presentation of T as an R-algebra.

For the underlying generators see Algebra.Generators.comp. The family of relations is indexed by σ' ⊕ σ.

We have two canonical maps: MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R induced by Sum.inr and aux : MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' S induced by the evaluation MvPolynomial ι R →ₐ[R] S (see below).

Now i : σ is mapped to the image of P.relation i under the first map and j : σ' is mapped to a pre-image under aux of Q.relation j (see comp_relation_aux for the construction of the pre-image and comp_relation_aux_map for a proof that it is indeed a pre-image).

The evaluation map factors as: MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' S →ₐ[R] T, where the first map is aux. The goal is to compute that the kernel of this composition is spanned by the relations indexed by σ' ⊕ σ (span_range_relation_eq_ker_comp). One easily sees that this kernel is the pre-image under aux of the kernel of the evaluation of Q, where the latter is by assumption spanned by the relations Q.relation j.

Since aux is surjective (aux_surjective), the pre-image is the sum of the ideal spanned by the constructed pre-images of the Q.relation j and the kernel of aux. It hence remains to show that the kernel of aux is spanned by the image of the P.relation i under the canonical map MvPolynomial ι R →ₐ[R] MvPolynomial (ι' ⊕ ι) R. By assumption this span is the kernel of the evaluation map of P. For this, we use the isomorphism MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' (MvPolynomial ι R) and MvPolynomial.ker_map.

noncomputable def Algebra.Presentation.compRelationAux {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) (r : σ') : MvPolynomial (ι' ⊕ ι) R

A choice of pre-image of Q.relation r under the canonical map MvPolynomial (ι' ⊕ ι) R →ₐ[R] MvPolynomial ι' S given by the evaluation of P.

noncomputable def Algebra.Presentation.comp {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) [Algebra R T] [IsScalarTower R S T] : Presentation R T (ι' ⊕ ι) (σ' ⊕ σ)

Given presentations of T over S and of S over R, we may construct a presentation of T over R.

theorem Algebra.Presentation.comp_relation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) [Algebra R T] [IsScalarTower R S T] (a✝ : σ' ⊕ σ) : (Q.comp P).relation a✝ = Sum.elim (Q.compRelationAux P) (fun (rp : σ) => (MvPolynomial.rename Sum.inr) (P.relation rp)) a✝

theorem Algebra.Presentation.toGenerators_comp {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) [Algebra R T] [IsScalarTower R S T] : (Q.comp P).toGenerators = Q.comp P.toGenerators

@[simp]

theorem Algebra.Presentation.comp_relation_inr {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) [Algebra R T] [IsScalarTower R S T] (r : σ) : (Q.comp P).relation (Sum.inr r) = (MvPolynomial.rename Sum.inr) (P.relation r)

theorem Algebra.Presentation.comp_aeval_relation_inl {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [CommRing T] [Algebra S T] (Q : Presentation S T ι' σ') (P : Presentation R S ι σ) [Algebra R T] [IsScalarTower R S T] (r : σ') : (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val))) ((Q.comp P).relation (Sum.inl r)) = Q.relation r

theorem Algebra.Presentation.relation_comp_localizationAway_inl {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_3} [CommRing T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Presentation R S ι σ) (h1 : P.σ (-1) = -1) (h0 : P.σ 0 = 0) (r : Unit) : ((localizationAway T g).comp P).relation (Sum.inl r) = (MvPolynomial.rename Sum.inr) (P.σ g) * MvPolynomial.X (Sum.inl ()) - 1

The composition of a presentation P with a localization away from an element has the form R[Xᵢ, Y]/(fⱼ, (P.σ g) Y - 1), if the chosen section of P preserves -1 and 0. Note: If S is non-trivial, we can ensure this by only modifying P.σ.

noncomputable def Algebra.Presentation.reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) : Presentation R S ι' σ'

Given a presentation P and equivalences ι' ≃ ι and σ' ≃ σ, this is the induced presentation with variables indexed by ι' and relations indexed by σ'

@[simp]

theorem Algebra.Presentation.reindex_toGenerators {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) : (P.reindex e f).toGenerators = P.reindex e

@[simp]

theorem Algebra.Presentation.dimension_reindex {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ) : (P.reindex e f).dimension = P.dimension

noncomputable def Algebra.Presentation.naive {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) : Presentation R (MvPolynomial σ R ⧸ Ideal.span (Set.range v)) σ ι

The naive presentation of a quotient R[Xᵢ] ⧸ (vⱼ). If the definitional equality of the section matters, it can be explicitly provided.

@[simp]

theorem Algebra.Presentation.naive_toGenerators {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) : (naive s hs).toGenerators = Generators.naive s hs

theorem Algebra.Presentation.naive_relation {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) : (naive s hs).relation = v

@[simp]

theorem Algebra.Presentation.naive_relation_apply {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) (i : ι) : (naive s hs).relation i = v i

theorem Algebra.Presentation.mem_ker_naive {R : Type u} {ι : Type w} {σ : Type t} [CommRing R] {v : ι → MvPolynomial σ R} (s : MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R := Function.surjInv ⋯) (hs : ∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x := by apply Function.surjInv_eq) (i : ι) : v i ∈ (naive s hs).ker

theorem Algebra.Generators.fg_ker_of_finitePresentation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] {α : Type u_1} (P : Generators R S α) [Finite α] : P.ker.FG