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 wrt a family of generators modulo a family of relations.

Equations

• P.Quotient = (P.Ring ⧸ P.ker)

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.

Equations

• P.quotientEquiv = Ideal.quotientKerAlgEquivOfRightInverse ⋯

@[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.

Equations

• P.dimension = Nat.card ι - Nat.card σ

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

@[deprecated Algebra.Presentation.fg_ker (since := "2025-05-27")]

theorem Algebra.Presentation.ideal_fg_of_isFinite {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

Alias of Algebra.Presentation.fg_ker.

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.

Equations

• Algebra.Presentation.ofFinitePresentationVars R S = ⋯.choose

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.

Equations

• Algebra.Presentation.ofFinitePresentationRels R S = ⋯.choose

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.

Equations

• Algebra.Presentation.ofFinitePresentation R S = ⋯.some

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.

Equations

• Algebra.Presentation.ofBijectiveAlgebraMap h = { toGenerators := Algebra.Generators.ofSurjectiveAlgebraMap ⋯, relation := PEmpty.elim, span_range_relation_eq_ker := ⋯ }

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.

Equations

• Algebra.Presentation.id R = Algebra.Presentation.ofBijectiveAlgebraMap ⋯

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 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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• Algebra.Presentation.baseChange T P = { toGenerators := P.baseChange, relation := fun (i : σ) => (MvPolynomial.map (algebraMap R T)) (P.relation i), span_range_relation_eq_ker := ⋯ }

@[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 = P.baseChange

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.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.

Equations

• One or more equations did not get rendered due to their size.

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 (Algebra.Presentation.comp_relation_aux✝ Q 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

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 `κ

Equations

• P.reindex e f = { toGenerators := P.reindex e, relation := ⇑(MvPolynomial.rename ⇑e.symm) ∘ P.relation ∘ ⇑f, span_range_relation_eq_ker := ⋯ }

@[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