def IsAffineVariety (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : Prop

An affine variety is an irreducible algebraic subset of affine $n$-space (Definition 12.7).

theorem IsAffineVariety.isAlgebraicSubset (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (h : IsAffineVariety k n V) : IsAlgebraicSubset k n V

An affine variety is in particular an algebraic subset.

theorem IsAffineVariety.nonempty (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (h : IsAffineVariety k n V) : V.Nonempty

An affine variety is nonempty (since irreducible algebraic sets are required to be nonempty).

theorem coordinateRingBar_isDomain (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAffineVariety k n V) : IsDomain (AffineCoordinateRingBar V)

The coordinate ring $\bar{k}[V]$ of an affine variety $V$ is an integral domain.

noncomputable def functionFieldBar (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (hV : IsAffineVariety k n V) : Type u_1

The function field $\bar{k}(V)$ of an affine variety, defined as the fraction field of the coordinate ring $\bar{k}[V]$.

@[reducible]

noncomputable def functionFieldBar.instField (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAffineVariety k n V) : Field (functionFieldBar k V hV)

The function field $\bar{k}(V)$ is a field.

@[implicit_reducible]

noncomputable instance instFieldFunctionFieldBar (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAffineVariety k n V) : Field (functionFieldBar k V hV)

@[reducible]

noncomputable def functionFieldBar.instAlgebra (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAffineVariety k n V) : Algebra (AlgebraicClosure k) (functionFieldBar k V hV)

The function field $\bar{k}(V)$ is an algebra over the algebraic closure $\bar{k}$.

@[implicit_reducible]

noncomputable instance instAlgebraAlgebraicClosureFunctionFieldBar (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAffineVariety k n V) : Algebra (AlgebraicClosure k) (functionFieldBar k V hV)

noncomputable def functionField_k (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (_hV : IsAffineVariety k n V) (_hdom : IsDomain (AffineCoordinateRing V)) : Type u_1

The $k$-rational function field $k(V)$ of an affine variety, defined as the fraction field of the $k$-coordinate ring $k[V]$ when it is a domain.

@[implicit_reducible]

noncomputable instance instFieldFunctionField_k (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (_hV : IsAffineVariety k n V) (hdom : IsDomain (AffineCoordinateRing V)) : Field (functionField_k k V _hV hdom)

noncomputable def varietyDim (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (hV : IsAffineVariety k n V) : Cardinal.{u_1}

The dimension of an affine variety $V$ is the transcendence degree of its function field $\bar{k}(V)$ over $\bar{k}$ (Definition 12.21).

def IsAlgebraicSetAffine (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : Prop

A subset $V \subseteq \mathbb{A}^n$ is an algebraic set if it is the zero locus $\mathcal{V}(S)$ of some set $S$ of polynomials.

def algebraicSetsCollection (k : Type u_1) [Field k] (n : ℕ) : Set (Set (AffineSpace_k k n))

The collection of all algebraic subsets of $\mathbb{A}^n$, used as the closed sets of the Zariski topology.

theorem algebraicSetsCollection_empty_mem (k : Type u_1) [Field k] (n : ℕ) : ∅ ∈ algebraicSetsCollection k n

The empty set is an algebraic set, namely $\mathcal{V}(\{1\})$.

theorem algebraicSetsCollection_sInter_mem (k : Type u_1) [Field k] (n : ℕ) (A : Set (Set (AffineSpace_k k n))) (hA : A ⊆ algebraicSetsCollection k n) : ⋂₀ A ∈ algebraicSetsCollection k n

An arbitrary intersection of algebraic sets is again algebraic.

theorem algebraicSetsCollection_union_mem (k : Type u_1) [Field k] (n : ℕ) (A : Set (AffineSpace_k k n)) (hA : A ∈ algebraicSetsCollection k n) (B : Set (AffineSpace_k k n)) (hB : B ∈ algebraicSetsCollection k n) : A ∪ B ∈ algebraicSetsCollection k n

The union of two algebraic sets is algebraic: $\mathcal{V}(S) \cup \mathcal{V}(T) = \mathcal{V}(ST)$.

@[reducible]

def zariskiTopology (k : Type u_1) [Field k] (n : ℕ) : TopologicalSpace (AffineSpace_k k n)

The Zariski topology on $\mathbb{A}^n_k$, whose closed sets are the algebraic sets.

theorem isClosed_zariskiTopology_iff_isAlgebraicSet (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : IsClosed V ↔ IsAlgebraicSetAffine k n V

A subset of $\mathbb{A}^n_k$ is closed in the Zariski topology iff it is an algebraic set.

noncomputable def polyMapEval (k : Type u_1) [Field k] (m n : ℕ) (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (P : AffineSpace_k k m) : AffineSpace_k k n

Evaluate a tuple of polynomials at a point, giving a map $\mathbb{A}^m \to \mathbb{A}^n$.

theorem eval_bind₁_eq_eval_polyMapEval (k : Type u_1) [Field k] {m n : ℕ} (P : AffineSpace_k k m) (f : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (g : MvPolynomial (Fin n) (AlgebraicClosure k)) : (MvPolynomial.eval P) ((MvPolynomial.bind₁ f) g) = (MvPolynomial.eval (polyMapEval k m n f P)) g

Evaluating $g \circ f$ at $P$ equals evaluating $g$ at $f(P)$, where $f$ is given by a tuple of polynomials.

theorem polyMapEval_bind₁ (k : Type u_1) [Field k] {m n r : ℕ} (P : AffineSpace_k k m) (f : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (g : Fin r → MvPolynomial (Fin n) (AlgebraicClosure k)) : polyMapEval k m r (fun (j : Fin r) => (MvPolynomial.bind₁ f) (g j)) P = polyMapEval k n r g (polyMapEval k m n f P)

Polynomial maps compose: $(g \circ f)(P) = g(f(P))$.

structure AffineMorphism (k : Type u_1) [Field k] (m n : ℕ) (X : Set (AffineSpace_k k m)) (Y : Set (AffineSpace_k k n)) : Type u_1

A morphism of affine varieties $X \to Y$ is given by an $n$-tuple of polynomials whose induced map sends $X$ into $Y$.

• polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)
• maps_to (P : AffineSpace_k k m) : P ∈ X → polyMapEval k m n self.polys P ∈ Y

noncomputable def AffineMorphism.toFun (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : AffineMorphism k m n X Y) (P : AffineSpace_k k m) : AffineSpace_k k n

The underlying set-theoretic map of an affine morphism.

theorem AffineMorphism.image_mem (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : AffineMorphism k m n X Y) {P : AffineSpace_k k m} (hP : P ∈ X) : toFun k φ P ∈ Y

The image of any point of $X$ under an affine morphism lies in $Y$.

noncomputable def AffineMorphism.id (k : Type u_1) [Field k] {n : ℕ} (X : Set (AffineSpace_k k n)) : AffineMorphism k n n X X

The identity affine morphism on $X$, given by the coordinate polynomials $X_1, \ldots, X_n$.

noncomputable def AffineMorphism.comp (k : Type u_1) [Field k] {m n r : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} {Z : Set (AffineSpace_k k r)} (g : AffineMorphism k n r Y Z) (f : AffineMorphism k m n X Y) : AffineMorphism k m r X Z

Composition of affine morphisms $g \circ f : X \to Z$.

theorem AffineMorphism.toFun_id (k : Type u_1) [Field k] {n : ℕ} {X : Set (AffineSpace_k k n)} (P : AffineSpace_k k n) : toFun k (id k X) P = P

The identity morphism evaluates to the identity function.

theorem AffineMorphism.toFun_comp (k : Type u_1) [Field k] {m n r : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} {Z : Set (AffineSpace_k k r)} (g : AffineMorphism k n r Y Z) (f : AffineMorphism k m n X Y) (P : AffineSpace_k k m) : toFun k (comp k g f) P = toFun k g (toFun k f P)

The underlying function of the composite of two affine morphisms is the composite of their underlying functions.

def IsOpenInVariety (k : Type u_1) [Field k] (m : ℕ) (X U : Set (AffineSpace_k k m)) : Prop

A subset $U$ of a variety $X$ is open in $X$ iff $U = X \cap W$ for some Zariski-open $W$.

def IsDenseInVariety (k : Type u_1) [Field k] (m : ℕ) (X U : Set (AffineSpace_k k m)) : Prop

A subset $U$ is dense in the variety $X$ iff $X$ is contained in the Zariski closure of $U$.

noncomputable def ratFunEval (k : Type u_1) [Field k] (m : ℕ) (num denom : MvPolynomial (Fin m) (AlgebraicClosure k)) (P : AffineSpace_k k m) : AlgebraicClosure k

Evaluate a rational function $\mathrm{num}/\mathrm{denom}$ at a point $P$.

noncomputable def ratMapEval (k : Type u_1) [Field k] (m n : ℕ) (nums denoms : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (P : AffineSpace_k k m) : AffineSpace_k k n

Evaluate a rational map $\mathbb{A}^m \dashrightarrow \mathbb{A}^n$ given by tuples of numerators and denominators.

def ratMapDom (k : Type u_1) [Field k] (m n : ℕ) (X : Set (AffineSpace_k k m)) (denoms : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) : Set (AffineSpace_k k m)

The domain of definition of a rational map: points of $X$ where every denominator is nonzero.

theorem ratMapDom_subset (k : Type u_1) [Field k] {m n : ℕ} (X : Set (AffineSpace_k k m)) (denoms : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) : ratMapDom k m n X denoms ⊆ X

The domain of a rational map is a subset of $X$.

theorem ratMapEval_eq_polyMapEval_of_denom_one (k : Type u_1) [Field k] {m n : ℕ} (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (P : AffineSpace_k k m) : ratMapEval k m n polys (fun (x : Fin n) => 1) P = polyMapEval k m n polys P

A rational map with all denominators equal to $1$ reduces to a polynomial map.

theorem ratMapDom_of_denom_one (k : Type u_1) [Field k] {m n : ℕ} (X : Set (AffineSpace_k k m)) : (ratMapDom k m n X fun (x : Fin n) => 1) = X

If all denominators are $1$, the domain of the rational map is all of $X$.

structure RationalMap (k : Type u_1) [Field k] (m n : ℕ) (X : Set (AffineSpace_k k m)) (Y : Set (AffineSpace_k k n)) : Type u_1

A rational map $X \dashrightarrow Y$ between affine varieties: a tuple of numerators/denominators, defined on an open dense subset of $X$, sending its domain into $Y$.

• nums : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)
• denoms : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)
• denoms_ne_zero (j : Fin n) : self.denoms j ≠ 0
• dom_open : IsOpenInVariety k m X (ratMapDom k m n X self.denoms)
• dom_dense : IsDenseInVariety k m X (ratMapDom k m n X self.denoms)
• maps_to (P : AffineSpace_k k m) : P ∈ ratMapDom k m n X self.denoms → ratMapEval k m n self.nums self.denoms P ∈ Y

def RationalMap.dom (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) : Set (AffineSpace_k k m)

The domain of definition of a rational map.

noncomputable def RationalMap.toFun (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) (P : AffineSpace_k k m) : AffineSpace_k k n

The underlying partial function of a rational map.

theorem RationalMap.image_mem (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) {P : AffineSpace_k k m} (hP : P ∈ dom k φ) : toFun k φ P ∈ Y

The image of a point in the domain of a rational map lies in $Y$.

noncomputable def AffineMorphism.toRationalMap (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : AffineMorphism k m n X Y) : RationalMap k m n X Y

Every affine morphism is a rational map (with all denominators equal to $1$).

@[simp]

theorem AffineMorphism.toRationalMap_dom (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : AffineMorphism k m n X Y) : RationalMap.dom k (toRationalMap k φ) = X

The domain of the rational map associated to an affine morphism is all of $X$.

def RationalMap.IsRegular (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) : Prop

A rational map is regular if its domain of definition is the entire source variety.

def RationalMap.toAffineMorphism (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) (hreg : IsRegular k φ) (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (hpolys : ∀ P ∈ X, polyMapEval k m n polys P = ratMapEval k m n φ.nums φ.denoms P) : AffineMorphism k m n X Y

Convert a regular rational map to an affine morphism, given an explicit choice of polynomials agreeing with $\varphi$ on $X$.

theorem AffineMorphism.toRationalMap_isRegular (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : AffineMorphism k m n X Y) : RationalMap.IsRegular k (toRationalMap k φ)

The rational map associated to an affine morphism is regular.

theorem AffineMorphism.toRationalMap_toFun_eq (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (f : AffineMorphism k m n X Y) (P : AffineSpace_k k m) : RationalMap.toFun k (toRationalMap k f) P = toFun k f P

The underlying function of the rational map associated to an affine morphism agrees with that of the morphism.

def IsRegularAtPoint (k : Type u_1) [Field k] {m : ℕ} (X : Set (AffineSpace_k k m)) (num denom : MvPolynomial (Fin m) (AlgebraicClosure k)) (P : AffineSpace_k k m) : Prop

A rational function $\mathrm{num}/\mathrm{denom}$ is regular at $P \in X$ if some equivalent representation $g/h$ has $g(P) \neq 0$, modulo the vanishing ideal of $X$.

def RationalFunctionDom (k : Type u_1) [Field k] {m : ℕ} (X : Set (AffineSpace_k k m)) (num denom : MvPolynomial (Fin m) (AlgebraicClosure k)) : Set (AffineSpace_k k m)

The domain of definition of a rational function $\mathrm{num}/\mathrm{denom}$ on $X$.

def RationalFunctionLiesInCoordinateRing (k : Type u_1) [Field k] {m : ℕ} (X : Set (AffineSpace_k k m)) (num denom : MvPolynomial (Fin m) (AlgebraicClosure k)) : Prop

A rational function $\mathrm{num}/\mathrm{denom}$ lies in the coordinate ring of $X$ if it is congruent to a polynomial modulo the vanishing ideal.

theorem regular_rational_function_is_polynomial (k : Type u_2) [Field k] {m : ℕ} {X : Set (AffineSpace_k k m)} (hX : IsAffineVariety k m X) (num denom : MvPolynomial (Fin m) (AlgebraicClosure k)) (_hdenom_ne_zero : denom ≠ 0) (hdenom_nonvanishing : ∀ P ∈ X, (MvPolynomial.eval P) denom ≠ 0) : ∃ (poly : MvPolynomial (Fin m) (AlgebraicClosure k)), ∀ P ∈ X, (MvPolynomial.eval P) poly = (MvPolynomial.eval P) num / (MvPolynomial.eval P) denom

On an affine variety $X$, a rational function whose denominator vanishes nowhere on $X$ agrees pointwise with a polynomial: there is $p \in \bar{k}[X_1, \ldots, X_m]$ with $p(P) = \mathrm{num}(P)/\mathrm{denom}(P)$ for all $P \in X$.

theorem regular_rational_map_is_morphism (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (hX : IsAffineVariety k m X) (φ : RationalMap k m n X Y) (hreg : RationalMap.IsRegular k φ) : ∃ (f : AffineMorphism k m n X Y), ∀ P ∈ X, AffineMorphism.toFun k f P = RationalMap.toFun k φ P

A regular rational map between affine varieties extends to an affine morphism that agrees with it pointwise on $X$.

def RationalMap.IsDominant (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (φ : RationalMap k m n X Y) : Prop

A rational map $\varphi : X \dashrightarrow Y$ is dominant if its image is Zariski-dense in $Y$.

def RationalMap.compDom (k : Type u_1) [Field k] {m n r : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} {Z : Set (AffineSpace_k k r)} (φ : RationalMap k n r Y Z) (ψ : RationalMap k m n X Y) : Set (AffineSpace_k k m)

The domain on which the composition $\varphi \circ \psi$ of rational maps is defined.

def IsBirationallyEquivalent (k : Type u_1) [Field k] {m n : ℕ} (X : Set (AffineSpace_k k m)) (Y : Set (AffineSpace_k k n)) : Prop

Two affine varieties $X, Y$ are birationally equivalent if there exist dominant rational maps $\varphi : X \dashrightarrow Y$ and $\psi : Y \dashrightarrow X$ that are mutually inverse where both compositions are defined.

def IsStrictVarietyChain (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) (d : ℕ) (chain : Fin (d + 1) → Set (AffineSpace_k k n)) : Prop

A strict chain $V_0 \subsetneq V_1 \subsetneq \cdots \subsetneq V_d = V$ of affine subvarieties of $V$.

noncomputable def geometricDim (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) : ℕ∞

The geometric dimension of an affine variety $V$ is the supremum of $d$ for which there exists a strict chain of affine subvarieties of length $d$ ending at $V$.