n-torsion or multiplication by n as an additive group hom

Stream: Is there code for X?

[Kevin Buzzard]

Let $A$ be an additive commutative group (for example the points on an elliptic curve) and let $n$ be a natural. I'd like to consider the $n$-torsion subgroup of $A$ either as a term of type Subgroup A or as a group (i.e. a type) in its own right. I guess I could do this if we have the multiplication-by-n map as a group homomorphism $A\to A$. Do we have any of this stuff in mathlib?

[Adam Topaz]

docs#smulAddHom

[Adam Topaz]

I hope we have the right instances for this to "just work" in your case.

[Adam Topaz]

import Mathlib

example (M : Type*) [AddCommGroup M] (n : ℕ) :
    M →+ M :=
  smulAddHom _ _ n

example (M : Type*) [AddCommGroup M] (n : ℕ) (m : M) :
  smulAddHom _ _ n m = n • m := rfl

[Adam Topaz]

Looking forward to some Tate modules :)

[Kevin Buzzard]

Do we have the $\mathbb{Z}/n\Z$-module structure on the kernel (promoted to a type)?

[Adam Topaz]

probably not.

[Adam Topaz]

The whole torsion framework could get a facelift... for example,

def torsion : Submonoid G where
  carrier := { x | IsOfFinOrder x }
...

is how we define the torsion subgroup. I don't see a definition of the $n$-torsion subgroup or anything related.

[Adam Topaz]

Also, roots of unity are defined as follows, again not using anything from torsion

def rootsOfUnity (k : ℕ+) (M : Type*) [CommMonoid M] : Subgroup Mˣ where
  carrier := {ζ | ζ ^ (k : ℕ) = 1}
...

[Kevin Buzzard]

One really nice thing about the whole "5 year" business is that one could imagine that I'll actually get around to making PRs fixing up stuff like this. Do you have an idea about what the general definitions should look like? I'm just running into this stuff now with FLT.

[Adam Topaz]

In the additive case, I think it makes sense to define $M[r]$ whenever $r : R$ and $M$ is an $R$-module

[Adam Topaz]

:light_bulb: WAIT: docs#Submodule.torsionBy

[Kevin Buzzard]

Will I then end up in hell if I try letting r be a natural? There's also the issue of setting it all up with AddCommGroups for Int and AddCommMonoids for Nat, right? Or will they work by magic? Oh -- but they should be to_additive of a multiplicative story which the module thing won't work for, right?

[Adam Topaz]

We also have docs#Module.IsTorsionBySet.module !

[Adam Topaz]

okay, the situation is much better than I had anticipated.

[Adam Topaz]

We should ask @Eric Wieser if he has any ideas on how to make all this work in the multiplicative case.

[Kevin Buzzard]

well in some sense, but in some sense it's much worse: I get a module structure for Z \/ (n) rather than ZMod n, for example.

[Adam Topaz]

Do you absolutely have to use ZMod?

[Kevin Buzzard]

So some stuff will have to be written specifically for integers and then there will maybe be diamonds to deal with.

[Kevin Buzzard]

Do I have to use ZMod? I don't really know yet. I want to set up deformation theory for mod p Galois reps but I haven't yet thought hard about what that will look like -- right now I just want to talk about the $p$-torsion in the Frey curve and say that it's 2-dimensioal.

[Adam Topaz]

I would imagine that working with \Z / (p^n) would actually be easier for deformations, given the general form of Schlessinger's criterion.

[Adam Topaz]

OTOH, we would have to formulate alternatives to things like docs#PadicInt.lift in terms of quotients of $\Z$ instead of ZMod.

[Adam Topaz]

Besides, IMO docs#ZMod.castHom can be a pain to work with sometimes.

[Kevin Buzzard]

I've only just started thinking about this stuff and I haven't started thinking about Schlessinger etc. Do you think this would be troublesome:

def ZMod.module (A : Type*) [AddCommGroup A] (n : ℕ) (hn : ∀ a : A, n • a = 0) :
    Module (ZMod n) A :=
  sorry

I just want to say that something is 2-dimensional!

[Adam Topaz]

if you just want to say it's two dimensional as a free module, you can just state that there exists some isomorphism as a $\Z$-module with $(\Z/n)^2$ without even requiring the $\Z/n$-module instance.

[Kevin Buzzard]

yeah. I just felt that "finrank (ZMod p) V = 2" was a much snappier way of saying this. Maybe I'll do what you suggest for now though.

[Eric Wieser]

Kevin Buzzard said:

Do you think this would be troublesome:

def ZMod.module (A : Type*) [AddCommGroup A] (n : ℕ) (hn : ∀ a : A, n • a = 0) :
    Module (ZMod n) A :=
  sorry

I just want to say that something is 2-dimensional!

A safer bet would be to assume Module (Zmod n) A where you need it I think

[Kevin Buzzard]

Wait -- what Adam suggested doesn't work :-( Almost immediately after defining it, I want to talk about whether E[p] is irreducible or not, so I need something like docs#Representation which needs a ground ring.

[Adam Topaz]

why can't you take the ground ring to be $\Z$?

[Antoine Chambert-Loir]

docs#ZMod.commRing

[Antoine Chambert-Loir]

But when you'll work with elliptic curves with complex multiplication, or higher stuff, you'll wish to have the endomorphism of the curve act on the Tate module. So today's gain will be tomorrow's pain.

[Junyan Xu]

There is docs#AddCommMonoid.zmodModule (upstreamed from PFR). But I agree with Adam that Z/nZ has better API than ZMod n.

[Kevin Buzzard]

How do I say nZ?

[David Ang]

I have a bunch of definitions for A[n] (.ker), nA (.range), A/nA, and A/A[n] (which is isomorphic to nA) that I'm developing locally using DistribMulAction.toAddMonoidHom and zpowGroupHom (because there's no MulDistribMulAction.toMonoidHom), which includes the associated maps (e.g. A[n] -> A'[n] given A -> A') and their images, the DistribMulAction by a monoid and their invariant subgroups, and some Galois theory for E(K)[n].

[Kevin Buzzard]

Can you start PRing this stuff?

[David Ang]

Sure, I’ll work on them this week

[David Ang]

I don’t have A[n] as a representation currently though

[Eric Wieser]

Kevin Buzzard said:

How do I say nZ?

docs#AddSubgroup.zmultiples

[Eric Wieser]

Or AddCircle n for Z/nZ

[Kevin Buzzard]

I would hope that the latter doesn't have a ring structure

[Kevin Buzzard]

And zmultiples is no good, I want the ideal

[Kevin Buzzard]

The answer looks like it's quite a mouthful compared to ZMod p

[Eric Wieser]

Kevin Buzzard said:

And zmultiples is no good, I want the ideal

.toIntSubmodule will give you that

[Eric Wieser]

Though that's probably an argument that Ideal.zmultiples should exist

[Eric Wieser]

Kevin Buzzard said:

I would hope that the latter doesn't have a ring structure

With suitable assumptions it seems reasonable for it to (perhaps a euclidean domain is right?)

[Kevin Buzzard]

$\Z[i]$ is a Euclidean domain and $p\Z$ isn't an ideal so the quotient won't naturally be a ring.

[Kevin Buzzard]

But the point is that this is some topological additive group construction and should have nothing to do with what I'm doing

[Eric Wieser]

Ah, I guess maybe the key thing here is that toIntSubmodule doesn't generalize very well, and so the instance would only exist for Int (and Nat if we did everything again for semirings)

[Eric Wieser]

From my perspective, the fact that "addcircle" is topological is a (pragmatic) accident; the definition of (𝕜 ⧸ AddSubgroup.zmultiples p) doesn't use the topology at all

[Kevin Buzzard]

it just has a completely different semantic meaning from what I'm trying to do, that's my concern. It's designed to be a topological additive group and the name indicates this. I am slightly stunned that people are suggesting anything other than ZMod p for the integers mod p -- that's exactly why we made that type. If there's more API for other things then my instinct is that the fix is to write more API for ZMod p.

[Eric Wieser]

I think a lot of the time we give answers to "what might be the shortest path to do X today" and not necessarily "what is the 'right' path to do X after building more API".

[Eric Wieser]

The needs of a student on a 3 month project are rather different than those of someone with a 5 year grant :)

[Kevin Buzzard]

OK nice :-) I think I'll blunder on with ZMod p and the hints above for torsion, and we'll see what happens :-)

[Eric Rodriguez]

I mean, my understanding for why we have ZMod is that if we used ideals we have very little hope of doing anything computational with it

[Adam Topaz]

Should we make a IsZMod n class?

[Adam Topaz]

Eric Rodriguez said:

I mean, my understanding for why we have ZMod is that if we used ideals we have very little hope of doing anything computational with it

I dont think this is true.

[Adam Topaz]

Namely the quotient by an ideal is still just a quotient. So maps from the quotient are still computable and in fact maps from quotients of Z will compile to maps from Z

[Eric Wieser]

I think the argument goes that Zmod is better computationally, in the same way that we don't implement Rat or Int with a quotient

[Eric Wieser]

Though I guess that's kind of irrelevant since both have native implementations behind the scenes anyway

[Adam Topaz]

Fair enough. I still think there is a good argument for an IsZMod class. ZMod p $\Z/p$ and $\Z_p/p$ are all useful in different contexts

[Kevin Buzzard]

The nice thing about having a class is that these rings have no automorphisms

[Junyan Xu]

Kevin Buzzard said:

How do I say nZ?

There's a notation R ∙ v for Submodule.span R {v}, so Ideal.span {n} can be written ℤ • n.

[Edward van de Meent]

(deleted)

[Edward van de Meent]

you might maybe also try this:

import Mathlib.Algebra.Algebra.Operations

variable (n:ℕ) (R:Type*) [Semiring R]

#check (n • (⊤:Ideal R))
#check (n • (⊤:Ideal ℤ))

i believe this notion of multiplication might be (close to) what leads to the notation $n\Z$ in the first place, although right now, this seems to only work for natural numbers n, via AddMonoid.toNatSMul : SMul ℕ (Ideal R) rather than via something like Submodule.toSMulSubModule :SMul R (Submodule R M)(which i think doesn't exist? not sure tho).

[Peiran Wu]

I have some relevant code from an ongoing project. I've opened a PR #11742 containing basically the following.

variable (A : Type*) [AddCommGroup A] (n : ℕ)

def torsionBy := (Submodule.torsionBy ℤ A n).toAddSubgroup

instance moduleZModTorsionBy [Fact (1 < n)] : Module (ZMod n) (torsionBy A n) := sorry

I could also prove that this definition of torsionBy A n is the same as (DistribMulAction.toAddMonoidHom A n).ker and so on, if that's deemed useful.