structure ProjectiveRegularFunction.HomogeneousRep (n : ℕ) (k : Type u_2) [Field k] : Type u_2

A homogeneous representative of a projective regular function: a pair of homogeneous polynomials $(\text{num}, \text{den})$ of the same degree on $\mathbb{P}^n$, with $\text{den} \neq 0$, representing the rational function $\text{num}/\text{den}$.

• num : MvPolynomial (Fin (n + 1)) k
• den : MvPolynomial (Fin (n + 1)) k
• deg : ℕ
• num_homog : self.num.IsHomogeneous self.deg
• den_homog : self.den.IsHomogeneous self.deg
• den_ne_zero : self.den ≠ 0

def ProjectiveRegularFunction.HomogeneousRep.isDefinedAt {n : ℕ} (k : Type u_1) [Field k] (r : HomogeneousRep n k) (P : Projectivization k (Fin (n + 1) → k)) : Prop

A homogeneous representative is defined at a projective point $P$ if its denominator does not vanish at $P$.

noncomputable def ProjectiveRegularFunction.HomogeneousRep.evalAt {n : ℕ} (k : Type u_1) [Field k] (r : HomogeneousRep n k) (P : Projectivization k (Fin (n + 1) → k)) : k

Evaluate a homogeneous representative $\text{num}/\text{den}$ at a projective point $P$. Well-defined when the denominator is nonzero.

def ProjectiveRegularFunction.HomogeneousRep.equivOn {n : ℕ} (k : Type u_1) [Field k] (r₁ r₂ : HomogeneousRep n k) (X : Set (Projectivization k (Fin (n + 1) → k))) : Prop

Two homogeneous representatives are equivalent on a set $X$ iff $\text{num}_1 \cdot \text{den}_2 - \text{num}_2 \cdot \text{den}_1$ vanishes on $X$ (i.e., they define the same rational function on $X$).

theorem ProjectiveRegularFunction.HomogeneousRep.equivOn_refl {n : ℕ} (k : Type u_1) [Field k] (r : HomogeneousRep n k) (X : Set (Projectivization k (Fin (n + 1) → k))) : equivOn k r r X

Reflexivity: any homogeneous representative is equivalent to itself on $X$.

theorem ProjectiveRegularFunction.HomogeneousRep.equivOn_symm {n : ℕ} (k : Type u_1) [Field k] (r₁ r₂ : HomogeneousRep n k) (X : Set (Projectivization k (Fin (n + 1) → k))) (h : equivOn k r₁ r₂ X) : equivOn k r₂ r₁ X

Symmetry of equivOn: if $r_1 \sim r_2$ on $X$ then $r_2 \sim r_1$ on $X$.

theorem ProjectiveRegularFunction.HomogeneousRep.equivOn_trans {n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (n' + 1) → k'))} (r₁ r₂ r₃ : HomogeneousRep n' k') (h₁₂ : equivOn k' r₁ r₂ X) (h₂₃ : equivOn k' r₂ r₃ X) (hirr : ∀ (p q : MvPolynomial (Fin (n' + 1)) k'), (∀ P ∈ X, (MvPolynomial.eval P.rep) (p * q) = 0) → (∀ P ∈ X, (MvPolynomial.eval P.rep) p = 0) ∨ ∀ P ∈ X, (MvPolynomial.eval P.rep) q = 0) (h₂_nondeg : (¬∀ P ∈ X, (MvPolynomial.eval P.rep) r₂.num = 0) ∨ ¬∀ P ∈ X, (MvPolynomial.eval P.rep) r₂.den = 0) : equivOn k' r₁ r₃ X

Transitivity of equivOn, using primality of the vanishing ideal of $X$ (an irreducibility hypothesis) plus a nondegeneracy condition on $r_2$.

theorem ProjectiveRegularFunction.projectiveVariety_vanishing_ideal_prime {n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (n' + 1) → k'))} (p q : MvPolynomial (Fin (n' + 1)) k') : (∀ P ∈ X, (MvPolynomial.eval P.rep) (p * q) = 0) → (∀ P ∈ X, (MvPolynomial.eval P.rep) p = 0) ∨ ∀ P ∈ X, (MvPolynomial.eval P.rep) q = 0

Axiom: the vanishing ideal of a projective variety $X$ is prime — if $pq$ vanishes on $X$, then $p$ vanishes on $X$ or $q$ does. Used implicitly throughout for irreducibility arguments.

theorem ProjectiveRegularFunction.HomogeneousRep.equivOn_trans' {n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (n' + 1) → k'))} (r₁ r₂ r₃ : HomogeneousRep n' k') (h₁₂ : equivOn k' r₁ r₂ X) (h₂₃ : equivOn k' r₂ r₃ X) : equivOn k' r₁ r₃ X

Cleaner transitivity statement: on a projective variety $X$, equivOn is transitive (the irreducibility hypothesis is inherited from the variety).

theorem ProjectiveRegularFunction.HomogeneousRep.evalAt_eq_of_equivOn {n : ℕ} (k : Type u_1) [Field k] (r₁ r₂ : HomogeneousRep n k) (X : Set (Projectivization k (Fin (n + 1) → k))) (P : Projectivization k (Fin (n + 1) → k)) (hPX : P ∈ X) (hequiv : equivOn k r₁ r₂ X) (h₁ : isDefinedAt k r₁ P) (h₂ : isDefinedAt k r₂ P) : evalAt k r₁ P = evalAt k r₂ P

Two equivalent homogeneous representatives evaluate to the same value at any common point of definition.

structure ProjectiveRegularFunction.ProjectiveRatFun (n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

A projective rational function on a set $X \subseteq \mathbb{P}^n_k$: an equivalence class of homogeneous representatives, packaged as a maximal nonempty set of mutually equivalent HomogeneousReps.

• reps : Set (HomogeneousRep n k)
• reps_nonempty : self.reps.Nonempty
• reps_equiv (r₁ : HomogeneousRep n k) : r₁ ∈ self.reps → ∀ r₂ ∈ self.reps, HomogeneousRep.equivOn k r₁ r₂ X
• reps_maximal (r : HomogeneousRep n k) : (∃ r₀ ∈ self.reps, HomogeneousRep.equivOn k r r₀ X) → r ∈ self.reps

theorem ProjectiveRegularFunction.ProjectiveRatFun.den_not_vanish_on {n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (n' + 1) → k'))} (r : ProjectiveRatFun n' k' X) (rep : HomogeneousRep n' k') (hrep : rep ∈ r.reps) : ¬∀ P ∈ X, (MvPolynomial.eval P.rep) rep.den = 0

The denominator of any representative of a projective rational function does not vanish identically on $X$ (else the function would be undefined everywhere).

def ProjectiveRegularFunction.ProjectiveRatFun.IsRegularAt {n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (n + 1) → k))} (r : ProjectiveRatFun n k X) (P : Projectivization k (Fin (n + 1) → k)) (_hP : P ∈ X) : Prop

A projective rational function is regular at a point $P \in X$ iff some representative is defined at $P$.

def ProjectiveRegularFunction.ProjectiveRatFun.regularDomain {n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (n + 1) → k))} (r : ProjectiveRatFun n k X) : Set (Projectivization k (Fin (n + 1) → k))

The regular domain (locus of regularity) of a projective rational function: all points of $X$ where some representative is defined.

theorem ProjectiveRegularFunction.ProjectiveRatFun.mem_regularDomain_iff {n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (n + 1) → k))} (r : ProjectiveRatFun n k X) (P : Projectivization k (Fin (n + 1) → k)) : P ∈ regularDomain k r ↔ ∃ (hP : P ∈ X), IsRegularAt k r P hP

Unfolding lemma: $P$ is in the regular domain of $r$ iff $P \in X$ and $r$ is regular at $P$.

noncomputable def ProjectiveRegularFunction.ProjectiveRatFun.evalAt {n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (n + 1) → k))} (r : ProjectiveRatFun n k X) (P : Projectivization k (Fin (n + 1) → k)) (hP : P ∈ regularDomain k r) : k

Evaluate a projective rational function $r$ at a point $P$ in its regular domain by choosing any representative defined at $P$ and evaluating it.

theorem ProjectiveRegularFunction.ProjectiveRatFun.evalAt_eq_rep {n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (n + 1) → k))} (r : ProjectiveRatFun n k X) (P : Projectivization k (Fin (n + 1) → k)) (hP : P ∈ regularDomain k r) (rep : HomogeneousRep n k) (hrep : rep ∈ r.reps) (hdef : HomogeneousRep.isDefinedAt k rep P) : evalAt k r P hP = HomogeneousRep.evalAt k rep P

The value of $r$ at $P$ agrees with the value computed from any representative defined at $P$.

structure ProjectiveRatMap.RationalMapTupleRep (m n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (m + 1) → k))) (Y : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

A tuple representative of a rational map $X \dashrightarrow Y$ between projective varieties: an $(n+1)$-tuple of homogeneous polynomials of common degree, not all vanishing on $X$, whose evaluation lands in $Y$ (as a projective point).

• polys : Fin (n + 1) → MvPolynomial (Fin (m + 1)) k
• deg : ℕ
• polys_homog (i : Fin (n + 1)) : (self.polys i).IsHomogeneous self.deg
• not_all_vanish : ∃ (i : Fin (n + 1)), ∃ P ∈ X, (MvPolynomial.eval P.rep) (self.polys i) ≠ 0
• image_in_Y (P : Projectivization k (Fin (m + 1) → k)) : P ∈ X → (∃ (i : Fin (n + 1)), (MvPolynomial.eval P.rep) (self.polys i) ≠ 0) → ∀ (f : MvPolynomial (Fin (n + 1)) k), (∀ Q ∈ Y, (MvPolynomial.eval Q.rep) f = 0) → (MvPolynomial.eval fun (j : Fin (n + 1)) => (MvPolynomial.eval P.rep) (self.polys j)) f = 0

def ProjectiveRatMap.RationalMapTupleRep.isDefinedAt {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : RationalMapTupleRep m n k X Y) (P : Projectivization k (Fin (m + 1) → k)) : Prop

A tuple representative is defined at $P$ iff at least one coordinate polynomial is nonzero at $P$.

noncomputable def ProjectiveRatMap.RationalMapTupleRep.evalVec {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : RationalMapTupleRep m n k X Y) (P : Projectivization k (Fin (m + 1) → k)) : Fin (n + 1) → k

The vector of values $(\varphi_0(P), \dots, \varphi_n(P))$ of a tuple representative at $P$.

def ProjectiveRatMap.RationalMapTupleRep.equivOn {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ ψ : RationalMapTupleRep m n k X Y) : Prop

Two tuple representatives are equivalent on $X$ iff $\varphi_i \psi_j - \varphi_j \psi_i$ vanishes on $X$ for all $i, j$ (i.e., they define the same projective point at every point of $X$).

theorem ProjectiveRatMap.RationalMapTupleRep.equivOn_refl {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : RationalMapTupleRep m n k X Y) : equivOn k φ φ

Reflexivity of tuple equivalence.

theorem ProjectiveRatMap.RationalMapTupleRep.equivOn_symm {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ ψ : RationalMapTupleRep m n k X Y) (h : equivOn k φ ψ) : equivOn k ψ φ

Symmetry of tuple equivalence.

theorem ProjectiveRatMap.RationalMapTupleRep.equivOn_trans {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ ψ χ : RationalMapTupleRep m n k X Y) (h₁ : equivOn k φ ψ) (h₂ : equivOn k ψ χ) (hirr : ∀ (p q : MvPolynomial (Fin (m + 1)) k), (∀ P ∈ X, (MvPolynomial.eval P.rep) (p * q) = 0) → (∀ P ∈ X, (MvPolynomial.eval P.rep) p = 0) ∨ ∀ P ∈ X, (MvPolynomial.eval P.rep) q = 0) (h₂_nondeg : ∃ (a : Fin (n + 1)), ¬∀ P ∈ X, (MvPolynomial.eval P.rep) (ψ.polys a) = 0) : equivOn k φ χ

Transitivity of tuple equivalence on $X$, using primality of the vanishing ideal plus a nondegeneracy hypothesis on $\psi$.

theorem ProjectiveRatMap.RationalMapTupleRep.equivOn_trans' {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ ψ χ : RationalMapTupleRep m n k X Y) (h₁ : equivOn k φ ψ) (h₂ : equivOn k ψ χ) : equivOn k φ χ

Cleaner transitivity statement: on a projective variety $X$, equivOn is transitive (using primality of the vanishing ideal).

structure ProjectiveRatMap.ProjectiveRationalMap (m n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (m + 1) → k))) (Y : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

A projective rational map $X \dashrightarrow Y$: an equivalence class of RationalMapTupleReps, packaged as a maximal nonempty equivalence class.

• reps : Set (RationalMapTupleRep m n k X Y)
• reps_nonempty : self.reps.Nonempty
• reps_equiv (φ₁ : RationalMapTupleRep m n k X Y) : φ₁ ∈ self.reps → ∀ φ₂ ∈ self.reps, RationalMapTupleRep.equivOn k φ₁ φ₂
• reps_maximal (φ : RationalMapTupleRep m n k X Y) : (∃ φ₀ ∈ self.reps, RationalMapTupleRep.equivOn k φ φ₀) → φ ∈ self.reps

def ProjectiveRatMap.ProjectiveRationalMap.IsRegularAt {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) (P : Projectivization k (Fin (m + 1) → k)) (_hP : P ∈ X) : Prop

A projective rational map is regular at $P \in X$ iff some representative is defined at $P$.

def ProjectiveRatMap.ProjectiveRationalMap.regularDomain {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) : Set (Projectivization k (Fin (m + 1) → k))

The regular domain of a projective rational map: the locus of points of $X$ where it is regular.

theorem ProjectiveRatMap.ProjectiveRationalMap.mem_regularDomain_iff {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) (P : Projectivization k (Fin (m + 1) → k)) : P ∈ regularDomain k φ ↔ ∃ (hP : P ∈ X), IsRegularAt k φ P hP

Unfolding lemma: $P$ is in the regular domain of $\varphi$ iff $P \in X$ and $\varphi$ is regular at $P$.

def ProjectiveRatMap.ProjectiveRationalMap.IsMorphism {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) : Prop

A projective rational map is a morphism iff it is regular at every point of its domain $X$.

structure ProjectiveRatMap.ProjectiveMorphism (m n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (m + 1) → k))) (Y : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

A projective morphism $X \to Y$: a projective rational map that is regular everywhere on $X$.

• toRatMap : ProjectiveRationalMap m n k X Y
• is_morphism : ProjectiveRationalMap.IsMorphism k self.toRatMap

def ProjectiveRatMap.ProjectiveRationalMap.image {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) : Set (Projectivization k (Fin (n + 1) → k))

The image of a projective rational map $\varphi: X \dashrightarrow Y$: points $Q \in Y$ that arise as $\varphi(P)$ for some $P$ in the regular domain.

def ProjectiveRatMap.IsZariskiDenseIn {n : ℕ} (k : Type u_2) [Field k] (S Y : Set (Projectivization k (Fin (n + 1) → k))) : Prop

$S$ is Zariski-dense in $Y$ iff any polynomial vanishing on $S$ also vanishes on $Y$ (i.e., $S$'s Zariski closure contains $Y$).

def ProjectiveRatMap.ProjectiveRationalMap.IsDominant {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRationalMap m n k X Y) : Prop

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

theorem ProjectiveThm1518.eval_bind₁ {k' : Type u_2} [CommSemiring k'] {σ : Type u_3} {τ : Type u_4} (v : τ → k') (f : σ → MvPolynomial τ k') (p : MvPolynomial σ k') : (MvPolynomial.eval v) ((MvPolynomial.bind₁ f) p) = (MvPolynomial.eval fun (i : σ) => (MvPolynomial.eval v) (f i)) p

Evaluation commutes with bind₁: evaluating $\text{bind}_1 f\, p$ at $v$ equals evaluating $p$ at the vector $i \mapsto \text{eval}\, v\, (f\, i)$.

theorem ProjectiveThm1518.bind₁_isHomogeneous {k' : Type u_2} [CommSemiring k'] {σ : Type u_3} {τ : Type u_4} {p : MvPolynomial σ k'} {dp : ℕ} (hp : p.IsHomogeneous dp) {f : σ → MvPolynomial τ k'} {df : ℕ} (hf : ∀ (i : σ), (f i).IsHomogeneous df) : ((MvPolynomial.bind₁ f) p).IsHomogeneous (df * dp)

If $p$ is homogeneous of degree $d_p$ and each $f_i$ is homogeneous of degree $d_f$, then $\text{bind}_1 f\, p$ is homogeneous of degree $d_f \cdot d_p$.

theorem ProjectiveThm1518.pullback_den_ne_zero {m' n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (m' + 1) → k'))} {Y : Set (Projectivization k' (Fin (n' + 1) → k'))} (φ : ProjectiveRatMap.ProjectiveRationalMap m' n' k' X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k' φ) (rep : ProjectiveRatMap.RationalMapTupleRep m' n' k' X Y) (hrep : rep ∈ φ.reps) (h : MvPolynomial (Fin (n' + 1)) k') (hh : ¬∀ P ∈ Y, (MvPolynomial.eval P.rep) h = 0) : (MvPolynomial.bind₁ rep.polys) h ≠ 0

The pullback of a polynomial that doesn't vanish identically on $Y$ via a dominant rational map is nonzero: a key nondegeneracy fact for defining the pullback ring homomorphism.

noncomputable def ProjectiveThm1518.pullbackHomogeneousRep {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (rep : ProjectiveRatMap.RationalMapTupleRep m n k X Y) (hrep : rep ∈ φ.reps) (hrfun : ProjectiveRegularFunction.HomogeneousRep n k) (hden_nonvanish : ¬∀ P ∈ Y, (MvPolynomial.eval P.rep) hrfun.den = 0) : ProjectiveRegularFunction.HomogeneousRep m k

Construct the pullback of a homogeneous representative on $Y$ via a dominant rational map $\varphi: X \dashrightarrow Y$: composition of the rational function with $\varphi$ yields a new homogeneous representative on $X$.

noncomputable def ProjectiveThm1518.dominantProjectiveRationalMapPullback {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) : ProjectiveRegularFunction.ProjectiveRatFun n k Y → ProjectiveRegularFunction.ProjectiveRatFun m k X

The pullback of projective rational functions along a dominant rational map: $\varphi^*: k(Y) \to k(X)$, sending $r$ to its composition with $\varphi$.

theorem ProjectiveThm1518.eval_scale_homog' {k' : Type u_2} [CommRing k'] {σ : Type u_3} (p : MvPolynomial σ k') (d : ℕ) (hp : p.IsHomogeneous d) (c : k') (v : σ → k') : (MvPolynomial.eval fun (i : σ) => c * v i) p = c ^ d * (MvPolynomial.eval v) p

Scaling lemma for homogeneous polynomials: if $p$ is homogeneous of degree $d$, then $p(c \cdot v) = c^d \cdot p(v)$.

theorem ProjectiveThm1518.pullback_eval_at_image {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (P : Projectivization k (Fin (m + 1) → k)) (hPX : P ∈ X) : ∃ (Q : Projectivization k (Fin (n + 1) → k)) (_ : Q ∈ Y), ∀ (r : ProjectiveRegularFunction.ProjectiveRatFun n k Y) (hPdom : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r)), ∃ (hQdom : Q ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r) P hPdom = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r Q hQdom

Compatibility: for $P \in X$ in the regular domain of $\varphi^* r$, there is a corresponding $Q = \varphi(P) \in Y$ in the regular domain of $r$ such that $(\varphi^* r)(P) = r(Q)$.

theorem ProjectiveThm1518.ProjectiveRatFun.ext_eval {n' : ℕ} {k' : Type u_2} [Field k'] {X : Set (Projectivization k' (Fin (n' + 1) → k'))} (r₁ r₂ : ProjectiveRegularFunction.ProjectiveRatFun n' k' X) : (∀ P ∈ X, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k' r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k' r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k' r₁ P hP₁ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k' r₂ P hP₂) → r₁ = r₂

Extensionality for projective rational functions: two projective rational functions on $X$ are equal iff they agree at every common point of their regular domains.

theorem ProjectiveThm1518.dominantProjectiveRationalMapPullback_map_eq {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (r₁ r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → dominantProjectiveRationalMapPullback k φ hdom r₁ = dominantProjectiveRationalMapPullback k φ hdom r₂

Pullback respects equality of projective rational functions: $r_1 = r_2$ (in the evaluation sense) implies $\varphi^* r_1 = \varphi^* r_2$.

theorem ProjectiveThm1518.dominantProjectiveRationalMapPullback_map_mul_eval {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (r₁ r₂ r₁r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂) (hP₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁r₂ P hP₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ * ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → ∀ P ∈ X, ∀ (hPθ₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₁)) (hPθ₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₂)) (hPθ₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₁r₂)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₁r₂) P hPθ₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₁) P hPθ₁ * ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₂) P hPθ₂

Pullback is multiplicative on values: if $r_1 r_2 = r_{1 \cdot 2}$ (pointwise on $Y$) then $\varphi^*(r_{1 \cdot 2}) = \varphi^* r_1 \cdot \varphi^* r_2$ (pointwise on $X$).

theorem ProjectiveThm1518.dominantProjectiveRationalMapPullback_map_add_eval {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (r₁ r₂ r₁r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂) (hP₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁r₂ P hP₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ + ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → ∀ P ∈ X, ∀ (hPθ₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₁)) (hPθ₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₂)) (hPθ₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r₁r₂)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₁r₂) P hPθ₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₁) P hPθ₁ + ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r₂) P hPθ₂

Pullback is additive on values: if $r_1 + r_2 = r_{1+2}$ (pointwise on $Y$) then $\varphi^*(r_{1+2}) = \varphi^* r_1 + \varphi^* r_2$ (pointwise on $X$).

theorem ProjectiveThm1518.dominantProjectiveRationalMapPullback_map_const_eval {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (c : k) (const_c : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k const_c), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k const_c P hP = c) → ∀ P ∈ X, ∀ (hP : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom const_c)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom const_c) P hP = c

Pullback preserves constants: if $r$ has constant value $c$ on $Y$, then $\varphi^* r$ has the same constant value $c$ on $X$.

structure ProjectiveThm1518.ProjectiveFunctionFieldHom (m n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (m + 1) → k))) (Y : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

A function-field homomorphism $k(Y) \to k(X)$ as data: a map on ProjectiveRatFun that is well-defined modulo equality of evaluations and that preserves the field structure (addition, multiplication, constants) in the pointwise evaluation sense.

• toFun : ProjectiveRegularFunction.ProjectiveRatFun n k Y → ProjectiveRegularFunction.ProjectiveRatFun m k X
• map_eq (r₁ r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → self.toFun r₁ = self.toFun r₂
• map_mul_eval (r₁ r₂ r₁r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂) (hP₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁r₂ P hP₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ * ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → ∀ P ∈ X, ∀ (hPθ₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₁)) (hPθ₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₂)) (hPθ₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₁r₂)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₁r₂) P hPθ₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₁) P hPθ₁ * ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₂) P hPθ₂
• map_add_eval (r₁ r₂ r₁r₂ : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₂) (hP₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k r₁r₂), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁r₂ P hP₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₁ P hP₁ + ProjectiveRegularFunction.ProjectiveRatFun.evalAt k r₂ P hP₂) → ∀ P ∈ X, ∀ (hPθ₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₁)) (hPθ₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₂)) (hPθ₁₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun r₁r₂)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₁r₂) P hPθ₁₂ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₁) P hPθ₁ + ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun r₂) P hPθ₂
• map_const_eval (c : k) (const_c : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : (∀ P ∈ Y, ∀ (hP : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k const_c), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k const_c P hP = c) → ∀ P ∈ X, ∀ (hP : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (self.toFun const_c)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (self.toFun const_c) P hP = c

noncomputable def ProjectiveThm1518.coordHomogRep (n : ℕ) (k : Type u_2) [Field k] (i : Fin (n + 1)) : ProjectiveRegularFunction.HomogeneousRep n k

The homogeneous representative for the $i$-th coordinate function $x_i/x_0$ on $\mathbb{P}^n$.

noncomputable def ProjectiveThm1518.coordRatFun (n : ℕ) (k : Type u_2) [Field k] (Y : Set (Projectivization k (Fin (n + 1) → k))) (i : Fin (n + 1)) : ProjectiveRegularFunction.ProjectiveRatFun n k Y

The projective rational function on $Y \subseteq \mathbb{P}^n$ given by the $i$-th coordinate $x_i/x_0$.

noncomputable def ProjectiveThm1518.inducedCoordRep {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) (i : Fin (n + 1)) : ProjectiveRegularFunction.HomogeneousRep m k

The chosen homogeneous representative of $\theta(x_i/x_0) \in k(X)$ given a function-field homomorphism $\theta: k(Y) \to k(X)$.

noncomputable def ProjectiveThm1518.inducedCommonDeg {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) : ℕ

The common degree shared by all the induced polynomials: the sum of the degrees of the coordinate representatives. Used to put all $\theta(x_i/x_0)$ on a common denominator.

noncomputable def ProjectiveThm1518.inducedPoly {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) (i : Fin (n + 1)) : MvPolynomial (Fin (m + 1)) k

The $i$-th coordinate polynomial of the projective map induced by $\theta$: the $i$-th numerator times the product of all other denominators (clearing denominators to common degree).

theorem ProjectiveThm1518.inducedPoly_homog {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) (i : Fin (n + 1)) : (inducedPoly k θ i).IsHomogeneous (inducedCommonDeg k θ)

Each induced polynomial is homogeneous of the common induced degree.

theorem ProjectiveThm1518.inducedPoly_not_all_vanish {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) : ∃ (i : Fin (n + 1)), ∃ P ∈ X, (MvPolynomial.eval P.rep) (inducedPoly k θ i) ≠ 0

The induced polynomials are not all vanishing on $X$: at some point $P \in X$ and some coordinate $i$, the induced polynomial is nonzero.

theorem ProjectiveThm1518.inducedPoly_image_in_Y {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) (P : Projectivization k (Fin (m + 1) → k)) : P ∈ X → (∃ (i : Fin (n + 1)), (MvPolynomial.eval P.rep) (inducedPoly k θ i) ≠ 0) → ∀ (f : MvPolynomial (Fin (n + 1)) k), (∀ Q ∈ Y, (MvPolynomial.eval Q.rep) f = 0) → (MvPolynomial.eval fun (j : Fin (n + 1)) => (MvPolynomial.eval P.rep) (inducedPoly k θ j)) f = 0

The induced polynomials land in $Y$: for any $P \in X$ where they don't all vanish, the resulting point $(\text{inducedPoly}_j(P))_j$ lies on the projective variety $Y$.

noncomputable def ProjectiveThm1518.functionFieldMorphismInducedProjectiveMap {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) : ProjectiveRatMap.ProjectiveRationalMap m n k X Y

Given a function-field homomorphism $\theta: k(Y) \to k(X)$, construct the corresponding projective rational map $X \dashrightarrow Y$ using the induced coordinate polynomials.

theorem ProjectiveThm1518.functionFieldMorphismInducedProjectiveMap_isDominant {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k (functionFieldMorphismInducedProjectiveMap k θ)

The projective rational map induced by a function-field homomorphism is automatically dominant.

noncomputable def ProjectiveThm1518.dominantProjectiveRationalMapPullbackHom {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) : ProjectiveFunctionFieldHom m n k X Y

Package the pullback of a dominant rational map together with its compatibility with addition, multiplication, constants, and equality into a ProjectiveFunctionFieldHom.

theorem ProjectiveThm1518.dominantProjectiveRationalMapPullbackHom_toFun {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) : (dominantProjectiveRationalMapPullbackHom k φ hdom).toFun = dominantProjectiveRationalMapPullback k φ hdom

The toFun of the packaged pullback hom is the underlying pullback map.

theorem ProjectiveThm1518.theorem_15_18_part_iii {m n : ℕ} (k : Type u_1) [Field k] {l : ℕ} {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} {Z : Set (Projectivization k (Fin (l + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (ψ : ProjectiveRatMap.ProjectiveRationalMap n l k Y Z) (hdomφ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (hdomψ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k ψ) (ψφ : ProjectiveRatMap.ProjectiveRationalMap m l k X Z) (hdomψφ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k ψφ) (hcomp : ∀ P ∈ X, ∀ repφ ∈ φ.reps, ∀ repψ ∈ ψ.reps, ∀ repψφ ∈ ψφ.reps, ProjectiveRatMap.RationalMapTupleRep.isDefinedAt k repφ P → ProjectiveRatMap.RationalMapTupleRep.isDefinedAt k repψφ P → ∀ (i j : Fin (l + 1)), ProjectiveRatMap.RationalMapTupleRep.evalVec k repψφ P i * (MvPolynomial.eval (ProjectiveRatMap.RationalMapTupleRep.evalVec k repφ P)) (repψ.polys j) = ProjectiveRatMap.RationalMapTupleRep.evalVec k repψφ P j * (MvPolynomial.eval (ProjectiveRatMap.RationalMapTupleRep.evalVec k repφ P)) (repψ.polys i)) (r : ProjectiveRegularFunction.ProjectiveRatFun l k Z) : dominantProjectiveRationalMapPullback k ψφ hdomψφ r = dominantProjectiveRationalMapPullback k φ hdomφ (dominantProjectiveRationalMapPullback k ψ hdomψ r)

Theorem 15.18, part (iii) — functoriality of the pullback: $(\psi \circ \varphi)^* = \varphi^* \circ \psi^*$ on projective rational functions, under a compatibility hypothesis between the compositional and direct representatives.

theorem ProjectiveThm1518.corollary_15_9_projective_roundtrip_maps {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) : have pullbackHom := dominantProjectiveRationalMapPullbackHom k φ hdom; have φ' := functionFieldMorphismInducedProjectiveMap k pullbackHom; ∀ rep₁ ∈ φ.reps, ∀ rep₂ ∈ φ'.reps, ProjectiveRatMap.RationalMapTupleRep.equivOn k rep₁ rep₂

Corollary 15.9, projective roundtrip for maps: starting from a dominant rational map $\varphi$, taking the pullback hom, then re-inducing a projective map recovers an equivalent map (same tuple-class).

theorem ProjectiveThm1518.pullback_induced_eval_eq {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) (r : ProjectiveRegularFunction.ProjectiveRatFun n k Y) : let φ := functionFieldMorphismInducedProjectiveMap k θ; have hdom := ⋯; ∀ P ∈ X, ∀ (hP₁ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (dominantProjectiveRationalMapPullback k φ hdom r)) (hP₂ : P ∈ ProjectiveRegularFunction.ProjectiveRatFun.regularDomain k (θ.toFun r)), ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (dominantProjectiveRationalMapPullback k φ hdom r) P hP₁ = ProjectiveRegularFunction.ProjectiveRatFun.evalAt k (θ.toFun r) P hP₂

Key compatibility: the pullback of the projective map induced by a function-field hom $\theta$ agrees pointwise with $\theta$ on values.

theorem ProjectiveThm1518.corollary_15_9_projective_roundtrip_morphisms {m n : ℕ} (k : Type u_1) [Field k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (θ : ProjectiveFunctionFieldHom m n k X Y) : let φ := functionFieldMorphismInducedProjectiveMap k θ; have hdom := ⋯; ∀ (r : ProjectiveRegularFunction.ProjectiveRatFun n k Y), dominantProjectiveRationalMapPullback k φ hdom r = θ.toFun r

Corollary 15.9, projective roundtrip for morphisms: starting from a function-field hom $\theta$, inducing the projective map and pulling back recovers $\theta$ exactly.

structure ProjectiveThm1518.ProjectiveContravariantEquivalence (m n : ℕ) (k : Type u_2) [Field k] (X : Set (Projectivization k (Fin (m + 1) → k))) (Y : Set (Projectivization k (Fin (n + 1) → k))) : Type u_2

Bundles the contravariant equivalence between dominant projective rational maps $X \dashrightarrow Y$ and function-field homomorphisms $k(Y) \to k(X)$: a pullback in one direction, an induced map in the other, plus the two roundtrip identities and a functoriality compatibility.

• pullback (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ → ProjectiveFunctionFieldHom m n k X Y
• inducedMap : ProjectiveFunctionFieldHom m n k X Y → { φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y // ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ }
• roundtrip_maps (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (hdom : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) : let φ' := ↑(self.inducedMap (self.pullback φ hdom)); ∀ rep₁ ∈ φ.reps, ∀ rep₂ ∈ φ'.reps, ProjectiveRatMap.RationalMapTupleRep.equivOn k rep₁ rep₂
• roundtrip_morphisms (θ : ProjectiveFunctionFieldHom m n k X Y) : let φ := ↑(self.inducedMap θ); let hdom := ⋯; ∀ (r : ProjectiveRegularFunction.ProjectiveRatFun n k Y), (self.pullback φ hdom).toFun r = θ.toFun r
• functorial {l : ℕ} {Z : Set (Projectivization k (Fin (l + 1) → k))} (φ : ProjectiveRatMap.ProjectiveRationalMap m n k X Y) (ψ : ProjectiveRatMap.ProjectiveRationalMap n l k Y Z) (hdomφ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k φ) (hdomψ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k ψ) (ψφ : ProjectiveRatMap.ProjectiveRationalMap m l k X Z) (hdomψφ : ProjectiveRatMap.ProjectiveRationalMap.IsDominant k ψφ) (hcomp : ∀ P ∈ X, ∀ repφ ∈ φ.reps, ∀ repψ ∈ ψ.reps, ∀ repψφ ∈ ψφ.reps, ProjectiveRatMap.RationalMapTupleRep.isDefinedAt k repφ P → ProjectiveRatMap.RationalMapTupleRep.isDefinedAt k repψφ P → ∀ (i j : Fin (l + 1)), ProjectiveRatMap.RationalMapTupleRep.evalVec k repψφ P i * (MvPolynomial.eval (ProjectiveRatMap.RationalMapTupleRep.evalVec k repφ P)) (repψ.polys j) = ProjectiveRatMap.RationalMapTupleRep.evalVec k repψφ P j * (MvPolynomial.eval (ProjectiveRatMap.RationalMapTupleRep.evalVec k repφ P)) (repψ.polys i)) (r : ProjectiveRegularFunction.ProjectiveRatFun l k Z) : dominantProjectiveRationalMapPullback k ψφ hdomψφ r = dominantProjectiveRationalMapPullback k φ hdomφ (dominantProjectiveRationalMapPullback k ψ hdomψ r)

theorem ProjectiveThm1518.theorem_15_18 {m n : ℕ} (k : Type u_1) [Field k] [IsAlgClosed k] {X : Set (Projectivization k (Fin (m + 1) → k))} {Y : Set (Projectivization k (Fin (n + 1) → k))} (hX : ProjectiveVarietyDef.IsProjectiveVariety k X) (hY : ProjectiveVarietyDef.IsProjectiveVariety k Y) : Nonempty (ProjectiveContravariantEquivalence m n k X Y)

Theorem 15.18: For projective varieties $X, Y$ over an algebraically closed field $k$, there is a contravariant equivalence between dominant projective rational maps $X \dashrightarrow Y$ and $k$-algebra homomorphisms $k(Y) \to k(X)$.