Evaluation of an element of the $\bar k$-coordinate ring $\bar k[X]$ at a point $P \in X$. Given a class $[f] \in \bar k[X] = \bar k[X_1, \dots, X_n]/I(X)$ and a point $P \in X$, this yields $f(P) \in \bar k$. Well-defined because $I(X)$ vanishes on $X$.
Instances For
Compatibility of evalBarAtPoint with the quotient map: evaluating the class of a
polynomial $f$ at $P$ equals the ordinary polynomial evaluation $f(P)$.
Definition 15.2 (regularity at a point). A rational function $r \in \bar k(X) = \mathrm{Frac}(\bar k[X])$ is regular at $P \in X$ if it can be written as a fraction $r = f/g$ with $f, g \in \bar k[X]$ and $g(P) \neq 0$. Equivalently: there exists $g \in \bar k[X]$ with $g(P) \neq 0$ such that $g \cdot r$ lies in the image of $\bar k[X]$ in the fraction field.
Instances For
The denominator ideal of a rational function $r \in \bar k(X)$: the ideal of elements $g \in \bar k[X]$ such that $g \cdot r$ lies in $\bar k[X]$. Its non-vanishing locus is the regular locus of $r$.
Instances For
Unfolding lemma: $g \in \text{denominatorIdeal}\, r$ iff $g \cdot r$ lies in the image of $\bar k[X]$ in $\bar k(X)$.
The regular domain (or regular locus) of $r \in \bar k(X)$: the set of points $P \in X$ at which $r$ is regular.
Instances For
Membership in regularDomain: $P$ lies in the regular domain of $r$ iff $P \in X$
and $r$ is regular at $P$.
Polynomial functions are regular everywhere: if $r = f$ comes from $\bar k[X]$, then $r$ is regular at every point $P \in X$ (take denominator $1$).
The regular domain of a polynomial function $f \in \bar k[X]$, viewed as an element of $\bar k(X)$, is all of $X$.
Evaluation of a rational function $r \in \bar k(X)$ at a point $P$ where $r$ is regular: choose a representation $r = f/g$ with $g(P) \neq 0$ and return $f(P)/g(P) \in \bar k$. The value is independent of the choice of representation (though that is not proven here).
Instances For
Key application of the Nullstellensatz: if $X$ is an algebraic subset and $J$ is an ideal of $\bar k[X]$ with no common zero on $X$ (i.e. for every $P \in X$ there exists $g \in J$ with $g(P) \neq 0$), then $J = \bar k[X]$ (the unit ideal).
If $1$ lies in the denominator ideal of $r$ (equivalently, the denominator ideal is the unit ideal), then $r$ itself is a polynomial function.
If $r \in \bar k(X)$ is regular on all of $X$, then its denominator ideal equals
$\bar k[X]$ (the unit ideal). Combines denominatorIdeal_eq_top_of_no_common_zero with
the definition of regularDomain.
Theorem 15.5 (regular everywhere equals polynomial). A rational function $r \in \bar k(X)$ is regular on all of $X$ if and only if it comes from a polynomial function in $\bar k[X]$. This is a key consequence of the Nullstellensatz.
A tuple $(\varphi_1, \dots, \varphi_{n_\mathrm{cod}})$ of rational functions in $\bar k(X)$ is regular at $P \in X$ if each component $\varphi_i$ is regular at $P$.
Instances For
Componentwise evaluation of a tuple of rational functions at a point of common regularity: produces a point of $\bar k^{n_\mathrm{cod}}$.
Instances For
Definition 15.4 (affine rational map). A rational map $\varphi : X \dashrightarrow Y$ between affine algebraic sets is a tuple of components $(\varphi_1, \dots, \varphi_{n_\mathrm{cod}})$ with each $\varphi_i \in \bar k(X)$, together with the requirement that whenever the tuple is regular at $P \in X$, the resulting point $(\varphi_1(P), \dots, \varphi_{n_\mathrm{cod}}(P))$ lies in the target $Y$.
- components : Fin n_cod → FractionRing (AffineCoordinateRingBar X)
- image_mem (P : Fin m → AlgebraicClosure k) (hP : P ∈ X) (hreg : IsTupleRegularAt self.components P hP) : evalTupleAt self.components P hP hreg ∈ Y
Instances For
The domain of definition of a rational map (as a tuple of rational functions): the set of points of $X$ where every component is regular.
Instances For
Lemma 15.3 (description of domain). The domain of definition of a rational map $\varphi : X \dashrightarrow Y$ is the intersection $X \cap \bigcap_i \mathrm{dom}(\varphi_i)$ of the regular domains of its components.
A rational map $\varphi$ is regular (a morphism of affine varieties) if it is regular at every point of $X$.
Instances For
The Zariski closure of a subset $S \subseteq \bar k^n$: the smallest algebraic set containing $S$, namely $\mathcal{V}(\mathcal{I}(S))$.
Instances For
The set-theoretic image of a rational map (defined on its domain): the set of all $Q \in \bar k^{n_\mathrm{cod}}$ that arise as the value of $\varphi$ at some point of $\mathrm{dom}(\varphi)$.
Instances For
Definition 15.7 (dominant rational map). A rational map $\varphi : X \dashrightarrow Y$ is dominant if its image is Zariski-dense in $Y$, i.e. the Zariski closure of the image equals $Y$.
Instances For
The composition domain of $\psi \circ \varphi$ where $\varphi : X \dashrightarrow Y$ and $\psi : Y \dashrightarrow X$: the set of points $P \in X$ where $\varphi$ is regular at $P$, $\varphi(P) \in Y$, and $\psi$ is regular at $\varphi(P)$.
Instances For
Pointwise evaluation of the composition $\psi \circ \varphi$ at $P \in \mathrm{compositionDomain}(\varphi, \psi)$: returns $\psi(\varphi(P)) \in \bar k^m$.
Instances For
Definition 15.10 (birational equivalence). Two affine algebraic sets $X$ and $Y$ are birationally equivalent if there exist dominant rational maps $\varphi : X \dashrightarrow Y$ and $\psi : Y \dashrightarrow X$ whose compositions (on their composition domains) agree with the respective identities.
Instances For
A ring homomorphism $\theta : \bar k(Y) \to \bar k(X)$ is a $\bar k$-algebra homomorphism of function fields if it fixes the scalars from $\bar k$ (under the canonical inclusions $\bar k \hookrightarrow \bar k[Y] \hookrightarrow \bar k(Y)$).
Instances For
The substitution homomorphism $\bar k[Y_1, \dots, Y_{n_\mathrm{cod}}] \to \bar k(X)$ sending each coordinate $Y_i$ to the corresponding component $\varphi_i \in \bar k(X)$. This is the first step in building the pullback induced by a rational map.
Instances For
Key technical lemma: the substitution homomorphism associated to a rational map $\varphi : X \dashrightarrow Y$ kills the ideal $\mathcal{I}(Y)$. Combines the Nullstellensatz with the property that the values of $\varphi$ land in $Y$. This is what allows the substitution map to descend to $\bar k[Y] \to \bar k(X)$.
Descent of the substitution homomorphism to a ring map $\bar k[Y] \to \bar k(X)$: since the substitution kills $\mathcal{I}(Y)$, it factors through the quotient $\bar k[Y_1,\dots,Y_{n_\mathrm{cod}}]/\mathcal{I}(Y) = \bar k[Y]$.
Instances For
Compatibility of the descended map with the quotient: evaluating on the class of $f$ gives the substitution applied to $f$.
Each coordinate $\varphi_i = \varphi^*(Y_i)$ lies in $\bar k[X] \subseteq \bar k(X)$, viewed via the substitution homomorphism. (This is the form needed for the pullback to descend to coordinate rings; the proof uses regularity of the rational map.)
Generalization to all of $\bar k[Y]$: every element $g \in \bar k[Y]$ is sent into
$\bar k[X] \subseteq \bar k(X)$ by dominantPullbackToFractionRing. Proved by induction
using the previous component-wise lemma.
Defining property of the chosen preimage: the chosen element of $\bar k[X]$ maps to $\varphi^*(g) \in \bar k(X)$.
The pullback ring homomorphism $\varphi^* : \bar k[Y] \to \bar k[X]$ on coordinate
rings induced by a dominant rational map $\varphi : X \dashrightarrow Y$. Built using the
choice function from dominantPullback_mem_range together with the injectivity of
$\bar k[X] \hookrightarrow \bar k(X)$.
Instances For
Compatibility square: the diagram of $\varphi^* : \bar k[Y] \to \bar k[X]$ followed by $\bar k[X] \hookrightarrow \bar k(X)$ commutes with the descended substitution homomorphism $\bar k[Y] \to \bar k(X)$.
The pullback $\varphi^* : \bar k[Y] \to \bar k[X]$ fixes the scalars: it sends the
class of a constant polynomial $C(r)$ in $\bar k[Y]$ to the class of $C(r)$ in $\bar k[X]$.
This is the coordinate-ring version of IsKbarFunctionFieldHom for $\varphi^*$.
Theorem 15.8(i) (injectivity of pullback). If $\varphi : X \dashrightarrow Y$ is dominant, then the composite $\bar k[Y] \xrightarrow{\varphi^*} \bar k[X] \hookrightarrow \bar k(X)$ is injective. The proof combines the Nullstellensatz with the density of the image of $\varphi$ in $Y$.
The function-field pullback $\varphi^* : \bar k(Y) \to \bar k(X)$ induced by a
dominant rational map. Obtained by extending the coordinate-ring pullback to fraction
fields using IsFractionRing.lift and the injectivity result.
Instances For
Commutative diagram linking the coordinate-ring pullback to the function-field pullback: the diagram of $\bar k[Y] \hookrightarrow \bar k(Y) \xrightarrow{\varphi^*} \bar k(X)$ and $\bar k[Y] \xrightarrow{\varphi^*} \bar k[X] \hookrightarrow \bar k(X)$ commutes.
Given an abstract ring homomorphism $\theta : \bar k(Y) \to \bar k(X)$, the components of the rational map it induces: for each coordinate $j$, the image $\theta(Y_j) \in \bar k(X)$. This is the data used to recover a rational map from a function-field homomorphism in Theorem 15.8(iii).
Instances For
Independence of representation for evalRatFunAt: any representation $r = f/g$ with
$g(P) \neq 0$ gives the same value $f(P)/g(P)$ for the evaluation of $r$ at $P$.
Technical "clearing denominators" lemma used in the proof of Theorem 15.8(iii): for any polynomial $f \in \bar k[Y_1, \dots, Y_{n_\mathrm{cod}}]$ and any point $P$ at which the components $(\theta(Y_1), \dots, \theta(Y_{n_\mathrm{cod}}))$ are all regular, there exist $g_0, f_0 \in \bar k[X]$ with $g_0(P) \neq 0$ such that $\theta_*(f) = f_0 / g_0$ in $\bar k(X)$ and $f(\theta(P)) \cdot g_0(P) = f_0(P)$.
Compatibility of a $\bar k$-algebra hom $\theta$ with the substitution homomorphism: applying $\theta$ to the class of $f \in \bar k[Y]$ in $\bar k(Y)$ equals evaluating $f$ via substitution at the components $\theta(Y_i)$.
Characterizing property of the induced rational map: evaluating a polynomial $f$ in the target coordinates at the image point $\theta(P)$ equals the value of $\theta(f)$ at the point $P$. This is the key step proving compatibility of $\theta$ with point evaluation.
Any ring homomorphism $\theta : \bar k(Y) \to \bar k(X)$ kills the ideal $\mathcal{I}(Y)$: the polynomial $f \in \mathcal{I}(Y)$ becomes zero in $\bar k[Y]$ (since the quotient is the coordinate ring), so its image in $\bar k(Y)$ is zero, hence $\theta(f) = 0$.
The zero rational function is regular at every point: with denominator $g = 1$ (which satisfies $g(P) = 1 \neq 0$), we have $g \cdot 0 = 0$ in the image of $\bar k[X]$.
The value of the zero rational function at any point is zero.
The image of the rational map induced by a $\bar k$-algebra homomorphism $\theta$ lands in $Y$: at any point $P$ where the components are regular, the evaluated tuple $(\theta(Y_1)(P), \dots, \theta(Y_{n_\mathrm{cod}})(P))$ satisfies every equation of $\mathcal{I}(Y)$, hence lies in $Y$.
The rational map induced by a $\bar k$-algebra homomorphism $\theta : \bar k(Y) \to \bar k(X)$: its components are $\theta(Y_1), \dots, \theta(Y_{n_\mathrm{cod}})$, and the
image-membership condition is provided by functionFieldMorphism_image_mem. This is the
construction of Theorem 15.8(iii) producing $\varphi$ from $\theta$.
Instances For
If a rational function $r \in \bar k(X)$ vanishes wherever it is regular together with a given tuple $\varphi$, then $r = 0$. The proof uses the Nullstellensatz to show that the corresponding numerator must be in $\mathcal{I}(X)$.
The rational map induced by a $\bar k$-algebra homomorphism of function fields is dominant: the image of the resulting rational map is Zariski-dense in $Y$. This is one of the key conclusions of Theorem 15.8(iii).
Compatibility of coordinate-ring pullbacks with composition: if $\psi \circ \varphi$ is a rational map matching the formal composition of pullbacks on coordinates, then $(\psi \circ \varphi)^* = \varphi^* \circ \psi^*$ as ring maps $\bar k[Z] \to \bar k[X]$.
Theorem 15.8(iii) (functoriality of the function-field pullback). For composable dominant rational maps $\varphi : X \dashrightarrow Y$ and $\psi : Y \dashrightarrow Z$ with composite $\psi \circ \varphi$, the function-field pullbacks compose contravariantly: $(\psi \circ \varphi)^* = \varphi^* \circ \psi^*$.
Corollary 15.9 (roundtrip on maps). Starting from a dominant rational map $\varphi$, forming its function-field pullback $\varphi^*$, and then taking the rational map induced by $\varphi^*$ recovers $\varphi$. This is one direction of the equivalence in Corollary 15.9.
Coordinate-ring version of the roundtrip on morphisms: a $\bar k$-algebra hom $\theta$ restricted to the image of $\bar k[Y]$ equals the function-field pullback of the rational map induced by $\theta$.
Corollary 15.9 (roundtrip on morphisms). Starting from a $\bar k$-algebra hom $\theta : \bar k(Y) \to \bar k(X)$, forming the induced rational map and then taking its function-field pullback recovers $\theta$. The other half of the equivalence in Corollary 15.9.
Theorem 15.8(ii). For every $\bar k$-algebra homomorphism $\theta : \bar k(Y) \to \bar k(X)$ there exists a unique dominant rational map $\varphi : X \dashrightarrow Y$ whose function-field pullback is $\theta$, and which is characterized by $f(\varphi(P)) = \theta(f)(P)$ at points where both sides are defined.
The natural ring homomorphism $k[X] \to \bar k[X]$ extending scalars from the base field $k$ to its algebraic closure $\bar k$: descends the map induced on polynomials by $k \hookrightarrow \bar k$ to the quotient defining $k[X]$.
Instances For
The composite $k[X] \to \bar k[X] \hookrightarrow \bar k(X)$ is injective. Needed to extend the scalar-extension map to the level of function fields.
Scalar extension on function fields: the natural homomorphism $k(X) \to \bar k(X)$ obtained by extending the coordinate-ring map $k[X] \to \bar k[X]$ to fraction fields.
Instances For
A rational map $\varphi : X \dashrightarrow Y$ is defined over $k$ if each of its components lies in the image of $k(X) \to \bar k(X)$, i.e. can be represented by a tuple of rational functions with coefficients in the base field $k$.
Instances For
The coordinate-ring pullback over $k$: for a dominant rational map defined over $k$ between $k$-defined varieties, the pullback descends to a ring map $k[Y] \to k[X]$ on the $k$-coordinate rings.
Instances For
Compatibility square between the $k$-pullback and the $\bar k$-pullback on coordinate rings: pulling back $g$ over $k$ and then extending scalars to $\bar k$ equals first extending scalars and then pulling back over $\bar k$.
Corollary 15.12 ($k$-rational function field pullback). For a dominant rational map $\varphi : X \dashrightarrow Y$ defined over $k$ between $k$-defined varieties, there exists a ring homomorphism $\psi : k(Y) \to k(X)$ compatible with the $\bar k$-pullback under scalar extension: $\mathrm{ext} \circ \psi = \varphi^* \circ \mathrm{ext}$.
The $\bar k$-algebra structure on $\bar k[Z]$ obtained from the natural map $\bar k \hookrightarrow \bar k[x_1, \dots, x_n]$ followed by the quotient.
Bundled object of the category of affine varieties (over $\bar k$) with domain coordinate ring: packages a dimension, a carrier set, the algebraic-subset condition, and the integral-domain property of $\bar k[X]$.
- dim : ℕ
- carrier : Set (Fin self.dim → AlgebraicClosure k)
- isAlgebraic : IsAlgebraicSubset k self.dim self.carrier
- isDomain : IsDomain (AffineCoordinateRingBar self.carrier)
Instances For
A morphism in AffineVarietyDom k: a dominant rational map between the underlying
varieties, bundling a rational map and a proof that it is dominant.
- map : AffineRationalMap V.carrier W.carrier
- dominant : IsDominantRationalMap W.carrier self.map
Instances For
The identity rational map on $V$: defined as the rational map induced by the identity ring homomorphism on $\bar k(V)$, which is a $\bar k$-algebra homomorphism.
Instances For
The identity rational map on $V$ is dominant: its image is all of $V$, hence its Zariski closure is $V$.
The function-field pullback $\varphi^*$ is a morphism over $\bar k$: it fixes the images of all constants $c \in \bar k$. (Primed variant used internally.)
Composition of morphisms in AffineVarietyDom: defined by composing the
function-field pullbacks and then taking the induced rational map.
Instances For
The composition of two morphisms of AffineVarietyDom is itself dominant.
Associativity of composition of morphisms in AffineVarietyDom, needed for the
category instance.
Category structure on AffineVarietyDom k: objects are affine varieties (with
domain coordinate ring) and morphisms are dominant rational maps. Identities and
composition come from idMap and compMap, with the category laws established by
id_comp, comp_id, and comp_assoc.
Bundled function field over $\bar k$: a field which is a finitely generated $\bar k$-algebra. Used as the object type of the category of function fields.
- carrier : Type u_3
- algInst : Algebra (AlgebraicClosure k) self.carrier
- finitelyGenerated : Algebra.FiniteType (AlgebraicClosure k) self.carrier
Instances For
Coerce a FunctionFieldObj to its underlying field.
A morphism $F \to G$ in the category of function fields is a $\bar k$-algebra homomorphism $G \to F$ on the underlying fields (note the direction: the category is contravariant relative to the algebra-homomorphism direction).
Instances For
Category structure on FunctionFieldObj k: objects are finitely generated function
fields over $\bar k$ and morphisms are $\bar k$-algebra homomorphisms in the reversed
direction (so the resulting equivalence with AffineVarietyDom is covariant in this
formalisation).
The function field $\bar k(V) = \mathrm{Frac}(\bar k[V])$ of an affine variety $V$ is a finitely generated $\bar k$-algebra.
Object-level map for the function-field functor: an affine variety $V$ is sent to the bundled function field $\bar k(V)$.
Instances For
The function-field pullback $\varphi^*$ is $\bar k$-linear in the sense that $\varphi^*(c \cdot x) = c \cdot \varphi^*(x)$ for any constant $c \in \bar k$ and $x \in \bar k(W)$.
The function-field pullback morphism, packaged as a FunctionFieldObj.Hom: a
$\bar k$-algebra homomorphism $\bar k(W) \to \bar k(V)$ obtained from a dominant
rational map $f : V \dashrightarrow W$. This is the morphism part of the
function-field functor.
Instances For
The function-field pullback of the identity rational map on $V$ is the identity on $\bar k(V)$ (functoriality of the pullback on identities).
Contravariant functoriality of the function-field pullback: the pullback of the composition $g \circ f$ equals the composition $f^* \circ g^*$ of the pullbacks.
The contravariant function-field functor $\mathbf{AffVar} \to \mathbf{FFld}$ (here realised as a covariant functor $\mathbf{AffVar}^{\mathrm{op}} \to \mathbf{FFld}$ via the convention used in this file): sends an affine variety $V$ to its function field $\bar k(V)$ and a dominant rational map $f$ to its pullback $f^*$.
Instances For
Public wrapper for the fact that the function-field pullback is a $\bar k$-algebra homomorphism (i.e. fixes the image of every constant).
Injectivity of the function-field pullback on rational maps: two dominant rational maps between affine varieties that induce the same pullback on function fields must themselves be equal.
Every $\bar k$-algebra homomorphism $\theta : \bar k(W) \to \bar k(V)$ is in
particular a $\bar k$-function-field homomorphism in the sense of IsKbarFunctionFieldHom:
the algebra-map condition implies fixing the image of every constant.
Categorical version of the morphisms roundtrip: starting from a $\bar k$-algebra homomorphism $\theta : \bar k(W) \to \bar k(V)$, taking the induced rational map and then its function-field pullback recovers $\theta$.
The function-field functor is faithful: it is injective on morphisms between any
two objects, by pullback_injective_on_maps.
The function-field functor is full: every $\bar k$-algebra homomorphism on function fields comes from a (unique) dominant rational map between the underlying varieties.
Essential surjectivity of the function-field functor on objects: every finitely generated function field over $\bar k$ is isomorphic to $\bar k(V)$ for some affine variety $V$ (this expresses the "geometric" side of Corollary 15.9).
Packaged essential surjectivity of the function-field functor.
Corollary 15.9 (functor is an equivalence). The function-field functor is full, faithful and essentially surjective, hence an equivalence of categories between $\mathbf{AffVar}$ (affine varieties with dominant rational maps) and $\mathbf{FFld}$ (finitely generated function fields over $\bar k$).
The categorical equivalence packaged as a CategoryTheory.Equivalence between
$\mathbf{AffineVarietyDom}\;k$ and $\mathbf{FunctionFieldObj}\;k$.
Instances For
Corollary 15.9 (final form). The category of affine varieties (with dominant rational maps) is equivalent to the category of finitely generated function fields over $\bar k$.
Instances For
If $\varphi : X \dashrightarrow Y$ and $\psi : Y \dashrightarrow X$ are dominant rational maps whose composition $\psi \circ \varphi$ is the identity on its domain in $X$, then the composition of their function-field pullbacks is the identity on $\bar k(X)$.
Categorical inverses give pointwise inverses on the domain of composition: if
$f : V \to W$ and $g : W \to V$ in AffineVarietyDom satisfy $g \circ f = \mathrm{id}_V$,
then $g(f(P)) = P$ for every $P$ where the composition is defined.
Two affine varieties (with domain coordinate rings) are birationally equivalent
in the sense of Definition 15.10 iff they are isomorphic in the category
AffineVarietyDom k.
Convert a categorical isomorphism in FunctionFieldObj to a $\bar k$-algebra
isomorphism of the underlying function fields.
Instances For
Inverse of functionFieldIsoToAlgEquiv: convert a $\bar k$-algebra isomorphism
of function fields to an isomorphism in FunctionFieldObj.
Instances For
Corollary 15.11 (forward direction). If $V$ and $W$ are birationally equivalent affine varieties, then their function fields $\bar k(V)$ and $\bar k(W)$ are isomorphic as $\bar k$-algebras.
Instances For
Corollary 15.11 (reverse direction). If the function fields $\bar k(V)$ and $\bar k(W)$ are $\bar k$-algebra isomorphic, then $V$ and $W$ are birationally equivalent.