Two Sided Ideals #
In this file, for any Ring R
, we reinterpret I : RingCon R
as a two-sided-ideal of a ring.
Main definitions and results #
TwoSidedIdeal
: For anyNonUnitalNonAssocRing R
,TwoSidedIdeal R
is a wrapper aroundRingCon R
.TwoSidedIdeal.setLike
: EveryI : TwoSidedIdeal R
can be interpreted as a set ofR
wherex ∈ I
if and only ifI.ringCon x 0
.TwoSidedIdeal.addCommGroup
: EveryI : TwoSidedIdeal R
is an abelian group.
A two-sided ideal of a ring R
is a subset of R
that contains 0
and is closed under addition,
negation, and absorbs multiplication on both sides.
- ringCon : RingCon R
every two-sided-ideal is induced by a congruence relation on the ring.
Instances For
Equations
the coercion from two-sided-ideals to sets is an order embedding
Equations
Instances For
Two-sided-ideals corresponds to congruence relations on a ring.
Equations
Instances For
The "set-theoretic-way" of constructing a two-sided ideal by providing:
- the underlying set
S
; - a proof that
0 ∈ S
; - a proof that
x + y ∈ S
ifx ∈ S
andy ∈ S
; - a proof that
-x ∈ S
ifx ∈ S
; - a proof that
x * y ∈ S
ify ∈ S
; - a proof that
x * y ∈ S
ifx ∈ S
.
Equations
Instances For
Equations
Equations
Equations
Equations
Equations
Equations
Equations
The coercion into the ring as a AddMonoidHom
Equations
Instances For
If I
is a two-sided ideal of R
, then {op x | x ∈ I}
is a two-sided ideal in Rᵐᵒᵖ
.
Equations
Instances For
If I
is a two-sided ideal of Rᵐᵒᵖ
, then {x.unop | x ∈ I}
is a two-sided ideal in R
.
Equations
Instances For
Two-sided-ideals of A
and that of Aᵒᵖ
corresponds bijectively to each other.