Maximal submodule

Stream: new members

[Haruhisa Enomoto]

I'm now defining the Jacobson radical of a (sub)module related to #13862, which is the intersection of all maximal submodules (containing a given submodule).
For ideal.jacobson, the definition uses the typeclass ideal.is_maximal. So if we want to generalize it to modules, maybe we want a new typeclass submodule.is_maximal, but we don't need it at least for defining the Jacobson radical (because a submodule N is maximal if is_coatom N is true).
I'm not sure whether we need submodule.is_maximal, and if so, also I can't see how this should be compatible with the already defined class ideal.is_maximal. Maybe if we define submodule.is_maximal, then for I : ideal R one can use is_maximal I since ideal R is defined to be submodule R R, so ideal.is_maximal will not be needed.

[Julian Külshammer]

In my opinion we should have both (maybe defined in terms of each other, so defining submodule.is_maximal N as is_coatom N, but then defininig ideal.is_maximal I as submodule.is_maximal I? Both concepts are widely used and some people will get confused seeing is_coatom instead.

[Haruhisa Enomoto]

I tried that, namely, define the typeclass submodule.is_maximal and put something like @[class] def ideal.is_maximal := submodule.is_maximal, but I got an ambiguity error for I : ideal R:

ambiguous overload, possible interpretations
  I.is_maximal
  submodule.is_maximal I

so problem is that is_maximal I has two interpretations, submodule.is_maximal I and ideal.is_maximal I, but of course they are equal (in some sense). How can I avoid it?

[Yaël Dillies]

Why are you even defining ideal.is_maximal in the first place? ideal is a thin wrapper around submodule, so you can use submodule.is_maximal directly.

[Haruhisa Enomoto]

I think we want ideal.is_maximal when using e.g. ideal.is_maximal.is_prime and dot notation. If we have h : is_maximal I for I : ideal R, some proofs in mathlib use the notation h.is_prime, but for this to work we need ideal.is_maximal.

[Yaël Dillies]

Well, you can rename ideal.is_maximal.is_prime to submodule.is_maximal.is_prime.

[Haruhisa Enomoto]

That renaming looks a little strange to me, because it seems to claim "submodule which is maximal is prime", but "is_prime" is only defined for ideals. Is it OK?

[Yaël Dillies]

This is not such a problem. Allowing dot notation usually takes priority over strict semantical meaning, because it is so nice having it.