@[reducible, inline]

abbrev HomogeneousPolynomial.IsHomogeneousOfDegree {σ : Type u_1} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (d : ℕ) : Prop

A multivariate polynomial $f$ is homogeneous of degree $d$ if every monomial in $f$ has total degree $d$. Abbreviation for Mathlib's MvPolynomial.IsHomogeneous.

def HomogeneousPolynomial.IsHomogeneous {σ : Type u_1} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : Prop

A polynomial $f$ is homogeneous if it is homogeneous of some degree $d \in \mathbb{N}$.

theorem HomogeneousPolynomial.isHomogeneous_eval_smul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (d : ℕ) (hf : f.IsHomogeneous d) (c : R) (x : σ → R) : (MvPolynomial.eval fun (i : σ) => c * x i) f = c ^ d * (MvPolynomial.eval x) f

Homogeneity under scaling: if $f$ is homogeneous of degree $d$, then $f(c x_1, \ldots, c x_n) = c^d \cdot f(x_1, \ldots, x_n)$ for every scalar $c$.

theorem HomogeneousPolynomial.isHomogeneous_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (d : ℕ) : IsHomogeneous 0

The zero polynomial is homogeneous (of every degree, witnessed here by any chosen $d$).

theorem HomogeneousPolynomial.isHomogeneous_C {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : R) : IsHomogeneous (MvPolynomial.C r)

A constant polynomial $C(r)$ is homogeneous of degree $0$.

theorem HomogeneousPolynomial.isHomogeneous_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) : IsHomogeneous (MvPolynomial.X i)

Each variable $X_i$ is homogeneous of degree $1$.

theorem HomogeneousPolynomial.sum_homogeneousComponent {σ : Type u_1} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) : ∑ i ∈ Finset.range (f.totalDegree + 1), (MvPolynomial.homogeneousComponent i) f = f

Decomposition into homogeneous components: every polynomial $f$ is the sum of its homogeneous components $f = \sum_{i \le \deg f} f_i$.

@[reducible, inline]

abbrev HomogeneousIdealDef.IsHomogeneousIdeal (σ : Type u_1) (R : Type u_2) [CommSemiring R] (I : Ideal (MvPolynomial σ R)) : Prop

An ideal $I \subseteq R[X_1, \ldots, X_n]$ is homogeneous if every $f \in I$ has all of its homogeneous components in $I$.

def AffinePatch.Projectivization.coordNeZero {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : Projectivization k (Fin (n + 1) → k) → Prop

Well-defined predicate on a projective point $p \in \mathbb{P}^n(k)$: "the $i$-th coordinate of any representative of $p$ is nonzero".

def AffinePatch.affinePatch {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : Set (Projectivization k (Fin (n + 1) → k))

The standard affine patch $U_i = \{[x_0 : \cdots : x_n] \in \mathbb{P}^n(k) \mid x_i \neq 0\}$.

@[simp]

theorem AffinePatch.mem_affinePatch_mk {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) (v : Fin (n + 1) → k) (hv : v ≠ 0) : Projectivization.mk k v hv ∈ affinePatch k i ↔ v i ≠ 0

Membership criterion in the patch $U_i$ in terms of an explicit representative $v \neq 0$.

theorem AffinePatch.mem_affinePatch_iff_rep {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) (p : Projectivization k (Fin (n + 1) → k)) : p ∈ affinePatch k i ↔ p.rep i ≠ 0

A projective point $p$ lies in $U_i$ iff its canonical representative p.rep has nonzero $i$-th coordinate.

theorem AffinePatch.insertNth_one_ne_zero {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) (a : Fin n → k) : i.insertNth 1 a ≠ 0

Inserting a $1$ at index $i$ produces a nonzero tuple.

noncomputable def AffinePatch.affinePatchEquiv {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : ↑(affinePatch k i) ≃ (Fin n → k)

The canonical bijection $U_i \simeq \mathbb{A}^n(k)$ sending the projective point $[x_0 : \cdots : x_n]$ with $x_i \neq 0$ to the affine point $(x_0 / x_i, \ldots, \widehat{x_i / x_i}, \ldots, x_n / x_i)$.

noncomputable def ProjectiveClosure.homogenize {n : ℕ} {R : Type u_1} [CommSemiring R] (f : MvPolynomial (Fin n) R) : MvPolynomial (Fin (n + 1)) R

Homogenization with respect to a new variable $X_0$: given $f \in R[X_1, \ldots, X_n]$ of degree $d$, produce the homogeneous polynomial $X_0^d f(X_1 / X_0, \ldots, X_n / X_0) \in R[X_0, X_1, \ldots, X_n]$.

theorem ProjectiveClosure.homogenize_def {n : ℕ} {R : Type u_1} [CommSemiring R] (f : MvPolynomial (Fin n) R) : homogenize f = ∑ m ∈ f.support, (MvPolynomial.monomial (Finsupp.mapDomain Fin.succ m + Finsupp.single 0 (f.totalDegree - m.sum fun (x : Fin n) (e : ℕ) => e))) (MvPolynomial.coeff m f)

Unfolding lemma exposing the definition of homogenize as a sum over the support of $f$.

def ProjectiveClosure.homogenizeSet {n : ℕ} {R : Type u_1} [CommSemiring R] (I : Ideal (MvPolynomial (Fin n) R)) : Set (MvPolynomial (Fin (n + 1)) R)

Image of an ideal $I$ under homogenization, as a set of homogeneous polynomials in $R[X_0, \ldots, X_n]$.

noncomputable def ProjectiveClosure.homogenizeIdeal {n : ℕ} {R : Type u_1} [CommSemiring R] (I : Ideal (MvPolynomial (Fin n) R)) : Ideal (MvPolynomial (Fin (n + 1)) R)

Homogenization of the ideal $I$: the ideal of $R[X_0, \ldots, X_n]$ generated by all homogenizations of elements of $I$.

theorem ProjectiveClosure.homogenize_mem_homogenizeIdeal {n : ℕ} {R : Type u_1} [CommSemiring R] {I : Ideal (MvPolynomial (Fin n) R)} {f : MvPolynomial (Fin n) R} (hf : f ∈ I) : homogenize f ∈ homogenizeIdeal I

The homogenization of any element $f \in I$ belongs to the homogenized ideal homogenizeIdeal I.

def ProjectiveClosure.projectiveVanishes {n : ℕ} (k : Type u_2) [Field k] (f : MvPolynomial (Fin (n + 1)) k) (p : Projectivization k (Fin (n + 1) → k)) : Prop

$f$ vanishes at the projective point $p$ if $f(p_{\mathrm{rep}}) = 0$ on (any) representative.

def ProjectiveClosure.projectiveZeroLocus {n : ℕ} (k : Type u_2) [Field k] (S : Set (MvPolynomial (Fin (n + 1)) k)) : Set (Projectivization k (Fin (n + 1) → k))

Projective zero locus of a set of polynomials: $V_+(S) = \{ p \in \mathbb{P}^n(k) \mid f(p) = 0 \text{ for all } f \in S\}$.

theorem ProjectiveClosure.projectiveZeroLocus_anti {n : ℕ} (k : Type u_2) [Field k] {S T : Set (MvPolynomial (Fin (n + 1)) k)} (h : S ⊆ T) : projectiveZeroLocus k T ⊆ projectiveZeroLocus k S

The projective zero locus is order-reversing: $S \subseteq T$ implies $V_+(T) \subseteq V_+(S)$.

def ProjectiveClosure.projectiveClosure {n : ℕ} (k : Type u_2) [Field k] (I : Ideal (MvPolynomial (Fin n) k)) : Set (Projectivization k (Fin (n + 1) → k))

The projective closure of the affine variety $V(I)$: the zero locus of the homogenized ideal homogenizeIdeal I inside $\mathbb{P}^n(k)$.

def ProjectiveClosure.projectiveClosureOfSet {n : ℕ} (k : Type u_2) [Field k] (Z : Set (Fin n → k)) : Set (Projectivization k (Fin (n + 1) → k))

Projective closure of an arbitrary set $Z \subseteq \mathbb{A}^n(k)$: defined as the projective closure of the affine vanishing ideal of $Z$.

noncomputable def AffineParts.dehomogenize {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin n) k

Dehomogenization with respect to the variable $X_i$: the ring homomorphism $R[X_0, \ldots, X_n] \to R[X_0, \ldots, \widehat{X_i}, \ldots, X_n]$ which sends $X_i \mapsto 1$.

def AffineParts.projectiveZeroLocus {n : ℕ} (k : Type u_1) [Field k] (S : Set (MvPolynomial (Fin (n + 1)) k)) : Set (Projectivization k (Fin (n + 1) → k))

Projective zero locus restricted to homogeneous polynomials: a projective point $p$ lies in $V_+(S)$ iff every homogeneous $f \in S$ vanishes at any representative of $p$.

def AffineParts.affinePart {n : ℕ} (k : Type u_1) [Field k] (V : Set (Projectivization k (Fin (n + 1) → k))) (i : Fin (n + 1)) : Set (Projectivization k (Fin (n + 1) → k))

Affine part of a projective set $V$ in the chart $U_i$: simply $V \cap U_i$.

noncomputable def AffineParts.dehomogenizedIdeal {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) (i : Fin (n + 1)) : Ideal (MvPolynomial (Fin n) k)

Image of an ideal $I$ under dehomogenization at index $i$: the ideal of $R[X_0, \ldots, \widehat{X_i}, \ldots, X_n]$ obtained from $I$ by setting $X_i = 1$.

def AffineParts.affinePartZeroLocus {n : ℕ} (k : Type u_1) [Field k] (S : Set (MvPolynomial (Fin (n + 1)) k)) (i : Fin (n + 1)) : Set (Fin n → k)

Affine zero locus in the chart $U_i$: an affine point $a$ lies in the locus iff every homogeneous $f \in S$ vanishes after dehomogenization at $X_i$.

def ProjectiveVanishingIdeal.homogVanishingSet {n : ℕ} (k : Type u_1) [Field k] (Z : Set (Projectivization k (Fin (n + 1) → k))) : Set (MvPolynomial (Fin (n + 1)) k)

Set of homogeneous polynomials vanishing on a projective subset $Z$.

noncomputable def ProjectiveVanishingIdeal.projectiveVanishingIdeal {n : ℕ} (k : Type u_1) [Field k] (Z : Set (Projectivization k (Fin (n + 1) → k))) : Ideal (MvPolynomial (Fin (n + 1)) k)

Projective vanishing ideal $I_+(Z) \subseteq k[X_0, \ldots, X_n]$: the homogeneous ideal generated by all homogeneous polynomials vanishing on $Z$.

def ProjectiveVarietyDef.ProjectiveAlgebraicSet {n : ℕ} (k : Type u_1) [Field k] (S : Set (MvPolynomial (Fin (n + 1)) k)) : Set (Projectivization k (Fin (n + 1) → k))

Definition 13.21 (projective algebraic set). The zero locus of a set $S$ of polynomials in $\mathbb{P}^n(k)$, considering only the homogeneous elements of $S$.

def ProjectiveVarietyDef.IsProjectiveAlgebraicSubset {n : ℕ} (k : Type u_1) [Field k] (Z : Set (Projectivization k (Fin (n + 1) → k))) : Prop

A subset $Z \subseteq \mathbb{P}^n(k)$ is projective algebraic if it arises as the projective zero locus of some set $S$ of polynomials.

def ProjectiveVarietyDef.IsIrreducibleProjectiveAlgebraicSet {n : ℕ} (k : Type u_1) [Field k] (Z : Set (Projectivization k (Fin (n + 1) → k))) : Prop

A projective algebraic set $Z$ is irreducible if it is nonempty and cannot be written as a union $Z = Z_1 \cup Z_2$ of two proper projective algebraic subsets.

def ProjectiveVarietyDef.IsProjectiveVariety {n : ℕ} (k : Type u_1) [Field k] (V : Set (Projectivization k (Fin (n + 1) → k))) : Prop

A projective variety is an irreducible projective algebraic subset of $\mathbb{P}^n(k)$.

theorem ProjectiveVarietyDef.IsProjectiveVariety.isIrreducible {n : ℕ} (k : Type u_1) [Field k] {V : Set (Projectivization k (Fin (n + 1) → k))} (hV : IsProjectiveVariety k V) : IsIrreducibleProjectiveAlgebraicSet k V

A projective variety is irreducible.

theorem ProjectiveVarietyDef.IsProjectiveVariety.nonempty {n : ℕ} (k : Type u_1) [Field k] {V : Set (Projectivization k (Fin (n + 1) → k))} (hV : IsProjectiveVariety k V) : V.Nonempty

A projective variety is nonempty.

theorem Theorem1323.eval_single_homogenized_monomial {n : ℕ} (k : Type u_1) [Field k] (m : Fin n →₀ ℕ) (c : k) (d : ℕ) (P : Fin n → k) : (MvPolynomial.eval (Fin.insertNth 0 1 P)) ((MvPolynomial.monomial (Finsupp.mapDomain Fin.succ m + Finsupp.single 0 (d - m.sum fun (x : Fin n) (e : ℕ) => e))) c) = c * m.prod fun (i : Fin n) (e : ℕ) => P i ^ e

Evaluating a single homogenized monomial at $(1, P_1, \ldots, P_n)$ yields $c \prod_i P_i^{m_i}$, the corresponding affine monomial value.

theorem Theorem1323.eval_homogenize_at_one_cons {n : ℕ} (k : Type u_1) [Field k] (f : MvPolynomial (Fin n) k) (P : Fin n → k) : (MvPolynomial.eval (Fin.insertNth 0 1 P)) (ProjectiveClosure.homogenize f) = (MvPolynomial.eval P) f

Key compatibility: evaluating the homogenization $F = \tilde f$ at $(1, P_1, \ldots, P_n)$ recovers the affine evaluation $f(P)$.

theorem Theorem1323.eval_comp_dehomogenize_eq {n : ℕ} (k : Type u_1) [Field k] (P : Fin n → k) : (MvPolynomial.eval P).comp (AffineParts.dehomogenize k 0) = MvPolynomial.eval (Fin.insertNth 0 1 P)

Composing dehomogenization-at-$X_0$ with affine evaluation at $P$ equals projective evaluation at $(1, P)$.

theorem Theorem1323.eval_dehomogenize_eq {n : ℕ} (k : Type u_1) [Field k] (g : MvPolynomial (Fin (n + 1)) k) (P : Fin n → k) : (MvPolynomial.eval P) ((AffineParts.dehomogenize k 0) g) = (MvPolynomial.eval (Fin.insertNth 0 1 P)) g

Pointwise version of eval_comp_dehomogenize_eq.

theorem Theorem1323.dehomogenize_monomial_mapDomain_succ {n : ℕ} (k : Type u_1) [Field k] (m : Fin n →₀ ℕ) (c : k) (e : ℕ) : (AffineParts.dehomogenize k 0) ((MvPolynomial.monomial (Finsupp.mapDomain Fin.succ m + Finsupp.single 0 e)) c) = (MvPolynomial.monomial m) c

Dehomogenization of the homogenized monomial $X_0^e \cdot X_1^{m_1} \cdots X_n^{m_n}$ at $X_0$ recovers the affine monomial $X_1^{m_1} \cdots X_n^{m_n}$.

theorem Theorem1323.eval_homogenize_dehomogenize_eq {n : ℕ} (k : Type u_1) [Field k] (f : MvPolynomial (Fin (n + 1)) k) (P : Fin n → k) : (MvPolynomial.eval (Fin.insertNth 0 1 P)) (ProjectiveClosure.homogenize ((AffineParts.dehomogenize k 0) f)) = (MvPolynomial.eval (Fin.insertNth 0 1 P)) f

Evaluating $\widetilde{f|_{X_0 = 1}}$ at $(1, P)$ agrees with evaluating $f$ at $(1, P)$: on the affine patch $U_0$, homogenize-after-dehomogenize is the identity.

theorem Theorem1323.homogenize_dehomogenize_mem_homogenizeIdeal {n : ℕ} (k : Type u_1) [Field k] {I : Ideal (MvPolynomial (Fin (n + 1)) k)} {f : MvPolynomial (Fin (n + 1)) k} (hf : f ∈ I) : ProjectiveClosure.homogenize ((AffineParts.dehomogenize k 0) f) ∈ ProjectiveClosure.homogenizeIdeal (Ideal.map (AffineParts.dehomogenize k 0) I)

If $f \in I$, then $\widetilde{f|_{X_0 = 1}}$ lies in the homogenization of the dehomogenized image of $I$.

theorem Theorem1323.projective_closure_cap_affine_eq {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin n) k)) : {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0} = {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval P) f = 0}

Theorem 13.23. Intersecting the projective closure with the affine patch $U_0$ recovers the original affine variety $V(I)$: the projective vanishing set of homogenizeIdeal I at points $(1, P)$ equals the affine vanishing set of $I$.

@[reducible, inline]

abbrev ProjectiveDimension.AffinePoint (k : Type u_1) [Field k] (N : ℕ) : Type u_1

Affine $N$-space over $\overline{k}$: tuples $(x_1, \ldots, x_N) \in \overline{k}^N$.

def ProjectiveDimension.zeroLocus (k : Type u_1) [Field k] (N : ℕ) (S : Set (MvPolynomial (Fin N) (AlgebraicClosure k))) : Set (AffinePoint k N)

Affine zero locus of a set $S$ over $\overline{k}$: the common $\overline{k}$-vanishing set of $S \subseteq \overline{k}[X_1, \ldots, X_N]$.

def ProjectiveDimension.vanishingIdeal' (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffinePoint k N)) : Ideal (MvPolynomial (Fin N) (AlgebraicClosure k))

Vanishing ideal of a set $V \subseteq \overline{k}^N$: the ideal of polynomials over $\overline{k}$ that vanish on every point of $V$.

@[reducible, inline]

abbrev ProjectiveDimension.coordinateRing' (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffinePoint k N)) : Type u_1

Coordinate ring of $V \subseteq \overline{k}^N$: the quotient $\overline{k}[X_1, \ldots, X_N] / I(V)$.

def ProjectiveDimension.HasAffineDimension (k : Type u_1) [Field k] (N : ℕ) (V : Set (AffinePoint k N)) (d : ℕ) : Prop

An affine algebraic set $V$ has dimension $d$ if the Krull dimension of its coordinate ring equals $d$.

noncomputable def ProjectiveDimension.jacobianMatrix (k : Type u_1) [Field k] (N m : ℕ) (f : Fin m → MvPolynomial (Fin N) (AlgebraicClosure k)) (P : AffinePoint k N) : Matrix (Fin m) (Fin N) (AlgebraicClosure k)

Jacobian matrix at the point $P$: the $m \times N$ matrix whose $(i, j)$-entry is $\partial f_i / \partial X_j \,(P)$.

def ProjectiveDimension.singularLocus' (k : Type u_1) [Field k] (N m r : ℕ) (f : Fin m → MvPolynomial (Fin N) (AlgebraicClosure k)) : Set (AffinePoint k N)

Singular locus of the system $f$: those zeros of $f$ at which the rank of the Jacobian is strictly less than the codimension threshold $r$.

def ProjectiveDimension.affinePartBaseChange {n : ℕ} (k : Type u_1) [Field k] (V : Set (Fin n → k)) : Set (AffinePoint k n)

Base change of an affine variety $V \subseteq k^n$ to $\overline{k}^n$ via the canonical algebra map $k \hookrightarrow \overline{k}$.

noncomputable def ProjectiveDimension.liftToAlgClosure (k : Type u_1) [Field k] (N : ℕ) : MvPolynomial (Fin N) k →+* MvPolynomial (Fin N) (AlgebraicClosure k)

Coefficient lift $k[X_1, \ldots, X_N] \to \overline{k}[X_1, \ldots, X_N]$ via the canonical algebra map.

noncomputable def ProjectiveDimension.affinePartGenerators {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (f : Fin m → MvPolynomial (Fin (n + 1)) k) (i : Fin (n + 1)) : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)

Generators of the affine piece in chart $U_i$ over $\overline{k}$: dehomogenize each $f_j$ at index $i$, then lift coefficients to $\overline{k}$.

def ProjectiveDimension.affinePartZeroLocusAlgClosed {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (f : Fin m → MvPolynomial (Fin (n + 1)) k) (i : Fin (n + 1)) : Set (AffinePoint k n)

Zero locus over $\overline{k}$ of the affine generators in chart $U_i$.

def ProjectiveDimension.HasProjectiveDimension {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (f : Fin m → MvPolynomial (Fin (n + 1)) k) (d : ℕ) : Prop

Projective dimension of the variety cut out by $f$: every affine chart has dimension $\le d$, and at least one chart realizes dimension $d$.

def ProjectiveDimension.IsAffinePartSmooth {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (g : Fin m → MvPolynomial (Fin n) (AlgebraicClosure k)) (d : ℕ) : Prop

An affine piece of dimension $d$ is smooth when its singular locus (rank $< n - d$) is empty.

def ProjectiveDimension.IsProjectiveSmooth {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (f : Fin m → MvPolynomial (Fin (n + 1)) k) : Prop

A projective variety is smooth if each of its affine charts of dimension $d_i$ is smooth.

theorem Theorem1324.dehomogenize_surjective {n : ℕ} (k : Type u_1) [Field k] (i : Fin (n + 1)) : Function.Surjective ⇑(AffineParts.dehomogenize k i)

Dehomogenization at any index $i$ is a surjective ring homomorphism $k[X_0, \ldots, X_n] \twoheadrightarrow k[X_0, \ldots, \widehat{X_i}, \ldots, X_n]$.

theorem Theorem1324.projective_closure_of_affinePart_eq {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) : {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0} = {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal (Ideal.map (AffineParts.dehomogenize k 0) I), (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0}

Theorem 13.24. For any ideal $I \subseteq k[X_0, \ldots, X_n]$, the affine piece $\{P \mid f(1, P) = 0 \,\forall f \in I\}$ equals the affine piece of the projective closure of $I$ dehomogenized at $X_0$ and re-homogenized.

theorem Corollary1326.vanishingIdeal_eq_of_set_eq {n : ℕ} (k : Type u_1) [Field k] (S T : Set (Fin n → k)) (h : S = T) : MvPolynomial.vanishingIdeal k S = MvPolynomial.vanishingIdeal k T

Functoriality: equal subsets have equal vanishing ideals.

noncomputable def Corollary1326.coordinateRingEquiv {n : ℕ} (k : Type u_1) [Field k] (V V' : Set (Fin n → k)) (hVV' : V = V') : MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V ≃+* MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V'

Ring isomorphism between coordinate rings induced by equality of varieties $V = V'$.

theorem Corollary1326.krullDim_eq {n : ℕ} (k : Type u_1) [Field k] (V V' : Set (Fin n → k)) (hVV' : V = V') : ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V) = ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V')

Equal varieties give coordinate rings with equal Krull dimension.

noncomputable def Corollary1326.functionFieldEquiv {n : ℕ} (k : Type u_1) [Field k] (V V' : Set (Fin n → k)) (hVV' : V = V') [(MvPolynomial.vanishingIdeal k V).IsPrime] [(MvPolynomial.vanishingIdeal k V').IsPrime] : FractionRing (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V) ≃+* FractionRing (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k V')

Equal irreducible varieties give isomorphic function fields.

noncomputable def Corollary1326.coordinateRingEquiv_of_projective_closure {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin n) k)) : MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0} ≃+* MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval P) f = 0}

Coordinate-ring isomorphism between the affine part of the projective closure of $V(I)$ and the affine variety $V(I)$ itself (Corollary 13.26).

theorem Corollary1326.krullDim_eq_of_projective_closure {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin n) k)) : ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0}) = ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval P) f = 0})

Dimension is preserved: the affine part of the projective closure of $V(I)$ has the same Krull dimension as $V(I)$.

theorem Corollary1326.affinePart_eq_dehomogenizedIdeal_zeroLocus {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) : {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0} = {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I, (MvPolynomial.eval P) g = 0}

The affine piece of a projective ideal $I$ over chart $U_0$ equals the zero locus of its dehomogenization at $X_0$.

noncomputable def Corollary1326.coordinateRingEquiv_of_affinePart {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) : MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0} ≃+* MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I, (MvPolynomial.eval P) g = 0}

Coordinate-ring isomorphism induced by affinePart_eq_dehomogenizedIdeal_zeroLocus.

theorem Corollary1326.krullDim_eq_of_affinePart {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) : ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0}) = ringKrullDim (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I, (MvPolynomial.eval P) g = 0})

Krull dimension agrees on the two presentations of the affine piece.

noncomputable def Corollary1326.functionFieldEquiv_of_affinePart {n : ℕ} (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin (n + 1)) k)) [(MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0}).IsPrime] [(MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I, (MvPolynomial.eval P) g = 0}).IsPrime] : FractionRing (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0}) ≃+* FractionRing (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I, (MvPolynomial.eval P) g = 0})

Function-field isomorphism for the two presentations of an irreducible affine piece.

theorem Corollary1326.corollary_13_26_part2_dimension {n : ℕ} (k : Type u_1) [Field k] {m : ℕ} (f : Fin m → MvPolynomial (Fin (n + 1)) k) (d : ℕ) (hd : ProjectiveDimension.HasProjectiveDimension k f d) (i : Fin (n + 1)) (d_i : ℕ) : ProjectiveDimension.HasAffineDimension k n (ProjectiveDimension.affinePartZeroLocusAlgClosed k f i) d_i → d_i ≤ d

Part of Corollary 13.26: if the projective dimension is $d$, then every chart's affine dimension is $\le d$.

theorem Corollary1326.corollary_13_26 {n : ℕ} (k : Type u_1) [Field k] (I₁ : Ideal (MvPolynomial (Fin n) k)) (I₂ : Ideal (MvPolynomial (Fin (n + 1)) k)) : Nonempty (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ ProjectiveClosure.homogenizeIdeal I₁, (MvPolynomial.eval (Fin.insertNth 0 1 P)) g = 0} ≃+* MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I₁, (MvPolynomial.eval P) f = 0}) ∧ Nonempty (MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ f ∈ I₂, (MvPolynomial.eval (Fin.insertNth 0 1 P)) f = 0} ≃+* MvPolynomial (Fin n) k ⧸ MvPolynomial.vanishingIdeal k {P : Fin n → k | ∀ g ∈ Ideal.map (AffineParts.dehomogenize k 0) I₂, (MvPolynomial.eval P) g = 0})

Corollary 13.26 (coordinate-ring compatibility). For any affine ideal $I_1 \subseteq k[X_1, \ldots, X_n]$ and any projective ideal $I_2 \subseteq k[X_0, \ldots, X_n]$, the affine pieces of $V_+(I_1)$ and $V(I_2)|_{U_0}$ have coordinate rings isomorphic to those of $V(I_1)$ and the dehomogenization of $I_2$ respectively.