Zulip Chat Archive

Stream: PR reviews

Topic: 4770 smul_comm_class


view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:07):

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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:08):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:10):

And generalize semimodule structure on linear_maps.

view this post on Zulip Heather Macbeth (Oct 24 2020 at 18:21):

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 ?

view this post on Zulip Johan Commelin (Oct 24 2020 at 18:24):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 18:25):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:32):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:34):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:43):

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₂.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:43):

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

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:46):

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

view this post on Zulip Heather Macbeth (Oct 24 2020 at 18:47):

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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:48):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:48):

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.

view this post on Zulip Reid Barton (Oct 24 2020 at 18:48):

Right, I think we want something more like the latter

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:49):

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

view this post on Zulip Heather Macbeth (Oct 24 2020 at 18:50):

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?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:51):

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.

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 18:54):

A Frobenius-linear map is just f:XYf:X\to Y such that f(λx)=λpf(x)f(\lambda x)=\lambda^p f(x). Here RR is a ring of characteristic pp acting on XX and YY, and xxpx\mapsto x^p is hence a ring homomorphism.

view this post on Zulip Reid Barton (Oct 24 2020 at 18:54):

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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:55):

Where bimodule is defined as ...?

view this post on Zulip Reid Barton (Oct 24 2020 at 18:55):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:55):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:56):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:56):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:56):

We can introduce notation for right smul.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 18:57):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:57):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:59):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 18:59):

Kevin Buzzard said:

A Frobenius-linear map is just f:XYf:X\to Y such that f(λx)=λpf(x)f(\lambda x)=\lambda^p f(x). Here RR is a ring of characteristic pp acting on XX and YY, and xxpx\mapsto x^p is hence a ring homomorphism.

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

view this post on Zulip Reid Barton (Oct 24 2020 at 19:00):

and likewise we would have linear_map conj V W?

view this post on Zulip Heather Macbeth (Oct 24 2020 at 19:04):

Reid Barton said:

Kevin Buzzard said:

A Frobenius-linear map is just f:XYf:X\to Y such that f(λx)=λpf(x)f(\lambda x)=\lambda^p f(x). Here RR is a ring of characteristic pp acting on XX and YY, and xxpx\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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:06):

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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:07):

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

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 19:16):

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

view this post on Zulip Heather Macbeth (Oct 24 2020 at 19:17):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:19):

We can think about it both ways

view this post on Zulip Heather Macbeth (Oct 24 2020 at 19:24):

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.

view this post on Zulip Kevin Buzzard (Oct 24 2020 at 19:26):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:58):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:58):

So, we have to choose what comes first.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 19:59):

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₂?

view this post on Zulip Reid Barton (Oct 24 2020 at 20:00):

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

view this post on Zulip Reid Barton (Oct 24 2020 at 20:01):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 20:01):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 20:02):

(where "soon" means "this year")

view this post on Zulip Reid Barton (Oct 24 2020 at 20:18):

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

view this post on Zulip Aaron Anderson (Dec 22 2020 at 21:14):

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?

view this post on Zulip Aaron Anderson (Dec 22 2020 at 21:15):

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

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 22:14):

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.

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:20):

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.

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 22:23):

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.

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:24):

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

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:25):

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

view this post on Zulip Eric Wieser (Dec 22 2020 at 22:59):

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

view this post on Zulip Eric Wieser (Dec 22 2020 at 22:59):

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

view this post on Zulip Eric Wieser (Dec 22 2020 at 23:00):

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

view this post on Zulip Eric Wieser (Dec 22 2020 at 23:01):

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.

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 23:06):

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

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 23:07):

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


Last updated: May 07 2021 at 18:19 UTC