The equivalence relation on $\bar k^{n+1} \setminus \{0\}$ identifying two nonzero tuples that differ by a nonzero scalar; the quotient is projective $n$-space $\mathbb{P}^n(\bar k)$.
Instances For
The set of $k$-rational points $\mathbb{P}^n(k) \subseteq \mathbb{P}^n(\bar k)$: those projective points admitting a representative all of whose coordinates lie in the image of $k \hookrightarrow \bar k$.
Instances For
A homogeneous polynomial of some degree $d$ in $n+1$ variables over $\bar k$: the package of an underlying polynomial together with the degree witness.
- poly : MvPolynomial (Fin (n + 1)) (AlgebraicClosure k)
- deg : ℕ
- isHomog : self.poly.IsHomogeneous self.deg
Instances For
Rescaling identity for homogeneous polynomials: $f(cv_0, \ldots, cv_n) = c^d \cdot f(v_0, \ldots, v_n)$, where $d$ is the homogeneous degree of $f$.
The projective vanishing set $V(S) \subseteq \mathbb{P}^n(\bar k)$ of a family of homogeneous polynomials $S$: those points where every $f \in S$ vanishes (the rescaling identity ensures the condition descends to the quotient).
Instances For
A subset of $\mathbb{P}^n(\bar k)$ is projectively algebraic if it arises as the common vanishing locus of some family of homogeneous polynomials.
Instances For
The collection of all projectively algebraic subsets of $\mathbb{P}^n(\bar k)$; its members serve as the closed sets of the projective Zariski topology.
Instances For
The empty set is projectively algebraic: it is cut out by the polynomial $1$, which has no zeros.
Arbitrary intersections of projectively algebraic sets are projectively algebraic: union the underlying homogeneous polynomial families.
The union of two projectively algebraic sets is projectively algebraic: take pairwise products of the defining homogeneous polynomials.
The projective Zariski topology on $\mathbb{P}^n(\bar k)$: closed sets are exactly the projectively algebraic subsets.
Instances For
The preimage of an algebraic set under a polynomial map is again algebraic:
$(\Phi)^{-1}V(S) = V(\Phi^*S)$, where $\Phi^* f = f \circ \Phi$ is computed via
bind₁.
The preimage of an algebraic subset under an affine morphism $\varphi$ is
again algebraic: pull back the defining polynomials along φ.polys.
Theorem 14.4. Every affine morphism $\varphi: X \to Y$ between algebraic subsets is continuous with respect to the Zariski topologies.
Definition 14.6. An affine isomorphism $X \cong Y$ consists of mutually inverse affine morphisms $X \to Y$ and $Y \to X$.
- toMorphism : AffineMorphism k m n X Y
- invMorphism : AffineMorphism k n m Y X
- left_inv (Q : AffineSpace_k k n) : Q ∈ Y → AffineMorphism.toFun k self.toMorphism (AffineMorphism.toFun k self.invMorphism Q) = Q
- right_inv (P : AffineSpace_k k m) : P ∈ X → AffineMorphism.toFun k self.invMorphism (AffineMorphism.toFun k self.toMorphism P) = P
Instances For
Two algebraic subsets $X$ and $Y$ are isomorphic as affine varieties if there exists an affine isomorphism between them.
Instances For
An affine morphism $f$ is an isomorphism iff it admits an affine inverse $g$ in the morphism sense (mutually inverse on the underlying point sets).
Instances For
Reflexivity for the isomorphism relation: the identity morphism realises $X \cong X$.
Instances For
Symmetry: an isomorphism $X \cong Y$ inverts to an isomorphism $Y \cong X$.
Instances For
Transitivity: composition of two affine isomorphisms is an affine isomorphism.
Instances For
Compatibility lemma for the contravariant equivalence: when a ring homomorphism $\theta: \bar k[Y] \to \bar k[X]$ is induced by polynomial maps $\mathrm{polys}$, the pullback of the resulting morphism agrees with $\theta$ upon evaluation on the coordinate ring.
Conversely: if the pullback of an affine morphism $\varphi$ is realised by
polynomial maps polys', then polys' agrees with φ.polys on the underlying
point set.
A ring homomorphism between coordinate rings over $\bar k$ is $\bar k$-algebra preserving if it fixes the scalar subring, i.e. sends $\bar r \in \bar k[Y]$ to $\bar r \in \bar k[X]$ for every $r \in \bar k$.
Instances For
Theorem 14.8 (data). A bundle of data witnessing the contravariant equivalence between affine varieties (and their morphisms) and their coordinate rings (with $\bar k$-algebra homomorphisms): a functor in each direction together with round-trip identities.
- coordRingFunctor : AffineMorphism k m n X Y → AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X
- coordRingFunctor_isAlgHom (φ : AffineMorphism k m n X Y) : IsAlgHomBar k (self.coordRingFunctor φ)
- varietyFunctor {θ : AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X} : IsAlgHomBar k θ → AffineMorphism k m n X Y
- functoriality {r : ℕ} {Z : Set (AffineSpace_k k r)} (ψ : AffineMorphism k n r Y Z) (φ : AffineMorphism k m n X Y) : AffineMorphism.pullback k (AffineMorphism.comp k ψ φ) = (AffineMorphism.pullback k φ).comp (AffineMorphism.pullback k ψ)
- roundTrip_algHom (θ : AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X) (hθ : IsAlgHomBar k θ) (g : MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k m) (hP : P ∈ X) : (evalOnCoordRing k X P hP) ((self.coordRingFunctor (self.varietyFunctor hθ)) ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g)) = (evalOnCoordRing k X P hP) (θ ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g))
- roundTrip_morphism (φ : AffineMorphism k m n X Y) (hφ : IsAlgHomBar k (self.coordRingFunctor φ)) (P : AffineSpace_k k m) (hP : P ∈ X) : AffineMorphism.toFun k (self.varietyFunctor hφ) P = AffineMorphism.toFun k φ P
Instances For
Corollary 14.9. Assuming $Y = V(I(Y))$, the construction $\varphi \mapsto \varphi^*$ together with its inverse $\theta \mapsto \theta^*$ exhibits a contravariant equivalence between the category of affine morphisms $X \to Y$ and the category of $\bar k$-algebra homomorphisms $\bar k[Y] \to \bar k[X]$.
Instances For
Axiom: any two nonempty affine charts of a projective variety have canonically isomorphic coordinate rings over $\bar k$.
Instances For
Axiom: the coordinate-ring isomorphism between two affine charts of a projective variety is a $\bar k$-algebra map.
Axiom: the inverse of the coordinate-ring isomorphism between two affine charts is also a $\bar k$-algebra map.
The function fields of any two nonempty affine charts of a projective variety are isomorphic, obtained by passing the coordinate-ring isomorphism to fraction fields.
Existential restatement: the coordinate rings of any two nonempty affine charts of a projective variety are isomorphic.
Each affine chart of a projective vanishing set is itself an algebraic subset, cut out by the dehomogenizations of the original polynomials.
Reverse direction of the categorical equivalence: a $\bar k$-algebra isomorphism between coordinate rings $\bar k[X] \cong \bar k[Y]$ induces an isomorphism of affine varieties $X \cong Y$.
A family of homogeneous polynomials $S$ defines a projective variety if its projective vanishing locus is a projective variety in the structural sense.
Instances For
Axiom: the vanishing ideal of an affine chart of a projective variety is the image of a homogeneous prime ideal under the dehomogenization map.
Every nonempty affine chart of a projective variety is itself an affine variety (algebraic and irreducible), following from Theorem 13.24 applied to the dehomogenization map.
Corollary 14.10. Any two nonempty affine charts of the same projective variety are isomorphic as affine varieties.
An affine morphism is defined over $k$ if each of its component polynomials lies in the image of $k[X_1, \ldots, X_m] \hookrightarrow \bar k[X_1, \ldots, X_m]$.
Instances For
An affine isomorphism is defined over $k$ if both its forward and inverse morphisms are.
Instances For
Two affine varieties are isomorphic over $k$ if there exists an affine isomorphism between them which is defined over $k$.
Instances For
If an affine morphism mapping $X$ into $Y$ is defined over $k$, then pullback along it sends the $k$-vanishing ideal of $Y$ into that of $X$: $f \in I_k(Y) \Rightarrow f \circ \mathrm{polys}_K \in I_k(X)$.
The pullback over $k$ of an affine morphism $\varphi$ that is defined over $k$: the induced $k$-algebra map $k[Y] \to k[X]$ between $k$-coordinate rings.