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.

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

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

def Ideal.isPrincipalNonZeroDivisorsSubmonoid (R : Type u_1) [CommRing R] : Submonoid ↥(nonZeroDivisors (Ideal R))

The non-zero-divisors principal ideals of R form a submonoid of (Ideal 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.

@[simp]

theorem Ideal.associatesEquivIsPrincipal_apply {R : Type u_1} [CommRing R] [IsDomain R] (x : R) : ↑((associatesEquivIsPrincipal R) (Associates.mk x)) = span {x}

@[simp]

theorem Ideal.associatesEquivIsPrincipal_symm_apply {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} (hI : Submodule.IsPrincipal I) : (associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = Associates.mk (Submodule.IsPrincipal.generator I)

theorem Ideal.associatesEquivIsPrincipal_mul {R : Type u_1} [CommRing R] [IsDomain R] (x y : Associates R) : ↑((associatesEquivIsPrincipal R) (x * y)) = ↑((associatesEquivIsPrincipal R) x) * ↑((associatesEquivIsPrincipal R) y)

@[simp]

theorem Ideal.associatesEquivIsPrincipal_map_zero {R : Type u_1} [CommRing R] [IsDomain R] : ↑((associatesEquivIsPrincipal R) 0) = 0

@[simp]

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

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

The MulEquiv version of Ideal.associatesEquivIsPrincipal.

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

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

@[simp]

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

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

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

@[simp]

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

noncomputable def Ideal.associatesNonZeroDivisorsMulEquivIsPrincipal (R : Type u_1) [CommRing R] [IsDomain R] : Associates ↥(nonZeroDivisors R) ≃* ↥(isPrincipalNonZeroDivisorsSubmonoid R)

The MulEquiv version of Ideal.associatesNonZeroDivisorsEquivIsPrincipal.

noncomputable def Ideal.isoBaseOfIsPrincipal {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I] (hI : I ≠ ⊥) : R ≃ₗ[R] ↥I

A nonzero principal ideal in an integral domain R is isomorphic to R as a module. The isomorphism we choose here sends 1 to the generator chosen by Ideal.generator.

@[simp]

theorem Ideal.isoBaseOfIsPrincipal_apply {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I] (hI : I ≠ ⊥) (x : R) : ↑((isoBaseOfIsPrincipal hI) x) = x * Submodule.IsPrincipal.generator I

theorem Ideal.subtype_isoBaseOfIsPrincipal_eq_mul {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} [hprinc : Submodule.IsPrincipal I] (h : I ≠ ⊥) : Submodule.subtype I ∘ₗ ↑(isoBaseOfIsPrincipal h) = (LinearMap.mul R R) (Submodule.IsPrincipal.generator I)