perf(linear_algebra): speed up graded_algebra instances (#14967)

alreadydone · alreadydone · commit 2a7ceb0e411e · 2022-07-08T02:55:28.000Z
Reduce `elaboration of graded_algebra` in: + `exterior_algebra.graded_algebra` from ~20s to 3s- + `tensor_algebra.graded_algebra` from 7s+ to 2s- + `clifford_algebra.graded_algebra` from 14s+ to 4s- (These numbers were before `lift_ι` and `lift_ι_eq` were extracted from `exterior_algebra.graded_algebra` and `lift_ι_eq` was extracted from `clifford_algebra.graded_algebra` in #12182.) Fix [timeout reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout/near/286996731) Also shorten the statements of the first two without reducing clarity (I think).
diff --git a/src/linear_algebra/clifford_algebra/grading.lean b/src/linear_algebra/clifford_algebra/grading.lean
@@ -78,12 +78,12 @@ rfl
 lemma graded_algebra.ι_sq_scalar (m : M) :
   graded_algebra.ι Q m * graded_algebra.ι Q m = algebra_map R _ (Q m) :=
 begin
-  rw [graded_algebra.ι_apply, direct_sum.of_mul_of, direct_sum.algebra_map_apply],
+  rw [graded_algebra.ι_apply Q, direct_sum.of_mul_of, direct_sum.algebra_map_apply],
   refine direct_sum.of_eq_of_graded_monoid_eq (sigma.subtype_ext rfl $ ι_sq_scalar _ _),
 end
 
 lemma graded_algebra.lift_ι_eq (i' : zmod 2) (x' : even_odd Q i') :
-  lift Q ⟨graded_algebra.ι Q, graded_algebra.ι_sq_scalar Q⟩ x' =
+  lift Q ⟨by apply graded_algebra.ι Q, graded_algebra.ι_sq_scalar Q⟩ x' =
     direct_sum.of (λ i, even_odd Q i) i' x' :=
 begin
   cases x' with x' hx',
@@ -96,7 +96,7 @@ begin
     { rw [alg_hom.commutes, direct_sum.algebra_map_apply], refl },
     { rw [alg_hom.map_add, ihx, ihy, ←map_add], refl },
     { obtain ⟨_, rfl⟩ := hm,
-      rw [alg_hom.map_mul, ih, lift_ι_apply, graded_algebra.ι_apply, direct_sum.of_mul_of],
+      rw [alg_hom.map_mul, ih, lift_ι_apply, graded_algebra.ι_apply Q, direct_sum.of_mul_of],
       refine direct_sum.of_eq_of_graded_monoid_eq (sigma.subtype_ext _ _);
         dsimp only [graded_monoid.mk, subtype.coe_mk],
       { rw [nat.succ_eq_add_one, add_comm, nat.cast_add, nat.cast_one] },
@@ -110,16 +110,17 @@ end
 /-- The clifford algebra is graded by the even and odd parts. -/
 instance graded_algebra : graded_algebra (even_odd Q) :=
 graded_algebra.of_alg_hom (even_odd Q)
-  (lift _ ⟨graded_algebra.ι Q, graded_algebra.ι_sq_scalar Q⟩)
+  -- while not necessary, the `by apply` makes this elaborate faster
+  (lift Q ⟨by apply graded_algebra.ι Q, graded_algebra.ι_sq_scalar Q⟩)
   -- the proof from here onward is mostly similar to the `tensor_algebra` case, with some extra
   -- handling for the `supr` in `even_odd`.
   (begin
     ext m,
     dsimp only [linear_map.comp_apply, alg_hom.to_linear_map_apply, alg_hom.comp_apply,
       alg_hom.id_apply],
-    rw [lift_ι_apply, graded_algebra.ι_apply, direct_sum.coe_alg_hom_of, subtype.coe_mk],
+    rw [lift_ι_apply, graded_algebra.ι_apply Q, direct_sum.coe_alg_hom_of, subtype.coe_mk],
   end)
-  (by exact graded_algebra.lift_ι_eq Q)
+  (by apply graded_algebra.lift_ι_eq Q)
 
 lemma supr_ι_range_eq_top : (⨆ i : ℕ, (ι Q).range ^ i) = ⊤ :=
 begin
diff --git a/src/linear_algebra/exterior_algebra/grading.lean b/src/linear_algebra/exterior_algebra/grading.lean
@@ -42,14 +42,14 @@ end
 primarily an auxiliary construction used to provide `exterior_algebra.graded_algebra`. -/
 def graded_algebra.lift_ι : exterior_algebra R M →ₐ[R]
   ⨁ (i : ℕ), ↥((ι R).range ^ i : submodule R (exterior_algebra R M)) :=
-lift R ⟨graded_algebra.ι R M, graded_algebra.ι_sq_zero R M⟩
+lift R ⟨by apply graded_algebra.ι R M, graded_algebra.ι_sq_zero R M⟩
 
-variables {R M}
+variables (R M)
 
 lemma graded_algebra.lift_ι_eq (i : ℕ)
   (x : ((ι R).range ^ i : submodule R (exterior_algebra R M))) :
   graded_algebra.lift_ι R M x =
-    direct_sum.of (λ i, (((ι R).range ^ i : submodule R (exterior_algebra R M)) : Type*)) i x :=
+    direct_sum.of (λ i, ↥((ι R).range ^ i : submodule R (exterior_algebra R M))) i x :=
 begin
   cases x with x hx,
   dsimp only [subtype.coe_mk, direct_sum.lof_eq_of],
@@ -58,23 +58,24 @@ begin
   { rw [alg_hom.commutes, direct_sum.algebra_map_apply], refl },
   { rw [alg_hom.map_add, ihx, ihy, ←map_add], refl },
   { obtain ⟨_, rfl⟩ := hm,
-    rw [alg_hom.map_mul, ih, graded_algebra.lift_ι, lift_ι_apply, graded_algebra.ι_apply,
-      direct_sum.of_mul_of],
-    exact direct_sum.of_eq_of_graded_monoid_eq (sigma.subtype_ext (add_comm _ _) rfl) }
+    rw [alg_hom.map_mul, ih, graded_algebra.lift_ι, lift_ι_apply,
+      graded_algebra.ι_apply R M, direct_sum.of_mul_of],
+    exact direct_sum.of_eq_of_graded_monoid_eq (sigma.subtype_ext (add_comm _ _) rfl) },
 end
 
 /-- The exterior algebra is graded by the powers of the submodule `(exterior_algebra.ι R).range`. -/
 instance graded_algebra :
-  graded_algebra
-    ((^) (ι R : M →ₗ[R] exterior_algebra R M).range : ℕ → submodule R (exterior_algebra R M)) :=
-graded_algebra.of_alg_hom _ (graded_algebra.lift_ι R M)
+  graded_algebra ((^) (ι R : M →ₗ[R] exterior_algebra R M).range : ℕ → submodule R _) :=
+graded_algebra.of_alg_hom _
+  -- while not necessary, the `by apply` makes this elaborate faster
+  (by apply graded_algebra.lift_ι R M)
   -- the proof from here onward is identical to the `tensor_algebra` case
   (begin
     ext m,
     dsimp only [linear_map.comp_apply, alg_hom.to_linear_map_apply, alg_hom.comp_apply,
       alg_hom.id_apply, graded_algebra.lift_ι],
-    rw [lift_ι_apply, graded_algebra.ι_apply, direct_sum.coe_alg_hom_of, subtype.coe_mk],
+    rw [lift_ι_apply, graded_algebra.ι_apply R M, direct_sum.coe_alg_hom_of, subtype.coe_mk],
   end)
-  (by exact graded_algebra.lift_ι_eq)
+  (by apply graded_algebra.lift_ι_eq R M)
 
 end exterior_algebra
diff --git a/src/linear_algebra/tensor_algebra/grading.lean b/src/linear_algebra/tensor_algebra/grading.lean
@@ -37,12 +37,12 @@ variables {R M}
 instance graded_algebra :
   graded_algebra ((^) (ι R : M →ₗ[R] tensor_algebra R M).range : ℕ → submodule R _) :=
 graded_algebra.of_alg_hom _
-  (lift _ $ graded_algebra.ι R M)
+  (lift R $ graded_algebra.ι R M)
   (begin
     ext m,
     dsimp only [linear_map.comp_apply, alg_hom.to_linear_map_apply, alg_hom.comp_apply,
       alg_hom.id_apply],
-    rw [lift_ι_apply, graded_algebra.ι_apply, direct_sum.coe_alg_hom_of, subtype.coe_mk],
+    rw [lift_ι_apply, graded_algebra.ι_apply R M, direct_sum.coe_alg_hom_of, subtype.coe_mk],
   end)
   (λ i x, begin
     cases x with x hx,
@@ -52,7 +52,7 @@ graded_algebra.of_alg_hom _
     { rw [alg_hom.commutes, direct_sum.algebra_map_apply], refl },
     { rw [alg_hom.map_add, ihx, ihy, ←map_add], refl },
     { obtain ⟨_, rfl⟩ := hm,
-      rw [alg_hom.map_mul, ih, lift_ι_apply, graded_algebra.ι_apply, direct_sum.of_mul_of],
+      rw [alg_hom.map_mul, ih, lift_ι_apply, graded_algebra.ι_apply R M, direct_sum.of_mul_of],
       exact direct_sum.of_eq_of_graded_monoid_eq (sigma.subtype_ext (add_comm _ _) rfl) }
   end)
 
