Merge branch 'main' of https://github.com/AntoineChambert-Loir/Divide…

…dPowers4 into main

DividedPowers/BasicLemmas.lean

@@ -77,7 +77,7 @@ theorem rewriting_4_fold_sums {α : Type _} [CommSemiring α] {m n u v : ℕ}
         if_true]
       · rintro ⟨⟨x, y⟩, ⟨z, t⟩⟩ hb hb'; rw [if_neg]; intro hb''
         simp only [Finset.mem_product, Finset.mem_antidiagonal] at hb
-        simp only [Ne.def, Prod.mk.inj_iff, not_and, and_imp] at hb'
+        simp only [ne_eq, Prod.mk.injEq, not_and, and_imp] at hb'
         simp only [Prod.mk.inj_iff] at hb''
         specialize hb' hb''.2.1 hb''.2.2
         rw [hb''.2.1, hb''.2.2] at hb

DividedPowers/DPAlgebra/PolynomialMap.lean

@@ -1,6 +1,7 @@
 import DividedPowers.PolynomialMap.Homogeneous
 import DividedPowers.DPAlgebra.Graded.Basic
 import DividedPowers.DPAlgebra.BaseChange
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-
 
@@ -82,8 +83,28 @@ theorem gamma_mem_grade (n : ℕ) (S : Type*) [CommRing S] [Algebra R S] (m : S
     obtain ⟨y', hy'⟩ := hy
     simp only [LinearMap.mem_range]
     -- we need the graded structure on the base change of a graded algebra
+    rw [← hx', ← hy']
+    /- more precisely, we have multiplication
+      grade R M k × grade R M l → grade R M (k + l)
+      induced by multiplication of DividedPowerAlgebra R M
+      thanks to `SetLike.GradedMul.mul_mem`
+      and we want to base change this bilinear map to
+      S ⊗[R] grade R M k × S ⊗[R] grade R M l → S⊗[R] grade R M (k + l)
+    -/
     sorry
 
+#check LinearMap.tensorProduct
+
+example (A : Type*) [CommRing A] (M N P : Type*) [AddCommGroup M] [Module A M]
+  [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P]
+  (Φ : M →ₗ[A] N →ₗ[A] P)
+  (R : Type*) [CommRing R] [Algebra A R] :
+  R ⊗[A] M →ₗ[R] R ⊗[A] N →ₗ[R] R ⊗[A] P := by
+  have := LinearMap.baseChange R Φ
+  apply LinearMap.comp ?_ this
+  have := LinearMap.tensorProduct A R N P
+  exact this
+
 /- to do this, it seems that we have to understand polynomial maps
 valued into a submodule (in this case, it is a direct factor,
 so it will exactly correspond to polynomial maps all of which evaluations