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

source

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 (AlgHom.toLinearMap g) I)

source

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

Equations

FractionalIdeal.map g I = { val := Submodule.map (AlgHom.toLinearMap g) ↑I, property := (_ : IsFractional S (Submodule.map (AlgHom.toLinearMap g) ↑I)) }

Instances For

source

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

↑(FractionalIdeal.map g I) = Submodule.map (AlgHom.toLinearMap g) ↑I

source

@[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 ∈ FractionalIdeal.map g I ↔ ∃ x ∈ I, g x = y

source

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

FractionalIdeal.map (AlgHom.id R P) I = I

source

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

FractionalIdeal.map (AlgHom.comp g' g) I = FractionalIdeal.map g' (FractionalIdeal.map g I)

source

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

FractionalIdeal.map g ↑I = ↑I

source

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

FractionalIdeal.map g 1 = 1

source

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

FractionalIdeal.map g 0 = 0

source

@[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 : FractionalIdeal S P) (J : FractionalIdeal S P) (g : P →ₐ[R] P') :

FractionalIdeal.map g (I + J) = FractionalIdeal.map g I + FractionalIdeal.map g J

source

@[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 : FractionalIdeal S P) (J : FractionalIdeal S P) (g : P →ₐ[R] P') :

FractionalIdeal.map g (I * J) = FractionalIdeal.map g I * FractionalIdeal.map g J

source

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

FractionalIdeal.map (↑(AlgEquiv.symm g)) (FractionalIdeal.map (↑g) I) = I

source

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

FractionalIdeal.map (↑g) (FractionalIdeal.map (↑(AlgEquiv.symm g)) I) = I

source

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 ∈ FractionalIdeal.map f I ↔ x ∈ I

source

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 (FractionalIdeal.map f)

source

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

Equations

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

Instances For

source

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

⇑(FractionalIdeal.mapEquiv g) = FractionalIdeal.map ↑g

source

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

(FractionalIdeal.mapEquiv g) I = FractionalIdeal.map (↑g) I

source

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

RingEquiv.symm (FractionalIdeal.mapEquiv g) = FractionalIdeal.mapEquiv (AlgEquiv.symm g)

source

@[simp]

theorem FractionalIdeal.mapEquiv_refl {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] :

FractionalIdeal.mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P)

source

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)

source

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

IsFractional S I

source

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 : FractionalIdeal S P} {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')

source

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) :

Submodule.FG ↑↑I ↔ Ideal.FG I

source

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)ˣ) :

Submodule.FG ↑↑I

source

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) :

Submodule.FG ↑I

source

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) :

Ideal.FG I

source

@[irreducible]

noncomputable def FractionalIdeal.canonicalEquiv {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : 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.

Equations

@FractionalIdeal.canonicalEquiv = FractionalIdeal.wrapped✝.1

Instances For

source

theorem FractionalIdeal.canonicalEquiv_def {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] :

FractionalIdeal.canonicalEquiv S P P' = FractionalIdeal.mapEquiv (let src := IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S); { toEquiv := src.toEquiv, map_mul' := (_ : ∀ (x y : P), (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun (x * y) = (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun x * (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun y), map_add' := (_ : ∀ (x y : P), (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun (x + y) = (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun x + (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv.toFun y), commutes' := (_ : ∀ (r : R), (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)) ((algebraMap R P) r) = (algebraMap R P') ((RingEquiv.refl R) r)) })

source

@[simp]

theorem FractionalIdeal.mem_canonicalEquiv_apply {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] {I : FractionalIdeal S P} {x : P'} :

x ∈ (FractionalIdeal.canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) (_ : ∀ y ∈ S, (RingHom.id R) y ∈ S)) y = x

source

@[simp]

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

RingEquiv.symm (FractionalIdeal.canonicalEquiv S P P') = FractionalIdeal.canonicalEquiv S P' P

source

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

(FractionalIdeal.canonicalEquiv S P P') ((FractionalIdeal.canonicalEquiv S P' P) I) = I

source

@[simp]

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

(FractionalIdeal.canonicalEquiv S P' P'') ((FractionalIdeal.canonicalEquiv S P P') I) = (FractionalIdeal.canonicalEquiv S P P'') I

source

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

RingEquiv.trans (FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.canonicalEquiv S P' P'') = FractionalIdeal.canonicalEquiv S P P''

source

@[simp]

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

(FractionalIdeal.canonicalEquiv S P P') ↑I = ↑I

source

@[simp]

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

FractionalIdeal.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.

source

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.

source

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) :

FractionalIdeal.map h I ≠ 0

source

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

FractionalIdeal.map h I = 0 ↔ I = 0

source

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

source

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

↑I = ↑J ↔ I = J

source

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

source

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 ≠ ⊥

source

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

source

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

source

theorem FractionalIdeal.num_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] {I : FractionalIdeal (nonZeroDivisors R) K} :

FractionalIdeal.num I = 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.

source

instance FractionalIdeal.instNontrivialFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] :

Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

(_ : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)) = (_ : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K))

source

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

I ≠ 0

source

theorem IsFractional.div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : Submodule R₁ K} {J : Submodule R₁ K} :

IsFractional (nonZeroDivisors R₁) I → IsFractional (nonZeroDivisors R₁) J → J ≠ 0 → IsFractional (nonZeroDivisors R₁) (I / J)

source

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

IsFractional (nonZeroDivisors R₁) (↑I / ↑J)

source

noncomputable instance FractionalIdeal.instDivFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] :

Div (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

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

source

@[simp]

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

I / 0 = 0

source

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

I / J = { val := ↑I / ↑J, property := (_ : IsFractional (nonZeroDivisors R₁) (↑I / ↑J)) }

source

@[simp]

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

↑(I / J) = ↑I / ↑J

source

theorem FractionalIdeal.mem_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) {x : K} :

x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

source

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

I * (1 / I) ≤ 1

source

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

I ≤ I * (1 / I)

source

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

I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J

source

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

I ≤ J / J' ↔ I * J' ≤ J

source

@[simp]

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

I / 1 = I

source

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] [frac : IsFractionRing R₁ K] [IsDomain R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) (J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) :

J = 1 / I

source

theorem FractionalIdeal.mul_div_self_cancel_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} :

I * (1 / I) = 1 ↔ ∃ (J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1

source

@[simp]

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

FractionalIdeal.map (↑h) (I / J) = FractionalIdeal.map (↑h) I / FractionalIdeal.map (↑h) J

source

theorem FractionalIdeal.map_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : 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') :

FractionalIdeal.map (↑h) (1 / I) = 1 / FractionalIdeal.map (↑h) I

source

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

source

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

source

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.

Equations

FractionalIdeal.spanFinset R₁ s f = { val := Submodule.span R₁ (f '' ↑s), property := (_ : IsFractional (nonZeroDivisors R₁) (Submodule.span R₁ (f '' ↑s))) }

Instances For

source

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

↑(FractionalIdeal.spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)

source

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

FractionalIdeal.spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

source

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} :

FractionalIdeal.spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0

source

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

IsFractional S (Submodule.span R {x})

source

@[irreducible]

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

FractionalIdeal S P

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

Equations

@FractionalIdeal.spanSingleton = FractionalIdeal.wrapped✝.1

Instances For

source

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

FractionalIdeal.spanSingleton S x = { val := Submodule.span R {x}, property := (_ : IsFractional S (Submodule.span R {x})) }

source

@[simp]

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

↑(FractionalIdeal.spanSingleton S x) = Submodule.span R {x}

source

@[simp]

theorem FractionalIdeal.mem_spanSingleton {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {y : P} :

x ∈ FractionalIdeal.spanSingleton S y ↔ ∃ (z : R), z • y = x

source

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

x ∈ FractionalIdeal.spanSingleton S x

source

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] [loc : IsLocalization S P] (I : FractionalIdeal S P) :

FractionalIdeal.spanSingleton S ((algebraMap R P) ↑(FractionalIdeal.den I)) * I = ↑(FractionalIdeal.num I)

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

source

@[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] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} :

FractionalIdeal.spanSingleton S x ≤ I ↔ x ∈ I

source

theorem FractionalIdeal.spanSingleton_eq_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] [NoZeroSMulDivisors R P] {x : P} {y : P} :

FractionalIdeal.spanSingleton S x = FractionalIdeal.spanSingleton S y ↔ ∃ (z : Rˣ), z • x = y

source

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

I = FractionalIdeal.spanSingleton S (Submodule.IsPrincipal.generator ↑I)

source

theorem FractionalIdeal.isPrincipal_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (I : FractionalIdeal S P) :

Submodule.IsPrincipal ↑I ↔ ∃ (x : P), I = FractionalIdeal.spanSingleton S x

source

@[simp]

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

FractionalIdeal.spanSingleton S 0 = 0

source

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

FractionalIdeal.spanSingleton S y = 0 ↔ y = 0

source

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

FractionalIdeal.spanSingleton S y ≠ 0 ↔ y ≠ 0

source

@[simp]

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

FractionalIdeal.spanSingleton S 1 = 1

source

@[simp]

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

FractionalIdeal.spanSingleton S x * FractionalIdeal.spanSingleton S y = FractionalIdeal.spanSingleton S (x * y)

source

@[simp]

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

FractionalIdeal.spanSingleton S x ^ n = FractionalIdeal.spanSingleton S (x ^ n)

source

@[simp]

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

↑(Ideal.span {x}) = FractionalIdeal.spanSingleton S ((algebraMap R P) x)

source

@[simp]

theorem FractionalIdeal.canonicalEquiv_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {P' : Type u_5} [CommRing P'] [Algebra R P'] [IsLocalization S P'] (x : P) :

(FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.spanSingleton S x) = FractionalIdeal.spanSingleton S ((IsLocalization.map P' (RingHom.id R) (_ : ∀ y ∈ S, (RingHom.id R) y ∈ S)) x)

source

theorem FractionalIdeal.mem_singleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {y : P} {I : FractionalIdeal S P} :

y ∈ FractionalIdeal.spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'

source

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 : Ideal R₁} {J : Ideal R₁} {x : R₁} {y : R₁} (hy : y ∈ nonZeroDivisors R₁) :

FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (IsLocalization.mk' K x { val := y, property := hy }) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J

source

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 : Ideal R₁} {J : Ideal R₁} {z : K} :

FractionalIdeal.spanSingleton (nonZeroDivisors R₁) z * ↑I = ↑J ↔ Ideal.span {(IsLocalization.sec (nonZeroDivisors R₁) z).1} * I = Ideal.span {↑(IsLocalization.sec (nonZeroDivisors R₁) z).2} * J

source

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 / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x⁻¹

source

@[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 / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d⁻¹ * J

source

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 = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) a)⁻¹ * ↑aI

source

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) :

Submodule.IsPrincipal ↑I

Equations

(_ : Submodule.IsPrincipal ↑I) = (_ : Submodule.IsPrincipal ↑I)

source

theorem FractionalIdeal.le_spanSingleton_mul_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} :

I ≤ FractionalIdeal.spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

source

theorem FractionalIdeal.spanSingleton_mul_le_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} :

FractionalIdeal.spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

source

theorem FractionalIdeal.eq_spanSingleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} :

I = FractionalIdeal.spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

source

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

↑(FractionalIdeal.num I) ≤ I

source

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

IsNoetherian R₁ ↥↑0

source

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, Submodule.FG ↑J

source

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

source

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

IsNoetherian R₁ ↥↑(FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) x)⁻¹ * I)

source

theorem FractionalIdeal.isNoetherian {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : 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.

source

theorem FractionalIdeal.isFractional_adjoin_integral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : 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.

source

def FractionalIdeal.adjoinIntegral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : 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.

Equations

FractionalIdeal.adjoinIntegral S x hx = { val := Subalgebra.toSubmodule (Algebra.adjoin R {x}), property := (_ : IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))) }