Zulip Chat Archive
Stream: Is there code for X?
Topic: AlgEquiv slow synthInstance?
Edison Xie (Mar 16 2025 at 18:09):
I'm trying to define the reduced norm/charpoly and my code of formalisation of theorem 2 of this post is really slow, I'm wondering if there is a "quicker" way (as in compile time) to do this?
import Mathlib
universe u v w
open scoped TensorProduct
variable (K F E K_bar: Type u) [Field K] [Field F] [Field E] [Algebra K F]
[Algebra K E] [Field K_bar] [Algebra K K_bar] [hK_bar : IsAlgClosure K K_bar] (A : CSA K)
(n : ℕ) [NeZero n] (e : F ⊗[K] A ≃ₐ[F] Matrix (Fin n) (Fin n) F)
suppress_compilation
set_option maxSynthPendingDepth 2 in
def Algebra.TensorProduct.assoc' (R S R' A B C : Type*) [CommSemiring R] [CommSemiring S]
[CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A]
[Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C]
[IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S]
[IsScalarTower R' S A] [IsScalarTower R S A]:
(A ⊗[R'] B) ⊗[R] C ≃ₐ[S] A ⊗[R'] B ⊗[R] C :=
AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc _ _ _ _ _ _)
rfl (LinearMap.map_mul_iff _|>.2 <| by ext; simp)
@[simp]
lemma Algebra.TensorProduct.assoc'_apply (R S R' A B C : Type*) [CommSemiring R] [CommSemiring S]
[CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A]
[Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C]
[IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S]
[IsScalarTower R' S A] [IsScalarTower R S A] (a : A) (b : B) (c : C):
(Algebra.TensorProduct.assoc' R S R' A B C) ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) := rfl
-- [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M]
-- [inst_8 : Module B M] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
-- [inst_12 : AddCommMonoid P] [inst_13 : Module A P] [inst_14 : AddCommMonoid Q] [inst_15 : Module R Q]
-- [inst_16 : Module R P] [inst_17 : IsScalarTower R A P] [inst_18 : Algebra A B] [inst_19 : IsScalarTower A B M] :
-- (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] P ⊗[R] Q := sorry
instance [Algebra F E] [IsScalarTower K F E]: IsScalarTower K (Algebra.ofId F E).range E where
smul_assoc k := fun ⟨f, hf⟩ x ↦ by
change (k • f) • _ = k • f • x
exact smul_assoc _ _ _
instance [Algebra F E] : Algebra (Algebra.ofId F E).range F :=
RingHom.toAlgebra (AlgEquiv.ofInjectiveField (Algebra.ofId F E)).symm
instance [Algebra F E] [IsScalarTower K F E]: IsScalarTower K (Algebra.ofId F E).range F where
smul_assoc k := fun ⟨e, he⟩ x ↦ by
simp only [RingHom.smul_toAlgebra, RingHom.coe_coe]
change (AlgEquiv.restrictScalars K (AlgEquiv.ofInjectiveField (Algebra.ofId F E)).symm) _ * _ = _
rw [map_smul]
simp
def matrixEquivTensor'.{u_1, u_2, u_3} (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring A]
[Algebra R A] [Fintype n] [DecidableEq n] :
Matrix n n A ≃ₐ[A] A ⊗[R] Matrix n n R :=
(AlgEquiv.ofRingEquiv (f := (matrixEquivTensor n R A).symm) <| fun a ↦ by
ext i j
simp [matrixEquivTensor, Matrix.algebraMap_eq_diagonal, Matrix.diagonal_apply, Matrix.one_apply] ).symm
@[simp] lemma matrixEquivTensor'_symm_apply.{u_1, u_2, u_3} (n : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring A]
[Algebra R A] [Fintype n] [DecidableEq n] (a : A) (m : Matrix n n R):
(matrixEquivTensor' n R A).symm (a ⊗ₜ m) = a • (m.map (algebraMap R A)) := rfl
omit [NeZero n] in
set_option maxSynthPendingDepth 3 in
set_option maxHeartbeats 600000 in
set_option synthInstance.maxHeartbeats 40000 in
lemma mat_over_extension [Algebra F E] [IsScalarTower K F E] (a : A):
∃ g : E ⊗[K] A ≃ₐ[E] Matrix (Fin n) (Fin n) E, g (1 ⊗ₜ a) =
(Algebra.ofId F E).mapMatrix (e (1 ⊗ₜ a)) := by
let e1 : (Algebra.ofId F E).range ≃ₐ[F] F := (AlgEquiv.ofInjectiveField (Algebra.ofId F E)).symm
let e1' : (Algebra.ofId F E).range ≃ₐ[(Algebra.ofId F E).range] F :=
AlgEquiv.ofRingEquiv (f := e1) (fun ⟨x, hx⟩ ↦ by
simp [e1, AlgEquiv.ofInjectiveField, Algebra.algebraMap_eq_smul_one, RingHom.smul_toAlgebra]
rfl)
let e' : F ⊗[K] A ≃ₐ[(Algebra.ofId F E).range] Matrix (Fin n) (Fin n) F :=
AlgEquiv.ofRingEquiv (f := e) <| fun ⟨x, hx⟩ ↦ by
simp [Algebra.TensorProduct.one_def]
simp [Algebra.algebraMap_eq_smul_one, RingHom.smul_toAlgebra]
conv_lhs => erw [← mul_one ((AlgEquiv.ofInjectiveField (Algebra.ofId F E)).symm ⟨x, hx⟩),
← smul_eq_mul, ← TensorProduct.smul_tmul', map_smul, map_one]
rfl
let e2 : E ≃ₐ[E] E ⊗[(Algebra.ofId F E).range] (Algebra.ofId F E).range :=
Algebra.TensorProduct.rid _ _ _|>.symm
let assoc := Algebra.TensorProduct.assoc' K E (Algebra.ofId F E).range
E (Algebra.ofId F E).range A
-- haveI : Algebra (Algebra.ofId F E).range (F ⊗[F] A)
let e3 : (Algebra.ofId F E).range ⊗[K] A ≃ₐ[(Algebra.ofId F E).range]
Matrix (Fin n) (Fin n) (Algebra.ofId F E).range :=
Algebra.TensorProduct.congr e1' AlgEquiv.refl |>.trans <| e'.trans e1'.mapMatrix.symm
let g : E ⊗[K] A ≃ₐ[E] Matrix (Fin n) (Fin n) E :=
Algebra.TensorProduct.congr e2 AlgEquiv.refl |>.trans <| assoc.trans <|
Algebra.TensorProduct.congr AlgEquiv.refl e3 |>.trans <|
(matrixEquivTensor' _ _ _).symm
use g
unfold g
simp only [Algebra.range_ofId, AlgEquiv.trans_apply, Algebra.TensorProduct.congr_apply,
AlgEquiv.refl_toAlgHom, Algebra.TensorProduct.map_tmul, AlgHom.coe_coe, map_one, AlgHom.coe_id,
id_eq, AlgHom.mapMatrix_apply]
rw [Algebra.TensorProduct.one_def]
erw [Algebra.TensorProduct.assoc'_apply]
simp only [Algebra.range_ofId, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
AlgHom.coe_coe, matrixEquivTensor'_symm_apply, one_smul]
ext i j
simp only [Matrix.map_apply]
unfold e3
simp only [Algebra.range_ofId, AlgEquiv.mapMatrix_symm, AlgEquiv.trans_apply,
Algebra.TensorProduct.congr_apply, AlgEquiv.refl_toAlgHom, Algebra.TensorProduct.map_tmul,
AlgHom.coe_coe, map_one, AlgHom.coe_id, id_eq, AlgEquiv.mapMatrix_apply, Matrix.map_apply]
change algebraMap _ _ (e1.symm (e (_) i j)) = _
change algebraMap _ _ ((AlgEquiv.ofInjective _ (FaithfulSMul.algebraMap_injective F E )) (e _ i j)) = _
change algebraMap _ _ ((algebraMap F E) (e _ i j)) = _
conv_lhs => rw [← RingHom.comp_apply]
change ((RingHom.id _).comp _) _ = _
simp [Algebra.ofId]
Edison Xie (Mar 16 2025 at 18:16):
and also this piece of code contains a generalisation of current matrixEquivTensor and Algebra.TensorProduct.assoc that I'm gonna PR once I got time so if anyone could help take a look at those will be appreciated. :))
Edison Xie (Mar 16 2025 at 18:17):
cc @Kevin Buzzard @Andrew Yang @Eric Wieser
Eric Wieser (Mar 16 2025 at 18:48):
Can you extract the existential to a def?
Kevin Buzzard (Mar 16 2025 at 22:39):
Your defeq checks are exploding for some reason:
[isDefEq] [0.018331] ✅️ SMulCommClass R (A ⊗[R'] B) (A ⊗[R'] B) =?= SMulCommClass R (A ⊗[R'] B) (A ⊗[R'] B) ▼
[] [0.017978] ✅️ SMulZeroClass.toSMul =?= SMulZeroClass.toSMul ▼
[] [0.017961] ✅️ DistribSMul.toSMulZeroClass.1 =?= DistribSMul.toSMulZeroClass.1 ▼
[] [0.017890] ✅️ { smul := fun x1 x2 ↦ x1 * x2 } =?= { smul := fun x1 x2 ↦ x1 * x2 } ▼
[] [0.017861] ✅️ fun x1 x2 ↦ x1 * x2 =?= fun x1 x2 ↦ x1 * x2 ▼
[] [0.017841] ✅️ x1✝ * x2✝ =?= x1✝ * x2✝ ▼
[] [0.017819] ✅️ instHMul.1 x1✝ x2✝ =?= instHMul.1 x1✝ x2✝ ▼
[] [0.017791] ✅️ Mul.mul x1✝ x2✝ =?= Mul.mul x1✝ x2✝ ▼
[] [0.017776] ✅️ MulZeroClass.toMul.1 x1✝ x2✝ =?= MulZeroClass.toMul.1 x1✝ x2✝ ▼
[] [0.017488] ✅️ (Algebra.TensorProduct.mul x1✝) x2✝ =?= (Algebra.TensorProduct.mul x1✝) x2✝ ▼
[] [0.017466] ✅️ LinearMap.instFunLike.1 (Algebra.TensorProduct.mul x1✝)
x2✝ =?= LinearMap.instFunLike.1 (Algebra.TensorProduct.mul x1✝) x2✝ ▼
[] [0.017411] ✅️ (Algebra.TensorProduct.mul x1✝).toFun x2✝ =?= (Algebra.TensorProduct.mul x1✝).toFun x2✝ ▼
[] [0.017390] ✅️ (Algebra.TensorProduct.mul x1✝).toAddHom.1 x2✝ =?= (Algebra.TensorProduct.mul x1✝).toAddHom.1 x2✝ ▼
[] [0.015948] ✅️ (Algebra.TensorProduct.mul x1✝).toAddHom.1 =?= (Algebra.TensorProduct.mul x1✝).toAddHom.1 ▼
[] [0.015823] ✅️ (Algebra.TensorProduct.mul x1✝).toAddHom =?= (Algebra.TensorProduct.mul x1✝).toAddHom ▼
[] [0.015789] ✅️ (Algebra.TensorProduct.mul x1✝).1 =?= (Algebra.TensorProduct.mul x1✝).1 ▼
[] [0.015687] ✅️ Algebra.TensorProduct.mul x1✝ =?= Algebra.TensorProduct.mul x1✝ ▼
[] [0.015665] ✅️ LinearMap.instFunLike.1 Algebra.TensorProduct.mul
x1✝ =?= LinearMap.instFunLike.1 Algebra.TensorProduct.mul x1✝ ▼
[] [0.015633] ✅️ Algebra.TensorProduct.mul.toFun x1✝ =?= Algebra.TensorProduct.mul.toFun x1✝ ▼
[] [0.015617] ✅️ Algebra.TensorProduct.mul.toAddHom.1 x1✝ =?= Algebra.TensorProduct.mul.toAddHom.1 x1✝ ▼
[] [0.015511] ✅️ (⇑(TensorProduct.homTensorHomMap R' A B A B) ∘
⇑(TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B)))
x1✝ =?= (⇑(TensorProduct.homTensorHomMap R' A B A B) ∘
⇑(TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B)))
x1✝ ▼
[] [0.015493] ✅️ (TensorProduct.homTensorHomMap R' A B A B)
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) =?= (TensorProduct.homTensorHomMap R' A B A B)
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) ▼
[] [0.015473] ✅️ LinearMap.instFunLike.1 (TensorProduct.homTensorHomMap R' A B A B)
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) =?= LinearMap.instFunLike.1
(TensorProduct.homTensorHomMap R' A B A B)
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) ▼
[] [0.015435] ✅️ (TensorProduct.homTensorHomMap R' A B A B).toFun
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) =?= (TensorProduct.homTensorHomMap R' A B A
B).toFun
((TensorProduct.map (LinearMap.mul R' A)
(LinearMap.mul R' B))
x1✝) ▶
(etc etc)
Kevin Buzzard (Mar 16 2025 at 22:41):
There are a gazillion things all taking 0.1 seconds because they're all going crazy like that.
Edison Xie (Mar 16 2025 at 22:51):
Kevin Buzzard said:
There are a gazillion things all taking 0.1 seconds because they're all going crazy like that.
Why though :((
Edison Xie (Mar 16 2025 at 22:53):
Eric Wieser said:
Can you extract the existential to a def?
I’ll give it a try :)
Kevin Buzzard (Mar 16 2025 at 22:53):
I don't know. Here's a more minimised version:
import Mathlib
universe u v w
open scoped TensorProduct
suppress_compilation
set_option trace.profiler true
theorem Algebra.TensorProduct.extracted_1.{u_6, u_5, u_4, u_3, u_2, u_1} (R : Type u_1)
(S : Type u_2) (R' : Type u_3)
(A : Type u_4) (B : Type u_5) (C : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring S]
[inst_2 : CommSemiring R'] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Semiring C]
[inst_6 : Algebra R R']
[inst_7 : Algebra R A] [inst_8 : Algebra R' A] [inst_9 : Algebra R B] [inst_10 : Algebra R' B]
[inst_11 : Algebra R C]
[inst_12 : IsScalarTower R R' A] [inst_13 : IsScalarTower R R' B] [inst_14 : Algebra S A]
[inst_15 : Algebra R S]
[inst_16 : Algebra R' S] [inst_17 : IsScalarTower R' S A] [inst_18 : IsScalarTower R S A] :
∀ (x y : (A ⊗[R'] B) ⊗[R] C),
(TensorProduct.AlgebraTensorModule.assoc R R' S A B C) (x * y) =
(TensorProduct.AlgebraTensorModule.assoc R R' S A B C) x *
(TensorProduct.AlgebraTensorModule.assoc R R' S A B C) y := by
let foo := LinearMap.map_mul_iff
(TensorProduct.AlgebraTensorModule.assoc R R' S A B C).toLinearMap -- takes 1.5 seconds
-- rw [foo] -- fails
erw [foo] -- works
ext -- takes 1.8 seconds
simp
Kevin Buzzard (Mar 16 2025 at 22:57):
[Meta.synthInstance] [0.211839] ✅️ NonUnitalSemiring ((A ⊗[R'] B) ⊗[R] C)
[Meta.synthInstance] [0.167447] ✅️ NonUnitalSemiring (A ⊗[R'] B ⊗[R] C)
[Meta.synthInstance] [0.284945] ✅️ SMulCommClass S ((A ⊗[R'] B) ⊗[R] C) ((A ⊗[R'] B) ⊗[R] C)
[Meta.synthInstance] [0.168705] ✅️ SMulCommClass S (A ⊗[R'] B ⊗[R] C) (A ⊗[R'] B ⊗[R] C)
(all from the trace with trace.Meta.synthInstance true). These don't bode well...
Kevin Buzzard (Mar 16 2025 at 23:07):
Here's a price you're paying in every result:
def Algebra.TensorProduct.assoc' (R S R' A B C : Type*) [CommSemiring R] [CommSemiring S]
[CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A]
[Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C]
[IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S]
[IsScalarTower R' S A] [IsScalarTower R S A]:
(A ⊗[R'] B) ⊗[R] C ≃ₐ[S] A ⊗[R'] B ⊗[R] C :=
letI : NonUnitalSemiring ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.20s
letI : NonUnitalSemiring (A ⊗[R'] B ⊗[R] C) := inferInstance -- 0.18s
letI : SMulCommClass S ((A ⊗[R'] B) ⊗[R] C) ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.29s
letI : IsScalarTower S ((A ⊗[R'] B) ⊗[R] C) ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.21s
AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc _ _ _ _ _ _)
rfl ((LinearMap.map_mul_iff _|>.2 <| by ext; simp))
Edison Xie (Mar 16 2025 at 23:15):
Kevin Buzzard said:
Here's a price you're paying in every result:
def Algebra.TensorProduct.assoc' (R S R' A B C : Type*) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A] [Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C] [IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S] [IsScalarTower R' S A] [IsScalarTower R S A]: (A ⊗[R'] B) ⊗[R] C ≃ₐ[S] A ⊗[R'] B ⊗[R] C := letI : NonUnitalSemiring ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.20s letI : NonUnitalSemiring (A ⊗[R'] B ⊗[R] C) := inferInstance -- 0.18s letI : SMulCommClass S ((A ⊗[R'] B) ⊗[R] C) ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.29s letI : IsScalarTower S ((A ⊗[R'] B) ⊗[R] C) ((A ⊗[R'] B) ⊗[R] C) := inferInstance -- 0.21s AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc _ _ _ _ _ _) rfl ((LinearMap.map_mul_iff _|>.2 <| by ext; simp))
:((
Kevin Buzzard (Mar 16 2025 at 23:23):
Maybe you could make some shortcut instances? i.e. make instances like
instance (R R' A B C : Type) [CommSemiring R]
[CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A]
[Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C]
[IsScalarTower R R' A] [IsScalarTower R R' B]
[IsScalarTower R' S A] [IsScalarTower R S A] : NonUnitalSemiring ((A ⊗[R'] B) ⊗[R] C) := inferInstance
at the top of the file, so you only pay once, and then these instances will be the first to be tried during the file.
Eric Wieser (Mar 16 2025 at 23:24):
I think the instances are a pretty small fraction of the cost in assoc'? the ext seems to take half the time
Eric Wieser (Mar 16 2025 at 23:25):
Just proving that TensorProduct.AlgebraTensorModule.assoc is multiplicative in a separate lemma, before bundling it, is likely to pay off
Eric Wieser (Mar 16 2025 at 23:26):
(it will be true in more generality, too)
Kevin Buzzard (Mar 16 2025 at 23:34):
Isn't the reason that ext is so expensive because it is solving many many typeclass problems, and they just all add up? (I made everything universe-monomorphic to pick up some other speedups too in the below, and I'm using a fast machine)
[Meta.synthInstance] [0.000019] ✅️ Module S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000035] ✅️ CommSemiring R ▶
[Meta.synthInstance] [0.000015] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000024] ✅️ Algebra R S ▶
[Meta.synthInstance] [0.000452] ✅️ AddCommMonoid (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.006896] ✅️ Module R (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.004218] ✅️ Module S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.024233] ✅️ IsScalarTower R S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000016] ✅️ AddCommMonoid C ▶
[Meta.synthInstance] [0.000014] ✅️ Module R C ▶
[Meta.synthInstance] [0.006927] ✅️ AddCommMonoid ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.021671] ✅️ Module R ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.041043] ✅️ Module S ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.032118] ✅️ IsScalarTower R S ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000019] ✅️ CommSemiring R' ▶
[Meta.synthInstance] [0.000011] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000012] ✅️ Algebra R' S ▶
[Meta.synthInstance] [0.000013] ✅️ AddCommMonoid A ▶
[Meta.synthInstance] [0.000014] ✅️ Module R' A ▶
[Meta.synthInstance] [0.000011] ✅️ Module S A ▶
[Meta.synthInstance] [0.000149] ✅️ IsScalarTower R' S A ▶
[Meta.synthInstance] [0.000014] ✅️ AddCommMonoid B ▶
[Meta.synthInstance] [0.000013] ✅️ Module R' B ▶
[Meta.synthInstance] [0.009171] ✅️ AddCommMonoid (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.032858] ✅️ Module R' (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.052595] ✅️ Module S (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.052476] ✅️ IsScalarTower R' S (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000014] ✅️ CommSemiring S ▶
[Meta.synthInstance] [0.000016] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000008] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000011] ✅️ AddCommMonoid A ▶
[Meta.synthInstance] [0.014502] ✅️ AddCommMonoid (B →ₗ[R'] C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000016] ✅️ Module S A ▶
[Meta.synthInstance] [0.069304] ✅️ Module S (B →ₗ[R'] C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000014] ✅️ CommSemiring R' ▶
[Meta.synthInstance] [0.003364] ✅️ Semiring R' ▶
[Meta.synthInstance] [0.000010] ✅️ Semiring R' ▶
[Meta.synthInstance] [0.000011] ✅️ AddCommMonoid B ▶
[Meta.synthInstance] [0.000009] ✅️ AddCommMonoid (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000015] ✅️ Module R' B ▶
[Meta.synthInstance] [0.000010] ✅️ Module R' (C →ₗ[R] (A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000011] ✅️ CommSemiring R ▶
[Meta.synthInstance] [0.003320] ✅️ Semiring R ▶
[Meta.synthInstance] [0.000010] ✅️ Semiring R ▶
[Meta.synthInstance] [0.000011] ✅️ AddCommMonoid C ▶
[Meta.synthInstance] [0.000010] ✅️ AddCommMonoid ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000013] ✅️ Module R C ▶
[Meta.synthInstance] [0.000010] ✅️ Module R ((A ⊗[R'] B) ⊗[R] C →ₗ[S] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000025] ✅️ Module S (A ⊗[R'] B) ▶
[] 47 more entries... ▼
[Meta.synthInstance] [0.000014] ✅️ Module S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000020] ✅️ CommSemiring R ▶
[Meta.synthInstance] [0.000011] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000012] ✅️ Algebra R S ▶
[Meta.synthInstance] [0.000017] ✅️ AddCommMonoid (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000020] ✅️ Module R (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000020] ✅️ Module S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000185] ✅️ IsScalarTower R S (A ⊗[R'] B) ▶
[Meta.synthInstance] [0.000012] ✅️ AddCommMonoid C ▶
[Meta.synthInstance] [0.000011] ✅️ Module R C ▶
[Meta.synthInstance] [0.000818] ✅️ AddCommMonoid (A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.007979] ✅️ Module R (A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000314] ✅️ Module S (A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.018293] ✅️ IsScalarTower R S (A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000019] ✅️ CommSemiring R' ▶
[Meta.synthInstance] [0.000011] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000011] ✅️ Algebra R' S ▶
[Meta.synthInstance] [0.000012] ✅️ AddCommMonoid A ▶
[Meta.synthInstance] [0.000013] ✅️ Module R' A ▶
[Meta.synthInstance] [0.000011] ✅️ Module S A ▶
[Meta.synthInstance] [0.000155] ✅️ IsScalarTower R' S A ▶
[Meta.synthInstance] [0.000013] ✅️ AddCommMonoid B ▶
[Meta.synthInstance] [0.000014] ✅️ Module R' B ▶
[Meta.synthInstance] [0.001906] ✅️ AddCommMonoid (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.008289] ✅️ Module R' (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.011287] ✅️ Module S (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.029848] ✅️ IsScalarTower R' S (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000021] ✅️ CommSemiring S ▶
[Meta.synthInstance] [0.000019] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000008] ✅️ Semiring S ▶
[Meta.synthInstance] [0.000013] ✅️ AddCommMonoid A ▶
[Meta.synthInstance] [0.003558] ✅️ AddCommMonoid (B →ₗ[R'] C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000018] ✅️ Module S A ▶
[Meta.synthInstance] [0.020392] ✅️ Module S (B →ₗ[R'] C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000012] ✅️ CommSemiring R' ▶
[Meta.synthInstance] [0.000015] ✅️ Semiring R' ▶
[Meta.synthInstance] [0.000008] ✅️ Semiring R' ▶
[Meta.synthInstance] [0.000011] ✅️ AddCommMonoid B ▶
[Meta.synthInstance] [0.000009] ✅️ AddCommMonoid (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000014] ✅️ Module R' B ▶
[Meta.synthInstance] [0.000009] ✅️ Module R' (C →ₗ[R] A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000017] ✅️ Semiring R ▶
[Meta.synthInstance] [0.000008] ✅️ Semiring R ▶
[Meta.synthInstance] [0.000011] ✅️ AddCommMonoid C ▶
[Meta.synthInstance] [0.000008] ✅️ AddCommMonoid (A ⊗[R'] B ⊗[R] C) ▶
[Meta.synthInstance] [0.000015] ✅️ Module R C ▶
[Meta.synthInstance] [0.000315] ✅️ Module R (A ⊗[R'] B ⊗[R] C) ▶
The shortcut instances might speed that up, I was thinking?
Kevin Buzzard (Mar 16 2025 at 23:36):
hmm, actually that mostly looks very quick (I need to sleep now, unfortunately)
Eric Wieser (Mar 16 2025 at 23:42):
Yes, I guess my claim is that about half of the typeclass search is incurred by ext, and so splitting out the inner lemma there might make things at least run in parallel
Edison Xie (Mar 17 2025 at 00:38):
Kevin Buzzard said:
Maybe you could make some shortcut instances? i.e. make instances like
instance (R R' A B C : Type) [CommSemiring R] [CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A] [Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C] [IsScalarTower R R' A] [IsScalarTower R R' B] [IsScalarTower R' S A] [IsScalarTower R S A] : NonUnitalSemiring ((A ⊗[R'] B) ⊗[R] C) := inferInstanceat the top of the file, so you only pay once, and then these instances will be the first to be tried during the file.
this would give error : cannot find synthesization order for instance
Eric Wieser (Mar 17 2025 at 01:17):
Drop S and it should work
Eric Wieser (Mar 17 2025 at 01:17):
I'm not sure such a shortcut is helpful though
Edison Xie (Mar 17 2025 at 01:22):
Eric Wieser said:
I'm not sure such a shortcut is helpful though
Yeah it didn't work :((
Last updated: May 02 2025 at 03:31 UTC