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
- ⋯ = ⋯
instance
TwoSidedIdeal.setLike
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
SetLike (TwoSidedIdeal R) R
Equations
- TwoSidedIdeal.setLike = { coe := fun (t : TwoSidedIdeal R) => {r : R | t.ringCon r 0}, coe_injective' := ⋯ }
theorem
TwoSidedIdeal.mem_iff
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
(x : R)
:
theorem
TwoSidedIdeal.rel_iff
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
(x : R)
(y : R)
:
def
TwoSidedIdeal.coeOrderEmbedding
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
TwoSidedIdeal R ↪o Set R
the coercion from two-sided-ideals to sets is an order embedding
Equations
- TwoSidedIdeal.coeOrderEmbedding = { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
@[simp]
theorem
TwoSidedIdeal.coeOrderEmbedding_apply
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
∀ (a : TwoSidedIdeal R), TwoSidedIdeal.coeOrderEmbedding a = ↑a
theorem
TwoSidedIdeal.le_iff
{R : Type u_1}
[NonUnitalNonAssocRing R]
{I : TwoSidedIdeal R}
{J : TwoSidedIdeal R}
:
def
TwoSidedIdeal.orderIsoRingCon
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
TwoSidedIdeal R ≃o RingCon R
Two-sided-ideals corresponds to congruence relations on a ring.
Equations
- TwoSidedIdeal.orderIsoRingCon = { toFun := TwoSidedIdeal.ringCon, invFun := TwoSidedIdeal.mk, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
theorem
TwoSidedIdeal.ringCon_injective
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
Function.Injective TwoSidedIdeal.ringCon
theorem
TwoSidedIdeal.ringCon_le_iff
{R : Type u_1}
[NonUnitalNonAssocRing R]
{I : TwoSidedIdeal R}
{J : TwoSidedIdeal R}
:
theorem
TwoSidedIdeal.ext
{R : Type u_1}
[NonUnitalNonAssocRing R]
{I : TwoSidedIdeal R}
{J : TwoSidedIdeal R}
(h : ∀ (x : R), x ∈ I ↔ x ∈ J)
:
I = J
theorem
TwoSidedIdeal.lt_iff
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
(J : TwoSidedIdeal R)
:
@[simp]
theorem
TwoSidedIdeal.zero_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
0 ∈ I
theorem
TwoSidedIdeal.add_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
{x : R}
{y : R}
(hx : x ∈ I)
(hy : y ∈ I)
:
theorem
TwoSidedIdeal.neg_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
{x : R}
(hx : x ∈ I)
:
Equations
- ⋯ = ⋯
theorem
TwoSidedIdeal.sub_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
{x : R}
{y : R}
(hx : x ∈ I)
(hy : y ∈ I)
:
theorem
TwoSidedIdeal.mul_mem_left
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
(x : R)
(y : R)
(hy : y ∈ I)
:
theorem
TwoSidedIdeal.mul_mem_right
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
(x : R)
(y : R)
(hx : x ∈ I)
:
theorem
TwoSidedIdeal.nsmul_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
{x : R}
(n : ℕ)
(hx : x ∈ I)
:
theorem
TwoSidedIdeal.zsmul_mem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
{x : R}
(n : ℤ)
(hx : x ∈ I)
:
def
TwoSidedIdeal.mk'
{R : Type u_1}
[NonUnitalNonAssocRing R]
(carrier : Set R)
(zero_mem : 0 ∈ carrier)
(add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
(neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
(mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
(mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier)
:
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
- TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right = { ringCon := { r := fun (x y : R) => x - y ∈ carrier, iseqv := ⋯, mul' := ⋯, add' := ⋯ } }
Instances For
@[simp]
theorem
TwoSidedIdeal.mem_mk'
{R : Type u_1}
[NonUnitalNonAssocRing R]
(carrier : Set R)
(zero_mem : 0 ∈ carrier)
(add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
(neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
(mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
(mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier)
(x : R)
:
x ∈ TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier
@[simp]
theorem
TwoSidedIdeal.coe_mk'
{R : Type u_1}
[NonUnitalNonAssocRing R]
(carrier : Set R)
(zero_mem : 0 ∈ carrier)
(add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier)
(neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier)
(mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier)
(mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier)
:
↑(TwoSidedIdeal.mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right) = carrier
instance
TwoSidedIdeal.instSMulMemClass
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
SMulMemClass (TwoSidedIdeal R) R R
Equations
- ⋯ = ⋯
instance
TwoSidedIdeal.instSMulMemClassMulOpposite
{R : Type u_1}
[NonUnitalNonAssocRing R]
:
SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R
Equations
- ⋯ = ⋯
instance
TwoSidedIdeal.instAddSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
Add ↥I
instance
TwoSidedIdeal.instZeroSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
Zero ↥I
Equations
- I.instZeroSubtypeMem = { zero := ⟨0, ⋯⟩ }
instance
TwoSidedIdeal.instSMulNatSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
instance
TwoSidedIdeal.instNegSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
Neg ↥I
instance
TwoSidedIdeal.instSubSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
Sub ↥I
instance
TwoSidedIdeal.instSMulIntSubtypeMem
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
instance
TwoSidedIdeal.addCommGroup
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
AddCommGroup ↥I
Equations
- I.addCommGroup = Function.Injective.addCommGroup (fun (a : ↥I) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
def
TwoSidedIdeal.coeAddMonoidHom
{R : Type u_1}
[NonUnitalNonAssocRing R]
(I : TwoSidedIdeal R)
:
↥I →+ R
The coercion into the ring as a AddMonoidHom
Equations
- I.coeAddMonoidHom = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
Instances For
instance
TwoSidedIdeal.instSMulMulOppositeSubtypeMem
{R : Type u_1}
[Ring R]
(I : TwoSidedIdeal R)
:
Equations
- I.leftModule = Function.Injective.module R I.coeAddMonoidHom ⋯ ⋯
@[simp]
Equations
- I.rightModule = Function.Injective.module Rᵐᵒᵖ I.coeAddMonoidHom ⋯ ⋯
@[simp]
theorem
TwoSidedIdeal.coe_mop_smul
{R : Type u_1}
[Ring R]
(I : TwoSidedIdeal R)
{r : Rᵐᵒᵖ}
{x : ↥I}
:
r • ↑x = ↑x * MulOpposite.unop r
instance
TwoSidedIdeal.instSMulCommClassMulOppositeSubtypeMem
{R : Type u_1}
[Ring R]
(I : TwoSidedIdeal R)
:
SMulCommClass R Rᵐᵒᵖ ↥I
Equations
- ⋯ = ⋯
@[simp]
theorem
TwoSidedIdeal.subtype_apply
{R : Type u_1}
[Ring R]
(I : TwoSidedIdeal R)
(x : ↥I)
:
I.subtype x = ↑x
For any RingCon R
, when we view it as an ideal in Rᵒᵖ
, subtype
is the injective Rᵐᵒᵖ
-linear
map I → Rᵐᵒᵖ
.
Equations
- I.subtypeMop = { toFun := fun (x : ↥I) => MulOpposite.op ↑x, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
TwoSidedIdeal.subtypeMop_apply
{R : Type u_1}
[Ring R]
(I : TwoSidedIdeal R)
(x : ↥I)
:
I.subtypeMop x = MulOpposite.op ↑x