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.isPrincipalNonZeroDivisorSubmonoid: the submonoid of (Ideal R)⁰ formed by the non-zero-divisors principal ideals of R.

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

• Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal: the MulEquiv between the monoid of Associates R⁰ and the submonoid of non-zero-divisors 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

def Ideal.isPrincipalNonZeroDivisorsSubmonoid (R : Type u_1) [CommRing R] : Submonoid { x : Ideal R // x ∈ nonZeroDivisors (Ideal R) }

The non-zero-divisors principal ideals of R form a submonoid of (Ideal R)⁰.

Equations

• Ideal.isPrincipalNonZeroDivisorsSubmonoid R = { carrier := {I : { x : Ideal R // x ∈ nonZeroDivisors (Ideal R) } | Submodule.IsPrincipal ↑I}, mul_mem' := ⋯, one_mem' := ⋯ }

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 ≃* { x : Ideal R // x ∈ Ideal.isPrincipalSubmonoid R }

The MulEquiv version of Ideal.associatesEquivIsPrincipal.

Equations

• Ideal.associatesMulEquivIsPrincipal R = { toEquiv := Ideal.associatesEquivIsPrincipal R, map_mul' := ⋯ }

noncomputable def Ideal.associatesNonZeroDivisorsEquivIsPrincipal (R : Type u_1) [CommRing R] [IsDomain R] : Associates { x : R // x ∈ nonZeroDivisors R } ≃ { I : { x : Ideal R // x ∈ nonZeroDivisors (Ideal R) } // Submodule.IsPrincipal ↑I }

A version of Ideal.associatesEquivIsPrincipal for non-zero-divisors generators.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply {R : Type u_1} [CommRing R] [IsDomain R] (x : { x : R // x ∈ nonZeroDivisors R }) : ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {↑x}

theorem Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe {R : Type u_1} [CommRing R] [IsDomain R] (x : Associates { x : R // x ∈ nonZeroDivisors R }) : ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) = ↑((Ideal.associatesEquivIsPrincipal R) ↑(associatesNonZeroDivisorsEquiv.symm x))

theorem Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul {R : Type u_1} [CommRing R] [IsDomain R] (x : Associates { x : R // x ∈ nonZeroDivisors R }) (y : Associates { x : R // x ∈ nonZeroDivisors R }) : ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) = ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) * ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) y)

@[simp]

theorem Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one {R : Type u_1} [CommRing R] [IsDomain R] : ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) 1) = 1

noncomputable def Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal (R : Type u_1) [CommRing R] [IsDomain R] : Associates { x : R // x ∈ nonZeroDivisors R } ≃* { x : { x : Ideal R // x ∈ nonZeroDivisors (Ideal R) } // x ∈ Ideal.isPrincipalNonZeroDivisorsSubmonoid R }

The MulEquiv version of Ideal.associatesNonZeroDivisorsEquivIsPrincipal.

Equations

• Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal R = { toEquiv := Ideal.associatesNonZeroDivisorsEquivIsPrincipal R, map_mul' := ⋯ }