Zulip Chat Archive

Stream: general

Topic: loogling for linear maps

Kevin Buzzard (Jun 13 2024 at 20:30):

@loogle ?A -> ?M →ₗ[?A] ?M

loogle (Jun 13 2024 at 20:30):

Failure! Bot is unavailable

Kevin Buzzard (Jun 13 2024 at 20:31):

Web error is

(deterministic) timeout at `isDefEq`, maximum number of heartbeats (200000) has been reached
use `set_option maxHeartbeats <num>` to set the limit
use `set_option diagnostics true` to get diagnostic information

Is that a bad query? I'm looking for the $A$ -linear map $M\to M$ defined by $m\mapsto a\cdot m$ for a given $a\in A$ (here $M$ is an $A$ -module).

Eric Wieser (Jun 13 2024 at 20:33):

docs#Algebra.lsmul ?

Eric Wieser (Jun 13 2024 at 20:33):

Though docs#DistribMulAction.toLinearMap may be enough

Kevin Buzzard (Jun 14 2024 at 07:55):

Thanks, this is enough. What about (again $A$ a commutative ring and $M$ an $A$ -module) the $A$ -linear map $A\to M$ given by $a\mapsto a\cdot m$ for some given $m\in M$ ? (there seems to be no rsmulor smulr in mathlib)

Kevin Buzzard (Jun 14 2024 at 07:57):

@loogle ?M -> ?A →ₗ[?A] ?M

loogle (Jun 14 2024 at 07:57):

Failure! Bot is unavailable

Kevin Buzzard (Jun 14 2024 at 07:58):

@loogle ?A →ₗ[?B] ?C →ₗ[?D] ?E

loogle (Jun 14 2024 at 07:59):

Failure! Bot is unavailable

Joachim Breitner (Jun 14 2024 at 08:00):

Very generic queries can make the bot crash, this is unfortunately well known. It may work better if you throw in some constants, like Module, to restrict the search.

Also, everytime it crashes it takes a minute or so to start again :-/

Joachim Breitner (Jun 14 2024 at 08:01):

Hmm, but yes, for this query it’s really hard to work with constants to narrow down the search

Kevin Buzzard (Jun 14 2024 at 08:01):

Oh sorry! I had no idea I was causing trouble. I don't know how to add typeclass inference parameters. I had assumed that the →ₗ[?B] was doing this for me: for that to even make sense we need that ?A is a ?B-module so I thought that this would be quickly inferred.

Joachim Breitner (Jun 14 2024 at 08:02):

Here is a query that is more general than what you want, but specific enough to make loogle not crash, and yields an acceptable number of results (11)
@loogle |- ?A →ₗ[?A] _

loogle (Jun 14 2024 at 08:02):

:search: Module.compHom.toLinearMap, Algebra.linearMap, and 9 more

Kevin Buzzard (Jun 14 2024 at 08:02):

For the query to even typecheck we need something like : ?A is a ?B-module and both ?C and ?E are ?D-modules.

Joachim Breitner (Jun 14 2024 at 08:04):

You are not causing trouble, loogle is causing trouble.

I don’t know exactly why your query is so expensive. Maybe withReducible isDefEq still isn’t as fast as I would like it to be. Maybe I need a matchesPattern that doesn’t reduce, and works purely syntactically, to make loogle more reliable here. isDefEq is just too dangerous

Joachim Breitner (Jun 14 2024 at 08:06):

The benefit of a query like AddCommMonoid, Module, LinearMap is that it is much faster and more reliable: There is no unification happening, just checking which constants are mentioned. In your particular case it’s too non-specific though, and thus not helpful.

Joachim Breitner (Jun 14 2024 at 08:07):

The 11-result-query points to LinearMap.lsmul (so some success), and I’d expect that that file would also contain the other direction if it existed.

Kevin Buzzard (Jun 14 2024 at 08:09):

My real world problem here is that I have undergraduates in Bonn constructing random linear maps and giving them names, and people like Eric (see example above) have put in these hugely general constructions which are almost always in far more generality than you need, because you usually only want A-modules but Eric has done something more general where there's some other ring R and everything is an R-module etc etc. There are too many of these maps like docs#Algebra.lsmul for me to remember, and when I see student code like

/-- Scalar multiplication in the first variable as a linear map. -/
noncomputable def LinearMap.smul₁ (M : Type*) [AddCommGroup M] [Module A M] (m : M):
    A →ₗ[A] M where
  toFun a := a • m
  map_add' := by simp [add_smul]
  map_smul' r n := by simp [mul_smul]

and

noncomputable def LinearMap.prodfst (M N : Type*) [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] :
    M × N →ₗ[A] M where
  toFun := Prod.fst
  map_add' := by simp
  map_smul' r n := by simp

my first thought is "do we have that already?" and my second thought is "how do I check?"

Kevin Buzzard (Jun 14 2024 at 08:10):

Of course exact? is quick to suggest 0, so I can't use that trick.

Joachim Breitner (Jun 14 2024 at 08:11):

Yeah, that’s not trivial; Loogle doesn't take the type class hierarchy into account (yet), and struggles with some pattern queries. I wish I could offer something better