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 and base change.

TODO

• Define composition of presentations.
• 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 : 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
• 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.

theorem Algebra.Presentation.span_range_relation_eq_ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (self : Algebra.Presentation R S) : 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 : Algebra.Presentation R S) (i : P.rels) : (MvPolynomial.aeval P.val) (P.relation i) = 0

@[reducible, inline]

abbrev Algebra.Presentation.Quotient {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.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 : Algebra.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 : Algebra.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 : Algebra.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 : Algebra.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 : Algebra.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.IsFinite.finite_vars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Presentation R S} [self : P.IsFinite] : Finite P.vars

theorem Algebra.Presentation.IsFinite.finite_rels {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Presentation R S} [self : P.IsFinite] : Finite P.rels

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

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

Equations

• ⋯ = ⋯

theorem Algebra.Presentation.finitePresentation_of_isFinite {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Presentation R S) [P.IsFinite] : Algebra.FinitePresentation R S

@[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), (Algebra.Presentation.localizationAway 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] : (Algebra.Presentation.localizationAway r).rels = Unit

noncomputable def Algebra.Presentation.localizationAway {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Algebra.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.

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

Equations

• ⋯ = ⋯

@[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] : (Algebra.Presentation.localizationAway r).dimension = 0

@[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 : Algebra.Presentation R S) (i : P.rels) : P.baseChange.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 : Algebra.Presentation R S) : P.baseChange.rels = P.rels

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 : Algebra.Presentation R S) : Algebra.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.