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) [CommRing R] [CommRing S] [Algebra R S] extends Algebra.Generators R S : Type (max (max (max (t + 1) u) v) (w + 1))

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.

• vars : Type w
• val : self.vars → S
• σ' : S → MvPolynomial self.vars R
• aeval_val_σ' (s : S) : (MvPolynomial.aeval self.val) (self.σ' s) = s
• algebra : Algebra (MvPolynomial self.vars R) S
• algebraMap_eq : algebraMap (MvPolynomial self.vars R) S = ↑(MvPolynomial.aeval self.val)
• rels : Type t

  The type of relations.

• relation : self.rels → 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} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) (i : P.rels) : (MvPolynomial.aeval P.val) (P.relation i) = 0

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

@[reducible, inline]

abbrev Algebra.Presentation.Quotient {R : Type u} {S : Type v} [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} [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} [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} [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} [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 P.vars - Nat.card P.rels

class Algebra.Presentation.IsFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) : Prop

A presentation is finite if there are only finitely-many relations and finitely-many relations.

• finite_vars : Finite P.vars
• finite_rels : Finite P.rels

theorem Algebra.Presentation.ideal_fg_of_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) [P.IsFinite] : P.ker.FG

instance Algebra.Presentation.instFinitePresentationQuotientOfIsFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) [P.IsFinite] : 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} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) [P.IsFinite] : FinitePresentation R S

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

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

Equations

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

instance Algebra.Presentation.instIsFiniteOfFinitePresentation {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : (ofFinitePresentation R S).IsFinite

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

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

Equations

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

instance Algebra.Presentation.ofBijectiveAlgebraMap_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (h : Function.Bijective ⇑(algebraMap R S)) : (ofBijectiveAlgebraMap h).IsFinite

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

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

Equations

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

instance Algebra.Presentation.instIsFiniteId {R : Type u} [CommRing R] : (id R).IsFinite

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

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

theorem Algebra.Presentation.localizationAway_rels {R : Type u} (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (localizationAway S r).rels = Unit

instance Algebra.Presentation.localizationAway_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (localizationAway S r).IsFinite

instance Algebra.Presentation.instFintypeRelsLocalizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Fintype (localizationAway S r).rels

Equations

• Algebra.Presentation.instFintypeRelsLocalizationAway r = inferInstanceAs (Fintype Unit)

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

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

@[simp]

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

theorem Algebra.Presentation.baseChange_rels {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_1) [CommRing T] [Algebra R T] (P : Presentation R S) : (baseChange T P).rels = P.rels

theorem Algebra.Presentation.baseChange_toGenerators {R : Type u} {S : Type v} [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

instance Algebra.Presentation.baseChange_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (T : Type u_3) [CommRing T] [Algebra R T] (P : Presentation R S) [P.IsFinite] : (baseChange T P).IsFinite

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 Q.rels ⊕ P.rels.

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

Now i : P.rels is mapped to the image of P.relation i under the first map and j : Q.rels 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 (Q.vars ⊕ P.vars) R →ₐ[R] MvPolynomial Q.vars 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 Q.rels ⊕ P.rels (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 P.vars R →ₐ[R] MvPolynomial (Q.vars ⊕ P.vars) R. By assumption this span is the kernel of the evaluation map of P. For this, we use the isomorphism MvPolynomial (Q.vars ⊕ P.vars) R ≃ₐ[R] MvPolynomial Q.vars (MvPolynomial P.vars R) and MvPolynomial.ker_map.

noncomputable def Algebra.Presentation.comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [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.

@[simp]

theorem Algebra.Presentation.comp_rels {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra S T] (Q : Presentation S T) (P : Presentation R S) [Algebra R T] [IsScalarTower R S T] : (Q.comp P).rels = (Q.rels ⊕ P.rels)

theorem Algebra.Presentation.comp_relation {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra S T] (Q : Presentation S T) (P : Presentation R S) [Algebra R T] [IsScalarTower R S T] (a✝ : Q.rels ⊕ P.rels) : (Q.comp P).relation a✝ = Sum.elim (Algebra.Presentation.comp_relation_aux✝ Q P) (fun (rp : P.rels) => (MvPolynomial.rename Sum.inr) (P.relation rp)) a✝

theorem Algebra.Presentation.toGenerators_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [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} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_4} [CommRing T] [Algebra S T] (Q : Presentation S T) (P : Presentation R S) [Algebra R T] [IsScalarTower R S T] (r : P.rels) : (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} [CommRing R] [CommRing S] [Algebra R S] {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.rels) : (MvPolynomial.aeval (Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val))) ((Q.comp P).relation (Sum.inl r)) = Q.relation r

instance Algebra.Presentation.comp_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_5} [CommRing T] [Algebra S T] (Q : Presentation S T) (P : Presentation R S) [Algebra R T] [IsScalarTower R S T] [P.IsFinite] [Q.IsFinite] : (Q.comp P).IsFinite

noncomputable def Algebra.Presentation.reindex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) : Presentation R S

Given a presentation P and equivalences ι ≃ P.vars and κ ≃ P.rels, this is the induced presentation with variables indexed by ι and relations indexed by `κ

Equations

• P.reindex e f = { toGenerators := P.reindex e, rels := κ, 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} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) : (P.reindex e f).toGenerators = P.reindex e

theorem Algebra.Presentation.reindex_relation {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) (a✝ : κ) : (P.reindex e f).relation a✝ = (⇑(MvPolynomial.rename ⇑e.symm) ∘ P.relation ∘ ⇑f) a✝

theorem Algebra.Presentation.reindex_rels {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) : (P.reindex e f).rels = κ

@[simp]

theorem Algebra.Presentation.isFinite_reindex_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) : (P.reindex e f).IsFinite ↔ P.IsFinite

theorem Algebra.Presentation.IsFinite.reindex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Presentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) : P.IsFinite → (P.reindex e f).IsFinite

Alias of the reverse direction of Algebra.Presentation.isFinite_reindex_iff.

@[simp]

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