Principal Ideals

This file deals with the set of principal ideals of a CommRing R.

Main definitions and results

• Ideal.isPrincipalSubmonoid: the submonoid of Ideal R formed by the principal ideals of R.

• Ideal.associatesMulEquivIsPrincipal: the MulEquiv between the monoid of Associates R and the submonoid of principal ideals of R.

def Ideal.isPrincipalSubmonoid (R : Type u_1) [CommRing R] : Submonoid (Ideal R)

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' := ⋯ }

theorem Ideal.mem_isPrincipalSubmonoid_iff {R : Type u_1} [CommRing R] {I : Ideal R} : I ∈ Ideal.isPrincipalSubmonoid R ↔ Submodule.IsPrincipal I

theorem Ideal.span_singleton_mem_isPrincipalSubmonoid {R : Type u_1} [CommRing R] (a : R) : Ideal.span {a} ∈ Ideal.isPrincipalSubmonoid R

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.

@[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

noncomputable def Ideal.associatesMulEquivIsPrincipal (R : Type u_1) [CommRing R] [IsDomain R] : Associates R ≃* ↥(Ideal.isPrincipalSubmonoid R)

The MulEquiv version of Ideal.associatesEquivIsPrincipal.

Equations

• Ideal.associatesMulEquivIsPrincipal R = let __spread.0 := Ideal.associatesEquivIsPrincipal R; { toEquiv := __spread.0, map_mul' := ⋯ }