more changes from meeting

DividedPowers/DPAlgebra/Dpow.lean

@@ -431,6 +431,7 @@ def _root_.MvPolynomial.CAlgHom {R : Type*} [CommRing R] {A : Type*} [CommRing A
 -- NOTE: we are having the same issues with `map_zero` and `map_add` that we did with `map_smul`
 -- (previously `AlgHom.map_smul`) in RobyLemma9.
 
+
 lemma Subalgebra_tensorProduct_top_bot [Algebra A R]
     (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S} (hS₀ : S₀ = ⊥)
     {T₀ : Subalgebra A R} (hT₀ : T₀ = ⊤) :

DividedPowers/DPAlgebra/RobyLemma9.lean

@@ -8,7 +8,7 @@ open scoped TensorProduct
 -- The goal is to prove lemma 9 in Roby (1965)
 section RingHom
 
-theorem RingHom.ker_eq_ideal_iff {A B : Type _} [CommRing A] [CommRing B] (f : A →+* B)
+theorem RingHom.ker_eq_ideal_iff {A B : Type*} [CommRing A] [CommRing B] (f : A →+* B)
     (I : Ideal A) :
     RingHom.ker f = I ↔
       ∃ h : I ≤ RingHom.ker f, Function.Injective (Ideal.Quotient.lift I f h) := by
@@ -25,7 +25,7 @@ end RingHom
 
 section AlgHom
 
-theorem AlgHom.ker_eq_ideal_iff {R A B : Type _} [CommRing R] [CommRing A] [Algebra R A]
+theorem AlgHom.ker_eq_ideal_iff {R A B : Type*} [CommRing R] [CommRing A] [Algebra R A]
     [CommRing B] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal A) :
     RingHom.ker f = I ↔
       ∃ h : I ≤ RingHom.ker f, Function.Injective (Ideal.Quotient.liftₐ I f h) := by
@@ -46,10 +46,10 @@ theorem AlgHom.ker_eq_ideal_iff {R A B : Type _} [CommRing R] [CommRing A] [Alge
 
 end AlgHom
 
-variable (R : Type _) [CommRing R] (S : Type _) [CommRing S]
+variable (R : Type*) [CommRing R] (S : Type*) [CommRing S]
 
-variable (M : Type _) [CommRing M] [Algebra R M] [Algebra S M]
-  (N : Type _) [CommRing N] [Algebra R N] [Algebra S N]
+variable (M : Type*) [CommRing M] [Algebra R M] [Algebra S M]
+  (N : Type*) [CommRing N] [Algebra R N] [Algebra S N]
 
 variable [Algebra R S] [IsScalarTower R S M]
 
@@ -99,6 +99,7 @@ lemma mkₐ_one_tmul_smul_one (s : S) :
   rw [Ideal.Quotient.eq]
   exact Ideal.subset_span ⟨s, Set.mem_univ s, rfl⟩
 
+
 variable [IsScalarTower R S N]
 
 -- [tensor_product.compatible_smul R S M N]
@@ -131,7 +132,8 @@ noncomputable def ψLeft : M →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N := {
   commutes' := fun s => by
     simp only [AlgHom.toFun_eq_coe, AlgHom.coe_comp, AlgHom.coe_restrictScalars',
       Function.comp_apply, includeLeft_apply, Algebra.algebraMap_eq_smul_one]
-    apply mkₐ_smul_one_tmul_one }
+    rfl
+    /- apply mkₐ_smul_one_tmul_one -/ }
 
 -- why is it noncomputable
 noncomputable def ψRight : N →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N := {
@@ -140,7 +142,12 @@ noncomputable def ψRight : N →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N := {
     simp only [AlgHom.toFun_eq_coe, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk,
       Function.comp_apply, includeRight_apply]
     simp only [Algebra.algebraMap_eq_smul_one]
-    apply mkₐ_one_tmul_smul_one }
+    rw [← (Ideal.Quotient.mk (kerφ R S M N)).map_one, ← Ideal.Quotient.mkₐ_eq_mk S, ← map_smul]
+    simp only [Ideal.Quotient.mkₐ_eq_mk]
+    apply symm
+    rw [Ideal.Quotient.eq]
+    exact Ideal.subset_span ⟨s, Set.mem_univ s, rfl⟩
+    /- apply mkₐ_one_tmul_smul_one -/ }
 
 noncomputable def ψ : M ⊗[S] N →ₐ[S] M ⊗[R] N ⧸ kerφ R S M N :=
   productMap (ψLeft R S M N) (ψRight R S M N)

DividedPowers/DPAlgebra/mwe.lean

@@ -1,30 +1,13 @@
-import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.TensorProduct.Basic
 
-open scoped TensorProduct
+open TensorProduct
 
-variable (R S M N : Type*) [CommRing R] [CommRing S]
-variable [CommRing M] [Algebra R M] [Algebra S M] [CommRing N] [Algebra R N]
-variable [Algebra R S] [IsScalarTower R S M]
+variable {R A : Type*} [CommRing R] [CommRing A]
 
-/-
-  The most general version `mkₐ_smul_one_tmul_one'` is the "correct" one, but it is the
-  slowest one inside the proof where we apply it.
+set_option profiler true
 
-  Main point: `AlgHom.map_smul` (which we were using before) is deprecated, and `map_smul` is
-  much slower.
-  -/
-
-lemma mkₐ_smul_one_tmul_one' (s : S) {B : Type*} [CommRing B] [Algebra R B]
-  [Algebra S B] [IsScalarTower R S B] (f : M ⊗[R] N →ₐ[S] B)  :
-    f ((s • (1 : M)) ⊗ₜ[R] (1 : N)) = s • (1 : B ) := by
-  suffices (s • (1 : M)) ⊗ₜ[R] (1 : N) = s • (1 : M ⊗[R] N) by
-    rw [this, map_smul, map_one]
-  rfl
-
-lemma mkₐ_smul_one_tmul_one (s : S) (I : Ideal (M ⊗[R] N)) :
-    (Ideal.Quotient.mkₐ S I) ((s • (1 : M)) ⊗ₜ[R] (1 : N)) =
-      s • (1 : M ⊗[R] N ⧸ I) := by
-  suffices (s • (1 : M)) ⊗ₜ[R] (1 : N) = s • (1 : M ⊗[R] N) by
-    rw [this, map_smul, map_one]
-  rfl
+lemma foo [Algebra A R] (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S}
+    {T₀ : Subalgebra A R} (x y : ↥T₀ ⊗[A] ↥S₀) :
+    (Algebra.TensorProduct.map T₀.val S₀.val) x + (Algebra.TensorProduct.map T₀.val S₀.val) y =
+    (Algebra.TensorProduct.map T₀.val S₀.val) (x + y) := by
+  exact Eq.symm (map_add (Algebra.TensorProduct.map T₀.val S₀.val) x y)