Ideals over a ring #
This file defines
Ideal R, the type of (left) ideals over a ring
Note that over commutative rings, left ideals and two-sided ideals are equivalent.
Implementation notes #
Support right ideals, and two-sided ideals over non-commutative rings.
The prime ideal is not the entire ring.
If a product lies in the prime ideal, then at least one element lies in the prime ideal.
P of a ring
R is prime if
P ≠ R and
xy ∈ P → x ∈ P ∨ y ∈ P
- out : IsCoatom I
The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.
An ideal is maximal if it is maximal in the collection of proper ideals.
Ideal.isSimpleOrder for the forward direction as an instance when
R is a
This result actually holds for all division semirings, but we lack the predicate to state it.