Atoms in order and algebra

Stream: maths

[Aaron Anderson]

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]

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

[Aaron Anderson]

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]

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]

What would be a good name for this predicate?

[Kevin Buzzard]

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

[Aaron Anderson]

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]

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.