noncomputable def evalOnCoordRing (k : Type u_1) [Field k] {n : ℕ} (X : Set (Fin n → AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ X) : AffineCoordinateRingBar X →+* AlgebraicClosure k

Evaluation at a point $P \in X$ as a ring homomorphism $\bar{k}[X] \to \bar{k}$ from the coordinate ring.

@[simp]

theorem evalOnCoordRing_mk (k : Type u_1) [Field k] {n : ℕ} (X : Set (Fin n → AlgebraicClosure k)) (P : Fin n → AlgebraicClosure k) (hP : P ∈ X) (g : MvPolynomial (Fin n) (AlgebraicClosure k)) : (evalOnCoordRing k X P hP) ((Ideal.Quotient.mk (idealOfAlgebraicSet X)) g) = (MvPolynomial.eval P) g

Evaluating the class of $g$ in the coordinate ring gives $g(P)$.

theorem bind₁_mem_idealOfAlgebraicSet_of_maps_to (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (hmaps : ∀ P ∈ X, polyMapEval k m n polys P ∈ Y) {f : MvPolynomial (Fin n) (AlgebraicClosure k)} (hf : f ∈ idealOfAlgebraicSet Y) : (MvPolynomial.bind₁ polys) f ∈ idealOfAlgebraicSet X

If a polynomial map sends $X$ into $Y$, then its substitution operator $\mathrm{bind}_1$ pulls back the vanishing ideal of $Y$ into the vanishing ideal of $X$.

noncomputable def AffineMorphism.pullback (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) : AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X

The pullback ring homomorphism $\varphi^* : \bar{k}[Y] \to \bar{k}[X]$ induced by an affine morphism $\varphi : X \to Y$.

@[simp]

theorem AffineMorphism.pullback_mk (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) (g : MvPolynomial (Fin n) (AlgebraicClosure k)) : (pullback k φ) ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g) = (Ideal.Quotient.mk (idealOfAlgebraicSet X)) ((MvPolynomial.bind₁ φ.polys) g)

Pullback acts on the class of $g$ by substituting the components of $\varphi$ into $g$.

theorem AffineMorphism.pullback_eval (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) (g : MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k m) (hP : P ∈ X) : (evalOnCoordRing k X P hP) ((pullback k φ) ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g)) = (evalOnCoordRing k Y (toFun k φ P) ⋯) ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g)

Evaluation commutes with pullback: $\mathrm{ev}_P(\varphi^* g) = \mathrm{ev}_{\varphi(P)}(g)$.

theorem ringHom_eq_eval_of_alg (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (θ : AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X) (hθ_alg : ∀ (r : AlgebraicClosure k), θ ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) (MvPolynomial.C r)) = (Ideal.Quotient.mk (idealOfAlgebraicSet X)) (MvPolynomial.C r)) (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)) (hpolys : ∀ (j : Fin n), (Ideal.Quotient.mk (idealOfAlgebraicSet X)) (polys j) = θ ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) (MvPolynomial.X j))) (P : AffineSpace_k k m) (hP : P ∈ X) : (evalOnCoordRing k X P hP).comp (θ.comp (Ideal.Quotient.mk (idealOfAlgebraicSet Y))) = MvPolynomial.eval (polyMapEval k m n polys P)

Any $\bar{k}$-algebra map $\theta : \bar{k}[Y] \to \bar{k}[X]$ is determined on the variable classes; evaluating $\mathrm{ev}_P \circ \theta$ at the class of $g$ equals evaluating $g$ at the point given by the chosen polynomial lifts.

theorem algebraHom_induces_morphism (k : Type u_1) [Field k] {m n : ℕ} {X : Set (AffineSpace_k k m)} {Y : Set (AffineSpace_k k n)} (hY : Y = AlgebraicSet k n ↑(idealOfAlgebraicSet Y)) (θ : AffineCoordinateRingBar Y →+* AffineCoordinateRingBar X) (hθ_alg : ∀ (r : AlgebraicClosure k), θ ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) (MvPolynomial.C r)) = (Ideal.Quotient.mk (idealOfAlgebraicSet X)) (MvPolynomial.C r)) : ∃ (polys : Fin n → MvPolynomial (Fin m) (AlgebraicClosure k)), (∀ P ∈ X, polyMapEval k m n polys P ∈ Y) ∧ ∀ (g : MvPolynomial (Fin n) (AlgebraicClosure k)) (P : AffineSpace_k k m) (hP : P ∈ X), (evalOnCoordRing k X P hP) (θ ((Ideal.Quotient.mk (idealOfAlgebraicSet Y)) g)) = (MvPolynomial.eval (polyMapEval k m n polys P)) g

(Corollary 14.9 / 15.9) Every $\bar{k}$-algebra homomorphism $\theta : \bar{k}[Y] \to \bar{k}[X]$ is induced by an affine morphism: there exist polynomials whose induced map sends $X$ into $Y$ and whose pullback is $\theta$.

theorem AffineMorphism.pullback_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)} (ψ : AffineMorphism k n r Y Z) (φ : AffineMorphism k m n X Y) : pullback k (comp k ψ φ) = (pullback k φ).comp (pullback k ψ)

The pullback is contravariantly functorial: $(\psi \circ \varphi)^* = \varphi^* \circ \psi^*$.