Bump mathlib

LeanCamCombi.lean

@@ -24,9 +24,7 @@ import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
 import LeanCamCombi.GrowthInGroups.LinearLowerBound
-import LeanCamCombi.GrowthInGroups.SpanRangeUpdate
 import LeanCamCombi.Impact
-import LeanCamCombi.Incidence
 import LeanCamCombi.Kneser.Kneser
 import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
@@ -35,10 +33,10 @@ import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Module.Submodule.Defs
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
-import LeanCamCombi.Mathlib.Algebra.MvPolynomial.CommRing
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow
+import LeanCamCombi.Mathlib.Algebra.Polynomial.CoeffMem
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
@@ -55,7 +53,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
-import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
@@ -64,7 +61,6 @@ import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.OpenPos
 import LeanCamCombi.Mathlib.Order.Flag
-import LeanCamCombi.Mathlib.Order.Monotone.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions

LeanCamCombi/GrowthInGroups/Chevalley.lean

@@ -22,21 +22,21 @@ lemma Ideal.span_range_update_divByMonic' {ι : Type*} [DecidableEq ι]
   · intro k
     by_cases hjk : j = k
     · subst hjk
-      rw [Function.update_same, modByMonic_eq_sub_mul_div (v j) H]
+      rw [Function.update_self, modByMonic_eq_sub_mul_div (v j) H]
       apply sub_mem (Ideal.subset_span ?_) (Ideal.mul_mem_right _ _
         (Ideal.mul_mem_left _ _ <| Ideal.subset_span ?_))
       · exact ⟨j, rfl⟩
       · exact ⟨i, rfl⟩
-    exact Ideal.subset_span ⟨k, (Function.update_noteq (.symm hjk) _ _).symm⟩
+    exact Ideal.subset_span ⟨k, (Function.update_of_ne (.symm hjk) _ _).symm⟩
   · intro k
     by_cases hjk : j = k
     · subst hjk
       nth_rw 2 [← modByMonic_add_div (v j) H]
       apply add_mem (Ideal.subset_span ?_) (Ideal.mul_mem_right _ _
         (Ideal.mul_mem_left _ _ <| Ideal.subset_span ?_))
-      · exact ⟨j, Function.update_same _ _ _⟩
-      · exact ⟨i, Function.update_noteq hij _ _⟩
-    exact Ideal.subset_span ⟨k, Function.update_noteq (.symm hjk) _ _⟩
+      · exact ⟨j, Function.update_self _ _ _⟩
+      · exact ⟨i, Function.update_of_ne hij _ _⟩
+    exact Ideal.subset_span ⟨k, Function.update_of_ne (.symm hjk) _ _⟩
 
 lemma foo_induction
     (P : ∀ (R : Type u) [CommRing R], Ideal R[X] → Prop)
@@ -103,7 +103,7 @@ lemma foo_induction
       · simp only [hv, ne_eq, not_exists, not_and, not_forall, not_le, funext_iff,
           Function.comp_apply, exists_prop, ofLex_toLex]
         use j
-        simp only [Function.update_same]
+        simp only [Function.update_self]
         refine ((degree_modByMonic_lt _ (monic_unit_leadingCoeff_inv_smul _ _)).trans_le
           ((degree_C_mul_eq_of_mul_ne_zero _ _ ?_).trans_le i_min)).ne
         rw [IsUnit.val_inv_mul]

LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean

@@ -6,14 +6,12 @@ import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow
+import LeanCamCombi.Mathlib.Algebra.Polynomial.CoeffMem
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
-import LeanCamCombi.Mathlib.Order.Monotone.Basic
 import LeanCamCombi.GrowthInGroups.ConstructibleSetData
-import LeanCamCombi.GrowthInGroups.SpanRangeUpdate
 
 variable {R S M A : Type*} [CommRing R] [CommRing S] [AddCommGroup M] [Module R M] [CommRing A]
   [Algebra R A]
@@ -138,7 +136,7 @@ lemma foo_induction (n : ℕ)
         · simp only [hv, ne_eq, not_exists, not_and, not_forall, not_le, funext_iff,
             Function.comp_apply, exists_prop, ofLex_toLex]
           use j
-          simp only [Function.update_same]
+          simp only [Function.update_self]
           refine ((degree_modByMonic_lt _ hi).trans_le i_min).ne
     -- Case II : The `e i ≠ 0` with minimal degree has non-invertible leading coefficient
     obtain ⟨i, hi, i_min⟩ : ∃ i, e.1 i ≠ 0 ∧ ∀ j, e.1 j ≠ 0 → (e.1 i).degree ≤ (e.1 j).degree := by
@@ -377,7 +375,7 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus :
     obtain ⟨S, hS, hS'⟩ := H f
     refine ⟨S, Eq.trans ?_ hS, ?_⟩
     · rw [← zeroLocus_span (Set.range _), ← zeroLocus_span (Set.range _),
-        Ideal.span_range_update_divByMonic _ hne hi]
+        idealSpan_range_update_divByMonic hne hi]
     · intro C hC
       let c' : InductionObj _ _ := ⟨Function.update c.val j (c.val j %ₘ c.val i)⟩
       have deg_bound₁ : c'.degBound ≤ c.degBound := by
@@ -561,7 +559,7 @@ lemma δ_pos (k : ℕ) (D : ℕ → ℕ) : ∀ n, 0 < δ k D n
   | 0 => by simp
   | (n + 1) => by
     simp only [δ_succ, CanonicallyOrderedCommSemiring.mul_pos]
-    exact ⟨Nat.pow_self_pos _, δ_pos _ _ _⟩
+    exact ⟨Nat.pow_self_pos, δ_pos _ _ _⟩
 
 lemma exists_constructibleSetData_comap_C_toSet_eq_toSet'
     {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n))
@@ -643,13 +641,12 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet'
     refine pow_inf_le.trans (inf_le_inf ?_ ?_)
     · refine (pow_le_pow_right' ?_ (Nat.pow_self_mono hS')).trans Submodule.mvPolynomial_pow_le
       simpa [MvPolynomial.coeff_one, apply_ite] using hM
-    · rw [← MvPolynomial.degreesLE_pow,
-        Submodule.restrictScalars_pow (Nat.pow_self_pos _).ne']
+    · rw [← MvPolynomial.degreesLE_pow, Submodule.restrictScalars_pow Nat.pow_self_pos.ne']
       refine pow_le_pow_right' ?_ (Nat.pow_self_mono hS')
       simp
   have h1M : 1 ≤ M := Submodule.one_le_iff.mpr hM
   obtain ⟨U, hU₁, hU₂⟩ := IH (M := M ^ N)
-    (SetLike.le_def.mp (le_self_pow' h1M (Nat.pow_self_pos _).ne') hM) _ _ T
+    (SetLike.le_def.mp (le_self_pow' h1M Nat.pow_self_pos.ne') hM) _ _ T
     (fun C hCT ↦ (hT₂ C hCT).1)
     (fun C hCT k ↦ this C hCT k)
   simp only [Multiset.map_nsmul _ (_ ^ _), smul_comm _ (_ ^ _),
@@ -672,7 +669,7 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet'
       ConstructibleSetData.toSet_map]
     show _ = _ '' ((comapEquiv e.toRingEquiv).symm ⁻¹' _)
     rw [← Equiv.image_eq_preimage, Set.image_image]
-    simp only [comapEquiv_apply, ← comap_eq_specComap', ← comap_comp_apply]
+    simp only [comapEquiv_apply, ← comap_apply, ← comap_comp_apply]
     congr!
     exact e.symm.toAlgHom.comp_algebraMap.symm
   · refine (ν_le_ν hS' _ fun _ _ ↦ ?_).trans
@@ -753,7 +750,7 @@ lemma chevalley_mvPolynomial_mvPolynomial
       ← Function.comp_def (g := finSumFinEquiv.symm), Set.range_comp,
       Equiv.range_eq_univ, Set.image_univ, Set.Sum.elim_range,
       Set.image_diff (hf := comap_injective_of_surjective g hg'), zeroLocus_union]
-    simp [hg'', ← Set.inter_diff_distrib_right, Set.diff_inter_right_comm]
+    simp [hg'', ← Set.inter_diff_distrib_right, Set.sdiff_inter_right_comm]
   obtain ⟨T, hT, hT'⟩ :=
     exists_constructibleSetData_comap_C_toSet_eq_toSet'
     (M := (MvPolynomial.degreesLE R (Fin m) Finset.univ.1).restrictScalars ℤ) (by simp) (k + m) d S'
@@ -786,7 +783,7 @@ lemma chevalley_mvPolynomial_mvPolynomial
   refine ⟨T, ?_, fun C hCT ↦ ⟨(hT' C hCT).1, fun i j ↦ ?_⟩⟩
   · rwa [← hg, comap_comp, ContinuousMap.coe_comp, Set.image_comp, hS']
   · have := (hT' C hCT).2 i
-    rw [← Submodule.restrictScalars_pow (hn := (δ_pos _ _ _).ne'), MvPolynomial.degreesLE_pow,
+    rw [← Submodule.restrictScalars_pow (δ_pos ..).ne', MvPolynomial.degreesLE_pow,
       Submodule.restrictScalars_mem, MvPolynomial.mem_degreesLE,
         Multiset.le_iff_count] at this
     simp only [Multiset.count_nsmul, Multiset.count_univ, mul_one] at this

LeanCamCombi/GrowthInGroups/ConstructibleSetData.lean

@@ -1,18 +1,38 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Andrew Yang
+-/
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Order.SuccPred.WithBot
 
-open Finset PrimeSpectrum
+/-!
+# Constructible sets in the prime spectrum
+
+This file provides tooling for manipulating constructible sets in the prime spectrum of a ring.
+
+## TODO
+
+Link to constructible sets in a topological space.
+-/
+
+open Finset
 open scoped Polynomial
 
+namespace PrimeSpectrum
 variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
 
-/-! ### Bare types -/
-
 variable (R) in
+/-- The data of a constructible set `s` is finitely many tuples `(f, g₁, ..., gₙ)` such that
+`s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`.
+
+To obtain `s` from its data, use `PrimeSpectrum.ConstructibleSetData.toSet`. -/
 abbrev ConstructibleSetData := Finset (Σ n, R × (Fin n → R))
 
 namespace ConstructibleSetData
 
+/-- Given the data of the constructible set `s`, build the data of the constructible set
+`{I | {x | f x ∈ I} ∈ s}`. -/
 def map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) : ConstructibleSetData S :=
   s.image <| Sigma.map id fun _n (r, g) ↦ (f r, f ∘ g)
 
@@ -23,28 +43,11 @@ lemma map_comp [DecidableEq S] [DecidableEq T] (f : S →+* T) (g : R →+* S)
     (s : ConstructibleSetData R) : s.map (f.comp g) = (s.map g).map f := by
   unfold map Sigma.map; simp [image_image, Function.comp_def]
 
-/-! ### Rings -/
-
-open scoped Classical in
-/-- Remove the zero polynomials from the data of a constructible set. -/
-noncomputable def reduce (S : ConstructibleSetData R) : ConstructibleSetData R :=
-  S.image fun ⟨_, r, f⟩ ↦ ⟨#{x | f x ≠ 0}, r, f ∘ Subtype.val ∘ (Finset.equivFin _).symm⟩
-
+/-- Given the data of a constructible set `s`, namely finitely many tuples `(f, g₁, ..., gₙ)` such
+that `s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`, return `s`. -/
 def toSet (S : ConstructibleSetData R) : Set (PrimeSpectrum R) :=
   ⋃ x ∈ S, zeroLocus (Set.range x.2.2) \ zeroLocus {x.2.1}
 
-@[simp]
-lemma toSet_reduce (S : ConstructibleSetData R) : S.reduce.toSet = S.toSet := by
-  classical
-  unfold toSet reduce
-  rw [Finset.set_biUnion_finset_image]
-  congr! 4 with y hy
-  simp only [Set.range_comp, ne_eq, Equiv.range_eq_univ, Set.image_univ,
-    Subtype.range_coe_subtype, mem_filter, mem_univ, true_and]
-  show zeroLocus (y.2.2 '' (y.2.2 ⁻¹' {0}ᶜ)) = _
-  rw [Set.image_preimage_eq_inter_range, ← Set.diff_eq_compl_inter,
-    zeroLocus_diff_singleton_zero]
-
 @[simp]
 lemma toSet_map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) :
     (s.map f).toSet = comap f ⁻¹' s.toSet := by
@@ -54,6 +57,7 @@ lemma toSet_map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) :
     Set.image_singleton, ← Set.range_comp]
   rfl
 
+/-- The degree bound on a constructible set for Chevalley's theorem for the inclusion `R ↪ R[X]`. -/
 def degBound (S : ConstructibleSetData R[X]) : ℕ := S.sup fun e ↦ ∑ i, (e.2.2 i).degree.succ
 
-end ConstructibleSetData
+end PrimeSpectrum.ConstructibleSetData

LeanCamCombi/Mathlib/Algebra/Algebra/Operations.lean

@@ -10,14 +10,10 @@ lemma one_le_iff {R S} [CommSemiring R] [Semiring S] [Module R S] {M : Submodule
 lemma restrictScalars_pow {A B C : Type*} [Semiring A] [Semiring B]
     [Semiring C] [SMul A B] [Module A C] [Module B C]
     [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C]
-    {I : Submodule B C} {n : ℕ} (hn : n ≠ 0) :
-    (I ^ n).restrictScalars A = I.restrictScalars A ^ n := by
-  cases' n with n
-  · contradiction
-  induction n with
-  | zero =>
-    simp [Submodule.pow_one]
-  | succ n IH =>
-    simp only [Submodule.pow_succ (n := n + 1), Submodule.restrictScalars_mul, IH (by simp)]
+    {I : Submodule B C} :
+    ∀ {n : ℕ}, (hn : n ≠ 0) → (I ^ n).restrictScalars A = I.restrictScalars A ^ n
+  | 1, _ => by simp [Submodule.pow_one]
+  | n + 2, _ => by
+    simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]
 
 end Submodule

LeanCamCombi/GrowthInGroups/SpanRangeUpdate.lean → LeanCamCombi/Mathlib/Algebra/Polynomial/CoeffMem.lean

@@ -1,19 +1,19 @@
-import Mathlib.Algebra.Polynomial.Div
+import Mathlib.Algebra.Polynomial.CoeffMem
 import Mathlib.RingTheory.Ideal.Span
 
-open Polynomial
-
+namespace Polynomial
 variable {R ι : Type*} [CommRing R] [DecidableEq ι]
 
-lemma Ideal.span_range_update_divByMonic (v : ι → R[X]) {i j : ι} (hij : i ≠ j) (H : (v i).Monic) :
+open Ideal in
+lemma idealSpan_range_update_divByMonic {v : ι → R[X]} {i j : ι} (hij : i ≠ j) (H : (v i).Monic) :
     span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v) := by
   refine le_antisymm ?_ ?_ <;> simp only [span_le, Set.range_subset_iff, SetLike.mem_coe] <;>
     intro k <;> obtain rfl | hjk := eq_or_ne j k
-  · rw [Function.update_same, modByMonic_eq_sub_mul_div (v j) H]
+  · rw [Function.update_self, modByMonic_eq_sub_mul_div (v j) H]
     exact sub_mem (subset_span ⟨j, rfl⟩) <| mul_mem_right _ _ <| subset_span ⟨i, rfl⟩
-  · exact subset_span ⟨k, (Function.update_noteq (.symm hjk) _ _).symm⟩
+  · exact subset_span ⟨k, (Function.update_of_ne (.symm hjk) _ _).symm⟩
   · nth_rw 2 [← modByMonic_add_div (v j) H]
     apply add_mem (subset_span ?_) (mul_mem_right _ _ (subset_span ?_))
-    · exact ⟨j, Function.update_same _ _ _⟩
-    · exact ⟨i, Function.update_noteq hij _ _⟩
-  · exact subset_span ⟨k, Function.update_noteq (.symm hjk) _ _⟩
+    · exact ⟨j, Function.update_self _ _ _⟩
+    · exact ⟨i, Function.update_of_ne hij _ _⟩
+  · exact subset_span ⟨k, Function.update_of_ne (.symm hjk) _ _⟩

LeanCamCombi/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -3,19 +3,18 @@ import LeanCamCombi.Mathlib.RingTheory.Localization.Integral
 
 variable {R S : Type*} [CommSemiring R] [CommSemiring S]
 
-lemma PrimeSpectrum.comap_eq_specComap (f : R →+* S) :
-  comap f = f.specComap := rfl
+namespace PrimeSpectrum
 
-lemma PrimeSpectrum.comap_eq_specComap' (f : R →+* S) (x) :
-  comap f x = f.specComap x := rfl
-open Polynomial
+lemma coe_comap (f : R →+* S) : comap f = f.specComap := rfl
 
-namespace PrimeSpectrum
+lemma comap_apply (f : R →+* S) (x) : comap f x = f.specComap x := rfl
+
+open Polynomial
 
 open Localization in
 lemma comap_C_eq_comap_localization_union_comap_quotient
     {R : Type*} [CommRing R] (s : Set (PrimeSpectrum R[X])) (c : R) :
-    .comap C '' s =
+    comap C '' s =
       comap (algebraMap R (Away c)) '' (comap C ''
         (comap (mapRingHom (algebraMap R (Away c))) ⁻¹' s)) ∪
       comap (Ideal.Quotient.mk (.span {c})) '' (comap C ''

LeanCamCombi/Mathlib/Data/Set/Basic.lean

@@ -3,7 +3,7 @@ import Mathlib.Data.Set.Basic
 namespace Set
 variable {α : Type*} {s : Set α} {a : α}
 
-lemma diff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t := by
+lemma sdiff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t := by
   ext; simp [and_right_comm]
 
 end Set

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fd52917a1ac853bcb73cd089ce43e6a4257c98e0",
+   "rev": "43d30441447b3b8da2ae24e2091751feb743640c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6fc4dca48a248328f93644edbbcef2a461dbbec7",
+   "rev": "68fbd252aa5d0168c5f582c0f66b3005dba683e1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",