is_atomistic submodule

Stream: Is there code for X?

[Adam Topaz]

Do we have the following?

import linear_algebra.basic
import order.atoms

variables {K M : Type*} [division_ring K] [add_comm_group M] [module K M]

example : is_atomistic (submodule K M) :=
sorry

(Ping @Yaël Dillies )

I only really care about fields, but I think this should be true for division rings as well?

[Yaël Dillies]

It seems like we have no concrete instance of is_atomistic! That would be great to have.

[Yaël Dillies]

but actually we do have it: docs#module.submodule.is_complemented

[Adam Topaz]

Aha! So one could use docs#is_atomistic_of_is_complemented

[Adam Topaz]

Yaël Dillies said:

but actually we do have it: docs#module.submodule.is_complemented

Over a field...

[Adam Topaz]

In any case, it would be useful to have a characterization of the atoms of submodule K V

[Adam Topaz]

Ping @Michael Blyth

[Yaël Dillies]

#10865 might help

[Alex J. Best]

Adam Topaz said:

Yaël Dillies said:

but actually we do have it: docs#module.submodule.is_complemented

Over a field...

Edit: I am wrong and can't read errors

[Adam Topaz]

Is there some simple way to get the relationship between the atoms of set and the atoms of submodule via spans?

[Adam Topaz]

@Alex J. Best this requires field as well docs#submodule.exists_is_compl

[Adam Topaz]

But it should be generalizable

[Adam Topaz]

e.g. docs#basis.exists_basis already uses division rings, and that's the key IMO