Bump mathlib

LeanCamCombi.lean

@@ -37,6 +37,7 @@ import LeanCamCombi.Mathlib.Algebra.Algebra.Operations
 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
@@ -57,16 +58,13 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Finset.Basic
-import LeanCamCombi.Mathlib.Data.Finset.Image
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.Finset.Powerset
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Defs
-import LeanCamCombi.Mathlib.Data.Nat.GCD.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
-import LeanCamCombi.Mathlib.Data.Set.Function
 import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement

LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean

@@ -5,9 +5,9 @@ import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import LeanCamCombi.Mathlib.Data.Finset.Image
 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.CoeffMem
 import LeanCamCombi.GrowthInGroups.ConstructibleSetData
@@ -685,43 +685,6 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet'
       ((δ_casesOn_succ k _ _ _).symm.trans_le (δ_le_δ le_rfl _ this))
     simp+contextual [mul_add, Nat.one_le_iff_ne_zero]
 
-theorem MvPolynomial.degrees_map_le {σ S} [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) :
-    (MvPolynomial.map f p).degrees ≤ p.degrees := by
-  classical
-  dsimp only [MvPolynomial.degrees]
-  apply Finset.sup_mono
-  apply MvPolynomial.support_map_subset
-
-theorem MvPolynomial.degrees_sub {σ R} [CommRing R] [DecidableEq σ] (p q : MvPolynomial σ R) :
-    (p - q).degrees ≤ p.degrees ⊔ q.degrees := by
-  simp_rw [MvPolynomial.degrees_def]; exact AddMonoidAlgebra.supDegree_sub_le
-
-lemma Set.diff_inter_right_comm {α} {s t u : Set α} : s \ t ∩ u = (s ∩ u) \ t := by
-  ext; simp [and_right_comm]
-
-noncomputable
-def MvPolynomial.commAlgEquiv (R S₁ S₂ : Type*) [CommSemiring R] :
-    MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R) :=
-  (MvPolynomial.sumAlgEquiv R S₁ S₂).symm.trans
-    ((MvPolynomial.renameEquiv _ (Equiv.sumComm S₁ S₂)).trans (MvPolynomial.sumAlgEquiv R S₂ S₁))
-
-lemma MvPolynomial.commAlgEquiv_C {R S₁ S₂ : Type*} [CommSemiring R] (p) :
-    MvPolynomial.commAlgEquiv R S₁ S₂ (.C p) = .map MvPolynomial.C p := by
-  suffices (MvPolynomial.commAlgEquiv R S₁ S₂).toAlgHom.comp
-      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) =
-        MvPolynomial.mapAlgHom (Algebra.ofId _ _) by
-    exact DFunLike.congr_fun this p
-  ext x : 1
-  simp [commAlgEquiv]
-
-lemma MvPolynomial.commAlgEquiv_C_X {R S₁ S₂ : Type*} [CommSemiring R] (i) :
-    MvPolynomial.commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i := by
-  simp [commAlgEquiv_C]
-
-lemma MvPolynomial.commAlgEquiv_X {R S₁ S₂ : Type*} [CommSemiring R] (i) :
-    MvPolynomial.commAlgEquiv R S₁ S₂ (.X i) = .C (.X i) := by
-  simp [commAlgEquiv]
-
 lemma chevalley_mvPolynomial_mvPolynomial
     {n m : ℕ} (f : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin n) R)
     (k : ℕ) (d : Multiset (Fin n))

LeanCamCombi/Mathlib/Algebra/MvPolynomial/CommRing.lean

@@ -0,0 +1,7 @@
+import Mathlib.Algebra.MvPolynomial.CommRing
+
+namespace MvPolynomial
+
+lemma degrees_sub_le {σ R} [CommRing R] [DecidableEq σ] (p q : MvPolynomial σ R) :
+    (p - q).degrees ≤ p.degrees ∪ q.degrees := by
+  simp_rw [degrees_def]; exact AddMonoidAlgebra.supDegree_sub_le

LeanCamCombi/Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -4,6 +4,13 @@ import LeanCamCombi.Mathlib.Algebra.Algebra.Operations
 namespace MvPolynomial
 variable {R σ : Type*} [CommSemiring R] {m n : Multiset σ} {p : MvPolynomial σ R}
 
+lemma degrees_map_le {σ S} [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) :
+    (MvPolynomial.map f p).degrees ≤ p.degrees := by
+  classical
+  dsimp only [MvPolynomial.degrees]
+  apply Finset.sup_mono
+  apply MvPolynomial.support_map_subset
+
 variable (R σ n) in
 def degreesLE : Submodule R (MvPolynomial σ R) where
   carrier := {p | p.degrees ≤ n}

LeanCamCombi/Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -11,4 +11,23 @@ lemma isEmptyRingEquiv_eq_coeff_zero {σ R : Type*} [CommSemiring R] [IsEmpty σ
   obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x
   simp
 
+noncomputable
+def commAlgEquiv (R S₁ S₂ : Type*) [CommSemiring R] :
+    MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R) :=
+  (sumAlgEquiv R S₁ S₂).symm.trans ((renameEquiv _ (.sumComm S₁ S₂)).trans (sumAlgEquiv R S₂ S₁))
+
+lemma commAlgEquiv_C {R S₁ S₂ : Type*} [CommSemiring R] (p) :
+    commAlgEquiv R S₁ S₂ (.C p) = .map C p := by
+  suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
+      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
+    exact DFunLike.congr_fun this p
+  ext x : 1
+  simp [commAlgEquiv]
+
+lemma commAlgEquiv_C_X {R S₁ S₂ : Type*} [CommSemiring R] (i) :
+    commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i := by simp [commAlgEquiv_C]
+
+lemma commAlgEquiv_X {R S₁ S₂ : Type*} [CommSemiring R] (i) :
+    commAlgEquiv R S₁ S₂ (.X i) = .C (.X i) := by simp [commAlgEquiv]
+
 end MvPolynomial

LeanCamCombi/Mathlib/Data/Set/Basic.lean

@@ -3,6 +3,9 @@ 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
+  ext; simp [and_right_comm]
+
 lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s := by aesop
 
 lemma insert_erase_invOn :

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "70fca3cdda5c8edf6a780dcfc8d49b3d0dd1faad",
+   "rev": "9c324ade60adf9b37f4f7b49776bd2bb3a82d5e9",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "933ad5493803f4c495f252678466ede6e1e2ee79",
+   "rev": "d70be405955bb990940792e1305e77fa17b6abea",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",