two-sided ideals

Stream: mathlib4

[Kevin Buzzard]

I need quaternion algebras for FLT and people are looking for things to do, so I'm about to start on them. I'm stuck on the definition :-) If $K$ is a field then a quaternion algebra over $K$ is a (non-commutative) $K$-algebra $D$ with centre $K$, 4-dimensional over $K$, and having no nontrivial two-sided ideals. Everything else is fine, but are we able to talk about the lattice of two-sided ideals of a non-commutative ring yet?

[Eric Wieser]

docs#RingCon has a lattice instance now :upside_down:

[Eric Wieser]

I assume docs#QuaternionAlgebra doesn't work for you?

[Johan Commelin]

That gives a construction, but Kevin wants a characteristic predicate, basically

[Kevin Buzzard]

Yes that's right, that's like asking if iota -> K works for vector spaces over K. I am defining IsQuaternionAlgebra

[Damiano Testa]

I'm guessing that asking for "all the left-ideals of dimension different from two" does not cut it, right? :smile:

[Eric Wieser]

IsSimpleOrder (RingCon K) should capture "no nontrivial two-sided ideals" I think

[Kevin Buzzard]

In a beautifully obscure way too :-)

[Johan Commelin]

@Kevin Buzzard your definition upstairs is for CSA's of degree 2, right? $M_2(K)$ is also an example.

[Johan Commelin]

(Not saying that is bad.)

[Johan Commelin]

But for me a quaternion algebra must be a division algebra...

[Kevin Buzzard]

Re: they're CSAs: Yes. I am in a slight quandary about all this. All I need is quaternion algebras over fields, and very quickly I will be needing things which are only true for quaternion algebras because I'll need assumptions about base extensions to the reals being the Hamiltonian quaternions. But I could do CSAs over fields or even Azumaya algebras over commutative rings.

I think it's pretty standard to allow M_2(K) to be a quaternion algebra. It's just a division ring. I have two books on quaternion algebras in front of me and both allow M_2(K).

[Kevin Buzzard]

Screenshot-from-2024-05-02-12-15-56.png
That's Pierce "Associative algebras" which I think is the bible

[Johan Commelin]

Fair enough.

[Kevin Buzzard]

Also, docs#QuaternionAlgebra is wrong in characteristic 2 (in the sense that it doesn't agree with the literature, there are more examples than those), just like EllipticCurve R is wrong for a general commutative ring R (but also very useful)

[David Loeffler]

If you don't allow M_2(K) to be an example of a quaternion algebra, then it makes life difficult when you want to talk about tensoring with the completion of K at a prime, which is definitely going to be important for FLT.

Lots of books / papers seem to square this circle by writing "quaternion algebra" for any deg 2 CSA, and "quaternion division algebra" when you really want to exclude M_2(K).

[Johan Commelin]

Yeah, my opinion shouldn't be taken too seriously. I've never worked extensively with specifically quaternion algebras.

[Johan Commelin]

I would have said "deg 2 CSA". But I can understand why people prefer to call them "quaternion algebra". The name is much nicer.

[Johan Commelin]

And reserving "quaternion division algebra" for the division case seems like a good solution!

[Oliver Nash]

I'm currently travelling with very little free time so I cannot finish the below but I believe it is correct and I think it is worth bearing in mind regarding the headline question:

import Mathlib.Algebra.Module.Bimodule

open MulOpposite TensorProduct

attribute [local instance] TensorProduct.Algebra.module

example (D : Type*) [Ring D] :
    Submodule (D ⊗[ℤ] Dᵐᵒᵖ) D ≃o RingCon D where
  toFun p :=
    { r := fun x y ↦ x - y ∈ p
      iseqv := ⟨by simp, fun {x y} h ↦ by simpa using p.neg_mem h,
        fun {x y z} hxy hyz ↦ by simpa using p.add_mem hxy hyz⟩
      mul' := by
        intro w x y z hwx hyz
        replace hwx : (w - x) * y ∈ p := Subbimodule.smul_mem' p (op y) hwx
        replace hyz : x * (y - z) ∈ p := Subbimodule.smul_mem p x hyz
        simpa [sub_mul, mul_sub] using p.add_mem hwx hyz
      add' := by
        intro w x y z
        simp only [add_sub_add_comm]
        exact p.add_mem }
  invFun r :=
    Subbimodule.mk
      { carrier := {x | r x 0}
        add_mem' := by
          intro x y hx hy
          simp only [Set.mem_setOf_eq] at hx hy ⊢
          simpa using r.add hx hy
        zero_mem' := r.refl 0}
      (by intro a b h; simpa using r.mul (r.refl a) h)
      (by intro a b h; simpa using r.mul h (r.refl (unop a)))
  left_inv := by
    -- This proof is sloooow for some reason
    intro p
    dsimp only [Set.mem_setOf_eq, eq_mp_eq_cast, id_eq, smul_eq_mul, eq_mpr_eq_cast, cast_eq,
      smul_eq_mul_unop]
    simp only [RingCon.rel_mk, Con.rel_mk, sub_zero]
    rfl
  right_inv := by
    sorry
  map_rel_iff' := by
    intro p q
    simp only [Equiv.coe_fn_mk, RingCon.le_def, RingCon.rel_mk, Con.rel_mk]
    refine ⟨fun h x hx ↦ ?_, fun h {x y} ↦ @h _⟩
    specialize @h x 0
    aesop

[Eric Wieser]

I suspect RingCon is much faster in terms of elaboration, but that equivalence is certainly something we should have.

[Steven Rossi]

Has there been any update on this?

[Kevin Buzzard]

+1. I have some undergraduate students working on central simple algebras and they're working around this for now. Jujian Zhang suggested making an instance of type SetLike (RingCon R) R :-) I have no idea what people like @Jireh Loreaux will think of that!

[Jireh Loreaux]

I'm about two weeks away from having some time to devote to ideals, but I don't see any immediate problem with having that instance.

[Mitchell Lee]

Can we somehow use the contents of this file? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Bimodule.html

[Jireh Loreaux]

This has been discussed at length before (although it's understandable you haven't seen it). The issue is that we need ideals in non-unital rings too, which that approach doesn't allow for.

[Steven Rossi]

Is there a reason that we haven't just introduced right and two sided ideals in the context of rings with identities just for the sake of users? Then we prove RingCon equivalence and introduce the non unital case later

[Steven Rossi]

Just asking because it seems like it was intended when Mathlib.RingTheory.Ideal.Basic was written based off the Todo

[Kevin Buzzard]

I'm certain that the general theory of ideals in mathlib was written by an undergraduate under my supervision in 2018 without any thought whatsoever going into how to deal with the non-commutative case. We needed them for schemes, which are built on the theory of commutative rings.

[Lior Silberman]

I have a summer student with the goal of contributing to mathlib. The student is interested in algebra so I proposed looking into CSAs.

[Lior Silberman]

I think Azumaya algebras would be too much.

[Lior Silberman]

Is anyone working on implementing Wedderburn--Artin? My student can start with that.

[Lior Silberman]

I agree that CSA/Quaternion algebra should include the split algebra M_n(K).

[Ruben Van de Velde]

There's a bit of code in the flt repo that I believe relates to this, btw

[Kevin Buzzard]

I have a working full proof the statement that every CSA is a matrix ring over a division ring, written last week by some students at Imperial. I'm seeing them today and I'll talk about PRing.

[Kevin Buzzard]

They also proved that the centre of the CSA and the division ring coincide. One of the people involved is currently in China for a short visit and this has held things up a bit

[Kevin Buzzard]

Happy to figure out how to collaborate here! We're only doing what I need for FLT, which is some concrete consequences regarding base change of quaternion algebras. We're following Bourbaki algebra chapter 8

[Junyan Xu]

I have stated Wedderburn--Artin (existence, not uniqueness) as a proof_wanted here, but haven't got around to work on it (working on elliptic curves lately). I intended to follow the Wikipedia proof and I'd be curious to see what the Imperial students came up with. Tackling the simple case first could be a way to structure the proof for the general (semisimple) case; it would be better to talk about simple artinian rings (without specifying a base field) instead of CSAs for this purpose, though. It's pretty easy to show a simple artinian ring is semisimple, and that a semisimple ring R that is isogeneous as an R-module (e.g. the matrix ring over a division ring) is simple:

image.png
image.png

(from Lorenz's Algebra II)

I also have a list of TODOs once an IsTwoSided predicate (typeclass) is introduced.

[Kevin Buzzard]

@Jujian Zhang or @Edison Xie can you PR your proof that a CSA is a matrix ring over a division ring? And also the SetLike (RingCon R) R API?

[Lior Silberman]

@Junyan Xu so does it make sense for me and my student to work on proving Wedderburn--Artin?

[Jujian Zhang]

#13401 This is a PR about interpreting RingCon as two-sided ideals

[Jujian Zhang]

Lior Silberman said:

Junyan Xu so does it make sense for me and my student to work on proving Wedderburn--Artin?

Here is a version of Wedderburn--Artin (sorry free) `. The statement is the following:

theorem Wedderburn_Artin'
    (A : Type u) [Ring A] [IsArtinianRing A] [simple : IsSimpleOrder (RingCon A)] :
    ∃ (n : ℕ) (S : Type u) (h : DivisionRing S),
    Nonempty (A ≃+* (M[Fin n, S])) := by

Here is a version of Wedderburn--Artin (sorry-free as well). The statement is the following:

--- the variables are not completely shown in the statement
lemma Wedderburn_Artin_algebra_version
    [sim : IsSimpleOrder (RingCon B)]:
    ∃ (n : ℕ) (S : Type u) (div_ring : DivisionRing S) (alg : Algebra K S),
    Nonempty (B ≃ₐ[K] (M[Fin n, S])) := by

Here K is a field, B a ring. IsSimpleOrder (RingCon B) is a weird way of saying B is a simple ring (in the sense that it has no non-trivial proper two-sided-ideals) and M[Fin n, S] is the n-by-n matrix with entries in S.

But we don't have anything to say about SemiSimple rings

[Jujian Zhang]

Jireh Loreaux said:

This has been discussed at length before (although it's understandable you haven't seen it). The issue is that we need ideals in non-unital rings too, which that approach doesn't allow for.

Disclaimer : I unfortunately did not read the discussion on two-sided-ideals. But the approach in #13401 works for nonunital rings in the sense that the following compiles

variable {R : Type*} [NonUnitalNonAssocRing R]

instance : SetLike (RingCon R) R where
  coe t := {r | t r 0}
  coe_injective' := ...

SetLike (RingCon R) R works for any NonUnitalNonAssocRing R, and any I : RingCon R is an abelian group as well.
I am not sure if it works for a semiring though (because in the proof of coe_injective', I used subtraction).

[Eric Wieser]

I'm pretty sure the ideal model fails for semirings anyway; certainly you can't quotient by them any more (unlike RingCon, which you can).

[Edison Xie]

Lior Silberman said:

Junyan Xu so does it make sense for me and my student to work on proving Wedderburn--Artin?

I thinks we already have the proof in our file

[Edison Xie]

Kevin Buzzard said:

Jujian Zhang or Edison Xie can you PR your proof that a CSA is a matrix ring over a division ring? And also the SetLike (RingCon R) R API?

I think Jujian made the SetLike theorem and the fact that CSA is a matrix ring over division ring follows from wedderburn?

[Junyan Xu]

It appears that you proved Wedderburn--Artin for simple artinian rings but not for general semisimple rings. Here's an outline of the approach I have in mind:

• First we want to decompose a semisimple module into a direct sum of simple submodules. To state this we should use docs#CompleteLattice.Independent or docs#CompleteLattice.SetIndependent: see docs#CompleteLattice.independent_iff_dfinsupp_lsum_injective. We can show more generally that any submodule of a semisimple module is the supremum of an independent set of submodules, and the proof is by Zorn's lemma: there exists a maximal independent set contained in the submodule, whose supremum must equal the submodule, otherwise we can take a simple submodule in a complement of the supremum and add it to the independent set. This part is similar to the existence of a basis of a vector space.

• The number of summands isomorphic to a simple R-module (irreducible representation) S in a direct sum decomposition of a semisimple R-module M is an invariant (called multiplicity) and can be defined as the dimension (Module.rank) of S →ₗ[R] M over the division ring (Module.End R S)ᵐᵒᵖ. We may not need to define the multiplicity if we only care about existence of a decomposition into a product of matrix rings, not uniqueness.

• We can group together isomorphic summands to form isotypic components. This doesn't actually require a direct sum decomposition; you can simply take the sum (supremum) of all submodules isomorphic to a particular simple module, and no other simple module can appear as a submodule of this supremum (otherwise the projection of some summand to this submodule is nonzero, but there's no nonzero linear map between two different simple modules).

• If the semisimple module is finitely generated (Submodule.FG) then any direct sum decomposition can only have finitely many nonzero summands (in particular simple summands). (Proof: the generators only have nonzero components in finitely many summands; the other direct summands must be zero.) Any ring considered as a module over itself is generated by one element, 1. So a semisimple ring decomposes into a direct sum of finitely many simple modules over itself.

• From the proof in one of the pictures above, in a simple artinian ring we can take a minimal (nonzero) left ideal, which is a simple module, and the ring is a sum of isomorphic copies of this module, and therefore isotypic. Its direct sum decomposition into simples also consists solely of this simple module, and so it's isomorphic to a Finsupp module ι →₀ S (also isomorphic to ι → S since ι is finite), not just a DFinsupp/DirectSum. We have Module.End R (ι →₀ S) ≃+* Matrix ι ι (Module.End R S), which together with this isomorphism concludes the proof of Wedderburn--Artin for simple artinian rings. For general semisimple rings there can be multiple isotypic components, and the whole endomorphism ring is the direct product of the endomorphism rings of the isotypic components.

• A CSA is by definition a finite dimensional algebra over a field, which is artinian by docs#IsArtinianRing.of_finite, and we can get rid of this proof.

@Lior Silberman If your student want to pursue this I can certainly review drafts and PR(s).

[Lior Silberman]

@Junyan Xu thanks! -- I'll have my student follow this approach.

[Lior Silberman]

@Junyan Xu the student is @Jiang Xu Wan

[Lior Silberman]

We'll follow the following outline

0. Fix a (possibly non-commutative) ring $R$ and an $R$-module $M$.
1. For a simple $R$-module $S$ define the isotypic component $M_S$ as the lattice join of the homomorphic images of $S$ in $M$.
2. $M_S$ is the direct sum of an independent set of homomorphic images; their number well-defined. $\mathrm{End}(M_S)$ is the matrix ring over $\mathrm{End}_R(S)$.
3. Any $R$-module homomorphism $M\to N$ maps $M_S$ to $N_S$.
4. The $\{M_S\}$ are independent (i.e. their sum is direct).
5. If $M$ is semisimple and artinian, the sum of the $M_S$ is $M$ (the complement would contain a simple module).
6. If, further, $M$ is finitely generated only finitely many isotypic components are nonzero and each is of finite dimension.
7. With these hypotheses $\mathrm{End}_R(M)$ is a finite product of matrix rings.
8. If $R$ is a semisimple artinian ring then $R^{\textrm{opp}} \cong \mathrm{End}_R(R)$.
9. Either (1) the opposite of a semisimple artinian ring is semisimple and artinian; or (2) the opposite of a product of matrix rings over division rings is a matrix ring over division rings.

[Junyan Xu]

Thanks for the outline; I just realized I was confusing "isotypic" with "isogeneous" :sweat_smile:

• 2. if the number of simple direct summands is infinite, then it's not isomorphic to mathlib's docs#Matrix, which is simply the type of two-dimensional arrays without the restriction that each row only has finitely many nonzero elements, and which doesn't have a ring structure when the index type is infinite.
• 5. doesn't need $M$ to be artinian: mathlib knows a submodule (in particular the complement) of a semisimple module is semisimple, so if it's nonzero then it contains a simple submodule, because mathlib also knows a semisimple module is the supremum of all simple submodules.
• 8. holds for any semiring, not necessary semisimple artinian. It's already shown in the CrazySimple branch, but here is a computable construction.
• 9. I think we need to show (2) to deduce Wedderburn--Artin and (1) will be a consequence of W--A. Semisimplicity of a ring is currently defined to mean the ring as a left module over itself is semisimple, and it's a nontrivial fact that it's equivalent to it being semisimple as a right module. It will also be a consequence that a semisimple ring is artinian (the proof_wanted here) (but a simple ring might not be!). (Alternatively, the direct sum decomposition into finitely many simples shows it's of finite length, hence artinian.)

[Lior Silberman]

Re: 9. Yes, I already realized that. We'll prove (2) using the fact that the opposite of a division ring is also a division ring, and deduce (1) from the theorem

[Junyan Xu]

@loogle Matrix, MulOpposite
helped me find docs#Matrix.transposeRingEquiv

[loogle]

:search: Matrix.isCentralScalar, Matrix.transposeRingEquiv, and 27 more

[Lior Silberman]

Re: 3/5. I would define a module to be semisimple if every submodule has a complement. This would include an infinite direct sum of simple modules, among other things.

Adding the artinian assumption means every submodule contains a simple one.

If "semisimple" means "finite direct sum of simple modules" then you're right.

[Junyan Xu]

Yeah, I think the current mathlib definition of docs#IsSemisimpleModule is that the lattice of submodule is a complemented lattice.

[Junyan Xu]

But we do know a semisimple module is the supremum of its simple submodules: docs#IsSemisimpleModule.sSup_simples_eq_top
as well as docs#IsSemisimpleModule.submodule

[Junyan Xu]

Sorry, after my previous edit of the post I didn't notice the wrong numbering produced by the way Zulip handles markdown ...

[Lior Silberman]

An infinite direct sum of simple modules is complemented but not artinian

[Junyan Xu]

I agree, I am only claiming that any semisimple module (not necessarily artinian) is the direct sum of its isotypic components.
If the module is the ring itself, then it's f.g. and can't be an infinite direct sum, so it's a finite direct sum of simples and therefore of finite length and artinian.

[Lior Silberman]

Got it. In 5,6 we'll assume f.g. = artinian (best add a proof of the equivalence), and then at step 8 will argue that a semisimple ring is f.g.

[Lior Silberman]

Regarding the opposite: it's not true that the opposite of a matrix ring is the same matrix ring -- it's the matrix ring over the opposite coefficient ring. Is the proof you found for commutative coefficient rings?

[Lior Silberman]

Checked: it is

[Junyan Xu]

Yeah, commutativity comes from the CommSemigroup instance, so mathlib doesn't have the desired RingEquiv apparently ... I also found nothing with Pi.semiring, MulOpposite.

[Lior Silberman]

We can write one

[Junyan Xu]

At least we have docs#MulOpposite.instDivisionRing ...

[Junyan Xu]

For 5 I'm claiming the following is true and I don't think you need to assume anything:

import Mathlib.RingTheory.SimpleModule

variable {R M} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M]

lemma IsSemisimpleModule.sSup_simples_eq (N : Submodule R M) :
    sSup {S | S ≤ N ∧ IsSimpleModule R S} = N := by
  apply le_antisymm
  · apply sSup_le; intro S hS; exact hS.1
  have := congr_arg (Submodule.map N.subtype) <|
    IsSemisimpleModule.sSup_simples_eq_top (R := R) (M := N)
  rw [Submodule.map_top, N.range_subtype] at this
  conv_lhs => rw [← this]
  rw [Submodule.map_le_iff_le_comap]
  apply sSup_le; intro S hS
  rw [← Submodule.map_le_iff_le_comap]
  apply le_sSup; constructor
  · rw [Submodule.map_le_iff_le_comap, Submodule.comap_subtype_self]; exact le_top
  rw [Set.mem_setOf] at hS
  exact IsSimpleModule.congr (S.equivMapOfInjective _ <| N.injective_subtype).symm

example {N : Submodule R M} (hN : N ≠ ⊥) : ∃ S ≤ N, IsSimpleModule R S := by
  by_contra!; apply hN
  rw [← IsSemisimpleModule.sSup_simples_eq N]
  convert sSup_empty
  apply Set.eq_empty_of_forall_not_mem
  intro S hS; exact this S hS.1 hS.2

[Lior Silberman]

I'm not sure: I don't think a complemented lattice need have minimal elements.

[Junyan Xu]

Hmm, it looks like exists_setIndependent_of_sSup_atoms_eq_top directly gives a direct sum decomposition into simples, given docs#IsSemisimpleModule.sSup_simples_eq_top (which is proved using docs#isAtomistic_of_complementedLattice, which uses the fact that the lattice of submodules is a compactly generated complete modular lattice).

[Junyan Xu]

Okay, it's a bit cumbersome to convert between sSup of submodules of a submodule and sSup in the original module, but I've worked out a proof and updated my post above.

[Junyan Xu]

The proofs can be simplified a lot using the atom(ist)ic API, and I opened #13636.

Here's an easy way to see the submodule lattice of a semisimple R-module is atomic: every nonzero element generates a cyclic submodule isomorphic to R/I for some ideal I. Take a maximal ideal M containing I, then the submodule M/I of R/I has a complement, which must be isomorphic to (R/I)/(M/I)=R/M, a simple R-module.

[Jiang Xu Wan]

@Junyan Xu I'm running into an issue involving the definition of an isotypic component; in particular, I'm struggling to get the clauses to work properly.

Here is one definition of isotypic component I've written: (I've written out multiple definitions of isotypic component and been playing around to see which one will lead to the easiest proofs later on, but the exact contents of the definitions are likely not creating the issue)

def isotypic {R} {M} [Ring R] [AddCommGroup M] [Module R M]
(S) [AddCommGroup S] [Module R S] : Submodule R M :=
  sSup {N : Submodule R M | ∃ f : S ≃ₗ[R] N, Function.Bijective f}

I am using this definition in the sum of all isotypic components of M:

def isotypic_sup (R) (M) [Ring R] [AddCommGroup M]
[Module R M] [IsSemisimpleModule R M] : Submodule R M :=
  sSup {I : Submodule R M | ∃ (S : Submodule R M), IsSimpleModule R S ∧ I = isotypic S}

The definition of isotypic component isn't perfect as we it only makes sense to talk about isotypic components when $S$ is a simple $R$-module, but when I add the clause [IsSimpleModule R S] to the definition of isotypic component and get:

def isotypic {R} {M} [Ring R] [AddCommGroup M] [Module R M]
(S) [AddCommGroup S] [Module R S] [IsSimpleModule R S] : Submodule R M :=
  sSup {N : Submodule R M | ∃ f : S ≃ₗ[R] N, Function.Bijective f}

then the above definition of isotypic_sup has an error, where the part I = isotypic S is labelled with the error

failed to synthesize instance
  IsSimpleModule R ↥S

In the end, I want to have the definition of isotypic component include the clause [IsSimpleModule R S], so is there a way to resolve the above issue?

[Jiang Xu Wan]

Another independent issue concerning specific definition of isotypic is how to induce an instance of Module R N if we have (N : Submodule R M). I have found the instance SubmoduleClass.module, but I'm not quite sure how to use it.

Edit: I might be able to work around this issue?

[Junyan Xu]

when I add the clause [IsSimpleModule R S] to the definition of isotypic component and get: ... then the above definition of isotypic_sup has an error, where the part I = isotypic S is labelled with the error

I think if you change ∃ (S : Submodule R M), IsSimpleModule R S ∧ I = isotypic S to ∃ (S : Submodule R M) (_ : IsSimpleModule R S) : I = isotypic S then the error should disappear. However, I don't recommend you add the clause [IsSimpleModule R S] to the definition of isotypic component.

Comments on the definition of isotypic:

• It seems strange to make R and M implicit arguments
• Function.Bijective is unnecessary (you can use docs#LinearEquiv.toEquiv + docs#Equiv.bijective)
• In mathlib you don't add assumptions to a def that isn't absolutely necessary, so for example here I wouldn't include [IsSimpleModule] in the def isotypic, nor include [IsSemisimpleModule] in isotypic_sup, to avoid creating unnecessary goals like the IsSimpleModule R ↥S that you encountered. In fact the unused_argument linter would probably complain if you do include them. When proving theorems about the defs, you are of course free to add whatever conditions needed.

Another independent issue concerning specific definition of isotypic is how to induce an instance of Module R N if we have (N : Submodule R M). I have found the instance SubmoduleClass.module, but I'm not quite sure how to use it.

I don't think you need to explicit invoke the instance; it automatically endows ↥N with an R-module structure given N : Submodule R M.

[Lior Silberman]

The reason for restricting isotypic(S) to simple modules is that otherwise the two natural definitions
$\sum \{ N\subset M: N\cong S\}$
and
$\sum \{ \textrm{Im} (f) \}_{f\in\textrm{Hom}_R(S,M)}$
disagree

[Lior Silberman]

Even worse, the theorem "the sum of the isotypic components is direct" would be false.

[Jiang Xu Wan]

@Junyan Xu I am aware that the Function.Bijective is unnecessary from the perspective that $f$ being a linear equivalence already means that it is bijective; the issue is that since I'm using an existential quantitier on $f$, I need to follow up with some proposition. Do you have any suggestions on how to fix this? i.e. is there a better way to write out that $S$ and $N$ need to be isomorphic to each other

[Jujian Zhang]

How about Nonempty (S \equiv N) (https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nonempty)

[Jujian Zhang]

Then Nonempty.some gives you the linear equiv (via axiom of choice if you don't mind)

[Kim Morrison]

Lior Silberman said:

Even worse, the theorem "the sum of the isotypic components is direct" would be false.

Junyan's point above is that the theorem would not be false, because that theorem would have an [IsSimpleModule] argument!

[Lior Silberman]

The theorem would be true, but it would not match how mathematicians think here. Instead of defining the notion from the literature we

Kim Morrison said:

Junyan's point above is that the theorem would not be false, because that theorem would have an [IsSimpleModule] argument!

I understand that -- but this isn't the theorem the reader would expect. I'm new here, so I'm happy to follow your lead, but that means first making an arbitrary generalization of a standard notion (which therefore should not be called "isotypical component" but something else), and then in every application adding an extra condition to return to the notion that is in use.

We'll do as you say.

If you are aware of any point in the literature where either generalization is used this would be different of course.

[Junyan Xu]

It's the same principle as defining division without the requirement that the denominator must be nonzero, because we don't want to supply the nonzeroness condition every time we write a/b. When b is zero we just assign the junk value 0 to a/b. And we still call it division even though it doesn't satisfy what you expect of a division (e.g. a/(a/b)=b may not be true if a=0) outside of its intended domain, so I see no reason why we can't call the definition isotypic without the IsSimpleModule assumption. In isotypic we don't even need to assign any junk value using if then else, which is nice.

Sometimes people choose junk values to make certain lemmas hold outside of the intended domain (e.g. 0⁻¹=0 makes a⁻¹⁻¹=a universally true, docs#minpoly is defined to make docs#minpoly.aeval universally true but not docs#minpoly.monic), but that's not a requirement.

[Kevin Buzzard]

One of my first lean experiences was defining the square root of a nonnegative real number as a sup and then being told that I should delete "nonnegative" in the definition because why make a function which demands an input and then never uses it? Turns out the sup of the empty set was defined to be 0. It's a very common phenomenon in lean formalisation to define things in more generality than makes mathematical sense. The hypotheses go in the theorems, not the definitions, in the model of formalisation which mathlib uses

[Jireh Loreaux]

Also, for example, docs#cfc. The fact that it doesn't take proposition arguments or bundled functions is a very important feature, in sharp contrast to the (mainly not for user consumption) docs#cfcHom

[Edison Xie]

So does any of you have the proof of uniqueness of wedderburn theorem yet?

[Edison Xie]

We really need that :((

[Kevin Buzzard]

Can you formalise the statement?

[Edison Xie]

of course we do we had it for decades no one can solve this

[Edison Xie]

import Mathlib.LinearAlgebra.Matrix.IsDiag

local notation "M[" ι "," R "]" => Matrix ι ι R

theorem Wedderburn_Artin_divisionRing_unique_algebra_version
    (D E : Type*) [DivisionRing D] [DivisionRing E] [Algebra K D] [Algebra K E]
    (m n : ℕ) (hm : m ≠ 0) (hn : n ≠ 0)
    (iso : M[Fin m, D] ≃ₐ[K] M[Fin n, E]) : Nonempty $ D ≃ₐ[K] E :=  sorry

[Kevin Buzzard]

This doesn't compile :-(

[Lior Silberman]

Our version of the theorem will have uniqueness

[Edison Xie]

good to know :)

[Kevin Buzzard]

Edison Xie said:

of course we do we had it for decades no one can solve this

You mean "I can't solve this", right? :-)

[Edison Xie]

Kevin Buzzard said:

Edison Xie said:

of course we do we had it for decades no one can solve this

You mean "I can't solve this", right? :-)

I mean no one in our group could :((

[Kevin Buzzard]

Do you have a maths proof?

[Edison Xie]

Yes but we somehow just stuck at the simple module part I sent u earlier

[Edison Xie]

All the other parts are working now

[Kevin Buzzard]

What's the simple module part?

[Edison Xie]

import Mathlib.Tactic

local notation "M[" ι "," R "]" => Matrix ι ι R
variable (K : Type*) [Field K](B : Type*) [Field K] [Ring B] [Algebra K B] [FiniteDimensional K B]

instance (M : Type*) [AddCommGroup M] [Module B M]  :
  Algebra K (Module.End B M) where
    smul := fun k x =>
    { toFun := fun m => x $ (algebraMap K B k) • m
      map_add' := fun m1 m2 => by simp
      map_smul' := fun b m => by
        simp only [LinearMapClass.map_smul, RingHom.id_apply]
        rw [← MulAction.mul_smul, Algebra.commutes k b, MulAction.mul_smul] }
    toFun k :=
    { toFun := fun m => algebraMap K B k • m
      map_add' := fun m1 m2 => by simp
      map_smul' := fun m1 m2 => by
        simp only [RingHom.id_apply]
        rw [← MulAction.mul_smul, Algebra.commutes k m1, MulAction.mul_smul] }
    map_one' := by simp only [_root_.map_one, one_smul]; rfl
    map_mul' a b := by
      ext m
      simp only [_root_.map_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply,
        LinearMapClass.map_smul]
      rw [← MulAction.mul_smul, Algebra.commutes, MulAction.mul_smul]
    map_zero' := by simp only [map_zero, zero_smul]; rfl
    map_add' a b := by
      ext m
      simp only [map_add, add_smul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply]
    commutes' a x := by
      ext m
      simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.mul_apply,
        LinearMap.coe_mk, AddHom.coe_mk, LinearMapClass.map_smul]
    smul_def' a x := by
      ext m
      change x _ = _
      simp only [_root_.map_smul, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
        LinearMap.mul_apply, LinearMap.coe_mk, AddHom.coe_mk]

def test' (D : Type*) [DivisionRing D] [Algebra K D] (m : ℕ) (hm : m ≠ 0)
    (Wdb : B ≃ₐ[K] M[Fin m, D]) (M : Type*)
    [AddCommGroup M] [Module B M] [IsSimpleModule B M] :
    Module.End B M ≃ₐ[K] Dᵐᵒᵖ := by sorry

this

[Kevin Buzzard]

Do you have a maths proof?

[Edison Xie]

and the proof is in https://stacks.math.columbia.edu/tag/074E here, lemma 11.4.6 (4)

[Edison Xie]

and the equivalence in the

Edison Xie said:

and the proof is in https://stacks.math.columbia.edu/tag/074E here, lemma 11.4.6 (4)

and the equivalence setup in this is the file MoritaEquivalence in the repository I invited u in

[Edison Xie]

@Kevin Buzzard

[Jujian Zhang]

In #14456, I tried to set up the lattice structure on two-sided ideal; however this results in a instance diamond: TwoSidedIdeal has two PartialOrder on it: one from SetLike instance, the other from CompleteLattice structure. Is there anyway to avoid this? Should I just attribute [-instance] SetLike.partialOrder or something?

[Johan Commelin]

But they have the same data, right? So can you spread the SetLike.partialOrder instance into the complete lattice instance?

[Jujian Zhang]

Thanks! Let me try.

[Jujian Zhang]

I was using Function.Injective.completeLattice to get a lattice structure almost for free which resulted in the diamond. I think I will just hand-write the lattice structure instead.

[Jujian Zhang]

Writing the instances by hand makes SetLike.instPartialOrder and CompleteLattice.partialOrder equal definitionally, thanks!

[Yaël Dillies]

I'm surprised the setlike and pulled back definitions differ. What are they defeq to?

[Jujian Zhang]

Using Function.Injective.CompleteLattice the partial order is given by RingCon’s order (ie propositional implication) since I am trying to pullback RingCon’s order; writing the instances by hand gives you the order by set inclusion. So defeq to SetLike.instPartialOrder.

[Yaël Dillies]

Yeah I get that, and I would expect those to be the same

[Yaël Dillies]

Ah no, I see

[Jujian Zhang]

For any ring con I the set are the elements related to 0

[Jujian Zhang]

So set inclusion is not literally propositional implication sadly.

[Yaël Dillies]

The ringcon version of I <= J reduces to forall a b, a ~_I b => a ~_J b while the setlike version is forall a, a ~_I 0 => a ~_J 0

[Yaël Dillies]

Anyway I really think we should yeet SetLike.instPartialOrder out of existence

[Kevin Buzzard]

You mean write all the instances manually? Does it cause at least one more diamond? My impression is that the reason things are problematic here is that this is an innovative use of SetLike.

[Yaël Dillies]

We also get issues with docs#UpperSet which is endowed with the order of reverse inclusion

[Yaël Dillies]

SetLike.instPartialOrder is like one of the original sins, since it creates data out of a prop

[Kevin Buzzard]

The docstring for UpperSet is the hugely unhelpful The type of upper sets of an order. BTW :-) (I have no idea what an upper set is, I thought that was the point of the docstring :-) )

[Yaël Dillies]

Uh sorry :sweat_smile: Will fix

[Kevin Buzzard]

Aha, having clicked through to IsUpperSet I now see the point. You want to model a as {x : a <= x} or something, so smaller upper sets correspond to bigger elements of the order.

[Kevin Buzzard]

I thought you were busy for a week, I'll fix it if you like :-) I am currently on a war against bad documentation.

[Yaël Dillies]

Yes, I am in the Baltic sea for another week, but apparently the Swedes are so modern that even the sea has 4G

[Yaël Dillies]

Kevin Buzzard said:

I thought you were busy for a week, I'll fix it if you like :-) I am currently on a war against bad documentation.

Please do!

[Ruben Van de Velde]

So much for a break from lean :)

[Kevin Buzzard]

#14467

[Notification Bot]

2 messages were moved from this topic to #mathlib4 > independent submodules by Johan Commelin.

[Jireh Loreaux]

I am also in favor of removing the partial order instance from SetLike. We just leave it as a reducible def and then use it in most places, but it shouldn't be forced.

[Eric Wieser]

I'd argue it's a feature here, as it means you have the defeq that lets you write hle hI : x \mem J where hI : x \mem I and hle : I ≤ J

[Eric Wieser]

This is arguably a big part of the API of ≤ across mathlib, whereas defeq with ringcon is more of an implementation detail

[Yaël Dillies]

Yeah, that's a good argument

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hello. I have run into issues with two-sided ideals just now when trying to prove something about matrix rings. Currently the Jacobson radical of an ideal $I$ is defined only as a left ideal, but mathlib doesn't know that if $I$ is two-sided then so is $J(I)$. I just proved this, but I don't know how to state it in a non-awkward way: doing this needs some way of relating left and two-sided ideals. The two concepts are defined in quite different ways, and I couldn't find any way to relate them. Am I missing something? Is there any consensus on how this API should look?

What I have proved is

theorem jacobson_mem_mul_right {I : Ideal R}
    (I_mem_mul_right : ∀ {x y}, x ∈ I → x * y ∈ I) :
    ∀ {x y}, x ∈ I.jacobson → x * y ∈ I.jacobson := by

Since there is no IsTwoSided predicate, I had to state right-absorption explicitly. If #14460 were merged, should I use (I : TwoSidedIdeal R).asIdeal.jacobson here?

[Jireh Loreaux]

I think you should just make the Jacobson radical into a TwoSidedIdeal. That being said, you probably can't do this yet, as the API isn't sufficiently developed.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Jireh Loreaux the problem is that it's not always two-sided, afaict (but do correct me if that's wrong); you need the base ideal to also be two sided. So such a change would make the definition less general.

[Jireh Loreaux]

Sorry, I tried to be quick because I was walking in to teach a class. What I mean is this: you can create a TwoSidedIdeal.jacobson whose argument and conclusion are TwoSidedIdeals, and then you can prove for I : TwoSidedIdeal R, that I.jacobson.asIdeal = I.asIdeal.jacobson.

Also, we should probably have a constructor that takes an I : Ideal R and a proof that ∀ x y, x ∈ I → x * y ∈ I and produces a TwoSidedIdeal, but I don't think that appears in #14460.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I see. Would it also make sense to have a predicate IsTwoSided (I : Ideal R) := ∃ (J : TwoSidedIdeal R), I = J.asIdeal?

[Jireh Loreaux]

:thinking: I doubt it. However, a CanLift instance would definitely make sense.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ok, I did this in #17341.

[Junyan Xu]

I've proved Hopkins–Levitzki in #17908 and introduced the typeclass Ideal.IsTwoSided along the way (following this outline), which I'll probably extract as a dependent PR.

How's it going with the development of Isotypic APIs? I plan to return to this soon.

[Junyan Xu]

Oh, I didn't realize @Jiang Xu Wan's PR has been open since two months ago: #16216

[Kim Morrison]

@Jiang Xu Wan, sincere apologies that your PR #16216 has not been reviewed. Unfortunately our CI setup requires that PRs are made from branches of the main repository, rather than from forks.

[Kim Morrison]

I've just sent an invitation for write access to the repository for your github account jxjwan. Would you mind accepting that, and then pushing the branch to the main repo and recreating the PR? If you post here, hopefully it will then get some prompt review.

[Jiang Xu Wan]

Sorry, I've been back in school since September, so I've been very busy. @Kim Morrison I have accepted your invitation. I am not entirely sure what to do next.

[Johan Commelin]

Do you have a copy of mathlib on your computer?

[Johan Commelin]

In that copy, please do the following:

• git checkout master -- to make sure you are on the main branch
• git pull -- to get the latest updates to mathlib
• git checkout -b jxjwan-isotopic -- to create your own branch
• Now copy your changes from #16216 to this new branch
• git add <filenames>
• git commit
• git push
• and follow the instructions to create a pull request.

[Johan Commelin]

https://leanprover-community.github.io/contribute/index.html contains many more details on this process

[Johan Commelin]

It's all a bit difficult, but that's because we want to run a bunch of checks on every pull request, and that's currently a lot harder if they're made from a fork.

[Lior Silberman]

Thanks. One lesson from our summer project is that it's best for the students to work directly off mathlib and not with a local fork

[Lior Silberman]

My bad for making the wrong choice back in May

[Johan Commelin]

To be fair, our workflow is very non-standard.

[Jiang Xu Wan]

I don't think I know how to get my changes into the new branch; I'm trying out a few things but it all doesn't seem to be affecting the branch.

[Johan Commelin]

If you have two separate directories on your computer, one with your own fork of mathlib, and the other with the new copy with the new branch, then you can just copy-paste changes.

[Jiang Xu Wan]

I don't think I have separate directories on my computer? I'm confused as to how the stuff on my computer is connected to branches on github. How I made my fork originally was that I played with code on my computer, then put those changes on the github editor.

[Johan Commelin]

Aha, I see.

[Johan Commelin]

If you want, you could do the same thing, but on https://github.com/leanprover-community/mathlib4

[Johan Commelin]

But you can also use some git commands on your computer. Which will be easier in the long run.

[Johan Commelin]

Are you happy to run commands in a terminal? Or would you prefer to avoid using a terminal?

[Jiang Xu Wan]

I could run commands in my terminal, but I don't really understand what I'm doing when I use commands in my terminal, so I can never tell when I do something wrong or when something worked.

[Jiang Xu Wan]

Okay, I've now made https://github.com/leanprover-community/mathlib4/pull/18646; can you check that this is proper?

[Jiang Xu Wan]

Oh I see some of the effects of this kind of pull request now; review dog is finding some styling issues automatically!

[Johan Commelin]

@Jiang Xu Wan Yes, this is a PR from a mathlib branch. That looks alright!

[Jireh Loreaux]

We're (or probably it's just me) still suffering from the fact that docs#Ideal is an abbrev for Submodule R R because it means that in non-unital rings we can still only talk about TwoSidedIdeals and not Ideals.

[Jireh Loreaux]

This came up because I'm trying to define the hereditary C⋆-subalgebra generated by a given set s, and the natural way to do it is to make its carrier (Ideal.span s).topologicalClosure ∩ star (Ideal.span s).topologicalClosure.

[Junyan Xu]

I made a PR #18969 to generalize only the definition of Module and Submodule to NonUnitalSemirings, and it slows down Mathlib by 2.55%.
It might get better or worse after we generalize all the lemmas ... Feel free to push to generalize whatever decls you want.

[Johan Commelin]

Thanks for starting this attempt! I really hope it ends up going the "might get better" path

[Matthew Ballard]

Can we start with adding SemigroupAction alone?

[Junyan Xu]

Do you mainly want to test the performance impact of introducing SemigroupAction?

I forgot that the main target is to generalize Ideal. I made the generalization and there are a few more breakages (most look like instance synthesis failure), but all are fixed by specifying certain arguments (or bumping maxHeartbeats to 400000 in one occasion).

[Matthew Ballard]

I think SemigroupAction

• is something we need itself as a natural notion
• won't be a source of much if any regression (untested)

It would be nice to tease out the most problematic instance synthesis chains by breaking things into smaller steps.

[Jireh Loreaux]

Ugh, I've been dreading adding all these non-unital actions. :disappointed:

Thanks for starting to work on this though @Junyan Xu

[Junyan Xu]

Actually I only added two (or three) non-unital actions ((Add)SemigroupAction and NonUnitalModule). I don't think there's anything else that is natural to add. If this looks promising please take over, because I'm not planning to spend much more time on this.

In the meantime I'm still diagnosing the 0.45/0.56% slowdown in the actual two-sided ideal PR (see this thread for my experiments), e.g. I'm still not sure why RingTheory.AdjoinRoot got 52.34% slower. I tried to use the profiler to identify which decls get slower, but the outputs are irregular (sometimes longer with more items, sometimes shorter, making them hard to align) and results fluctuate. I'm now trying to use #count_heartbeats but it applies to one decl a time only, which is inconvenient if you want the data for all decls. Is there a convenient way to get heartbeat data, e.g. by extracting it from the !bench results? (Are "instructions" in the !bench results the same as heartbeats?)

[Jireh Loreaux]

Can you (very briefly) remind me why we should want Ideal.IsTwoSided in addition to docs#TwoSidedIdeal ? It seems like one of those situations where we're again asking type class synthesis to do something that should be baked into the type (e.g., docs#IsClosed).

[Jireh Loreaux]

I wonder if some of the performance hit in #18969 comes from changing DistribMulAction to extend DistribSMul instead of the existing (priority := 100) instance.

[Jireh Loreaux]

I'm working on extracting only the SemigroupAction material from #18969 into #19046

[Jireh Loreaux]

@Matthew Ballard said:

• won't be a source of much if any regression (untested)

https://github.com/leanprover-community/mathlib4/pull/19046#issuecomment-2477408304 :sad:

[Jireh Loreaux]

It's not the worst I've ever seen, but given that we didn't generalize any lemmas here, it's a bit depressing.

[Matthew Ballard]

Very interesting. In my mind, we only took a node in the instance graph and expanded it to two nodes joined by a single edge. Am I wrong?

[Eric Wieser]

I would guess that without lean4#2905 having landed, the cost includes some extra edges too

[Matthew Ballard]

Then it should disappear on nightly-testing?

[Eric Wieser]

Yes, I think we should also profile the effect of this PR there.

[Junyan Xu]

...  I don't think there's anything else that is natural to add. ...

Actually it would be natural to introduce DistribSemigroupAction too ...

[Junyan Xu]

Jireh Loreaux said:

Can you (very briefly) remind me why we should want Ideal.IsTwoSided in addition to docs#TwoSidedIdeal ? It seems like one of those situations where we're again asking type class synthesis to do something that should be baked into the type (e.g., docs#IsClosed).

Here are some reasons why TwoSidedIdeal would be a more cumbersome approach and not necessarily better performance-wise:

To avoid duplication, if a declaration about quotient rings that currently assumes CommRing+Ideal can be generalized to the noncommutative setting, you'd like to change the assumptions to Ring+TwoSidedIdeal without keeping the original version. But there will be certain results in later files that don't generalize or you don't want to touch, and in order for the declarations in earlier files you generalized to continue to apply, you have to introduce a coercion that automatically converts an Ideal over a CommRing to a TwoSidedIdeal. However, if I : Ideal R then R⧸I makes sense (from Submodule.hasQuotient) without the coercion (it's an AddCommGroup with a (left) R-Module structure), and I don't think it's possible to tell Lean to insert the coercion only when you want to consider the ring structure. The two quotients (with or without the coercion) are defeq but either you need to explicitly convert between them (with a LinearEquiv or else) or it can be another source of slowness (it's similar to (ab?)using the defeq between ↥E, ↥E.toSubalgebra, ↥E.toSubalgebra.toSubmodule for an intermediate field E, for example).

As of now, there have been no results about commutative quotient rings that have been generalized using TwoSidedIdeal as far as I know, while my PR does many generalizations. (Apparently you can't write R⧸I for I : TwoSidedIdeal R yet and have to write I.ringCon.Quotient.)

Also, operations like sup, inf, add, mul, pow etc. are the same on TwoSidedIdeal as on Ideal, and it would be cumbersome to define them again for TwoSidedIdeal and awkward to coerce to the same type in order to perform the operations.

[Eric Wieser]

Junyan Xu said:

Also, operations like sup, inf, add, mul, pow etc. are the same on TwoSidedIdeal as on Ideal, and it would be cumbersome to define them again for TwoSidedIdeal and awkward to coerce to the same type in order to perform the operations.

I think we already have the first two of these on TwoSidedIdeal via RingCon

[Jireh Loreaux]

Eric Wieser said:

Yes, I think we should also profile the effect of this PR there.

@Eric Wieser what do I need to do in order to accomplish that? I assume I just rebase this PR on top of nightly testing, and create a new PR, but I assume there won't be any run to bench against?

[Eric Wieser]

I would recommend merging rather than rebasing. I don't know for sure how the benchmarking tools work

[Jireh Loreaux]

@Matthew Ballard Is there a way to benchmark something against nightly testing?

[Matthew Ballard]

Benchmark the previous commit?

[Jireh Loreaux]

So, branch nightly testing, make a PR, !bench, then merge in the changes and !bench again?

[Matthew Ballard]

I think you can just make a PR from nightly-testing itself, !bench, then merge the changes and do it again. You have to go into the speedcenter and select the two runs to compare after that

[Kim Morrison]

I have a script that will run the benchmark comparing two arbitrary commits. I'm not at a computer until Monday, but if someone asks again then I'll post it.

[Damiano Testa]

I adapted this from the bench_summary action: save this file

/-
Copyright (c) 2024 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/

import Lean.Elab.Command

/-!
# Summary of `!bench` results

This file contains a script that converts data retrieved from the speed-center into a
shorter, more accessible format, and post a comment with this summary on github.
-/

namespace BenchAction

open Lean

/-- `Bench` is a structure with the data used to compute the `!bench` summary.
It contains
* a string `file` (that could be `build`, `lint` or `~Mathlib.Path.To.File`);
* an integer `diff` representing the change in number of instructions for `file`;
* a float `reldiff` representing the percentage change in number of instructions for `file`.
-/
structure Bench where
  file    : String
  diff    : Int
  reldiff : Float
  deriving FromJson, ToJson, Inhabited

/-- `intDecs z exp prec` is a "generic" formatting of an integer `z`.
It writes `z` in the form `x.y * 10 ^ exp` (for non-negative integers `x`, `y` and `z`),
such that `y` has `prec` digits and returns
* the sign of `z` as a string (in fact, just either `+` or `-`);
* the integer `x`;
* the natural number `y` (that has `prec` digits).
-/
def intDecs (z : Int) (exp : Nat := 9) (prec : Nat := 3) : String × Int × Nat :=
  let sgn := z.sign
  let z := sgn * z
  let p10 : Int := 10 ^ (exp - prec)
  let idec := z / p10
  (if sgn < 0 then "-" else "+", idec / (10 ^ prec), (idec % 10 ^ prec).toNat)

/-- `formatDiff z` uses `intDecs` to format an integer `z` as `±x.y⬝10⁹`. -/
def formatDiff (z : Int) : String :=
  let (sgn, intDigs, decDigs) := intDecs z
  s!"{sgn}{intDigs}.{decDigs}⬝10⁹"

/-- Convert a `Float` into a formatted string of the form `±z.w%`. -/
def formatPercent (reldiff : Float) : String :=
  -- shift by `2` twice: once to get a percentage, again for two decimal digits of precision
  let reldiff := reldiff * 10 ^ 4
  let sgn : Int := if reldiff < 0 then -1 else 1
  let reldiff := (.ofInt sgn) * reldiff
  let (sgn, intDigs, decDigs) := intDecs (sgn * reldiff.toUInt32.val) 0 2
  -- the `if ... then ... else ...` makes sure that the output includes leading `0`s
  s!"({sgn}{intDigs}.{if decDigs < 10 then "0" else ""}{decDigs}%)"

/--
info: [(+0.00%), (+14.28%), (+0.20%), (-0.60%), (-0.08%), (+1.02%)]
---
info: [+0.0⬝10⁹, +1.0⬝10⁹, +30.200⬝10⁹, -0.460⬝10⁹]
-/
#guard_msgs in
run_cmd
  let floats : Array Float := #[0, 1/7, 0.002, -0.006, -8.253600406145226E-4, 0.0102]
  logInfo m!"{floats.map formatPercent}"
  let ints : Array Int := #[0, 10^9, 302*10^8, -460000000]
  logInfo m!"{ints.map formatDiff}"

/--
`formatFile file` converts a `String` into a formatted string of the form `` `file` ``,
removing leading non-letters. It is expected that `~` is the only leading non-letter.
-/
def formatFile (file : String) : String := s!"`{file.dropWhile (!·.isAlpha)}`"

/--
`summary bc` converts a `Bench` into a formatted string of the form
``| `file` | ±x.y⬝10⁹ | ±z.w% |`` (technically, without the spaces).
-/
def summary (bc : Bench) : String :=
  let middle := [formatFile bc.file, formatDiff bc.diff, formatPercent bc.reldiff]
  "|".intercalate (""::middle ++ [""])

/--
`toTable bcs` formats an array of `Bench`es into a markdown table whose columns are
the file name, the absolute change in instruction counts and the relative change as a percentage.
A typical entry may look like ``|`Mathlib.Analysis.Seminorm`|+2.509⬝10⁹|(+1.41%)|``.
-/
def toTable (bcs : Array Bench) : String :=
  let header := "|File|Instructions|%|\n|-|-:|:-:|"
  "\n".intercalate (header :: (bcs.map summary).toList)

/--
`toCollapsibleTable bcs roundDiff` is similar to `toTable bcs`, except that it returns
output enclosed in a `<details><summary>` html-block.
The `<summary>` part tallies the number of entries in `bcs` whose instructions increased
resp. decreased by at least the amount `roundDiff`.
-/
def toCollapsibleTable (bcs : Array Bench) (roundDiff : Int) : String :=
  s!"<details><summary>{bcs.size} files, Instructions {formatDiff <| roundDiff * 10 ^ 9}\
    </summary>\n\n{toTable (bcs.qsort (·.diff > ·.diff))}\n</details>\n"

/-- Assuming that the input is a `json`-string formatted to produce an array of `Bench`,
`benchOutput` returns the "significant" changes in numbers of instructions as a string. -/
def benchOutput (jsonInput : String) : IO String := do
  let data ← IO.ofExcept (Json.parse jsonInput >>= fromJson? (α := Array Bench))
  -- `head` contains the changes for `build` and `lint`,
  -- `data` contains the instruction changes for individual files:
  -- each filename is prefixed by `~`.
  let (head, data) := data.partition (·.file.take 1 != "~")
  -- Partition the `Bench`es into "bins", i.e. the subsets of all `Bench`es whose difference
  -- in instructions lies in an interval `[n·10⁹, (n+1)·10⁹)`.
  -- The values `n` need not be consecutive: we only retain non-empty bins.
  let grouped := ((data.groupByKey (·.diff / (10 ^ 9))).toArray.qsort (·.1 > ·.1)).toList
  -- We consider `build` and `lint` as their own groups, in this order.
  let sortHead := (head.qsort (·.file < ·.file)).toList.map (0, #[·])
  let togetherSorted := sortHead ++ grouped
  -- For better formatting, we merge consecutive bins with just a single *file* into one.
  -- This covers the two steps `ts1` and `ts2`.
  -- For example, `[..., (bound₁, #[a₁]), (bound₂, #[a₂]), (bound₃, #[a₃]), ...]` gets collapsed to
  -- `[..., (none, #[a₁, a₂, a₃]), ...]`.
  -- The `boundᵢ` entry becomes `none` for the collapsed entries, so that we know that these
  -- should be printed individually instead of inside a `<details><summary>`-block.
  -- A single bin with just a single file is also marked with `none`, for the same reason.
  let ts1 := togetherSorted.splitBy (·.2.size == 1 && ·.2.size == 1)
  let ts2 := List.flatten <| ts1.map fun l ↦
    if (l.getD 0 default).2.size == 1 then
      [(none, l.foldl (· ++ ·.2) #[])]
    else
      l.map fun (n, ar) ↦ (some n, ar)

  let mut overall := []
  for (bound, gs) in ts2 do
    overall := overall ++ [
      match bound with
        -- These entries are from "singleton" files in their range; we print them individually.
        | none => toTable gs
        -- These get a collapsible summary instead.
        | some roundedDiff => toCollapsibleTable gs roundedDiff]
  return "\n".intercalate overall

open Lean Elab Command in
/-- `addBenchSummaryComment PR repo tempFile` adds a summary of benchmarking results
as a comment to a pull request.  It takes as input
* the number `PR` and the name `repo` as a `String` containing the relevant pull-request
  (it reads and posts comments there)
* the `String` `tempFile` of a temporary file where the command stores transient information.

The code itself interfaces with the shell to retrieve and process json data and eventually
uses `benchOutput`.
Here is a summary of the steps:
* retrieve the last comment to the PR (using `gh pr view ...`),
* check if it was posted by `leanprover-bot`,
* try to retrieve the source and target commits from the url that the bot posts
  and store them in `source` and `target`,
* query the speed center for the benchmarking data (using `curl url`),
* format and filter the returned JSON data (various times),
  saving intermediate steps into `tempFile` (using `jq` multiple times),
* process the final string to produce a summary (using `benchOutput`),
* finally post the resulting output to the PR (using `gh pr comment ...`).
-/
def addBenchSummaryComment (source target : String) (tempFile : String := "benchOutput.json") :
    CommandElabM Unit := do
  if (source.length, target.length) != (36, 36) then
    logInfo m!"Found\nsource: '{source}'\ntarget: '{target}'\ninstead of two commit hashes."
    return

  -- retrieve the data from the speed-center
  let curlSpeedCenter : IO.Process.SpawnArgs :=
    { cmd := "curl"
      args := #[s!"http://speed.lean-fro.org/mathlib4/api/compare/{source}/to/{target}?all_values=true"] }
  let bench ← IO.Process.run curlSpeedCenter
  IO.FS.writeFile (tempFile ++ ".src") bench

  -- Extract all instruction changes whose magnitude is larger than `threshold`.
  let threshold := s!"{10 ^ 9}"
  let jq1 : IO.Process.SpawnArgs :=
    { cmd := "jq"
      args := #["-r", "--arg", "thr", threshold,
        ".differences | .[] | ($thr|tonumber) as $th |
        select(.dimension.metric == \"instructions\" and ((.diff >= $th) or (.diff <= -$th)))",
        (tempFile ++ ".src")] }
  let firstFilter ← IO.Process.run jq1
  -- we leave `tempFile.src` unchanged and we switch to updating `tempfile`: this is useful for
  -- debugging, as it preserves the original data downloaded from the speed-center
  IO.FS.writeFile tempFile firstFilter
  -- Write these in compact form, in the format suitable for `benchOutput`.
  let jq2 : IO.Process.SpawnArgs :=
    { cmd := "jq"
      args := #["-c", "[{file: .dimension.benchmark, diff: .diff, reldiff: .reldiff}]", tempFile] }
  let secondFilter ← IO.Process.run jq2
  IO.FS.writeFile tempFile secondFilter
  let jq3 : IO.Process.SpawnArgs :=
    { cmd := "jq", args := #["-n", "reduce inputs as $in (null; . + $in)", tempFile] }
  let thirdFilter ← IO.Process.run jq3
  let report ← benchOutput thirdFilter
  IO.println report

end BenchAction

-- run_cmd BenchAction.addBenchSummaryComment "6d0e3011-c591-42e4-9ef6-5c94a9211134" "7a3268cc-0fa1-4bc2-bab4-4fdc6bd381f0"

[Damiano Testa]

If you then replace in the last line (the one that is commented) the "source" and "target" that bench wants, it will print the report.

[Damiano Testa]

Note that it will create files called benchOutput.json with a few variations on your computer.

[Damiano Testa]

If it is useful to run this kind of command by inputting the commits to compare manually, I can restructure the action and expose this function.

[Kim Morrison]

Kim Morrison said:

I have a script that will run the benchmark comparing two arbitrary commits. I'm not at a computer until Monday, but if someone asks again then I'll post it.

Oh, oops, my script relies on admin privileges, sorry.

[Jireh Loreaux]

@Damiano Testa I tried to use the code above, but I didn't succeed. The commits I want to compare are:
14ad97c5b4e4cfe6121add2d07614583fbf8d6ea and d4bfe2bbbe1c94de513d8813c1619953e00e230e

If I substitute these strings directly in your run_cmd line, then I get:

/-
Found
source: '14ad97c5b4e4cfe6121add2d07614583fbf8d6ea'
target: 'd4bfe2bbbe1c94de513d8813c1619953e00e230e'
instead of two commit hashes.
-/
run_cmd BenchAction.addBenchSummaryComment "14ad97c5b4e4cfe6121add2d07614583fbf8d6ea" "d4bfe2bbbe1c94de513d8813c1619953e00e230e"

and if I try to format the commit hashes by inserting dashes and deleting the tails, I get:

/-
process 'jq' exited with code 5
-/
run_cmd BenchAction.addBenchSummaryComment "14ad97c5-b4e4-cfe6-121a-dd2d07614583" "d4bfe2bb-be1c-94de-513d-8813c1619953"

What have I done wrong?

[Damiano Testa]

I have had a similar experience with the commits that you suggested in the "header perf" PR. I am not sure what is going on, because the bot uses that information and succeeds on PRs...

[Damiano Testa]

Let me try to investigate some more. I was also not able to get the URL that the script uses in the other case to work, so there may be an issue with the speed-center in these cases.

[Damiano Testa]

(Btw, I think that it is the hashes with the dashes that should be used.)

[Damiano Testa]

In your case, it seems that at least the target PR was not benchmarked:

WhatsApp Image 2024-11-19 at 21.52.02.jpeg

[Jireh Loreaux]

no, they both were, but I just figured out part of the problem. The hash that the speed center uses is not the commit hash.

[Damiano Testa]

Ah, then I do not know why it is telling me that the target hash in your example is not available...

[Jireh Loreaux]

Here is the first run and the second run

[Matthew Ballard]

http://speed.lean-fro.org/mathlib4/compare/27af5825-fff1-4911-a47e-59dfbed48db3/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=d4bfe2bbbe1c94de513d8813c1619953e00e230e

[Damiano Testa]

Ok, let me investigate.

[Jireh Loreaux]

but

run_cmd BenchAction.addBenchSummaryComment "27af5825-fff1-4911-a47e-59dfbed48db3" "c2b490ed-aca1-4d0b-bdbf-c9d263020915"

still fails for me (I pulled these strings from the URLs in the links above, because they had the correct format of dashes).

[Damiano Testa]

The link that Matt sent has an extra hash2=d4bfe2bbbe1c94de513d8813c1619953e00e230e ending that confuses the script.

[Matthew Ballard]

Screenshot 2024-11-19 at 4.58.44 PM.png
You need to click on the little scales icon and then search for the other commit.

[Jireh Loreaux]

okay, so the answer is that nightly testing essentially does nothing for us on #19046: without nightly testing and with nightly testing

[Matthew Ballard]

You will get multiple hits but hopefully there is only one with whose little scale is not grayed out

[Matthew Ballard]

I think we have to dig into a bad file and step through the instance synthesis. I've run out of time for the day though.

[Damiano Testa]

For the link that did not have the hash2 ending, the script above works and gives

File	Instructions	%
build	+515.897⬝10⁹	(+0.32%)
lint	+106.593⬝10⁹	(+1.48%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings	+69.400⬝10⁹	(+19.32%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward	+42.799⬝10⁹	(+45.87%)
Mathlib.Analysis.Fourier.FourierTransformDeriv	+19.542⬝10⁹	(+4.62%)
Mathlib.MeasureTheory.Group.FundamentalDomain	+10.875⬝10⁹	(+6.96%)
<details><summary>2 files, Instructions +7.0⬝10⁹</summary>

File	Instructions	%
Mathlib.Algebra.Module.LocalizedModule.Basic	+7.708⬝10⁹	(+4.03%)
Mathlib.MeasureTheory.Group.GeometryOfNumbers	+7.294⬝10⁹	(+19.81%)
</details>

<details><summary>3 files, Instructions +5.0⬝10⁹</summary>

File	Instructions	%
Mathlib.Analysis.Convex.Between	+5.586⬝10⁹	(+2.77%)
Mathlib.RingTheory.DedekindDomain.Different	+5.584⬝10⁹	(+2.38%)
Mathlib.Algebra.Module.FinitePresentation	+5.266⬝10⁹	(+3.58%)
</details>

<details><summary>7 files, Instructions +4.0⬝10⁹</summary>

File	Instructions	%
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances	+4.980⬝10⁹	(+1.37%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify	+4.920⬝10⁹	(+5.31%)
Mathlib.Topology.MetricSpace.IsometricSMul	+4.414⬝10⁹	(+8.40%)
Mathlib.RingTheory.TensorProduct.Basic	+4.389⬝10⁹	(+1.37%)
Mathlib.CategoryTheory.Linear.Basic	+4.341⬝10⁹	(+24.77%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict	+4.330⬝10⁹	(+1.77%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order	+4.176⬝10⁹	(+1.70%)
</details>

<details><summary>7 files, Instructions +3.0⬝10⁹</summary>

File	Instructions	%
Mathlib.CategoryTheory.Quotient.Linear	+3.916⬝10⁹	(+21.81%)
Mathlib.Analysis.NormedSpace.BallAction	+3.654⬝10⁹	(+4.90%)
Mathlib.Algebra.Homology.ShortComplex.Linear	+3.567⬝10⁹	(+6.15%)
Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt	+3.448⬝10⁹	(+3.66%)
Mathlib.Analysis.Calculus.ContDiff.Basic	+3.444⬝10⁹	(+0.85%)
Mathlib.RingTheory.Flat.Equalizer	+3.408⬝10⁹	(+1.50%)
Mathlib.Analysis.Calculus.FDeriv.Symmetric	+3.309⬝10⁹	(+2.91%)
</details>

<details><summary>22 files, Instructions +2.0⬝10⁹</summary>

File	Instructions	%
Mathlib.Analysis.Convolution	+2.955⬝10⁹	(+0.71%)
Mathlib.GroupTheory.GroupAction.Blocks	+2.947⬝10⁹	(+5.88%)
Mathlib.MeasureTheory.Measure.Hausdorff	+2.871⬝10⁹	(+3.41%)
Mathlib.Analysis.InnerProductSpace.Adjoint	+2.816⬝10⁹	(+1.27%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear	+2.613⬝10⁹	(+1.51%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group	+2.588⬝10⁹	(+1.35%)
Mathlib.GroupTheory.PushoutI	+2.576⬝10⁹	(+2.84%)
Mathlib.LinearAlgebra.TensorProduct.Tower	+2.487⬝10⁹	(+2.20%)
Mathlib.Algebra.Homology.Linear	+2.313⬝10⁹	(+9.65%)
Mathlib.Topology.Algebra.ConstMulAction	+2.294⬝10⁹	(+5.49%)
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries	+2.272⬝10⁹	(+1.16%)
Mathlib.Analysis.Calculus.FDeriv.Mul	+2.265⬝10⁹	(+0.58%)
Mathlib.Analysis.NormedSpace.Pointwise	+2.217⬝10⁹	(+4.36%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic	+2.176⬝10⁹	(+0.73%)
Mathlib.Analysis.Convex.Combination	+2.167⬝10⁹	(+1.74%)
Mathlib.MeasureTheory.Integral.Bochner	+2.165⬝10⁹	(+1.05%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation	+2.127⬝10⁹	(+2.97%)
Mathlib.RingTheory.RingHom.Locally	+2.116⬝10⁹	(+1.83%)
Mathlib.Algebra.Category.ModuleCat.Algebra	+2.75⬝10⁹	(+14.87%)
Mathlib.MeasureTheory.Group.MeasurableEquiv	+2.13⬝10⁹	(+6.53%)
Mathlib.GroupTheory.Complement	+2.13⬝10⁹	(+3.02%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace	+2.3⬝10⁹	(+1.18%)
</details>

<details><summary>74 files, Instructions +1.0⬝10⁹</summary>

File	Instructions	%
Mathlib.LinearAlgebra.CliffordAlgebra.Equivs	+1.935⬝10⁹	(+2.34%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry	+1.920⬝10⁹	(+0.88%)
Mathlib.MeasureTheory.Group.Action	+1.873⬝10⁹	(+5.42%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Grading	+1.856⬝10⁹	(+3.57%)
Mathlib.RingTheory.DedekindDomain.Ideal	+1.852⬝10⁹	(+0.85%)
Mathlib.Analysis.Calculus.FDeriv.Analytic	+1.842⬝10⁹	(+0.69%)
Mathlib.Algebra.Category.ModuleCat.Basic	+1.822⬝10⁹	(+3.17%)
Mathlib.Analysis.Convex.Side	+1.817⬝10⁹	(+1.97%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit	+1.776⬝10⁹	(+1.80%)
Mathlib.GroupTheory.CosetCover	+1.750⬝10⁹	(+2.32%)
Mathlib.MeasureTheory.Function.LpSeminorm.Basic	+1.748⬝10⁹	(+1.85%)
Mathlib.LinearAlgebra.AffineSpace.AffineMap	+1.712⬝10⁹	(+1.37%)
Mathlib.Analysis.CStarAlgebra.ContinuousMap	+1.705⬝10⁹	(+2.85%)
Mathlib.RingTheory.AdicCompletion.Algebra	+1.678⬝10⁹	(+2.41%)
Mathlib.LinearAlgebra.PiTensorProduct	+1.671⬝10⁹	(+1.05%)
Mathlib.LinearAlgebra.TensorProduct.Basic	+1.670⬝10⁹	(+0.75%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric	+1.627⬝10⁹	(+0.87%)
Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating	+1.605⬝10⁹	(+3.15%)
Mathlib.LinearAlgebra.Multilinear.Basic	+1.602⬝10⁹	(+1.15%)
Mathlib.Topology.ContinuousMap.Algebra	+1.591⬝10⁹	(+1.42%)
Mathlib.GroupTheory.GroupAction.Quotient	+1.499⬝10⁹	(+3.23%)
Mathlib.Algebra.Group.Pointwise.Finset.Basic	+1.498⬝10⁹	(+1.28%)
Mathlib.GroupTheory.HNNExtension	+1.487⬝10⁹	(+1.31%)
Mathlib.Topology.ContinuousMap.Bounded	+1.477⬝10⁹	(+1.12%)
Mathlib.LinearAlgebra.QuadraticForm.Basic	+1.464⬝10⁹	(+0.71%)
Mathlib.Algebra.Order.Module.Defs	+1.464⬝10⁹	(+1.38%)
Mathlib.Analysis.Complex.Conformal	+1.446⬝10⁹	(+5.82%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation	+1.428⬝10⁹	(+0.85%)
Mathlib.AlgebraicGeometry.AffineScheme	+1.426⬝10⁹	(+0.54%)
Mathlib.Analysis.Calculus.ContDiff.Bounds	+1.399⬝10⁹	(+0.92%)
Mathlib.Topology.Algebra.Group.Basic	+1.380⬝10⁹	(+1.20%)
Mathlib.RingTheory.Kaehler.TensorProduct	+1.371⬝10⁹	(+0.71%)
Mathlib.RingTheory.Localization.Free	+1.368⬝10⁹	(+3.73%)
Mathlib.Analysis.Fourier.FourierTransform	+1.366⬝10⁹	(+1.44%)
Mathlib.RingTheory.ClassGroup	+1.365⬝10⁹	(+1.31%)
Mathlib.RingTheory.HahnSeries.Multiplication	+1.361⬝10⁹	(+1.40%)
Mathlib.LinearAlgebra.AffineSpace.AffineSubspace	+1.358⬝10⁹	(+0.91%)
Mathlib.MeasureTheory.Group.Measure	+1.351⬝10⁹	(+1.97%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow	+1.330⬝10⁹	(+0.67%)
Mathlib.MeasureTheory.Group.Arithmetic	+1.314⬝10⁹	(+2.31%)
Mathlib.Algebra.DualNumber	+1.290⬝10⁹	(+2.66%)
Mathlib.RepresentationTheory.Rep	+1.287⬝10⁹	(+1.04%)
Mathlib.Algebra.Group.Action.Defs	+1.287⬝10⁹	(+7.14%)
Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup	+1.264⬝10⁹	(+2.13%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital	+1.258⬝10⁹	(+0.54%)
Mathlib.LinearAlgebra.Semisimple	+1.252⬝10⁹	(+1.15%)
Mathlib.LinearAlgebra.TensorProduct.Graded.External	+1.252⬝10⁹	(+0.77%)
Mathlib.Geometry.Manifold.Instances.Sphere	+1.232⬝10⁹	(+0.75%)
Mathlib.RingTheory.Generators	+1.220⬝10⁹	(+0.85%)
Mathlib.LinearAlgebra.Matrix.SesquilinearForm	+1.211⬝10⁹	(+0.87%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Prod	+1.210⬝10⁹	(+1.61%)
Mathlib.CategoryTheory.Monoidal.Internal.Module	+1.200⬝10⁹	(+0.77%)
Mathlib.Algebra.Module.Torsion	+1.198⬝10⁹	(+1.31%)
Mathlib.Algebra.Module.LocalizedModule.Submodule	+1.196⬝10⁹	(+2.00%)
Mathlib.GroupTheory.Sylow	+1.191⬝10⁹	(+2.10%)
Mathlib.Algebra.TrivSqZeroExt	+1.189⬝10⁹	(+0.87%)
Mathlib.Data.Set.Pointwise.SMul	+1.178⬝10⁹	(+2.39%)
Mathlib.RingTheory.Kaehler.Basic	+1.164⬝10⁹	(+0.31%)
Mathlib.Analysis.Complex.UpperHalfPlane.Basic	+1.155⬝10⁹	(+1.47%)
Mathlib.Algebra.Lie.Weights.Killing	+1.150⬝10⁹	(+0.54%)
Mathlib.Algebra.Order.BigOperators.Expect	+1.149⬝10⁹	(+3.11%)
Mathlib.CategoryTheory.Galois.IsFundamentalgroup	+1.148⬝10⁹	(+4.54%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno	+1.124⬝10⁹	(+0.60%)
Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar	+1.120⬝10⁹	(+0.97%)
Mathlib.RingTheory.HahnSeries.Summable	+1.102⬝10⁹	(+1.53%)
Mathlib.Analysis.Analytic.Basic	+1.100⬝10⁹	(+0.44%)
Mathlib.NumberTheory.NumberField.Embeddings	+1.87⬝10⁹	(+0.86%)
Mathlib.GroupTheory.OreLocalization.Basic	+1.81⬝10⁹	(+1.84%)
Mathlib.LinearAlgebra.Eigenspace.Basic	+1.59⬝10⁹	(+0.77%)
Mathlib.RepresentationTheory.Basic	+1.56⬝10⁹	(+1.74%)
Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits	+1.46⬝10⁹	(+5.24%)
Mathlib.RingTheory.WittVector.Isocrystal	+1.35⬝10⁹	(+1.69%)
Mathlib.Analysis.Analytic.CPolynomial	+1.7⬝10⁹	(+0.71%)
Mathlib.RingTheory.Filtration	+1.7⬝10⁹	(+2.39%)
</details>

File	Instructions	%
Mathlib.LinearAlgebra.Dual	-1.27⬝10⁹	(-0.22%)
Mathlib.RingTheory.FiniteType	-2.716⬝10⁹	(-2.84%)
<details><summary>3 files, Instructions -5.0⬝10⁹</summary>

File	Instructions	%
Mathlib.RingTheory.LittleWedderburn	-4.162⬝10⁹	(-12.43%)
Mathlib.RingTheory.LinearDisjoint	-4.269⬝10⁹	(-2.14%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict	-4.856⬝10⁹	(-3.68%)
</details>

File	Instructions	%
Mathlib.FieldTheory.Galois.Profinite	-6.313⬝10⁹	(-9.97%)
<details><summary>2 files, Instructions -8.0⬝10⁹</summary>

File	Instructions	%
Mathlib.FieldTheory.Relrank	-7.549⬝10⁹	(-2.93%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution	-7.718⬝10⁹	(-4.97%)
</details>

File	Instructions	%
Mathlib.Algebra.Algebra.Subalgebra.Rank	-11.508⬝10⁹	(-10.52%)
Mathlib.Algebra.Category.ModuleCat.Presheaf	-24.941⬝10⁹	(-9.24%)

[Jireh Loreaux]

I've bumped #19046 to the latest Mathlib. It's certainly on my agenda to try and understand the problems, but for the most part they are outside my area of Mathlib, so someone familiar with this might be able to provide more insight. In particular, 3 of the worst offending files all live in Algebra.Category.ModuleCat.

[Jireh Loreaux]

There are also two places that needed a heartbeat bump (unless we find better changes). One was to maxHeartbeats (and it was very slow) and the other was for synthInstance, and it's only just above the threshold.

[Kim Morrison]

I think we need to stop abusing defeq with restrictScalars in PresheafOfModules.

[Junyan Xu]

Oh it's this problem again?

[Jireh Loreaux]

If either of you have a quick fix, please feel free to push to the PR. (although I understand if the defeq abuse runs deeper.)

[Jireh Loreaux]

Matthew Ballard said:

Very interesting. In my mind, we only took a node in the instance graph and expanded it to two nodes joined by a single edge. Am I wrong?

I think the reason it's more costly than this is two-fold:

1. When we need one_smul we need to synthesize MulAction α, but if we also need mul_smul, then we now need to synthesize SemigroupAction, and so we don't get the payoff of having done the search already with the cached results.
2. Same applies for the arguments: in one case we synthesize Monoid α, and in the other we need Semigroup α.

That being said, this seems an unreasonably high price for such a small change.