## Stream: maths

### Topic: Atoms in order and algebra

#### Aaron Anderson (Dec 20 2020 at 19:00):

I'd like to define the predicateis_atom in an order_bot, and is_coatom in an order_top, where is_atom means that an element is not bot but has nothing else below it, and conversely for is_coatom.

#### Aaron Anderson (Dec 20 2020 at 19:01):

These happen also to be the definitions of minimal and maximal submodules/ideals.

#### Aaron Anderson (Dec 20 2020 at 19:02):

I'd then like to rephrase ideal.is_maximal to be in terms of is_coatom. I'm guessing the correct way to do that would be with an abbreviation, so we keep the term ideal.is_maximal, or at least submodule.is_maximal?

#### Aaron Anderson (Dec 20 2020 at 19:04):

Also, I'd like to define a predicate (probably a class) on bounded_lattices, indicating that there are only two elements. This would be equivalent to is_atom top or is_coatom bot. Then this could be used to describe simple modules and several other kind of "simple" objects in algebra.

#### Aaron Anderson (Dec 20 2020 at 19:04):

What would be a good name for this predicate?

#### Kevin Buzzard (Dec 20 2020 at 19:07):

is_simple? That's what it's called in group theory.

#### Aaron Anderson (Dec 20 2020 at 19:09):

I guess one approach might even be to define it as having exactly two distinct elements... in which case it'd live near things like nontrivial and unique in the library

#### Aaron Anderson (Dec 20 2020 at 19:09):

but I'm not sure how useful that is elsewhere, so I'd be fine with just defining is_simple on bounded lattices, or really something simultaneously extending has_bot and has_top.

Last updated: May 11 2021 at 16:22 UTC