Regular functions on algebraic sets

9 fully proved

Fraction Ring

DefinitionRegularity of a fraction at an evaluation#✓fully proved

Let \(A\) and \(K\) be commutative rings and \(\mathrm{ev} : A \to K\) a ring homomorphism. An element \(r\) of the total ring of fractions of \(A\) (its localization at the non-zero-divisors) is regular at \(\mathrm{ev}\) when there is some \(g \in A\) with \(\mathrm{ev}(g) \neq 0\) such that \(g r\) lies in the image of \(A\) in its total ring of fractions.

def IsRegularAt (ev : A →+* K) (r : FractionRing A) : Prop :=
  ∃ g : A, ev g ≠ 0 ∧
    algebraMap A (FractionRing A) g * r ∈
      Set.range (algebraMap A (FractionRing A))

Used by 4

Used byRegularity of a rational function at a point · Elements of the base ring are regular · One is regular · Zero is regular

TheoremElements of the base ring are regular#✓fully proved

Let \(A\) be a commutative ring and \(K\) a nontrivial commutative ring. For every ring homomorphism \(\mathrm{ev} : A \to K\) and every \(a \in A\), the image of \(a\) in the total ring of fractions of \(A\) is regular at \(\mathrm{ev}\).

theorem isRegularAt_algebraMap (ev : A →+* K) (a : A) :
    IsRegularAt ev (algebraMap A (FractionRing A) a)

Uses 1 · Used by 3

Statement usesRegularity of a fraction at an evaluation

Used byElements of the coordinate ring are regular · One is regular · Zero is regular

TheoremZero is regular#✓fully proved

Let \(A\) be a commutative ring and \(K\) a nontrivial commutative ring. For every ring homomorphism \(\mathrm{ev} : A \to K\), the element \(0\) of the total ring of fractions of \(A\) is regular at \(\mathrm{ev}\).

theorem isRegularAt_zero (ev : A →+* K) : IsRegularAt ev 0

Uses 2

Statement usesRegularity of a fraction at an evaluation

Proof usesElements of the base ring are regular

TheoremOne is regular#✓fully proved

Let \(A\) be a commutative ring and \(K\) a nontrivial commutative ring. For every ring homomorphism \(\mathrm{ev} : A \to K\), the element \(1\) of the total ring of fractions of \(A\) is regular at \(\mathrm{ev}\).

theorem isRegularAt_one (ev : A →+* K) : IsRegularAt ev 1

Uses 2

Statement usesRegularity of a fraction at an evaluation

Proof usesElements of the base ring are regular

Mv Polynomial

AbbreviationAffine coordinate ring#✓fully proved

Let \(K\) be a field, \(\sigma\) an index set and \(X \subseteq K^\sigma\) a set of points. The affine coordinate ring of \(X\) is the quotient \(K[x_i : i \in \sigma] / I(X)\) of the polynomial ring over \(K\) in variables indexed by \(\sigma\) by the vanishing ideal \(I(X)\), the ideal of all polynomials that vanish at every point of \(X\).

abbrev AffineCoordinateRing (X : Set (σ → K)) :=
  MvPolynomial σ K ⧸ vanishingIdeal K X

Used by 4

Used byEvaluation at a point of an affine set · Evaluating a residue class · Regularity of a rational function at a point · Elements of the coordinate ring are regular

Affine Coordinate Ring

DefinitionEvaluation at a point of an affine set#✓fully proved

Let \(K\) be a field, \(\sigma\) an index set and \(X \subseteq K^\sigma\) a set of points. For a point \(P \in X\), evaluation at \(P\) is the ring homomorphism from the affine coordinate ring of \(X\) to \(K\) that sends the residue class of a polynomial \(f\) to \(f(P)\); it is well defined because every polynomial in the vanishing ideal of \(X\) vanishes at \(P\).

noncomputable def evalAt (X : Set (σ → K)) (P : X) : AffineCoordinateRing X →+* K :=
  Ideal.Quotient.lift _ (MvPolynomial.aeval (R := K) P.1)
    (fun _ hp ↦ (MvPolynomial.mem_vanishingIdeal_iff.mp hp) P.1 P.2)

Uses 1 · Used by 3

Statement usesAffine coordinate ring

Used byEvaluating a residue class · Regularity of a rational function at a point · Elements of the coordinate ring are regular

TheoremEvaluating a residue class#✓fully proved

Let \(K\) be a field, \(\sigma\) an index set, \(X \subseteq K^\sigma\) a set of points and \(P \in X\). For every polynomial \(f\) over \(K\) in variables indexed by \(\sigma\), evaluating the residue class of \(f\) in the affine coordinate ring of \(X\) at \(P\) gives \(f(P)\).

@[simp]
theorem evalAt_mk (X : Set (σ → K)) (P : X) (f : MvPolynomial σ K) :
    evalAt X P (Ideal.Quotient.mk _ f) = MvPolynomial.aeval P.1 f

Uses 2

Statement usesAffine coordinate ring · Evaluation at a point of an affine set

DefinitionRegularity of a rational function at a point#✓fully proved

Let \(K\) be a field, \(\sigma\) an index set and \(X \subseteq K^\sigma\) a set of points whose affine coordinate ring \(A\) is an integral domain. A rational function on \(X\) is an element \(r\) of the field of fractions of \(A\); it is regular at a point \(P \in X\) when there is some \(g \in A\) whose value \(g(P)\) under evaluation at \(P\) is nonzero such that \(g r\) lies in the image of \(A\) in its field of fractions.

def IsRegularAt (X : Set (σ → K)) [IsDomain (AffineCoordinateRing X)]
    (r : FractionRing (AffineCoordinateRing X)) (P : X) : Prop :=
  FractionRing.IsRegularAt (evalAt X P) r

Uses 3 · Used by 1

Statement usesRegularity of a fraction at an evaluation · Affine coordinate ring · Evaluation at a point of an affine set

Used byElements of the coordinate ring are regular

TheoremElements of the coordinate ring are regular#✓fully proved

Let \(K\) be a field, \(\sigma\) an index set and \(X \subseteq K^\sigma\) a set of points whose affine coordinate ring \(A\) is an integral domain. For every \(a \in A\) and every point \(P \in X\), the image of \(a\) in the field of fractions of \(A\) is a rational function on \(X\) that is regular at \(P\).

theorem isRegularAt_algebraMap (X : Set (σ → K)) [IsDomain (AffineCoordinateRing X)]
    (a : AffineCoordinateRing X) (P : X) :
    IsRegularAt X (algebraMap (AffineCoordinateRing X)
      (FractionRing (AffineCoordinateRing X)) a) P

Uses 4

Statement usesAffine coordinate ring · Regularity of a rational function at a point

Proof usesElements of the base ring are regular · Evaluation at a point of an affine set

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.