Mathlib.Algebraic­Geometry.Polynomial­Image­Dimension

lemma affineZariskiClosure_idem {ι : Type*} (A : Set (ι → ℂ)) : affineZariskiClosure (affineZariskiClosure A) = affineZariskiClosure A := by apply Set.Subset.antisymm · intro x hx P hP exact hx P (fun y hy => hy P hP) · exact affineZariskiClosure_extensive _

lemma affineZariskiClosure_inter {ι : Type*} {A B : Set (ι → ℂ)} (hA : affineZariskiClosure A = A) (hB : affineZariskiClosure B = B) : affineZariskiClosure (A ∩ B) = A ∩ B := by apply Set.Subset.antisymm · intro x hx exact ⟨hA ▸ affineZariskiClosure_mono Set.inter_subset_left hx, hB ▸ affineZariskiClosure_mono Set.inter_subset_right hx⟩ · exact affineZariskiClosure_extensive _

lemma affineZariskiClosure_zero_of_polynomial {ι : Type*} (P : MvPolynomial ι ℂ) : affineZariskiClosure {x | eval x P = 0} = {x | eval x P = 0} := by apply Set.Subset.antisymm · intro x hx exact hx P (fun y hy => by simpa [MvPolynomial.aeval_def] using hy) · exact affineZariskiClosure_extensive _

lemma affineZariskiClosure_union {ι : Type*} {A B : Set (ι → ℂ)} (hA : affineZariskiClosure A = A) (hB : affineZariskiClosure B = B) : affineZariskiClosure (A ∪ B) = A ∪ B := by apply Set.Subset.antisymm · intro x hx by_contra hnot have hxA : x ∉ A := fun h => hnot (inl h) have hxB : x ∉ B := fun h => hnot (inr h) have hxAc : x ∉ affineZariskiClosure A := by simpa [hA] using hxA have hxBc : x ∉ affineZariskiClosure B := by simpa [hB] using hxB simp only [affineZariskiClosure, MvPolynomial.mem_zeroLocus_iff, MvPolynomial.aeval_def] at hxAc hxBc push_neg at hxAc hxBc obtain ⟨P, hPA, hPx⟩ := hxAc obtain ⟨Q, hQB, hQx⟩ := hxBc have hpq : P * Q ∈ vanishingIdeal ℂ (A ∪ B) := by intro y hy rcases hy with hy | hy · rw [map_mul, hPA y hy, zero_mul] · rw [map_mul, hQB y hy, mul_zero] have := hx (P * Q) hpq rw [map_mul] at this exact mul_ne_zero hPx hQx this · exact affineZariskiClosure_extensive _

lemma vanishingIdeal_ne_top_of_nonempty {ι : Type*} {Z : Set (ι → ℂ)} (hZ : Z.Nonempty) : vanishingIdeal ℂ Z ≠ ⊤ := by rintro htop obtain ⟨x, hx⟩ := hZ have hone : (1 : MvPolynomial ι ℂ) ∈ vanishingIdeal ℂ Z := by rw [htop] trivial simpa using hone x hx

lemma nonempty_zeroLocus_of_prime {ι : Type*} [Finite ι] (P : Ideal (MvPolynomial ι ℂ)) [P.IsPrime] : (zeroLocus ℂ P).Nonempty := by by_contra hempty have htop : vanishingIdeal ℂ (zeroLocus ℂ P) = ⊤ := by rw [Set.not_nonempty_iff_eq_empty.mp hempty, MvPolynomial.vanishingIdeal_empty] rw [MvPolynomial.IsPrime.vanishingIdeal_zeroLocus P] at htop exact Ideal.IsPrime.ne_top' htop

theorem irreducible_zeroLocus_of_prime {ι : Type*} [Finite ι] (P : Ideal (MvPolynomial ι ℂ)) [P.IsPrime] : IsIrreducibleAffineClosed (zeroLocus ℂ P) := by have hc : affineZariskiClosure (zeroLocus ℂ P) = zeroLocus ℂ P := by unfold affineZariskiClosure rw [MvPolynomial.IsPrime.vanishingIdeal_zeroLocus P] have hn := nonempty_zeroLocus_of_prime P apply (irreducibleAffineClosed_iff_isPrime hc hn).mpr rw [MvPolynomial.IsPrime.vanishingIdeal_zeroLocus P] infer_instance

lemma vanishingIdeal_strict_anti {ι : Type*} {A B : Set (ι → ℂ)} (hA : affineZariskiClosure A = A) (hB : affineZariskiClosure B = B) (hAB : A ⊂ B) : vanishingIdeal ℂ B < vanishingIdeal ℂ A := by refine lt_of_le_of_ne (MvPolynomial.vanishingIdeal_anti_mono hAB.le) ?_ intro heq apply hAB.ne rw [← hA, ← hB, affineZariskiClosure, affineZariskiClosure, heq]

lemma zeroLocus_strict_anti {ι : Type*} [Finite ι] {P Q : Ideal (MvPolynomial ι ℂ)} [P.IsPrime] [Q.IsPrime] (hPQ : P < Q) : zeroLocus ℂ Q ⊂ zeroLocus ℂ P := by refine lt_of_le_of_ne (MvPolynomial.zeroLocus_anti_mono hPQ.le) ?_ intro heq have := congrArg (vanishingIdeal ℂ) heq rw [MvPolynomial.IsPrime.vanishingIdeal_zeroLocus Q, MvPolynomial.IsPrime.vanishingIdeal_zeroLocus P] at this exact hPQ.ne this.symm

lemma IsPolynomialMap.comp {ι κ τ : Type*} {f : (ι → ℂ) → (κ → ℂ)} {g : (κ → ℂ) → (τ → ℂ)} (hg : IsPolynomialMap g) (hf : IsPolynomialMap f) : IsPolynomialMap (g ∘ f) := by classical choose Pf hPf using hf intro t obtain ⟨Q, hQ⟩ := hg t refine ⟨MvPolynomial.eval₂ C Pf Q, ?_⟩ intro x rw [MvPolynomial.eval_eval₂] have hC : (eval x).comp C = id ℂ := by ext z simp rw [hC, MvPolynomial.eval₂_id] calc eval (fun k => eval x (Pf k)) Q = eval (f x) Q := by apply congrArg (fun v => eval v Q) funext k exact hPf k x _ = g (f x) t := hQ (f x)

lemma IsPolynomialMap.eval_comp {ι κ : Type*} {f : (ι → ℂ) → (κ → ℂ)} (hf : IsPolynomialMap f) (Q : MvPolynomial κ ℂ) : ∃ P : MvPolynomial ι ℂ, ∀ x, eval x P = eval (f x) Q := by classical choose Pf hPf using hf refine ⟨MvPolynomial.eval₂ C Pf Q, ?_⟩ intro x rw [MvPolynomial.eval_eval₂] have hC : (eval x).comp C = id ℂ := by ext z simp rw [hC, MvPolynomial.eval₂_id] apply congrArg (fun v => eval v Q) funext k exact hPf k x

lemma polynomial_preimage_closed {ι κ : Type*} {f : (ι → ℂ) → (κ → ℂ)} (hf : IsPolynomialMap f) {A : Set (κ → ℂ)} (hA : affineZariskiClosure A = A) : affineZariskiClosure (f ⁻¹' A) = f ⁻¹' A := by apply Set.Subset.antisymm · intro x hx rw [← hA] intro Q hQ change eval (f x) Q = 0 obtain ⟨P, hP⟩ := hf.eval_comp Q rw [← hP x] exact hx P (by intro y hy change eval y P = 0 rw [hP y] simpa [MvPolynomial.aeval_def, MvPolynomial.eval₂_id] using hQ (f y) hy) · exact affineZariskiClosure_extensive _

lemma polynomial_fixedPoints_closed {ι : Type*} {f : (ι → ℂ) → (ι → ℂ)} (hf : IsPolynomialMap f) : affineZariskiClosure {x | f x = x} = {x | f x = x} := by apply Set.Subset.antisymm · intro x hx funext i obtain ⟨P, hP⟩ := hf i let Q := P - MvPolynomial.X i have hQ : ∀ y ∈ {y | f y = y}, eval y Q = 0 := by intro y hy simp [Q, hP y, congrFun hy i] have := hx Q hQ exact sub_eq_zero.mp (by simpa [Q, hP x] using this) · exact affineZariskiClosure_extensive _

lemma polynomial_image_closed_of_retract {ι κ : Type*} {f : (ι → ℂ) → (κ → ℂ)} {g : (κ → ℂ) → (ι → ℂ)} (hf : IsPolynomialMap f) (hg : IsPolynomialMap g) (hleft : LeftInverse g f) {A : Set (ι → ℂ)} (hA : affineZariskiClosure A = A) : affineZariskiClosure (f '' A) = f '' A := by have hrange := polynomial_range_closed_of_retract hf hg hleft have hpre := polynomial_preimage_closed hg hA have heq : f '' A = range f ∩ g ⁻¹' A := by ext y constructor · rintro ⟨x, hx, rfl⟩ exact ⟨⟨x, rfl⟩, by simpa [hleft x] using hx⟩ · rintro ⟨⟨x, rfl⟩, hx⟩ exact ⟨x, by simpa [hleft x] using hx, rfl⟩ rw [heq] exact affineZariskiClosure_inter hrange hpre

lemma primeOfIrreducible_lt {ι : Type*} [Finite ι] {A B : Set (ι → ℂ)} (hA : IsIrreducibleAffineClosed A) (hB : IsIrreducibleAffineClosed B) (hAB : A ⊂ B) : primeOfIrreducible B hB < primeOfIrreducible A hA := by exact vanishingIdeal_strict_anti hA.1 hB.1 hAB

lemma linearMap_isPolynomial {ι κ : Type*} [Finite ι] (F : (ι → ℂ) →ₗ[ℂ] (κ → ℂ)) : IsPolynomialMap F := by classical letI := Fintype.ofFinite ι intro k let P : MvPolynomial ι ℂ := ∑ i, C (F (single i 1) k) * X i refine ⟨P, ?_⟩ intro x have hx : x = ∑ i, x i • (single i (1 : ℂ) : ι → ℂ) := by funext j rw [Finset.sum_apply, Finset.sum_eq_single j] · simp · intro b _ hb simp [Pi.single_eq_of_ne hb.symm] · simp have hFx : F x k = ∑ i, x i * F (single i 1) k := by calc F x k = F (∑ i, x i • (single i (1 : ℂ) : ι → ℂ)) k := congrArg (fun y => F y k) hx _ = ∑ i, x i * F (single i 1) k := by rw [map_sum] simp simpa [P, mul_comm] using hFx.symm

lemma affineLinearMap_isPolynomial {ι κ : Type*} [Finite ι] (F : (ι → ℂ) →ₗ[ℂ] (κ → ℂ)) (c : κ → ℂ) : IsPolynomialMap (fun x => c + F x) := by obtain hF := linearMap_isPolynomial F intro k obtain ⟨P, hP⟩ := hF k refine ⟨MvPolynomial.C (c k) + P, ?_⟩ intro x simp [hP x]

lemma map_quotient_strictMono {R : Type*} [CommRing R] (I A B : Ideal R) (hIA : I ≤ A) (hAB : A < B) : A.map (Ideal.Quotient.mk I) < B.map (Ideal.Quotient.mk I) := by refine lt_of_le_of_ne (Ideal.map_mono hAB.le) ?_ intro heq apply hAB.ne have hc := congrArg (Ideal.comap (Ideal.Quotient.mk I)) heq simpa [Ideal.comap_map_mk hIA, Ideal.comap_map_mk (hIA.trans hAB.le)] using hc

theorem no_three_chain_of_minimalPrime_span {ι : Type*} [Finite ι] {C X : Set (ι → ℂ)} (hC : IsIrreducibleAffineClosed C) (hX : IsIrreducibleAffineClosed X) (P : MvPolynomial ι ℂ) (hmin : MvPolynomial.vanishingIdeal ℂ C ∈ (MvPolynomial.vanishingIdeal ℂ X ⊔ span {P}).minimalPrimes) : ¬ ∃ chain : Fin 3 → Set (ι → ℂ), StrictMono chain ∧ (∀ i, IsIrreducibleAffineClosed (chain i)) ∧ chain 0 = C ∧ chain (last 2) = X := by rintro ⟨chain, hmono, hirr, hzero, hlast⟩ let mid : Fin 3 := ⟨1, by omega⟩ have h0mid : (0 : Fin 3) < mid := by simp [mid] have hmidlast : mid < last 2 := by simp [mid, last] have hCY : C ⊂ chain mid := by simpa [hzero] using hmono h0mid have hYX : chain mid ⊂ X := by have h := hmono hmidlast rw [hlast] at h exact h let I : Ideal (MvPolynomial ι ℂ) := MvPolynomial.vanishingIdeal ℂ X let J : Ideal (MvPolynomial ι ℂ) := MvPolynomial.vanishingIdeal ℂ C let K : Ideal (MvPolynomial ι ℂ) := MvPolynomial.vanishingIdeal ℂ (chain mid) have hIK : I < K := by exact vanishingIdeal_strict_anti (hirr mid).1 hX.1 hYX have hKJ : K < J := by exact vanishingIdeal_strict_anti hC.1 (hirr mid).1 hCY haveI hIprime : I.IsPrime := (irreducibleAffineClosed_iff_isPrime hX.1 hX.2.1).mp hX haveI hKprime : K.IsPrime := (irreducibleAffineClosed_iff_isPrime (hirr mid).1 (hirr mid).2.1).mp (hirr mid) haveI hJprime : J.IsPrime := (irreducibleAffineClosed_iff_isPrime hC.1 hC.2.1).mp hC let q := Ideal.Quotient.mk I have hmapKJ : K.map q < J.map q := map_quotient_strictMono I K J hIK.le hKJ have hmapIK : I.map q < K.map q := map_quotient_strictMono I I K le_rfl hIK haveI hmapKprime : (K.map q).IsPrime := Ideal.isPrime_map_quotientMk_of_isPrime hIK.le haveI hmapJprime : (J.map q).IsPrime := Ideal.isPrime_map_quotientMk_of_isPrime (hIK.le.trans hKJ.le) have hheightJ : (J.map q).height ≤ 1 := by exact Ideal.map_height_le_one_of_mem_minimalPrimes hmin have hheightK_lt : (K.map q).height < 1 := (Ideal.height_le_iff.mp hheightJ) (K.map q) inferInstance hmapKJ have hmapIbot : I.map q = ⊥ := Ideal.map_quotient_self I have hbotK : (⊥ : Ideal ((MvPolynomial ι ℂ) ⧸ I)) < K.map q := by simpa [hmapIbot] using hmapIK have hheightK_pos : (0 : ℕ∞) < (K.map q).height := by have hstrict := Ideal.height_strict_mono_of_isPrime hbotK simpa [Ideal.height_bot] using hstrict have hheightK_zero : (K.map q).height = 0 := ENat.lt_one_iff_eq_zero.mp hheightK_lt simp [hheightK_zero] at hheightK_pos

theorem no_intermediate_of_exact_affine_dimensions {ι : Type*} {d : ℕ} {C X : Set (ι → ℂ)} (hX : IsIrreducibleAffineClosed X) (hCdim : HasAffineZariskiDimension d C) (hXdim : HasAffineZariskiDimension (d + 1) X) : ¬ ∃ Y, IsIrreducibleAffineClosed Y ∧ C ⊂ Y ∧ Y ⊂ X := by rintro ⟨Y, hY, hCY, hYX⟩ obtain ⟨chain, hmono, hirr, hsub⟩ := hCdim.1 apply hXdim.2 refine ⟨affineAppendTwo chain Y X, affineAppendTwo_strictMono hmono hsub hCY hYX, ?_, ?_⟩ · intro i by_cases hi : i.val < d + 1 · simpa [affineAppendTwo, hi] using hirr ⟨i.val, hi⟩ · by_cases hy : i.val = d + 1 · simpa [affineAppendTwo, hi, hy] using hY · simpa [affineAppendTwo, hi, hy] using hX · intro i by_cases hi : i.val < d + 1 · simpa [affineAppendTwo, hi] using (hsub ⟨i.val, hi⟩).trans (hCY.le.trans hYX.le) · by_cases hy : i.val = d + 1 · simpa [affineAppendTwo, hy] using hYX.le · have hi' : ¬ i.val ≤ d := by omega simp [affineAppendTwo, hi', hy]

theorem irreducibleAffineComponent_of_no_intermediate {ι : Type*} {C Z X : Set (ι → ℂ)} (hC : IsIrreducibleAffineClosed C) (hCZ : C ⊆ Z) (hZX : Z ⊆ X) (hne : Z ≠ X) (hno : ¬ ∃ Y, IsIrreducibleAffineClosed Y ∧ C ⊂ Y ∧ Y ⊂ X) : IsIrreducibleAffineComponent C Z := by refine ⟨hC, hCZ, ?_⟩ intro Y hY hCY hYZ apply Set.Subset.antisymm · by_contra hYC have hCneY : C ≠ Y := by intro heq apply hYC rw [heq] have hCYstrict : C ⊂ Y := Set.ssubset_iff_subset_ne.mpr ⟨hCY, hCneY⟩ have hYX : Y ⊆ X := hYZ.trans hZX have hYXne : Y ≠ X := by intro heq apply hne exact Set.Subset.antisymm hZX (by simpa [heq] using hYZ) exact hno ⟨Y, hY, hCYstrict, Set.ssubset_iff_subset_ne.mpr ⟨hYX, hYXne⟩⟩ · exact hCY

theorem vanishingIdeal_mem_minimalPrimes_span_of_no_intermediate {ι : Type*} [Finite ι] {C X : Set (ι → ℂ)} (hC : IsIrreducibleAffineClosed C) (hX : IsIrreducibleAffineClosed X) (hCX : C ⊆ X) (P : MvPolynomial ι ℂ) (hPC : P ∈ MvPolynomial.vanishingIdeal ℂ C) (hPX : P ∉ MvPolynomial.vanishingIdeal ℂ X) (hno : ¬ ∃ Y, IsIrreducibleAffineClosed Y ∧ C ⊂ Y ∧ Y ⊂ X) : MvPolynomial.vanishingIdeal ℂ C ∈ (MvPolynomial.vanishingIdeal ℂ X ⊔ span {P}).minimalPrimes := by let I := MvPolynomial.vanishingIdeal ℂ X let J := MvPolynomial.vanishingIdeal ℂ C haveI hIprime : I.IsPrime := (irreducibleAffineClosed_iff_isPrime hX.1 hX.2.1).mp hX haveI hJprime : J.IsPrime := (irreducibleAffineClosed_iff_isPrime hC.1 hC.2.1).mp hC have hIJ : I ≤ J := MvPolynomial.vanishingIdeal_anti_mono hCX have hspanJ : span {P} ≤ J := Ideal.span_le.mpr (by simpa [J] using hPC) have hsupJ : I ⊔ span {P} ≤ J := sup_le hIJ hspanJ refine ⟨⟨inferInstance, hsupJ⟩, ?_⟩ intro Q hQ hQJ haveI hQprime : Q.IsPrime := hQ.1 have hIQ : I ≤ Q := le_sup_left.trans hQ.2 have hPQ : P ∈ Q := hQ.2 (Ideal.mem_sup_right (Ideal.subset_span (by simp))) have hIQne : I ≠ Q := by intro heq apply hPX change P ∈ I rw [heq] exact hPQ have hIQlt : I < Q := lt_of_le_of_ne hIQ hIQne by_contra hJQ change ¬ J ≤ Q at hJQ change Q ≤ J at hQJ have hQJne : Q ≠ J := by intro heq apply hJQ rw [← heq] have hQJlt : Q < J := lt_of_le_of_ne hQJ hQJne have hzeroJ : zeroLocus ℂ J = C := by simpa [J, affineZariskiClosure] using hC.1 have hzeroI : zeroLocus ℂ I = X := by simpa [I, affineZariskiClosure] using hX.1 apply hno exact ⟨MvPolynomial.zeroLocus ℂ Q, irreducible_zeroLocus_of_prime Q, by simpa only [hzeroJ] using (zeroLocus_strict_anti hQJlt), by simpa only [hzeroI] using (zeroLocus_strict_anti hIQlt)⟩

theorem polynomialImageClosure_vanishingIdeal {ι κ : Type*} (f : κ → MvPolynomial ι ℂ) : vanishingIdeal ℂ (polynomialImageClosure f) = ker (polynomialPullback f) := by -- First replace the closure by the original range: a polynomial vanishes on -- a set iff it vanishes on the zero locus of that set's vanishing ideal. -- Membership in the range ideal is then `eval_polynomialPullback`; the -- reverse implication uses `MvPolynomial.funext` in the finite source. ext P constructor · intro hP change polynomialPullback f P = 0 apply MvPolynomial.funext intro x rw [eval_polynomialPullback] exact hP _ (affineZariskiClosure_extensive _ ⟨x, rfl⟩) · intro hP change polynomialPullback f P = 0 at hP intro y hy change y ∈ zeroLocus ℂ (vanishingIdeal ℂ (range (polynomialCoordinateMap f))) at hy exact hy P (by intro z hz obtain ⟨x, rfl⟩ := hz change eval (polynomialCoordinateMap f x) P = 0 rw [← eval_polynomialPullback, hP] exact map_zero _)

lemma affineZariskiClosure_polynomial_image_of_dense {ι κ : Type*} {f : (ι → ℂ) → (κ → ℂ)} (hf : IsPolynomialMap f) {A : Set (ι → ℂ)} (hA : affineZariskiClosure A = univ) : affineZariskiClosure (f '' A) = affineZariskiClosure (range f) := by apply Set.Subset.antisymm · exact affineZariskiClosure_mono (Set.image_subset_range f A) · intro y hy P hP change eval y P = 0 obtain ⟨Q, hQ⟩ := hf.eval_comp P have hQA : ∀ x ∈ A, eval x Q = 0 := by intro x hx rw [hQ x] exact hP (f x) ⟨x, hx, rfl⟩ have hQall : ∀ x, eval x Q = 0 := by intro x have hx : x ∈ affineZariskiClosure A := by rw [hA]; trivial exact hx Q hQA exact hy P (by rintro _ ⟨x, rfl⟩ have hx : eval (f x) P = 0 := (hQ x).symm.trans (hQall x) simpa [MvPolynomial.aeval_def, MvPolynomial.eval₂_id] using hx)

theorem irreducible_affineClosure_polynomial_image_of_dense {ι κ : Type*} [Finite ι] {f : (ι → ℂ) → (κ → ℂ)} (hf : IsPolynomialMap f) {A : Set (ι → ℂ)} (hA : affineZariskiClosure A = Set.univ) (hne : A.Nonempty) : IsIrreducibleAffineClosed (affineZariskiClosure (f '' A)) := by refine ⟨affineZariskiClosure_idem _, hne.image f |>.mono (affineZariskiClosure_extensive _), ?_⟩ intro B C hB hC hBC have hpreB := polynomial_preimage_closed hf hB have hpreC := polynomial_preimage_closed hf hC have hpreUnion : affineZariskiClosure (f ⁻¹' (B ∪ C)) = f ⁻¹' (B ∪ C) := by rw [Set.preimage_union] exact affineZariskiClosure_union hpreB hpreC have hrange : range f ⊆ B ∪ C := by intro y hy have hyc : y ∈ affineZariskiClosure (f '' A) := by rw [affineZariskiClosure_polynomial_image_of_dense hf hA] exact affineZariskiClosure_extensive _ hy rw [hBC] at hyc exact hyc have huniv : Set.univ = f ⁻¹' B ∪ f ⁻¹' C := by rw [← Set.preimage_union] symm apply Set.eq_univ_of_forall intro x exact hrange ⟨x, rfl⟩ have hirrUniv : IsIrreducibleAffineClosed (Set.univ : Set (ι → ℂ)) := by have hzero : vanishingIdeal ℂ (Set.univ : Set (ι → ℂ)) = ⊥ := by apply le_antisymm · intro P hP apply MvPolynomial.funext intro x exact hP x trivial · exact bot_le have hclosed : affineZariskiClosure (Set.univ : Set (ι → ℂ)) = Set.univ := by exact Set.eq_univ_of_forall (fun _ => affineZariskiClosure_extensive _ trivial) apply (irreducibleAffineClosed_iff_isPrime hclosed Set.univ_nonempty).mpr rw [hzero] infer_instance rcases hirrUniv.2.2 _ _ hpreB hpreC huniv with hfull | hfull · left apply Set.Subset.antisymm · have him : f '' A ⊆ B := by rintro _ ⟨x, _, rfl⟩ have : x ∈ f ⁻¹' B := by rw [← hfull]; trivial exact this simpa [hB] using affineZariskiClosure_mono him · intro y hy rw [hBC] exact Or.inl hy · right apply Set.Subset.antisymm · have him : f '' A ⊆ C := by rintro _ ⟨x, _, rfl⟩ have : x ∈ f ⁻¹' C := by rw [← hfull]; trivial exact this simpa [hC] using affineZariskiClosure_mono him · intro y hy rw [hBC] exact inr hy

lemma finiteCoordinateRange_closed {κ : Type*} (c : κ) (S : Finset ℂ) : affineZariskiClosure {x : κ → ℂ | x c ∈ S} = {x | x c ∈ S} := by have heq : {x : κ → ℂ | x c ∈ S} = {x | eval x (coordinateValuePolynomial c S) = 0} := by ext x simp [coordinateValuePolynomial, Finset.prod_eq_zero_iff, sub_eq_zero] rw [heq] exact affineZariskiClosure_zero_of_polynomial _

lemma pderiv_polynomialPullback {ι κ : Type*} [Fintype κ] (f : κ → MvPolynomial ι ℂ) (P : MvPolynomial κ ℂ) (i : ι) : pderiv i (polynomialPullback f P) = ∑ j : κ, polynomialPullback f (pderiv j P) * pderiv i (f j) := by classical induction P using MvPolynomial.induction_on with | C a => simp [polynomialPullback] | add P Q hP hQ => simp only [map_add, hP, hQ] rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro j _ ring | mul_X P j hP => simp only [map_mul, MvPolynomial.pderiv_mul, MvPolynomial.pderiv_X, map_add, hP] simp_rw [add_mul] rw [Finset.sum_add_distrib] congr 1 · rw [Finset.sum_mul] apply Finset.sum_congr rfl intro x _ ring · simp [polynomialPullback, Pi.single_apply]

lemma totalDegree_pderiv_lt {σ R : Type*} [CommSemiring R] {i : σ} {P : MvPolynomial σ R} (hP : pderiv i P ≠ 0) : (pderiv i P).totalDegree < P.totalDegree := by classical have hdeg_pos : 0 < P.totalDegree := by apply Nat.pos_of_ne_zero intro hdeg apply hP rw [(MvPolynomial.totalDegree_eq_zero_iff_eq_C).mp hdeg, MvPolynomial.pderiv_C] have hle : (pderiv i P).totalDegree ≤ P.totalDegree - 1 := by have hpderiv : pderiv i P = ∑ m ∈ P.support, pderiv i (monomial m (P.coeff m)) := by simpa only [map_sum] using congrArg (pderiv i) P.as_sum rw [hpderiv] apply MvPolynomial.totalDegree_finsetSum_le intro m hm rw [MvPolynomial.pderiv_monomial] by_cases hmi : m i = 0 · simp [hmi] · refine (MvPolynomial.totalDegree_monomial_le _ _).trans ?_ change (m - Finsupp.single i 1).degree ≤ P.totalDegree - 1 have hmdeg : (m - Finsupp.single i 1).degree + 1 = m.degree := by simpa [Finsupp.degree_eq_weight_one] using (Finsupp.weight_sub_single_add (w := fun _ : σ => (1 : ℕ)) hmi) have hmle : m.degree ≤ P.totalDegree := by simpa [Finsupp.degree_apply, Finsupp.sum] using MvPolynomial.le_totalDegree hm omega exact hle.trans_lt (sub_lt hdeg_pos Nat.zero_lt_one)

lemma sum_X_mul_pderiv_eq_sum_degree {σ R : Type*} [Fintype σ] [CommSemiring R] (P : MvPolynomial σ R) : (∑ i : σ, X i * pderiv i P) = ∑ m ∈ P.support, m.degree • monomial m (P.coeff m) := by classical calc (∑ i : σ, X i * pderiv i P) = ∑ i : σ, X i * pderiv i (∑ m ∈ P.support, monomial m (P.coeff m)) := by apply Finset.sum_congr rfl intro i _ exact congrArg (fun Q => X i * pderiv i Q) P.as_sum _ = _ := by simp_rw [map_sum, Finset.mul_sum, MvPolynomial.X_mul_pderiv_monomial] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro m _ rw [← Finset.sum_smul, ← Finsupp.degree_eq_sum]

lemma eq_C_of_forall_pderiv_eq_zero {σ K : Type*} [Finite σ] [Field K] [CharZero K] (P : MvPolynomial σ K) (hP : ∀ i, pderiv i P = 0) : P = C (P.coeff 0) := by classical letI := ofFinite σ have heuler := sum_X_mul_pderiv_eq_sum_degree (R := K) P have hleft : (∑ i : σ, (MvPolynomial.X i : MvPolynomial σ K) * pderiv i P) = 0 := by simp [hP] have heuler0 : (0 : MvPolynomial σ K) = _ := hleft.symm.trans heuler have hdegree : ∀ m ∈ P.support, m.degree = 0 := by intro m hm have hc := congrArg (coeff m) heuler0 have hrhs : coeff m (∑ x ∈ P.support, x.degree • monomial x (P.coeff x)) = (m.degree : K) * P.coeff m := by calc _ = ∑ x ∈ P.support, coeff m (x.degree • monomial x (P.coeff x)) := MvPolynomial.coeff_sum P.support (fun x => x.degree • monomial x (P.coeff x)) m _ = _ := by have hcoeff_nsmul (n : ℕ) (Q : MvPolynomial σ K) : coeff m (n • Q) = n • coeff m Q := (MvPolynomial.coeffAddMonoidHom m).map_nsmul n Q simp_rw [hcoeff_nsmul, MvPolynomial.coeff_monomial] rw [Finset.sum_eq_single m] · simp [nsmul_eq_mul] · intro x hx hxm simp [hxm] · exact fun hnot => (hnot hm).elim have hmul : (m.degree : K) * P.coeff m = 0 := by calc _ = coeff m _ := hrhs.symm _ = coeff m 0 := hc.symm _ = 0 := by simp have hcoeff : P.coeff m ≠ 0 := MvPolynomial.mem_support_iff.mp hm have hcast : (m.degree : K) = 0 := (mul_eq_zero.mp hmul).resolve_right hcoeff exact_mod_cast hcast apply MvPolynomial.totalDegree_eq_zero_iff_eq_C.mp rw [totalDegree] exact Finset.sup_eq_zero.mpr fun m hm => by change degree m = 0 exact hdegree m hm

theorem algebraicIndependent_of_polynomialJacobianMinor_ne_zero {ι κ : Type*} {d : ℕ} (f : κ → MvPolynomial ι ℂ) (rows : Fin d → κ) (cols : Fin d → ι) (hminor : polynomialJacobianMinor f rows cols ≠ 0) : AlgebraicIndependent ℂ (fun a => f (rows a)) := by classical let g : Fin d → MvPolynomial ι ℂ := fun a => f (rows a) by_contra hAI rw [algebraicIndependent_iff] at hAI push_neg at hAI obtain ⟨P₀, hP₀ker, hP₀ne⟩ := hAI let bad : ℕ → Prop := fun n => ∃ P : MvPolynomial (Fin d) ℂ, P ≠ 0 ∧ polynomialPullback g P = 0 ∧ P.totalDegree = n have hbad : ∃ n, bad n := by refine ⟨P₀.totalDegree, P₀, hP₀ne, ?_, rfl⟩ simpa [g, polynomialPullback] using hP₀ker let n := find hbad obtain ⟨P, hPne, hPker, hPdeg⟩ : bad n := Nat.find_spec hbad let J : Matrix (Fin d) (Fin d) (MvPolynomial ι ℂ) := of fun a b => pderiv (cols b) (g a) let v : Fin d → MvPolynomial ι ℂ := fun a => polynomialPullback g (pderiv a P) have hchain (b : Fin d) : ∑ a : Fin d, polynomialPullback g (pderiv a P) * pderiv (cols b) (g a) = 0 := by have hp := congrArg (pderiv (cols b)) hPker simpa [pderiv_polynomialPullback] using hp have hmul : mulVec J.transpose v = 0 := by funext b simpa [J, v, mulVec, transpose, dotProduct, mul_comm] using hchain b have hdet : J.transpose.det ≠ 0 := by rw [Matrix.det_transpose] simpa [J, g, polynomialJacobianMinor] using hminor have hv : v = 0 := Matrix.eq_zero_of_mulVec_eq_zero hdet hmul have hpartials : ∀ a : Fin d, pderiv a P = 0 := by intro a have hQker : polynomialPullback g (pderiv a P) = 0 := by have ha := congrFun hv a simpa [v] using ha by_contra hQne have hlt := totalDegree_pderiv_lt hQne have hbadQ : bad (pderiv a P).totalDegree := ⟨MvPolynomial.pderiv a P, hQne, hQker, rfl⟩ have hmin : n ≤ (pderiv a P).totalDegree := by dsimp [n] exact Nat.find_min' hbad hbadQ exact (not_lt_of_ge hmin) (hlt.trans_eq hPdeg) have hconst := eq_C_of_forall_pderiv_eq_zero P hpartials have hcoeff : P.coeff 0 = 0 := by have hk := hPker rw [hconst] at hk simpa [polynomialPullback] using hk apply hPne rw [hconst, hcoeff, MvPolynomial.C_0]

theorem polynomialImageClosure_dimension_of_jacobian_and_surjection {ι κ : Type*} [Finite ι] [Finite κ] {d : ℕ} (f : κ → MvPolynomial ι ℂ) (rows : Fin d → κ) (cols : Fin d → ι) (hminor : polynomialJacobianMinor f rows cols ≠ 0) (present : MvPolynomial (Fin d) ℂ →ₐ[ℂ] polynomialCoordinateSubalgebra f) (hsurj : Surjective present) : HasAffineZariskiDimension d (polynomialImageClosure f) := by exact polynomialImageClosure_dimension_of_jacobian f rows cols hminor (by simpa using coordinateSubalgebra_trdeg_le_of_surjection f present hsurj)

lemma image_strictMono_on {α β ι : Type*} [Preorder ι] (f : α → β) {S : Set α} (hf : InjOn f S) {chain : ι → Set α} (hc : StrictMono chain) (hsub : ∀ i, chain i ⊆ S) : StrictMono (fun i => f '' chain i) := by intro i j hij have hs := hc hij refine Set.ssubset_iff_subset_ne.mpr ⟨Set.image_mono hs.le, ?_⟩ intro heq change f '' chain i = f '' chain j at heq apply hs.ne ext x constructor · intro hx have him : f x ∈ f '' chain j := by rw [← heq] exact ⟨x, hx, rfl⟩ obtain ⟨y, hy, hfy⟩ := him exact hf (hsub i hx) (hsub j hy) hfy.symm ▸ hy · intro hx have him : f x ∈ f '' chain i := by rw [heq] exact ⟨x, hx, rfl⟩ obtain ⟨y, hy, hfy⟩ := him exact hf (hsub j hx) (hsub i hy) hfy.symm ▸ hy

lemma irreducible_image_polynomial_retract {ι κ : Type*} {f : (ι → ℂ) → (κ → ℂ)} {g : (κ → ℂ) → (ι → ℂ)} (hf : IsPolynomialMap f) (hg : IsPolynomialMap g) (hleft : LeftInverse g f) {A : Set (ι → ℂ)} : IsIrreducibleAffineClosed A → IsIrreducibleAffineClosed (f '' A) := by intro hA refine ⟨polynomial_image_closed_of_retract hf hg hleft hA.1, hA.2.1.image f, ?_⟩ intro B C hB hC hBC have hpreB := polynomial_preimage_closed hf hB have hpreC := polynomial_preimage_closed hf hC have hApre : A = f ⁻¹' B ∪ f ⁻¹' C := by ext x constructor · intro hx exact (Set.ext_iff.mp hBC (f x)).mp ⟨x, hx, rfl⟩ · intro hx have him : f x ∈ f '' A := (Set.ext_iff.mp hBC (f x)).mpr hx obtain ⟨y, hy, hfy⟩ := him exact hleft.injective hfy ▸ hy rcases hA.2.2 _ _ hpreB hpreC hApre with h | h · left ext y constructor · rintro ⟨x, hx, rfl⟩ have : x ∈ f ⁻¹' B := by rw [← h]; exact hx exact this · intro hy exact (Set.ext_iff.mp hBC y).mpr (inl hy) · right ext y constructor · rintro ⟨x, hx, rfl⟩ have : x ∈ f ⁻¹' C := by rw [← h]; exact hx exact this · intro hy exact (Set.ext_iff.mp hBC y).mpr (inr hy)

theorem finiteTypeDomain_ringKrullDim_eq_trdeg (K A : Type*) [Field K] [CommRing A] [Algebra K A] [IsDomain A] [FiniteType K A] (d : ℕ) (htrdeg : trdeg K A = d) : ringKrullDim A = d := by -- `exists_finite_inj_algHom_of_fg` gives `g : K[X₁, ..., Xₛ] →ₐ[K] A`. -- For the upper dimension inequality, contract prime chains along `g`; strictness -- follows from `Ideal.comap_lt_comap_of_integral_mem_sdiff`. For the lower -- inequality, lift each finite `LTSeries` one prime at a time with -- `Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime` (going up). -- `MvPolynomial.ringKrullDim_of_isNoetherianRing` computes the normalized ring. -- Finally `Algebra.trdeg_add_eq`, `Algebra.IsAlgebraic.trdeg_eq_zero`, and -- `MvPolynomial.trdeg_of_isDomain` identify `s` with the certified `d`. obtain ⟨s, g, hg_inj, hg_int⟩ := exists_integral_inj_algHom_of_fg K A let a : Algebra (MvPolynomial (Fin s) K) A := g.toRingHom.toAlgebra letI : Algebra (MvPolynomial (Fin s) K) A := a have ha_int : @Algebra.IsIntegral (MvPolynomial (Fin s) K) A _ _ a := by refine @Algebra.IsIntegral.mk (MvPolynomial (Fin s) K) A _ _ a ?_ intro x exact hg_int x let f : PrimeSpectrum A → PrimeSpectrum (MvPolynomial (Fin s) K) := PrimeSpectrum.comap g.toRingHom have hf_mono : StrictMono f := by intro I J hIJ change I.asIdeal < J.asIdeal at hIJ change I.asIdeal.comap g.toRingHom < J.asIdeal.comap g.toRingHom obtain ⟨hIJle, x, hxJ, hxI⟩ := SetLike.lt_iff_le_and_exists.mp hIJ apply @Ideal.comap_lt_comap_of_integral_mem_sdiff (MvPolynomial (Fin s) K) _ A _ I.asIdeal J.asIdeal a I.isPrime hIJle · exact ⟨hxJ, hxI⟩ · exact hg_int x have lift_chain : ∀ (n : ℕ) (p : LTSeries (PrimeSpectrum (MvPolynomial (Fin s) K))), p.length = n → ∃ q : LTSeries (PrimeSpectrum A), q.length = n ∧ f q.last = p.last := by intro n induction n with | zero => intro p hp obtain ⟨Q, hQ⟩ := hg_int.comap_surjective hg_inj p.last refine ⟨LTSeries.mk 0 (fun _ => Q) (by intro i j hij fin_cases i fin_cases j exact (lt_irrefl _ hij).elim), rfl, ?_⟩ exact hQ | succ n ih => intro p hp let p' : LTSeries (PrimeSpectrum (MvPolynomial (Fin s) K)) := p.eraseLast have hp' : p'.length = n := by simp [p', hp] obtain ⟨q, hq_len, hq_last⟩ := ih p' hp' have hlast : p'.last < p.last := by simpa [p'] using p.eraseLast_last_rel_last (by simp [hp]) have hle : q.last.asIdeal.comap g.toRingHom ≤ p.last.asIdeal := by calc q.last.asIdeal.comap g.toRingHom = (f q.last).asIdeal := rfl _ = p'.last.asIdeal := congrArg PrimeSpectrum.asIdeal hq_last _ ≤ p.last.asIdeal := hlast.le obtain ⟨Q, hQ_ge, hQ_prime, hQ_comap⟩ := @Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime (MvPolynomial (Fin s) K) _ A _ a ha_int p.last.asIdeal p.last.isPrime q.last.asIdeal q.last.isPrime hle let Q' : PrimeSpectrum A := ⟨Q, hQ_prime⟩ have hqQ : q.last < Q' := by change q.last.asIdeal < Q refine lt_of_le_of_ne hQ_ge ?_ intro h_eq have h_eq' : p'.last.asIdeal = p.last.asIdeal := by calc p'.last.asIdeal = q.last.asIdeal.comap g.toRingHom := by exact (congrArg PrimeSpectrum.asIdeal hq_last).symm _ = Q.comap g.toRingHom := congrArg (Ideal.comap g.toRingHom) h_eq _ = p.last.asIdeal := hQ_comap apply hlast.ne exact PrimeSpectrum.ext h_eq' refine ⟨q.snoc Q' hqQ, ?_, ?_⟩ · simp [hq_len] · apply PrimeSpectrum.ext simp only [RelSeries.last_snoc] change Q.comap g.toRingHom = p.last.asIdeal exact hQ_comap have hdim : ringKrullDim A = ringKrullDim (MvPolynomial (Fin s) K) := by apply le_antisymm · exact Order.krullDim_le_of_strictMono f hf_mono · rw [MvPolynomial.ringKrullDim_of_isNoetherianRing] rw [ringKrullDim_eq_zero_of_field] simp only [zero_add, Nat.card_eq_fintype_card, Fintype.card_fin] apply (Order.le_krullDim_iff).mpr have hpoly : (s : WithBot ℕ∞) = Order.krullDim (PrimeSpectrum (MvPolynomial (Fin s) K)) := by change (s : WithBot ℕ∞) = ringKrullDim (MvPolynomial (Fin s) K) rw [MvPolynomial.ringKrullDim_of_isNoetherianRing, ringKrullDim_eq_zero_of_field] simp obtain ⟨p, hp⟩ := (Order.le_krullDim_iff.mp hpoly.le) obtain ⟨q, hq, _⟩ := lift_chain s p hp exact ⟨q, hq⟩ rw [hdim, MvPolynomial.ringKrullDim_of_isNoetherianRing] have ha_alg : @Algebra.IsAlgebraic (MvPolynomial (Fin s) K) A _ _ a := @Algebra.IsIntegral.isAlgebraic (MvPolynomial (Fin s) K) A _ _ a (inferInstance) ha_int haveI : IsScalarTower K (MvPolynomial (Fin s) K) A := IsScalarTower.of_algebraMap_eq' (by ext x exact (g.commutes x).symm) haveI : FaithfulSMul (MvPolynomial (Fin s) K) A := (faithfulSMul_iff_algebraMap_injective (MvPolynomial (Fin s) K) A).mpr (by change Injective g.toRingHom exact hg_inj) have hzero : @trdeg (MvPolynomial (Fin s) K) A _ _ a = 0 := @trdeg_eq_zero (MvPolynomial (Fin s) K) A _ _ a ha_alg have h := @lift_trdeg_add_eq K (MvPolynomial (Fin s) K) A _ _ _ (inferInstance) (inferInstance) a (inferInstance) (inferInstance) (inferInstance) (inferInstance) (inferInstance) rw [hzero, lift_zero, add_zero] at h have hs : s = d := by have hnat := congrArg Cardinal.toNat h simp only [Cardinal.toNat_lift] at hnat rw [MvPolynomial.trdeg_of_isDomain, htrdeg] at hnat simpa using hnat simp [ringKrullDim_eq_zero_of_field, hs]

theorem coordinateSubalgebra_trdeg_le_of_surjection {ι κ τ : Type*} [Finite τ] (f : κ → MvPolynomial ι ℂ) (present : MvPolynomial τ ℂ →ₐ[ℂ] polynomialCoordinateSubalgebra f) (hsurj : Surjective present) : @trdeg ℂ (polynomialCoordinateSubalgebra f) _ _ (coordinateSubalgebraAlgebra f) ≤ card τ := by -- Apply `Algebra.trdeg_le_of_surjective present hsurj`, rewrite the source -- with `MvPolynomial.trdeg_of_isDomain`, then simplify `#(Fin d)` to `d`. let calgebra : Algebra ℂ (polynomialCoordinateSubalgebra f) := coordinateSubalgebraAlgebra f letI := ofFinite τ have h := @lift_trdeg_le_of_surjective ℂ (MvPolynomial τ ℂ) (polynomialCoordinateSubalgebra f) _ _ _ _ calgebra present hsurj simpa [calgebra, Nat.card_eq_fintype_card] using h

theorem coordinateSubalgebra_trdeg_le_of_polynomial_factorization {ι κ τ : Type} [Finite τ] (f : κ → MvPolynomial ι ℂ) (g : τ → MvPolynomial ι ℂ) (h : κ → MvPolynomial τ ℂ) (hfac : ∀ k, bind₁ g (h k) = f k) : @trdeg ℂ (polynomialCoordinateSubalgebra f) _ _ (Subalgebra.algebra (polynomialCoordinateSubalgebra f)) ≤ card τ := by letI := ofFinite τ let A := polynomialCoordinateSubalgebra f let B := polynomialCoordinateSubalgebra g letI : Algebra ℂ A := Subalgebra.algebra A letI : Algebra ℂ B := Subalgebra.algebra B have hAB : A ≤ B := by rintro q ⟨P, rfl⟩ refine ⟨MvPolynomial.bind₁ h P, ?_⟩ change bind₁ g (bind₁ h P) = bind₁ f P rw [MvPolynomial.bind₁_bind₁] rw [show (fun k => bind₁ g (h k)) = f from funext hfac] let inc : A →ₐ[ℂ] B := Subalgebra.inclusion hAB have hinc : Injective inc := Subalgebra.inclusion_injective hAB have hleAB := @trdeg_le_of_injective ℂ A _ _ (Subalgebra.algebra A) B _ (Subalgebra.algebra B) inc hinc have hleB := @trdeg_le_of_surjective ℂ (MvPolynomial τ ℂ) _ _ _ B _ (Subalgebra.algebra B) (polynomialPullback g).rangeRestrict (polynomialPullback g).rangeRestrict_surjective change @trdeg ℂ A _ _ (Subalgebra.algebra A) ≤ card τ exact hleAB.trans (by simpa [B] using hleB)