Mathlib.AlgebraicGeometry
Algebraic-geometry infrastructure for affine Zariski closures, coordinate rings, and exact dimension of polynomial images.
RationalDerivative 7 core · 4 supporting This module compiles vanishing of the full Fréchet derivative of a finite-dimensional real rational scalar coordinate into one polynomial equation. ★ derivative_zero_locus
Rational scalar derivative compiler
This module compiles vanishing of the full Fréchet derivative of a finite-dimensional real rational scalar coordinate into one polynomial equation. The quotient-rule numerators are combined by a sum of squares; nonzeroness follows either from formal nonconstancy, an explicit derivative witness, or semantic nonconstancy on a convex domain.
structure RationalScalar reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
A real rational scalar coordinate is a numerator and denominator multivariate polynomial.
Definition (Lean source)
def eval reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
For a rational scalar and source assignment, the evaluated scalar is its numerator evaluation divided by its denominator evaluation. Division is total: where the denominator vanishes the value is zero, so this is the rational function's value only on points where it is defined.
Definition (Lean source)
parameters
def
eval r x :
ℝ
def DefinedOn reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
For a rational scalar and domain, being defined on the domain means that its denominator never vanishes there.
Definition (Lean source)
def derivativeNumerator reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
For a rational scalar and source coordinate, the cleared quotient-rule numerator is the polynomial numerator of that coordinate derivative.
Definition (Lean source)
parameters
def
def IsFormallyNonconstant reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
For a rational scalar, formal nonconstancy means that at least one cleared partial-derivative numerator is a nonzero polynomial.
Definition (Lean source)
parameters
S :
Type u_1
r :
def
IsFormallyNonconstant r :
Prop
given by
∃ i, r.derivativeNumerator i ≠ 0
def derivativePolynomial reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
For a rational scalar, the full derivative certificate polynomial is the sum of squares of all cleared quotient-rule partial numerators.
Definition (Lean source)
theorem derivative_zero_locus reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalScalar
Given a rational scalar coordinate r on a domain where its denominator does not vanish, the points where its full Fréchet derivative vanishes are exactly one real polynomial zero locus within that domain.
Formal statement
hypotheses
conclusion
{x | x ∈ D ∧ fderiv ℝ r.eval x = 0}
= D ∩ mvPolynomialZeroLocus r.derivativePolynomial
Proof (Lean source)
theorem derivative_zero_locus [Fintype S] [DecidableEq S]
(r : RationalScalar S) (D : Set (S → ℝ)) (hD : r.DefinedOn D) :
{x | x ∈ D ∧ fderiv ℝ r.eval x = 0} =
D ∩ mvPolynomialZeroLocus r.derivativePolynomial := by
ext x
simp only [Set.mem_ofPred_eq, Set.mem_inter_iff,
mvPolynomialZeroLocus]
apply and_congr_right
intro hx
exact fderiv_eq_zero_iff_derivativePolynomial_eq_zero r x (hD x hx)
4 supporting declarations (lemmas, instances)
-
fderiv_eq_zero_iff_derivativePolynomial_eq_zerotheorem — Given a rational scalar, source assignment, and nonzero denominator at that assignment, the full Fréchet derivative vanishes exactly when its certificate polynomial vanishes.hypothesesProof (Lean source)
theorem fderiv_eq_zero_iff_derivativePolynomial_eq_zero [Fintype S] [DecidableEq S] (r : RationalScalar S) (x : S → ℝ) (hden : eval x r.den ≠ 0) : fderiv ℝ r.eval x = 0 ↔ eval x r.derivativePolynomial = 0 := by rw [(hasFDerivAt_eval r x hden).fderiv, continuousLinearMap_eq_zero_iff_single] change (∀ i, rationalDerivative r x (single i 1) = 0) ↔ eval x (conjunctionPolynomial r.derivativeNumerator) = 0 rw [eval_conjunctionPolynomial_eq_zero_iff] constructor · intro h i have hz := h i rw [rationalDerivative_single r x hden i] at hz rcases div_eq_zero_iff.mp hz with hi | hpow · exact hi · exact (pow_ne_zero 2 hden hpow).elim · intro h i rw [rationalDerivative_single r x hden i, h i, zero_div] -
derivativePolynomial_ne_zero_of_formallyNonconstanttheorem — Given a rational scalar satisfying formal nonconstancy, the full derivative certificate polynomial is nonzero.hypothesesconclusionr.derivativePolynomial ≠ 0Proof (Lean source)
theorem derivativePolynomial_ne_zero_of_formallyNonconstant [Fintype S] (r : RationalScalar S) (h : r.IsFormallyNonconstant) : r.derivativePolynomial ≠ 0 := by rcases h with ⟨i, hi⟩ rcases exists_polynomial_eval_ne_zero (r.derivativeNumerator i) hi with ⟨x, hx⟩ exact conjunctionPolynomial_ne_zero_of_witness r.derivativeNumerator x i hx -
derivativePolynomial_ne_zero_of_witnesstheorem — Given a rational scalar, source assignment, coordinate, and a nonzero cleared derivative numerator there, the full derivative certificate polynomial is nonzero.hypothesesconclusionr.derivativePolynomial ≠ 0Proof (Lean source)
theorem derivativePolynomial_ne_zero_of_witness [Fintype S] (r : RationalScalar S) (x : S → ℝ) (i : S) (h : eval x (r.derivativeNumerator i) ≠ 0) : r.derivativePolynomial ≠ 0 := by exact conjunctionPolynomial_ne_zero_of_witness r.derivativeNumerator x i h -
derivativePolynomial_ne_zero_of_nonconstantOn_convextheorem — Given a rational scalar on a convex domain, a nowhere-vanishing denominator, two domain points, and distinct rational values, the full derivative certificate polynomial is nonzero.hypothesesr :D :Set (S → ℝ)hconvex :Convex ℝ DhD :r.DefinedOn Dx y :S → ℝhx :x ∈ Dhy :y ∈ Dhne :r.eval x ≠ r.eval yconclusionr.derivativePolynomial ≠ 0Proof (Lean source)
theorem derivativePolynomial_ne_zero_of_nonconstantOn_convex [Fintype S] [DecidableEq S] (r : RationalScalar S) (D : Set (S → ℝ)) (hconvex : Convex ℝ D) (hD : r.DefinedOn D) (x y : S → ℝ) (hx : x ∈ D) (hy : y ∈ D) (hne : r.eval x ≠ r.eval y) : r.derivativePolynomial ≠ 0 := by intro hzero have hdiffAt : ∀ z ∈ D, DifferentiableAt ℝ r.eval z := by intro z hz exact (hasFDerivAt_eval r z (hD z hz)).differentiableAt have hfderiv : ∀ z ∈ D, fderiv ℝ r.eval z = 0 := by intro z hz apply (fderiv_eq_zero_iff_derivativePolynomial_eq_zero r z (hD z hz)).mpr rw [hzero] simp have hdiffOn : DifferentiableOn ℝ r.eval D := by intro z hz exact (hdiffAt z hz).differentiableWithinAt have hfderivWithin : ∀ z ∈ D, fderivWithin ℝ r.eval D z = 0 := by intro z hz have hzeroAt : HasFDerivAt r.eval (0 : (S → ℝ) →L[ℝ] ℝ) z := by rw [← hfderiv z hz] exact (hdiffAt z hz).hasFDerivAt rw [fderivWithin_def] simp [hzeroAt.hasFDerivWithinAt] exact hne (hconvex.is_const_of_fderivWithin_eq_zero hdiffOn hfderivWithin hx hy)
RationalMap 17 core · 13 supporting This module represents coordinate-indexed real rational maps by numerator and denominator polynomials (the locus compilers below assume finitely many output coordinates). ★ rationalMap_eq_locus
Rational maps and algebraic-locus compilers
This module represents coordinate-indexed real rational maps by numerator and denominator polynomials (the locus compilers below assume finitely many output coordinates). It clears coordinatewise equality, compiles finite conjunctions by sums of squares and finite unions by products, and supplies polynomial-matrix and adjugate/determinant inverse specializations.
structure RationalMap reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
A real rational map with an arbitrary index set of output coordinates stores one numerator and denominator multivariate polynomial for each output coordinate.
Definition (Lean source)
def eval reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
Evaluating a rational map substitutes the source coordinates into each numerator and denominator and divides coordinatewise. Division is total: a coordinate whose denominator vanishes evaluates to zero, so this agrees with the rational map only where it is defined in the sense of DefinedOn.
Definition (Lean source)
parameters
def
eval f x :
T → ℝ
def DefinedOn reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
A rational map is defined on a domain when every coordinate denominator is nonzero at every point of that domain.
Definition (Lean source)
def ofPolynomial reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
A polynomial coordinate map is viewed as a rational map with denominator one in every coordinate.
Definition (Lean source)
parameters
def
def equalityPolynomial reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
The cleared numerator for equality of one coordinate of two rational maps is the cross-product of their numerators and denominators.
Definition (Lean source)
parameters
def
given by
f.num t * g.den t - g.num t * f.den t
def conjunctionPolynomial reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
The conjunction polynomial of finitely many real polynomials is their sum of squares.
Definition (Lean source)
parameters
def
given by
∑ t, (p t) ^ 2
def unionConjunctionPolynomial reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
The union-of-conjunctions polynomial multiplies the sum-of-squares certificate for every branch.
Definition (Lean source)
parameters
def
given by
∏ b, conjunctionPolynomial (p b)
theorem rationalMap_eq_locus reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
Given two finite-coordinate rational maps f and g on a common domain where the denominators of the first map do not vanish and the denominators of the second map do not vanish, the whole-output equality condition is one real polynomial zero locus.
Formal statement
hypotheses
conclusion
{x | x ∈ D ∧ f.eval x = g.eval x}
= D ∩ mvPolynomialZeroLocus (conjunctionPolynomial (RationalMap.equalityPolynomial f g))
Proof (Lean source)
theorem rationalMap_eq_locus [Fintype T]
(f g : RationalMap S T) (D : Set (S → ℝ))
(hf : f.DefinedOn D) (hg : g.DefinedOn D) :
{x | x ∈ D ∧ f.eval x = g.eval x} =
D ∩ mvPolynomialZeroLocus
(conjunctionPolynomial (RationalMap.equalityPolynomial f g)) := by
ext x
simp only [Set.mem_ofPred_eq, Set.mem_inter_iff,
mvPolynomialZeroLocus]
apply and_congr_right
intro hx
rw [eval_conjunctionPolynomial_eq_zero_iff]
constructor
· intro h t
exact (RationalMap.eval_eq_iff_equalityPolynomial_eq_zero f g x t
(hf x hx t) (hg x hx t)).mp (congrFun h t)
· intro h
funext t
exact (RationalMap.eval_eq_iff_equalityPolynomial_eq_zero f g x t
(hf x hx t) (hg x hx t)).mpr (h t)
abbrev RationalMatrixMap reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
A rational matrix map is a rational map whose output coordinates are row-column pairs.
Definition (Lean source)
def evalMatrix reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMatrixMap
Evaluating a rational matrix map and reshaping its pair-indexed output gives an ordinary matrix-valued function.
Definition (Lean source)
def evalPolynomialMatrix reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
Evaluating a matrix of multivariate polynomials substitutes the source point in every matrix entry.
Definition (Lean source)
parameters
S :
Type u_1
T :
Type u_2
U :
Type u_3
A :
Matrix T U (MvPolynomial S ℝ)
x :
S → ℝ
def
given by
A.map (eval x)
def polynomialMatrixRationalMap reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
A polynomial matrix is represented as a rational matrix map with denominator one entrywise.
Definition (Lean source)
parameters
def
given by
RationalMap.ofPolynomial (fun ij => A ij.1 ij.2)
def polynomialMatrixInverseRationalMap reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
The adjugate-over-determinant representation is the rational matrix map associated with the inverse of a square polynomial matrix.
Definition (Lean source)
parameters
def
def renameSource reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
Renaming the source variables of a rational map along a coordinate map renames every numerator and denominator polynomial.
Definition (Lean source)
parameters
def
given by
clause 1
num := fun t => MvPolynomial.rename e (f.num t)
clause 2
den := fun t => MvPolynomial.rename e (f.den t)
def leftLift reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
The left lift of a rational map makes it depend on the left coordinates of a disjoint-sum parameter space.
Definition (Lean source)
def rightLift reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry.RationalMap
The right lift of a rational map makes it depend on the right coordinates of a disjoint-sum parameter space.
Definition (Lean source)
def sumProductDomain reviewed
⚑ flagged
Causalean.Mathlib.AlgebraicGeometry
The sum-coordinate form of a product domain requires the left and right restrictions of one assignment to lie in their respective domains.
13 supporting declarations (lemmas, instances)
-
eval_ofPolynomialtheorem — For a polynomial coordinate map and source assignment, the denominator-one rational representation has ordinary polynomial evaluation.hypothesesconclusion(ofPolynomial p).eval x = fun t => eval x (p t)Proof (Lean source)
theorem eval_ofPolynomial (p : T → MvPolynomial S ℝ) (x : S → ℝ) : (ofPolynomial p).eval x = fun t => eval x (p t) := by funext t simp [eval, ofPolynomial] -
eval_eq_iff_equalityPolynomial_eq_zerotheorem — Given two rational maps, a source assignment, an output coordinate, and nonzero first and second denominators, the rational values agree exactly when the cleared equality polynomial vanishes.hypothesesS :sharedType u_1T :sharedType u_2f g :RationalMap S Tx :S → ℝt :Thf :eval x (f.den t) ≠ 0hg :eval x (g.den t) ≠ 0conclusionf.eval x t = g.eval x t ↔ eval x (equalityPolynomial f g t) = 0Proof (Lean source)
theorem eval_eq_iff_equalityPolynomial_eq_zero (f g : RationalMap S T) (x : S → ℝ) (t : T) (hf : eval x (f.den t) ≠ 0) (hg : eval x (g.den t) ≠ 0) : f.eval x t = g.eval x t ↔ eval x (equalityPolynomial f g t) = 0 := by simp only [eval, equalityPolynomial, MvPolynomial.eval_sub, MvPolynomial.eval_mul, sub_eq_zero] exact div_eq_div_iff hf hg -
eval_conjunctionPolynomial_eq_zero_ifftheorem — For a finite polynomial family and source assignment, the conjunction polynomial vanishes exactly when every constituent polynomial vanishes.hypothesesconclusionProof (Lean source)
theorem eval_conjunctionPolynomial_eq_zero_iff [Fintype T] (p : T → MvPolynomial S ℝ) (x : S → ℝ) : eval x (conjunctionPolynomial p) = 0 ↔ ∀ t, eval x (p t) = 0 := by simp only [conjunctionPolynomial, MvPolynomial.eval_sum, MvPolynomial.eval_pow] constructor · intro h t have ht : (eval x (p t)) ^ 2 = 0 := by exact (Finset.sum_eq_zero_iff_of_nonneg (fun i _ => sq_nonneg (eval x (p i)))).mp h t (Finset.mem_univ t) exact sq_eq_zero_iff.mp ht · intro h apply Finset.sum_eq_zero intro t _ simp [h t] -
conjunctionPolynomial_ne_zero_of_witnesstheorem — Given a finite polynomial family, source assignment, coordinate, and a nonzero value at that coordinate, the conjunction polynomial is nonzero.hypothesesconclusionconjunctionPolynomial p ≠ 0Proof (Lean source)
theorem conjunctionPolynomial_ne_zero_of_witness [Fintype T] (p : T → MvPolynomial S ℝ) (x : S → ℝ) (t : T) (h : eval x (p t) ≠ 0) : conjunctionPolynomial p ≠ 0 := by intro hp have hz : eval x (conjunctionPolynomial p) = 0 := by rw [hp] simp exact h ((eval_conjunctionPolynomial_eq_zero_iff p x).mp hz t) -
eval_unionConjunctionPolynomial_eq_zero_ifftheorem — For a finite family of finite polynomial systems and source assignment, the union certificate vanishes exactly when one branch vanishes coordinatewise.hypothesesconclusion= 0 ↔ ∃ b, ∀ t, eval x (p b t) = 0Proof (Lean source)
theorem eval_unionConjunctionPolynomial_eq_zero_iff [Fintype B] [Fintype T] (p : B → T → MvPolynomial S ℝ) (x : S → ℝ) : eval x (unionConjunctionPolynomial p) = 0 ↔ ∃ b, ∀ t, eval x (p b t) = 0 := by classical simp only [unionConjunctionPolynomial, MvPolynomial.eval_prod, Finset.prod_eq_zero_iff, Finset.mem_univ, true_and] apply exists_congr intro b exact eval_conjunctionPolynomial_eq_zero_iff (p b) x -
unionConjunctionPolynomial_ne_zero_of_witnessestheorem — Given a finite polynomial-system family, branchwise witness assignments, branchwise coordinates, and nonzero witness values, the union certificate is nonzero.hypothesesS :sharedType u_1T :sharedType u_2Fintype Tp :B → T → MvPolynomial S ℝwitness :B → S → ℝcoordinate :B → Th :∀ b, eval (witness b) (p b (coordinate b)) ≠ 0conclusionProof (Lean source)
theorem unionConjunctionPolynomial_ne_zero_of_witnesses [Fintype B] [Fintype T] (p : B → T → MvPolynomial S ℝ) (witness : B → S → ℝ) (coordinate : B → T) (h : ∀ b, eval (witness b) (p b (coordinate b)) ≠ 0) : unionConjunctionPolynomial p ≠ 0 := by apply mvPolynomial_fintype_prod_ne_zero intro b exact conjunctionPolynomial_ne_zero_of_witness (p b) (witness b) (coordinate b) (h b) -
rationalMap_eq_union_locustheorem — Given finite families of rational maps on a common domain, with all first and second denominators nonvanishing, the union of their equality conditions is one polynomial zero locus.hypothesesS :sharedType u_1T :sharedType u_2Fintype Tf g :B → RationalMap S TD :Set (S → ℝ)hf :∀ b, (f b).DefinedOn Dhg :∀ b, (g b).DefinedOn Dconclusion{x | x ∈ D ∧ ∃ b, (f b).eval x = (g b).eval x}= D ∩ mvPolynomialZeroLocus (unionConjunctionPolynomial (fun b => RationalMap.equalityPolynomial (f b) (g b)))Proof (Lean source)
theorem rationalMap_eq_union_locus [Fintype B] [Fintype T] (f g : B → RationalMap S T) (D : Set (S → ℝ)) (hf : ∀ b, (f b).DefinedOn D) (hg : ∀ b, (g b).DefinedOn D) : {x | x ∈ D ∧ ∃ b, (f b).eval x = (g b).eval x} = D ∩ mvPolynomialZeroLocus (unionConjunctionPolynomial (fun b => RationalMap.equalityPolynomial (f b) (g b))) := by ext x simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, mvPolynomialZeroLocus] apply and_congr_right intro hx rw [eval_unionConjunctionPolynomial_eq_zero_iff] apply exists_congr intro b constructor · intro h t exact (RationalMap.eval_eq_iff_equalityPolynomial_eq_zero (f b) (g b) x t (hf b x hx t) (hg b x hx t)).mp (congrFun h t) · intro h funext t exact (RationalMap.eval_eq_iff_equalityPolynomial_eq_zero (f b) (g b) x t (hf b x hx t) (hg b x hx t)).mpr (h t) -
polynomialMatrixRationalMap_evaltheorem — For a polynomial matrix and source assignment, the rational-matrix representation agrees with entrywise polynomial evaluation.hypothesesS :sharedType u_1T :sharedType u_2U :sharedType u_3A :Matrix T U (MvPolynomial S ℝ)x :S → ℝconclusionProof (Lean source)
theorem polynomialMatrixRationalMap_eval (A : Matrix T U (MvPolynomial S ℝ)) (x : S → ℝ) : (polynomialMatrixRationalMap A).evalMatrix x = evalPolynomialMatrix A x := by ext i j simp [RationalMatrixMap.evalMatrix, polynomialMatrixRationalMap, RationalMap.eval_ofPolynomial, evalPolynomialMatrix] -
polynomialMatrixInverseRationalMap_evaltheorem — Given a square polynomial matrix, source assignment, and nonzero evaluated determinant, the adjugate-over-determinant map evaluates to the matrix inverse.hypothesesconclusionProof (Lean source)
theorem polynomialMatrixInverseRationalMap_eval [Fintype T] [DecidableEq T] (A : Matrix T T (MvPolynomial S ℝ)) (x : S → ℝ) (hdet : eval x A.det ≠ 0) : (polynomialMatrixInverseRationalMap A).evalMatrix x = (evalPolynomialMatrix A x)⁻¹ := by rw [Matrix.inv_def] ext i j change eval x (A.adjugate i j) / eval x A.det = (Ring.inverse (A.map (eval x)).det • (A.map (eval x)).adjugate) i j rw [show (A.map (eval x)).det = eval x A.det from (RingHom.map_det (eval x) A).symm, show (A.map (eval x)).adjugate = A.adjugate.map (eval x) from (RingHom.map_adjugate (eval x) A).symm] by_cases hd : eval x A.det = 0 · exact (hdet hd).elim · simp [Ring.inverse_eq_inv, Matrix.smul_apply, div_eq_mul_inv, mul_comm] -
polynomialMatrixInverseRationalMap_definedOntheorem — Given a square polynomial matrix, domain, and a nowhere-vanishing evaluated determinant, the inverse representation is defined on the domain.hypothesesS :sharedType u_1A :Matrix T T (MvPolynomial S ℝ)D :Set (S → ℝ)hdet :∀ x ∈ D, eval x A.det ≠ 0conclusion(polynomialMatrixInverseRationalMap A).DefinedOn DProof (Lean source)
theorem polynomialMatrixInverseRationalMap_definedOn [Fintype T] [DecidableEq T] (A : Matrix T T (MvPolynomial S ℝ)) (D : Set (S → ℝ)) (hdet : ∀ x ∈ D, eval x A.det ≠ 0) : (polynomialMatrixInverseRationalMap A).DefinedOn D := by intro x hx ij exact hdet x hx -
eval_renameSourcetheorem — For a rational map, coordinate renaming, and renamed-source assignment, the renamed map evaluates as the original map on the pulled-back assignment.hypothesesconclusion(f.renameSource e).eval x = f.eval (x ∘ e)Proof (Lean source)
theorem eval_renameSource (f : RationalMap S T) (e : S → U) (x : U → ℝ) : (f.renameSource e).eval x = f.eval (x ∘ e) := by funext t simp [eval, renameSource, MvPolynomial.eval_rename] -
rationalMap_imageIntersection_locustheorem — Given finite-coordinate rational maps f and g on domains, with nonvanishing denominators for the first map and the second map, the pairs of parameters at which their images meet form one polynomial zero locus.hypothesesS :sharedType u_5U :sharedType u_6f :RationalMap S Tg :RationalMap U TD :Set (S → ℝ)E :Set (U → ℝ)hf :f.DefinedOn Dhg :g.DefinedOn Econclusion= sumProductDomain D E ∩ mvPolynomialZeroLocus (conjunctionPolynomial (RationalMap.equalityPolynomial f.leftLift g.rightLift))Proof (Lean source)
theorem rationalMap_imageIntersection_locus [Fintype T] (f : RationalMap S T) (g : RationalMap U T) (D : Set (S → ℝ)) (E : Set (U → ℝ)) (hf : f.DefinedOn D) (hg : g.DefinedOn E) : {z | z ∈ sumProductDomain D E ∧ f.eval (z ∘ inl) = g.eval (z ∘ inr)} = sumProductDomain D E ∩ mvPolynomialZeroLocus (conjunctionPolynomial (RationalMap.equalityPolynomial f.leftLift g.rightLift)) := by have hleft : f.leftLift.DefinedOn (sumProductDomain D E) := by intro z hz t change eval z (MvPolynomial.rename inl (f.den t)) ≠ 0 rw [MvPolynomial.eval_rename] exact hf (z ∘ inl) hz.1 t have hright : g.rightLift.DefinedOn (sumProductDomain D E) := by intro z hz t change eval z (MvPolynomial.rename inr (g.den t)) ≠ 0 rw [MvPolynomial.eval_rename] exact hg (z ∘ inr) hz.2 t simpa only [RationalMap.eval_renameSource, RationalMap.leftLift, RationalMap.rightLift] using (rationalMap_eq_locus f.leftLift g.rightLift (sumProductDomain D E) hleft hright) -
rationalMatrixMap_imageIntersection_locustheorem — Given rational matrix maps on domains, with nonvanishing denominators for both maps, the parameter pairs at which their matrix images meet form one polynomial zero locus.hypothesesS :sharedType u_5U :sharedType u_6R :sharedType u_8C :sharedType u_9Fintype RFintype Cf :RationalMatrixMap S R Cg :RationalMatrixMap U R CD :Set (S → ℝ)E :Set (U → ℝ)hf :f.DefinedOn Dhg :g.DefinedOn Econclusion= sumProductDomain D E ∩ mvPolynomialZeroLocus (conjunctionPolynomial (RationalMap.equalityPolynomial f.leftLift g.rightLift))Proof (Lean source)
theorem rationalMatrixMap_imageIntersection_locus [Fintype R] [Fintype C] (f : RationalMatrixMap S R C) (g : RationalMatrixMap U R C) (D : Set (S → ℝ)) (E : Set (U → ℝ)) (hf : f.DefinedOn D) (hg : g.DefinedOn E) : {z | z ∈ sumProductDomain D E ∧ f.evalMatrix (z ∘ inl) = g.evalMatrix (z ∘ inr)} = sumProductDomain D E ∩ mvPolynomialZeroLocus (conjunctionPolynomial (RationalMap.equalityPolynomial f.leftLift g.rightLift)) := by rw [← rationalMap_imageIntersection_locus f g D E hf hg] ext z simp only [Set.mem_ofPred_eq] apply and_congr_right intro _ constructor · intro h funext ij exact congrFun (congrFun h ij.1) ij.2 · intro h ext i j exact congrFun h (i, j)