meeting changes and mwe

DividedPowers/DPAlgebra/Dpow.lean

@@ -444,8 +444,9 @@ lemma Subalgebra_tensorProduct_top_bot [Algebra A R]
     induction x using TensorProduct.induction_on with
     | zero =>
         use 0
-        --simp only [TensorProduct.zero_tmul, map_zero]
-        sorry
+        simp only [TensorProduct.zero_tmul]
+        exact (map_zero (Algebra.TensorProduct.map T₀.val S₀.val)).symm
+        -- `rw [map_zero]` used to work, and it was much faster.
     | tmul a b =>
       rcases a with ⟨a, ha⟩
       rcases b with ⟨b, hb⟩
@@ -455,10 +456,14 @@ lemma Subalgebra_tensorProduct_top_bot [Algebra A R]
       simp only [TensorProduct.smul_tmul, Algebra.TensorProduct.map_tmul, Subalgebra.coe_val,
         Algebra.algebraMap_eq_smul_one]
     | add x y hx hy =>
-      obtain ⟨x, hx⟩ := hx
-      obtain ⟨y, hy⟩ := hy
-      use x + y
-      rw [TensorProduct.add_tmul, hx, hy, AlgHom.map_add] -- TODO: find out how to fix this.
+      obtain ⟨rx, hx⟩ := hx
+      obtain ⟨ry, hy⟩ := hy
+      use rx + ry
+      rw [TensorProduct.add_tmul, hx, hy]
+      -- NOTE: The following `rw` times out. `rw [AlgHom.map_add]` used to work, but
+      -- it is now deprecated.
+      --rw [map_add (Algebra.TensorProduct.map T₀.val S₀.val) x y]
+      exact Eq.symm (map_add (Algebra.TensorProduct.map T₀.val S₀.val) x y)
   · rintro ⟨r, rfl⟩
     exact ⟨⟨r, by rw [hT₀]; exact Algebra.mem_top⟩ ⊗ₜ[A] 1, rfl⟩
 

DividedPowers/DPAlgebra/mwe.lean

@@ -0,0 +1,30 @@
+import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.TensorProduct.Basic
+
+open scoped 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]
+
+/-
+  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.
+
+  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

DividedPowers/ForMathlib/MvPowerSeries/Substitution.lean

@@ -301,19 +301,15 @@ noncomputable def substAlgHom (ha : SubstDomain a) :
   classical
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   exact MvPowerSeries.aeval ha.evalDomain
 
 @[simp]
 theorem coe_substAlgHom (ha : SubstDomain a) :
     ⇑(substAlgHom ha) = subst (R := R) a :=
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   coe_aeval (SubstDomain.evalDomain ha)
 
 theorem subst_add (ha : SubstDomain a) (f g : MvPowerSeries σ R) :
@@ -336,9 +332,7 @@ theorem substAlgHom_coe (ha : SubstDomain a) (p : MvPolynomial σ R) :
     substAlgHom (R := R) ha p = MvPolynomial.aeval a p :=
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   aeval_coe ha.evalDomain p
 
 theorem substAlgHom_X (ha : SubstDomain a) (s : σ) :
@@ -369,20 +363,14 @@ theorem continuous_subst (ha : SubstDomain a) :
     Continuous (subst a : MvPowerSeries σ R → MvPowerSeries τ S) :=
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
-  -- Q : is it better to use the following instance to replace the 3 previous ones?
-  --haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   continuous_eval₂ (continuous_algebraMap _ _) ha.evalDomain
 
 theorem coeff_subst_finite (ha : SubstDomain a) (f : MvPowerSeries σ R) (e : τ →₀ ℕ) :
     Set.Finite (fun d ↦ (coeff R d f) • (coeff S e (d.prod fun s e => (a s) ^ e))).support :=
   letI : UniformSpace S := ⊥
   letI : UniformSpace R := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   Set.Finite.support_of_summable _
     ((hasSum_aeval ha.evalDomain f).map (coeff S e) (continuous_coeff S e)).summable
 
@@ -391,9 +379,7 @@ theorem coeff_subst (ha : SubstDomain a) (f : MvPowerSeries σ R) (e : τ →₀
       finsum (fun d ↦ (coeff R d f) • (coeff S e (d.prod fun s e => (a s) ^ e))) := by
   letI : UniformSpace S := ⊥
   letI : UniformSpace R := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   have := ((hasSum_aeval ha.evalDomain f).map (coeff S e) (continuous_coeff S e))
   erw [← coe_substAlgHom ha, ← this.tsum_eq, tsum_def]
   erw [dif_pos this.summable, if_pos (coeff_subst_finite ha f e)]
@@ -428,10 +414,8 @@ theorem comp_substAlgHom (ha : SubstDomain a) :
       ε.comp (substAlgHom ha) = aeval (EvalDomain.map hε ha.evalDomain) :=
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
   haveI : ContinuousSMul R T := DiscreteTopology.instContinuousSMul R T
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
   fun hε ↦ comp_aeval ha.evalDomain hε
 
 theorem comp_subst (ha : SubstDomain a) :
@@ -520,12 +504,8 @@ theorem substAlgHom_comp_substAlgHom (ha : SubstDomain a) (hb : SubstDomain b) :
   letI : UniformSpace R := ⊥
   letI : UniformSpace S := ⊥
   letI : UniformSpace T := ⊥
-  haveI : ContinuousSMul R S := DiscreteTopology.instContinuousSMul R S
-  haveI : ContinuousSMul S (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries τ S) := IsScalarTower.continuousSMul S
-  haveI : ContinuousSMul R T := DiscreteTopology.instContinuousSMul R T
-  haveI : ContinuousSMul T (MvPowerSeries υ T) := DiscreteTopology.instContinuousSMul _ _
-  haveI : ContinuousSMul R (MvPowerSeries υ T) := IsScalarTower.continuousSMul T
+  haveI : ContinuousSMul R (MvPowerSeries τ S) := DiscreteTopology.instContinuousSMul _ _
+  haveI : ContinuousSMul R (MvPowerSeries υ T) := DiscreteTopology.instContinuousSMul _ _
   apply comp_aeval (R := R) (ε := (substAlgHom hb).restrictScalars R)
     ha.evalDomain
   simp only [AlgHom.coe_restrictScalars', coe_substAlgHom]