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.isPrincipalNonZeroDivisorsSubmonoid: 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.spanSubmonoid {R : Type u_1} [CommRing R] (S : Submonoid R) : Submonoid (Ideal R)

The principal ideals generated by an element of a submonoid S of R form a submonoid of Ideal R.

Equations

• Ideal.spanSubmonoid S = { carrier := Set.range fun (x : ↥S) => Ideal.span {↑x}, mul_mem' := ⋯, one_mem' := ⋯ }

theorem Ideal.mem_spanSubmonoid_iff {R : Type u_1} [CommRing R] (S : Submonoid R) {I : Ideal R} : I ∈ spanSubmonoid S ↔ ∃ (x : ↥S), I = span {↑x}

theorem Ideal.span_singleton_mem_spanSubmonoid {R : Type u_1} [CommRing R] {S : Submonoid R} {a : R} (ha : a ∈ S) : span {a} ∈ spanSubmonoid S

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 ∈ isPrincipalSubmonoid R ↔ Submodule.IsPrincipal I

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

theorem Ideal.spanSubmonoid_le_isPrincipalSubmonoid {R : Type u_1} [CommRing R] (S : Submonoid R) : spanSubmonoid S ≤ isPrincipalSubmonoid R

@[simp]

theorem Ideal.spanSubmonoid_top {R : Type u_1} [CommRing R] : spanSubmonoid ⊤ = 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)⁰.

Equations

• Ideal.isPrincipalNonZeroDivisorsSubmonoid R = { carrier := {I : ↥(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) : ↑((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.

Equations

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

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.

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 : ↥(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.

Equations

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

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.

Equations

• Ideal.isoBaseOfIsPrincipal hI = (LinearEquiv.toSpanNonzeroSingleton R R (Submodule.IsPrincipal.generator I) ⋯).trans (LinearEquiv.ofEq (R ∙ Submodule.IsPrincipal.generator I) I ⋯)

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