Ideals over a ring #
This file contains an assortment of definitions and results for Ideal R
,
the type of (left) ideals over a ring R
.
Note that over commutative rings, left ideals and two-sided ideals are equivalent.
Implementation notes #
Ideal R
is implemented using Submodule R R
, where •
is interpreted as *
.
TODO #
Support right ideals, and two-sided ideals over non-commutative rings.
A bijection between (left) ideals of a division ring and {0, 1}
, sending ⊥
to 0
and ⊤
to 1
.
Equations
Instances For
Ideals of a DivisionSemiring
are a simple order. Thanks to the way abbreviations work,
this automatically gives an IsSimpleModule K
instance.
Also see Ideal.isSimpleOrder
for the forward direction as an instance when R
is a
division (semi)ring.
This result actually holds for all division semirings, but we lack the predicate to state it.
When a ring is not a field, the maximal ideals are nontrivial.