# Zulip Chat Archive

## Stream: new members

### Topic: Maximal submodule

#### Haruhisa Enomoto (May 31 2022 at 02:12):

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 (May 31 2022 at 05:45):

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 (May 31 2022 at 10:52):

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 (May 31 2022 at 10:54):

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 (May 31 2022 at 11:09):

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 (May 31 2022 at 11:15):

Well, you can rename `ideal.is_maximal.is_prime`

to `submodule.is_maximal.is_prime`

.

#### Haruhisa Enomoto (Jun 01 2022 at 01:11):

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 (Jun 01 2022 at 07:32):

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

Last updated: Dec 20 2023 at 11:08 UTC