More operations on fractional ideals

Main definitions

• map is the pushforward of a fractional ideal along an algebra morphism

Let K be the localization of R at R⁰ = R \ {0} (i.e. the field of fractions).

• FractionalIdeal R⁰ K is the type of fractional ideals in the field of fractions
• Div (FractionalIdeal R⁰ K) instance: the ideal quotient I / J (typically written $I : J$, but a : operator cannot be defined)

Main statement

• isNoetherian states that every fractional ideal of a Noetherian integral domain is Noetherian

References

• https://en.wikipedia.org/wiki/Fractional_ideal

Tags

fractional ideal, fractional ideals, invertible ideal

theorem IsFractional.map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') {I : Submodule R P} : IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)

def FractionalIdeal.map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : FractionalIdeal S P → FractionalIdeal S P'

I.map g is the pushforward of the fractional ideal I along the algebra morphism g

@[simp]

theorem FractionalIdeal.coe_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : FractionalIdeal S P) : ↑(map g I) = Submodule.map g.toLinearMap ↑I

@[simp]

theorem FractionalIdeal.mem_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {I : FractionalIdeal S P} {g : P →ₐ[R] P'} {y : P'} : y ∈ map g I ↔ ∃ x ∈ I, g x = y

@[simp]

theorem FractionalIdeal.map_id {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : map (AlgHom.id R P) I = I

@[simp]

theorem FractionalIdeal.map_comp {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {P'' : Type u_4} [CommRing P''] [Algebra R P''] (I : FractionalIdeal S P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P'') : map (g'.comp g) I = map g' (map g I)

@[simp]

theorem FractionalIdeal.map_coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : Ideal R) : map g ↑I = ↑I

@[simp]

theorem FractionalIdeal.map_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : map g 1 = 1

@[simp]

theorem FractionalIdeal.map_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : map g 0 = 0

@[simp]

theorem FractionalIdeal.map_add {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I J : FractionalIdeal S P) (g : P →ₐ[R] P') : map g (I + J) = map g I + map g J

@[simp]

theorem FractionalIdeal.map_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I J : FractionalIdeal S P) (g : P →ₐ[R] P') : map g (I * J) = map g I * map g J

@[simp]

theorem FractionalIdeal.map_map_symm {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P) (g : P ≃ₐ[R] P') : map (↑g.symm) (map (↑g) I) = I

@[simp]

theorem FractionalIdeal.map_symm_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P') (g : P ≃ₐ[R] P') : map (↑g) (map (↑g.symm) I) = I

theorem FractionalIdeal.map_mem_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {f : P →ₐ[R] P'} (h : Function.Injective ⇑f) {x : P} {I : FractionalIdeal S P} : f x ∈ map f I ↔ x ∈ I

theorem FractionalIdeal.map_injective {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (f : P →ₐ[R] P') (h : Function.Injective ⇑f) : Function.Injective (map f)

def FractionalIdeal.mapEquiv {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : FractionalIdeal S P ≃+* FractionalIdeal S P'

If g is an equivalence, map g is an isomorphism

@[simp]

theorem FractionalIdeal.coeFun_mapEquiv {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : ⇑(mapEquiv g) = map ↑g

@[simp]

theorem FractionalIdeal.mapEquiv_apply {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') (I : FractionalIdeal S P) : (mapEquiv g) I = map (↑g) I

@[simp]

theorem FractionalIdeal.mapEquiv_symm {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : (mapEquiv g).symm = mapEquiv g.symm

@[simp]

theorem FractionalIdeal.mapEquiv_refl {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P)

theorem FractionalIdeal.isFractional_span_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {s : Set P} : IsFractional S (Submodule.span R s) ↔ ∃ a ∈ S, ∀ b ∈ s, IsLocalization.IsInteger R (a • b)

theorem FractionalIdeal.isFractional_of_fg {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {I : Submodule R P} (hI : I.FG) : IsFractional S I

theorem FractionalIdeal.mem_span_mul_finite_of_mem_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I J : FractionalIdeal S P} {x : P} (hx : x ∈ I * J) : ∃ (T : Finset P) (T' : Finset P), ↑T ⊆ ↑I ∧ ↑T' ⊆ ↑J ∧ x ∈ Submodule.span R (↑T * ↑T')

theorem Units.submodule_isFractional {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (I : (Submodule R P)ˣ) : IsFractional S ↑I

def FractionalIdeal.unitsMulEquivSubmodule {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] : (FractionalIdeal S P)ˣ ≃* (Submodule R P)ˣ

If P is a localization of R, invertible R-submodules of P are all fractional (expressed as an isomorphism of groups).

theorem FractionalIdeal.coeIdeal_fg {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] (inj : Function.Injective ⇑(algebraMap R P)) (I : Ideal R) : (↑↑I).FG ↔ I.FG

theorem FractionalIdeal.fg_unit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : (FractionalIdeal S P)ˣ) : (↑↑I).FG

theorem FractionalIdeal.fg_of_isUnit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (h : IsUnit I) : (↑I).FG

theorem Ideal.fg_of_isUnit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (inj : Function.Injective ⇑(algebraMap R P)) (I : Ideal R) (h : IsUnit ↑I) : I.FG

theorem FractionalIdeal.canonicalEquiv_def {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] : canonicalEquiv S P P' = mapEquiv (let __src := IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯; { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })

@[irreducible]

noncomputable def FractionalIdeal.canonicalEquiv {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] : FractionalIdeal S P ≃+* FractionalIdeal S P'

canonicalEquiv f f' is the canonical equivalence between the fractional ideals in P and in P', which are both localizations of R at S.

@[simp]

theorem FractionalIdeal.mem_canonicalEquiv_apply {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] {I : FractionalIdeal S P} {x : P'} : x ∈ (canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

@[simp]

theorem FractionalIdeal.canonicalEquiv_symm {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] : (canonicalEquiv S P P').symm = canonicalEquiv S P' P

theorem FractionalIdeal.canonicalEquiv_flip {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] (I : FractionalIdeal S P') : (canonicalEquiv S P P') ((canonicalEquiv S P' P) I) = I

@[simp]

theorem FractionalIdeal.canonicalEquiv_canonicalEquiv {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] (I : FractionalIdeal S P) : (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) = (canonicalEquiv S P P'') I

theorem FractionalIdeal.canonicalEquiv_trans_canonicalEquiv {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] : (canonicalEquiv S P P').trans (canonicalEquiv S P' P'') = canonicalEquiv S P P''

@[simp]

theorem FractionalIdeal.canonicalEquiv_coeIdeal {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [IsLocalization S P] [IsLocalization S P'] (I : Ideal R) : (canonicalEquiv S P P') ↑I = ↑I

@[simp]

theorem FractionalIdeal.canonicalEquiv_self {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [IsLocalization S P] : canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)

IsFractionRing section

This section concerns fractional ideals in the field of fractions, i.e. the type FractionalIdeal R⁰ K where IsFractionRing R K.

theorem FractionalIdeal.exists_ne_zero_mem_isInteger {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} [Nontrivial R] (hI : I ≠ 0) : ∃ (x : R), x ≠ 0 ∧ (algebraMap R K) x ∈ I

Nonzero fractional ideals contain a nonzero integer.

theorem FractionalIdeal.map_ne_zero {R : Type u_1} [CommRing R] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R K'] [IsFractionRing R K'] {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R] (hI : I ≠ 0) : map h I ≠ 0

@[simp]

theorem FractionalIdeal.map_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R K'] [IsFractionRing R K'] {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R] : map h I = 0 ↔ I = 0

theorem FractionalIdeal.coeIdeal_injective {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] : Function.Injective fun (I : Ideal R) => ↑I

theorem FractionalIdeal.coeIdeal_inj {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I J : Ideal R} : ↑I = ↑J ↔ I = J

@[simp]

theorem FractionalIdeal.coeIdeal_eq_zero {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I = 0 ↔ I = ⊥

theorem FractionalIdeal.coeIdeal_ne_zero {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I ≠ 0 ↔ I ≠ ⊥

@[simp]

theorem FractionalIdeal.coeIdeal_eq_one {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I = 1 ↔ I = 1

theorem FractionalIdeal.coeIdeal_ne_one {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I ≠ 1 ↔ I ≠ 1

theorem FractionalIdeal.num_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) K} : I.num = 0 ↔ I = 0

quotient section

This section defines the ideal quotient of fractional ideals.

In this section we need that each non-zero y : R has an inverse in the localization, i.e. that the localization is a field. We satisfy this assumption by taking S = nonZeroDivisors R, R's localization at which is a field because R is a domain.

instance FractionalIdeal.instNontrivialNonZeroDivisors {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)

theorem FractionalIdeal.ne_zero_of_mul_eq_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : I ≠ 0

theorem IsFractional.div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : Submodule R₁ K} : IsFractional (nonZeroDivisors R₁) I → IsFractional (nonZeroDivisors R₁) J → J ≠ 0 → IsFractional (nonZeroDivisors R₁) (I / J)

theorem FractionalIdeal.isFractional_div_of_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : IsFractional (nonZeroDivisors R₁) (↑I / ↑J)

@[deprecated FractionalIdeal.isFractional_div_of_ne_zero (since := "2025-09-14")]

theorem FractionalIdeal.fractional_div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : IsFractional (nonZeroDivisors R₁) (↑I / ↑J)

Alias of FractionalIdeal.isFractional_div_of_ne_zero.

noncomputable instance FractionalIdeal.instDivNonZeroDivisors {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] : Div (FractionalIdeal (nonZeroDivisors R₁) K)

@[simp]

theorem FractionalIdeal.div_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I / 0 = 0

theorem FractionalIdeal.div_of_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : I / J = ⟨↑I / ↑J, ⋯⟩

@[deprecated FractionalIdeal.div_of_ne_zero (since := "2025-09-14")]

theorem FractionalIdeal.div_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : I / J = ⟨↑I / ↑J, ⋯⟩

Alias of FractionalIdeal.div_of_ne_zero.

@[simp]

theorem FractionalIdeal.coe_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (hJ : J ≠ 0) : ↑(I / J) = ↑I / ↑J

theorem FractionalIdeal.mem_div_iff_of_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) {x : K} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

@[deprecated FractionalIdeal.mem_div_iff_of_ne_zero (since := "2025-09-14")]

theorem FractionalIdeal.mem_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) {x : K} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

Alias of FractionalIdeal.mem_div_iff_of_ne_zero.

theorem FractionalIdeal.mul_one_div_le_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * (1 / I) ≤ 1

theorem FractionalIdeal.le_self_mul_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≤ 1) : I ≤ I * (1 / I)

theorem FractionalIdeal.le_div_iff_of_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J J' : FractionalIdeal (nonZeroDivisors R₁) K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J

@[deprecated FractionalIdeal.le_div_iff_of_ne_zero (since := "2025-09-14")]

theorem FractionalIdeal.le_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J J' : FractionalIdeal (nonZeroDivisors R₁) K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J

Alias of FractionalIdeal.le_div_iff_of_ne_zero.

theorem FractionalIdeal.le_div_iff_mul_le {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I J J' : FractionalIdeal (nonZeroDivisors R₁) K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ I * J' ≤ J

@[simp]

theorem FractionalIdeal.div_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I / 1 = I

theorem FractionalIdeal.eq_one_div_of_mul_eq_one_right {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : J = 1 / I

theorem FractionalIdeal.mul_div_self_cancel_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * (1 / I) = 1 ↔ ∃ (J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1

@[simp]

theorem FractionalIdeal.map_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I J : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : map (↑h) (I / J) = map (↑h) I / map (↑h) J

theorem FractionalIdeal.map_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : map (↑h) (1 / I) = 1 / map (↑h) I

theorem FractionalIdeal.eq_zero_or_one {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [IsFractionRing K L] (I : FractionalIdeal (nonZeroDivisors K) L) : I = 0 ∨ I = 1

theorem FractionalIdeal.eq_zero_or_one_of_isField {R₁ : Type u_3} {K : Type u_4} [CommRing R₁] [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] (hF : IsField R₁) (I : FractionalIdeal (nonZeroDivisors R₁) K) : I = 0 ∨ I = 1

def FractionalIdeal.spanFinset (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K) : FractionalIdeal (nonZeroDivisors R₁) K

FractionalIdeal.span_finset R₁ s f is the fractional ideal of R₁ generated by f '' s.

@[simp]

theorem FractionalIdeal.spanFinset_coe (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K) : ↑(spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)

@[simp]

theorem FractionalIdeal.spanFinset_eq_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K} : spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

theorem FractionalIdeal.spanFinset_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K} : spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0

theorem FractionalIdeal.isFractional_span_singleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) : IsFractional S (R ∙ x)

theorem FractionalIdeal.spanSingleton_def {R : Type u_5} [CommRing R] (S : Submonoid R) {P : Type u_6} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) : spanSingleton S x = ⟨R ∙ x, ⋯⟩

@[irreducible]

def FractionalIdeal.spanSingleton {R : Type u_5} [CommRing R] (S : Submonoid R) {P : Type u_6} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) : FractionalIdeal S P

spanSingleton x is the fractional ideal generated by x if 0 ∉ S

@[simp]

theorem FractionalIdeal.coe_spanSingleton {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) : ↑(spanSingleton S x) = R ∙ x

@[simp]

theorem FractionalIdeal.mem_spanSingleton {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x y : P} : x ∈ spanSingleton S y ↔ ∃ (z : R), z • y = x

theorem FractionalIdeal.mem_spanSingleton_self {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) : x ∈ spanSingleton S x

theorem FractionalIdeal.den_mul_self_eq_num' {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [IsLocalization S P] (I : FractionalIdeal S P) : spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num

A version of FractionalIdeal.den_mul_self_eq_num in terms of fractional ideals.

@[simp]

theorem FractionalIdeal.spanSingleton_le_iff_mem {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x : P} {I : FractionalIdeal S P} : spanSingleton S x ≤ I ↔ x ∈ I

theorem FractionalIdeal.spanSingleton_eq_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] [IsDomain R] [Module.IsTorsionFree R P] {x y : P} : spanSingleton S x = spanSingleton S y ↔ ∃ (z : Rˣ), z • x = y

theorem FractionalIdeal.eq_spanSingleton_of_principal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (I : FractionalIdeal S P) [(↑I).IsPrincipal] : I = spanSingleton S (Submodule.IsPrincipal.generator ↑I)

theorem FractionalIdeal.isPrincipal_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (I : FractionalIdeal S P) : (↑I).IsPrincipal ↔ ∃ (x : P), I = spanSingleton S x

@[simp]

theorem FractionalIdeal.spanSingleton_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] : spanSingleton S 0 = 0

theorem FractionalIdeal.spanSingleton_eq_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {y : P} : spanSingleton S y = 0 ↔ y = 0

theorem FractionalIdeal.spanSingleton_ne_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {y : P} : spanSingleton S y ≠ 0 ↔ y ≠ 0

@[simp]

theorem FractionalIdeal.spanSingleton_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] : spanSingleton S 1 = 1

@[simp]

theorem FractionalIdeal.spanSingleton_mul_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x y : P) : spanSingleton S x * spanSingleton S y = spanSingleton S (x * y)

@[simp]

theorem FractionalIdeal.spanSingleton_pow {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) (n : ℕ) : spanSingleton S x ^ n = spanSingleton S (x ^ n)

@[simp]

theorem FractionalIdeal.coeIdeal_span_singleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : R) : ↑(Ideal.span {x}) = spanSingleton S ((algebraMap R P) x)

@[simp]

theorem FractionalIdeal.canonicalEquiv_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {P' : Type u_5} [CommRing P'] [Algebra R P'] [IsLocalization S P'] (x : P) : (canonicalEquiv S P P') (spanSingleton S x) = spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)

theorem FractionalIdeal.mem_singleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x y : P} {I : FractionalIdeal S P} : y ∈ spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'

theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal {R₁ : Type u_3} [CommRing R₁] (K : Type u_4) [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {I J : Ideal R₁} {x y : R₁} (hy : y ∈ nonZeroDivisors R₁) : spanSingleton (nonZeroDivisors R₁) (IsLocalization.mk' K x ⟨y, hy⟩) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J

theorem FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {I J : Ideal R₁} {z : K} : spanSingleton (nonZeroDivisors R₁) z * ↑I = ↑J ↔ Ideal.span {(IsLocalization.sec (nonZeroDivisors R₁) z).1} * I = Ideal.span {↑(IsLocalization.sec (nonZeroDivisors R₁) z).2} * J

theorem FractionalIdeal.one_div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (x : K) : 1 / spanSingleton (nonZeroDivisors R₁) x = spanSingleton (nonZeroDivisors R₁) x⁻¹

@[simp]

theorem FractionalIdeal.div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (J : FractionalIdeal (nonZeroDivisors R₁) K) (d : K) : J / spanSingleton (nonZeroDivisors R₁) d = spanSingleton (nonZeroDivisors R₁) d⁻¹ * J

theorem FractionalIdeal.exists_eq_spanSingleton_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) : ∃ (a : R₁) (aI : Ideal R₁), a ≠ 0 ∧ I = spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) a)⁻¹ * ↑aI

theorem FractionalIdeal.ideal_factor_ne_zero {R : Type u_6} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) {a : R} {J : Ideal R} (haJ : I = spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J) : J ≠ 0

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then J is nonzero.

theorem FractionalIdeal.constant_factor_ne_zero {R : Type u_6} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I ≠ 0) {a : R} {J : Ideal R} (haJ : I = spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * ↑J) : Ideal.span {a} ≠ 0

If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then a is nonzero.

instance FractionalIdeal.isPrincipal {K : Type u_4} [Field K] {R : Type u_5} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) : (↑I).IsPrincipal

theorem FractionalIdeal.le_spanSingleton_mul_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x : P} {I J : FractionalIdeal S P} : I ≤ spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

theorem FractionalIdeal.spanSingleton_mul_le_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x : P} {I J : FractionalIdeal S P} : spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

theorem FractionalIdeal.eq_spanSingleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] {x : P} {I J : FractionalIdeal S P} : I = spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

theorem FractionalIdeal.num_le {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (I : FractionalIdeal S P) : ↑I.num ≤ I

theorem FractionalIdeal.isPrincipal_of_isPrincipal_num {R : Type u_1} [CommRing R] [IsDomain R] (I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)) (hI : Submodule.IsPrincipal I.num) : (↑I).IsPrincipal

If the numerator ideal of a fractional ideal is principal, then so is the fractional ideal.

theorem FractionalIdeal.isNoetherian_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] : IsNoetherian R₁ ↥↑0

theorem FractionalIdeal.isNoetherian_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : IsNoetherian R₁ ↥↑I ↔ ∀ J ≤ I, (↑J).FG

theorem FractionalIdeal.isNoetherian_coeIdeal {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsNoetherianRing R₁] (I : Ideal R₁) : IsNoetherian R₁ ↥↑↑I

theorem FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (x : R₁) {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : IsNoetherian R₁ ↥↑I) : IsNoetherian R₁ ↥↑(spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) x)⁻¹ * I)

theorem FractionalIdeal.isNoetherian {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] [IsNoetherianRing R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) : IsNoetherian R₁ ↥↑I

Every fractional ideal of a Noetherian integral domain is Noetherian.

theorem FractionalIdeal.isFractional_adjoin_integral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) (hx : IsIntegral R x) : IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))

A[x] is a fractional ideal for every integral x.

def FractionalIdeal.adjoinIntegral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) (hx : IsIntegral R x) : FractionalIdeal S P

FractionalIdeal.adjoinIntegral (S : Submonoid R) x hx is R[x] as a fractional ideal, where hx is a proof that x : P is integral over R.

@[simp]

theorem FractionalIdeal.adjoinIntegral_coe {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) (hx : IsIntegral R x) : ↑(adjoinIntegral S x hx) = Subalgebra.toSubmodule (Algebra.adjoin R {x})

theorem FractionalIdeal.mem_adjoinIntegral_self {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (x : P) (hx : IsIntegral R x) : x ∈ adjoinIntegral S x hx