4770 smul_comm_class

Stream: PR reviews

[Yury G. Kudryashov]

In #4770 I suggest we add a typeclass smul_comm_class saying that two actions on the same space commute. I'd like to have some feedback on the idea before I spend time porting existing definitions to this typeclass.

[Yury G. Kudryashov]

@Frédéric Dupuis I think that this class can be used for conjugate semimodules if we regard them as semimodules over opposite complex.

[Yury G. Kudryashov]

And generalize semimodule structure on linear_maps.

[Heather Macbeth]

I don't understand, can you spell out the idea a little more? The conjugate semimodule is defined to be a scalar multiplication of opposite ℂ on the same space, but then how do linear maps work when the first space is over opposite ℂ and the second space is over ℂ?

[Johan Commelin]

Would this also help in representation theory, where the action of G on V and the action of K on V commute?

[Johan Commelin]

Currently we treat representations as modules over monoid_algebra K G but that leads to "ugly" statements

[Yury G. Kudryashov]

We should have an instance generating an action of monoid_algebra K G from the fact that two actions commute.

[Yury G. Kudryashov]

@Heather Macbeth I was thinking about sesqlinear forms, not conjugate linear maps. Let me think about it a bit more.

[Yury G. Kudryashov]

One way to generalize this is to have [has_canonical_ring_hom R S] typeclass with instances has_canonical_ring_hom R R and [algebra R A] : has_canonical_ring_hom R A and do some parts of linear algebra for maps from semimodule R M to semimodule S M₂.

[Yury G. Kudryashov]

with notation M →ₗ[R] M' using R=S.

[Kevin Buzzard]

Sometimes there is more than one "canonical" ring hom from R to S :-(

[Heather Macbeth]

OK, this sounds doable. Even though it would be a huge refactor, at least it's a joint generalization of linear and conjugate-linear maps, rather than a direct duplication of linear-map theory to conjugate-linear-map theory.

[Yury G. Kudryashov]

@Kevin Buzzard Then we can have linear_map (f : R →+* S) M M'

[Reid Barton]

Also, often all of R, S and the ring hom f : R -> S would be variables, and then it will be annoying to stuff f into an instance even to write the statements of lemmas.

[Reid Barton]

Right, I think we want something more like the latter

[Yury G. Kudryashov]

With notation both for the general form and linear_map (ring_hom.id R) M M'.

[Heather Macbeth]

In an earlier discussion about conjugate-linear maps, Johan mentioned Frobenius-linear maps. I don't know anything about them, but are they covered by this construction?

[Reid Barton]

I agree this is a useful notion--in technical mumbo-jumbo we're describing the category of (rings+modules) as a displayed category over the category of rings.

[Kevin Buzzard]

A Frobenius-linear map is just $f:X\to Y$ such that $f(\lambda x)=\lambda^p f(x)$. Here $R$ is a ring of characteristic $p$ acting on $X$ and $Y$, and $x\mapsto x^p$ is hence a ring homomorphism.

[Reid Barton]

About the original PR, I think this notion is useful too, but some things that could be instances of it might better be thought of as bimodules.

[Yury G. Kudryashov]

Where bimodule is defined as ...?

[Reid Barton]

But we don't have right modules yet and thus don't have bimodules either.

[Reid Barton]

Like in the traditional way--a left action of something and a right action of something else, that commute.

[Yury G. Kudryashov]

I suggest that we use [semimodule R M] [semimodule (opposite R) M] [smul_comm_class R (opposite R) M] for bimodules.

[Reid Barton]

I think this sounds pretty miserable... writing things in the wrong order is a pain, and so is opposite

[Yury G. Kudryashov]

We can introduce notation for right smul.

[Yury G. Kudryashov]

Something like a ⋅' b = (op b) ⋅ a.

[Reid Barton]

Yes, something like that might be okay (and then we should have right_submodule R M := submodule (opposite R) M, etc.)

[Reid Barton]

Anyways we should wait until someone really wants right modules/bimodules before doing anything there.

[Reid Barton]

Kevin Buzzard said:

A Frobenius-linear map is just $f:X\to Y$ such that $f(\lambda x)=\lambda^p f(x)$. Here $R$ is a ring of characteristic $p$ acting on $X$ and $Y$, and $x\mapsto x^p$ is hence a ring homomorphism.

So it's a linear_map frobenius X Y, right?

[Reid Barton]

and likewise we would have linear_map conj V W?

[Heather Macbeth]

Reid Barton said:

Kevin Buzzard said:

A Frobenius-linear map is just $f:X\to Y$ such that $f(\lambda x)=\lambda^p f(x)$. Here $R$ is a ring of characteristic $p$ acting on $X$ and $Y$, and $x\mapsto x^p$ is hence a ring homomorphism.

So it's a linear_map frobenius X Y, right?

Reid Barton said:

and likewise we would have linear_map conj V W?

This sounds totally workable, and therefore evidence in favour of Yury's idea.

[Yury G. Kudryashov]

We'll need someone to write a tactic that takes a fact about linear_map f M N and turns it into a fact about linear_map (ring_hom.id R) M N replacing all applications of f with ids and removing S from the arguments. While I understand how to_additive works, it doesn't modify arity of functions etc.

[Yury G. Kudryashov]

(the new theorem should be defeq to the old one, so no need to convert the proof)

[Kevin Buzzard]

Note that we've seen several examples here where R=S but the canonical map isn't the identity.

[Heather Macbeth]

In the conjugation example, I think the map is between opposite ℂ and ℂ, rather than from ℂ to itself?

[Yury G. Kudryashov]

We can think about it both ways

[Heather Macbeth]

There is the following advantage to making it the conjugation homomorphism a map from is_R_or_C to itself (rather than opposite): if I understand correctly, the conjugation will then be defeq to the identity in the case of ℝ, and so a conjugate-linear map over ℝ will, definitionally, be a linear map. This would allow for cleaner statements of some of the results in @Frédéric Dupuis ' PR.

[Kevin Buzzard]

If R=S then an f-linear map will be linear over the subring of R consisting of things fixed by f I guess.

[Yury G. Kudryashov]

Unfortunately, we can't make a symm instance for smul_comm_class in Lean 3.

[Yury G. Kudryashov]

So, we have to choose what comes first.

[Yury G. Kudryashov]

instance [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] :
  has_scalar S (M →ₗ[R] M₂) :=
⟨λ a f, ⟨λ b, a • f b, λ x y, by rw [f.map_add, smul_add],
  λ c x, by simp only [f.map_smul, smul_comm c]⟩⟩

Should it be like this or smul_comm_class S R M₂?

[Reid Barton]

The class is a Prop anyways, so I think there's not much danger in just picking randomly at the use site and providing both orders at the instance definition site

[Reid Barton]

... though with bimodules you won't have this problem :upside_down:

[Yury G. Kudryashov]

I hope we'll see Lean 4 soon, and add symm instance.

[Yury G. Kudryashov]

(where "soon" means "this year")

[Reid Barton]

As a temporary measure we can have a symm lemma and, though it might not actually be worthwhile, a linter which checks that each instance has a symm version

[Aaron Anderson]

Yury G. Kudryashov said:

I suggest that we use [semimodule R M] [semimodule (opposite R) M] [smul_comm_class R (opposite R) M] for bimodules.

smul_comm_class is in mathlib now. Is there a reason (other than time) that I shouldn't make a PR with this definition of bimodule and the other basic API for bimodules that's been discussed?

[Aaron Anderson]

I'd really like to see ideals and two-sided ideals distinguished from each other.

[Yury G. Kudryashov]

Go ahead. I don't know whether we should have a bimodule typeclass that extends three typeclasses, or use these three arguments every time we speak about bimodules. And we need some notation for op a • b (something like b •ᵣ a). If you keep it as a notation (not a def), then you can apply lemmas about smul directly.

[Aaron Anderson]

I ran into trouble getting a bimoduletypeclass that extends all three off the ground, so I'm writing a draft that is just an abbreviation for smul_comm_class. I think defining right modules and bimodules is easy enough, but subbimodules may get kind of weird.

[Yury G. Kudryashov]

You can extend two semimodule classes, have an axiom equivalent to smul_comm_class, and an instances from [bimodule R M] to smul_comm_class R (opposite R) M and smul_comm_class (opposite R) R M. Then you'll be able to apply theorems about smul_comm_class.

[Aaron Anderson]

The problem was with extending two semimodule classes. It didn't work for me, either with or without old_structure_cmd.

[Aaron Anderson]

I've pushed to branch#bimodule, although the API for subbimodule isn't really there yet

[Eric Wieser]

If you define right_semimodule := semimodule (opposite R) M, can you extend right_semimodule without old_structure_cmd?

[Eric Wieser]

Because right now your problem is:

• old_structure_cmd = True: you have two zero_add fields, which have different types
• old_structure_cmd = False: you have two to_semimodule fields, which have different types

[Eric Wieser]

My thinking is maybe you can trick lean into generating one field called to_right_semimodule

[Eric Wieser]

Oh, this is something Reid (I think) told me not to do anyway, for the same reason that semimodule does not extend semiring; you shouldn't extend things that don't use all your type arguments.

[Yury G. Kudryashov]

Sorry, I haven't realized that we're going to have bimodule R S M, not bimodule R M.

[Yury G. Kudryashov]

Yes, bimodule R S M may be an abbreviation (or even a notation) for smul_comm_class R (opposite S) M.