Principal Ideals #
This file deals with the set of principal ideals of a CommRing R
.
Main definitions and results #
Ideal.isPrincipalSubmonoid
: the submonoid ofIdeal R
formed by the principal ideals ofR
.Ideal.associatesMulEquivIsPrincipal
: theMulEquiv
between the monoid ofAssociates R
and the submonoid of principal ideals ofR
.
The principal ideals of R
form a submonoid of Ideal R
.
Equations
- Ideal.isPrincipalSubmonoid R = { carrier := {I : Ideal R | Submodule.IsPrincipal I}, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
noncomputable def
Ideal.associatesEquivIsPrincipal
(R : Type u_1)
[CommRing R]
[IsDomain R]
:
Associates R ≃ { I : Ideal R // Submodule.IsPrincipal I }
The equivalence between Associates R
and the principal ideals of R
defined by sending the
class of x
to the principal ideal generated by x
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Ideal.associatesEquivIsPrincipal_apply
{R : Type u_1}
[CommRing R]
[IsDomain R]
(x : R)
:
↑((Ideal.associatesEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {x}
@[simp]
theorem
Ideal.associatesEquivIsPrincipal_symm_apply
{R : Type u_1}
[CommRing R]
[IsDomain R]
{I : Ideal R}
(hI : Submodule.IsPrincipal I)
:
(Ideal.associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = Associates.mk (Submodule.IsPrincipal.generator I)
theorem
Ideal.associatesEquivIsPrincipal_mul
{R : Type u_1}
[CommRing R]
[IsDomain R]
(x : Associates R)
(y : Associates R)
:
↑((Ideal.associatesEquivIsPrincipal R) (x * y)) = ↑((Ideal.associatesEquivIsPrincipal R) x) * ↑((Ideal.associatesEquivIsPrincipal R) y)
@[simp]
theorem
Ideal.associatesEquivIsPrincipal_map_zero
{R : Type u_1}
[CommRing R]
[IsDomain R]
:
↑((Ideal.associatesEquivIsPrincipal R) 0) = 0
@[simp]
theorem
Ideal.associatesEquivIsPrincipal_map_one
{R : Type u_1}
[CommRing R]
[IsDomain R]
:
↑((Ideal.associatesEquivIsPrincipal R) 1) = 1
The MulEquiv
version of Ideal.associatesEquivIsPrincipal
.
Equations
- Ideal.associatesMulEquivIsPrincipal R = let __spread.0 := Ideal.associatesEquivIsPrincipal R; { toEquiv := __spread.0, map_mul' := ⋯ }