# Documentation

Mathlib.RingTheory.FractionalIdeal

# Fractional ideals #

This file defines fractional ideals of an integral domain and proves basic facts about them.

## Main definitions #

Let S be a submonoid of an integral domain R, P the localization of R at S, and f the natural ring hom from R to P.

• IsFractional defines which R-submodules of P are fractional ideals
• FractionalIdeal S P is the type of fractional ideals in P
• a coercion coeIdeal : Ideal R → FractionalIdeal S P
• CommSemiring (FractionalIdeal S P) instance: the typical ideal operations generalized to fractional ideals
• Lattice (FractionalIdeal S P) instance
• 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)

## Implementation notes #

Fractional ideals are considered equal when they contain the same elements, independent of the denominator a : R such that a I ⊆ R. Thus, we define FractionalIdeal to be the subtype of the predicate IsFractional, instead of having FractionalIdeal be a structure of which a is a field.

Most definitions in this file specialize operations from submodules to fractional ideals, proving that the result of this operation is fractional if the input is fractional. Exceptions to this rule are defining (+) := (⊔) and ⊥ := 0, in order to re-use their respective proof terms. We can still use simp to show ↑I + ↑J = ↑(I + J) and ↑⊥ = ↑0.

Many results in fact do not need that P is a localization, only that P is an R-algebra. We omit the IsLocalization parameter whenever this is practical. Similarly, we don't assume that the localization is a field until we need it to define ideal quotients. When this assumption is needed, we replace S with R⁰, making the localization a field.

## References #

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

## Tags #

fractional ideal, fractional ideals, invertible ideal

def IsFractional {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] (I : ) :

A submodule I is a fractional ideal if a I ⊆ R for some a ≠ 0.

Instances For
def FractionalIdeal {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] :
Type u_2

The fractional ideals of a domain R are ideals of R divided by some a ∈ R.

More precisely, let P be a localization of R at some submonoid S, then a fractional ideal I ⊆ P is an R-submodule of P, such that there is a nonzero a : R with a I ⊆ R.

Instances For
def FractionalIdeal.coeToSubmodule {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :

Map a fractional ideal I to a submodule by forgetting that ∃ a, a I ⊆ R.

This implements the coercion FractionalIdeal S P → Submodule R P.

Instances For

Map a fractional ideal I to a submodule by forgetting that ∃ a, a I ⊆ R.

This coercion is typically called coeToSubmodule in lemma names (or coe when the coercion is clear from the context), not to be confused with IsLocalization.coeSubmodule : Ideal R → Submodule R P (which we use to define coe : Ideal R → FractionalIdeal S P).

theorem FractionalIdeal.isFractional {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
instance FractionalIdeal.instSetLikeFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
SetLike () P
@[simp]
theorem FractionalIdeal.mem_coe {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {x : P} :
x I x I
theorem FractionalIdeal.ext {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } :
(∀ (x : P), x I x J) → I = J
def FractionalIdeal.copy {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (p : ) (s : Set P) (hs : s = p) :

Copy of a FractionalIdeal with a new underlying set equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem FractionalIdeal.coe_copy {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (p : ) (s : Set P) (hs : s = p) :
↑() = s
theorem FractionalIdeal.coe_eq {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (p : ) (s : Set P) (hs : s = p) :
= p
@[simp]
theorem FractionalIdeal.val_eq_coe {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
I = I
@[simp]
theorem FractionalIdeal.coe_mk {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (hI : ) :
{ val := I, property := hI } = I
theorem FractionalIdeal.coeToSet_coeToSubmodule {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
I = I

Transfer instances from Submodule R P to FractionalIdeal S P.

theorem FractionalIdeal.coeToSubmodule_injective {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
Function.Injective fun I => I
theorem FractionalIdeal.coeToSubmodule_inj {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } :
I = J I = J
theorem FractionalIdeal.isFractional_of_le_one {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (h : I 1) :
theorem FractionalIdeal.isFractional_of_le {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } (hIJ : I J) :
def FractionalIdeal.coeIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :

Map an ideal I to a fractional ideal by forgetting I is integral.

This is the function that implements the coercion Ideal R → FractionalIdeal S P.

Instances For

Map an ideal I to a fractional ideal by forgetting I is integral.

This is a bundled version of IsLocalization.coeSubmodule : Ideal R → Submodule R P, which is not to be confused with the coe : FractionalIdeal S P → Submodule R P, also called coeToSubmodule in theorem names.

This map is available as a ring hom, called FractionalIdeal.coeIdealHom.

@[simp]
theorem FractionalIdeal.coe_coeIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
I =
@[simp]
theorem FractionalIdeal.mem_coeIdeal {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] {x : P} {I : } :
x I x', x' I ↑() x' = x
theorem FractionalIdeal.mem_coeIdeal_of_mem {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] {x : R} {I : } (hx : x I) :
↑() x I
theorem FractionalIdeal.coeIdeal_le_coeIdeal' {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [] (h : ) {I : } {J : } :
I J I J
@[simp]
theorem FractionalIdeal.coeIdeal_le_coeIdeal {R : Type u_1} [] (K : Type u_3) [] [Algebra R K] [] {I : } {J : } :
I J I J
instance FractionalIdeal.instZeroFractionalIdeal {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] :
Zero ()
@[simp]
theorem FractionalIdeal.mem_zero_iff {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] {x : P} :
x 0 x = 0
@[simp]
theorem FractionalIdeal.coe_zero {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
0 =
@[simp]
theorem FractionalIdeal.coeIdeal_bot {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
= 0
@[simp]
theorem FractionalIdeal.exists_mem_algebraMap_eq {R : Type u_1} [] {S : } (P : Type u_2) [] [Algebra R P] [loc : ] {x : R} {I : } (h : ) :
(x', x' I ↑() x' = ↑() x) x I
theorem FractionalIdeal.coeIdeal_injective' {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (h : ) :
Function.Injective fun I => I
theorem FractionalIdeal.coeIdeal_inj' {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (h : ) {I : } {J : } :
I = J I = J
theorem FractionalIdeal.coeIdeal_eq_zero' {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {I : } (h : ) :
I = 0 I =
theorem FractionalIdeal.coeIdeal_ne_zero' {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {I : } (h : ) :
I 0 I
theorem FractionalIdeal.coeToSubmodule_eq_bot {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
I = I = 0
theorem FractionalIdeal.coeToSubmodule_ne_bot {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
I I 0
instance FractionalIdeal.instInhabitedFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
instance FractionalIdeal.instOneFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
One ()
@[simp]
theorem FractionalIdeal.coeIdeal_top {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] :
= 1
theorem FractionalIdeal.mem_one_iff {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] {x : P} :
x 1 x', ↑() x' = x
theorem FractionalIdeal.coe_mem_one {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] (x : R) :
↑() x 1
theorem FractionalIdeal.one_mem_one {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] :
1 1
theorem FractionalIdeal.coe_one_eq_coeSubmodule_top {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :

(1 : FractionalIdeal S P) is defined as the R-submodule f(R) ≤ P.

However, this is not definitionally equal to 1 : Submodule R P, which is proved in the actual simp lemma coe_one.

@[simp]
theorem FractionalIdeal.coe_one {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
1 = 1

### Lattice section #

Defines the order on fractional ideals as inclusion of their underlying sets, and ports the lattice structure on submodules to fractional ideals.

@[simp]
theorem FractionalIdeal.coe_le_coe {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } :
I J I J
theorem FractionalIdeal.zero_le {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
0 I
instance FractionalIdeal.orderBot {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
@[simp]
theorem FractionalIdeal.bot_eq_zero {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
= 0
@[simp]
theorem FractionalIdeal.le_zero_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
I 0 I = 0
theorem FractionalIdeal.eq_zero_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
I = 0 ∀ (x : P), x Ix = 0
theorem IsFractional.sup {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } :
IsFractional S (I J)
theorem IsFractional.inf_right {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
∀ (J : ), IsFractional S (I J)
instance FractionalIdeal.instInfFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
Inf ()
@[simp]
theorem FractionalIdeal.coe_inf {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I J) = I J
instance FractionalIdeal.instSupFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
Sup ()
theorem FractionalIdeal.coe_sup {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I J) = I J
instance FractionalIdeal.lattice {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
instance FractionalIdeal.instSemilatticeSupFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
instance FractionalIdeal.instAddFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
@[simp]
theorem FractionalIdeal.sup_eq_add {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
I J = I + J
@[simp]
theorem FractionalIdeal.coe_add {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I + J) = I + J
@[simp]
theorem FractionalIdeal.coeIdeal_sup {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I J) = I + J
theorem IsFractional.nsmul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } (n : ) :
IsFractional S (n I)
instance FractionalIdeal.instSMulNatFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
theorem FractionalIdeal.coe_nsmul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (n : ) (I : ) :
↑(n I) = n I
theorem IsFractional.mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } :
IsFractional S (I * J)
theorem IsFractional.pow {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } (h : ) (n : ) :
IsFractional S (I ^ n)
theorem FractionalIdeal.mul_def' {R : Type u_3} [] {S : } {P : Type u_4} [] [Algebra R P] (I : ) (J : ) :
= { val := I * J, property := (_ : IsFractional S (I * J)) }
@[irreducible]
def FractionalIdeal.mul {R : Type u_3} [] {S : } {P : Type u_4} [] [Algebra R P] (I : ) (J : ) :

FractionalIdeal.mul is the product of two fractional ideals, used to define the Mul instance.

This is only an auxiliary definition: the preferred way of writing I.mul J is I * J.

Elaborated terms involving FractionalIdeal tend to grow quite large, so by making definitions irreducible, we hope to avoid deep unfolds.

Instances For
instance FractionalIdeal.instMulFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
Mul ()
@[simp]
theorem FractionalIdeal.mul_eq_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
= I * J
theorem FractionalIdeal.mul_def {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
I * J = { val := I * J, property := (_ : IsFractional S (I * J)) }
@[simp]
theorem FractionalIdeal.coe_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I * J) = I * J
@[simp]
theorem FractionalIdeal.coeIdeal_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (J : ) :
↑(I * J) = I * J
theorem FractionalIdeal.mul_left_mono {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
Monotone ((fun x x_1 => x * x_1) I)
theorem FractionalIdeal.mul_right_mono {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
Monotone fun J => J * I
theorem FractionalIdeal.mul_mem_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } {i : P} {j : P} (hi : i I) (hj : j J) :
i * j I * J
theorem FractionalIdeal.mul_le {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } {K : } :
I * J K ∀ (i : P), i I∀ (j : P), j Ji * j K
instance FractionalIdeal.instPowFractionalIdealNat {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
Pow ()
@[simp]
theorem FractionalIdeal.coe_pow {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (n : ) :
↑(I ^ n) = I ^ n
theorem FractionalIdeal.mul_induction_on {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } {C : PProp} {r : P} (hr : r I * J) (hm : (i : P) → i I(j : P) → j JC (i * j)) (ha : (x y : P) → C xC yC (x + y)) :
C r
instance FractionalIdeal.instNatCastFractionalIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
theorem FractionalIdeal.coe_nat_cast {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (n : ) :
n = n
instance FractionalIdeal.commSemiring {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
@[simp]
theorem FractionalIdeal.coeSubmoduleHom_apply {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] (I : ) :
↑() I = I
def FractionalIdeal.coeSubmoduleHom {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] :

FractionalIdeal.coeToSubmodule as a bundled RingHom.

Instances For
theorem FractionalIdeal.add_le_add_left {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } (hIJ : I J) (J' : ) :
J' + I J' + J
theorem FractionalIdeal.mul_le_mul_left {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } (hIJ : I J) (J' : ) :
J' * I J' * J
theorem FractionalIdeal.le_self_mul_self {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } (hI : 1 I) :
I I * I
theorem FractionalIdeal.mul_self_le_self {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } (hI : I 1) :
I * I I
theorem FractionalIdeal.coeIdeal_le_one {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
I 1
theorem FractionalIdeal.le_one_iff_exists_coeIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {J : } :
J 1 I, I = J
@[simp]
theorem FractionalIdeal.one_le {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } :
1 I 1 I
@[simp]
theorem FractionalIdeal.coeIdealHom_apply {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] (I : ) :
↑() I = I
def FractionalIdeal.coeIdealHom {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] :

coeIdealHom (S : Submonoid R) P is (↑) : Ideal R → FractionalIdeal S P as a ring hom

Instances For
theorem FractionalIdeal.coeIdeal_pow {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] (I : ) (n : ) :
↑(I ^ n) = I ^ n
theorem FractionalIdeal.coeIdeal_finprod {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [] {α : Sort u_3} {f : α} (hS : ) :
↑(∏ᶠ (a : α), f a) = ∏ᶠ (a : α), ↑(f a)
theorem IsFractional.map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') {I : } :
def FractionalIdeal.map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') :

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

Instances For
@[simp]
theorem FractionalIdeal.coe_map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : ) :
↑() =
@[simp]
theorem FractionalIdeal.mem_map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {I : } {g : P →ₐ[R] P'} {y : P'} :
y x, x I g x = y
@[simp]
theorem FractionalIdeal.map_id {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) :
@[simp]
theorem FractionalIdeal.map_comp {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {P'' : Type u_4} [CommRing P''] [Algebra R P''] (I : ) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P'') :
@[simp]
theorem FractionalIdeal.map_coeIdeal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : ) :
= I
@[simp]
theorem FractionalIdeal.map_one {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') :
= 1
@[simp]
theorem FractionalIdeal.map_zero {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') :
= 0
@[simp]
theorem FractionalIdeal.map_add {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : ) (J : ) (g : P →ₐ[R] P') :
@[simp]
theorem FractionalIdeal.map_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : ) (J : ) (g : P →ₐ[R] P') :
@[simp]
theorem FractionalIdeal.map_map_symm {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : ) (g : P ≃ₐ[R] P') :
@[simp]
theorem FractionalIdeal.map_symm_map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : ) (g : P ≃ₐ[R] P') :
theorem FractionalIdeal.map_mem_map {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {f : P →ₐ[R] P'} (h : ) {x : P} {I : } :
f x x I
theorem FractionalIdeal.map_injective {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (f : P →ₐ[R] P') (h : ) :
def FractionalIdeal.mapEquiv {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') :

If g is an equivalence, map g is an isomorphism

Instances For
@[simp]
theorem FractionalIdeal.coeFun_mapEquiv {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') :
@[simp]
theorem FractionalIdeal.mapEquiv_apply {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') (I : ) :
↑() I = FractionalIdeal.map (g) I
@[simp]
theorem FractionalIdeal.mapEquiv_symm {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') :
@[simp]
theorem FractionalIdeal.mapEquiv_refl {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] :
theorem FractionalIdeal.isFractional_span_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {s : Set P} :
IsFractional S () a, a S ∀ (b : P), b sIsLocalization.IsInteger R (a b)
theorem FractionalIdeal.isFractional_of_fg {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {I : } (hI : ) :
theorem FractionalIdeal.mem_span_mul_finite_of_mem_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] {I : } {J : } {x : P} (hx : x I * J) :
T T', T I T' J x Submodule.span R (T * T')
theorem FractionalIdeal.coeIdeal_fg {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] (inj : Function.Injective ↑()) (I : ) :
Submodule.FG I
theorem FractionalIdeal.fg_unit {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ()ˣ) :
Submodule.FG I
theorem FractionalIdeal.fg_of_isUnit {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (I : ) (h : ) :
theorem Ideal.fg_of_isUnit {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] (inj : Function.Injective ↑()) (I : ) (h : IsUnit I) :
theorem FractionalIdeal.canonicalEquiv_def {R : Type u_5} [] (S : ) (P : Type u_6) [] [Algebra R P] [loc : ] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : ] :
= FractionalIdeal.mapEquiv (let src := IsLocalization.ringEquivOfRingEquiv P P' () (_ : ); { toEquiv := src.toEquiv, map_mul' := (_ : ∀ (x y : P), Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv (x * y) = Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv x * Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv y), map_add' := (_ : ∀ (x y : P), Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv (x + y) = Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv x + Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' () (_ : )).toEquiv y), commutes' := (_ : ∀ (r : R), ↑(IsLocalization.ringEquivOfRingEquiv P P' () (_ : )) (↑() r) = ↑(algebraMap R P') (↑() r)) })
@[irreducible]
noncomputable def FractionalIdeal.canonicalEquiv {R : Type u_5} [] (S : ) (P : Type u_6) [] [Algebra R P] [loc : ] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : ] :

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

Instances For
@[simp]
theorem FractionalIdeal.mem_canonicalEquiv_apply {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] {I : } {x : P'} :
x ↑() I y, y I ↑(IsLocalization.map P' () (_ : ∀ (y : R), y S↑() y S)) y = x
@[simp]
theorem FractionalIdeal.canonicalEquiv_symm {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] :
theorem FractionalIdeal.canonicalEquiv_flip {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] (I : ) :
↑() (↑() I) = I
@[simp]
theorem FractionalIdeal.canonicalEquiv_canonicalEquiv {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] (I : ) :
↑() (↑() I) = ↑() I
theorem FractionalIdeal.canonicalEquiv_trans_canonicalEquiv {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] :
@[simp]
theorem FractionalIdeal.canonicalEquiv_coeIdeal {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : ] (I : ) :
↑() I = I
@[simp]
theorem FractionalIdeal.canonicalEquiv_self {R : Type u_1} [] (S : ) (P : Type u_2) [] [Algebra R P] [loc : ] :

### 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} [] {K : Type u_3} [] [Algebra R K] [] {I : } [] (hI : I 0) :
x, x 0 ↑() x I

Nonzero fractional ideals contain a nonzero integer.

theorem FractionalIdeal.map_ne_zero {R : Type u_1} [] {K : Type u_3} {K' : Type u_4} [] [Field K'] [Algebra R K] [] [Algebra R K'] [] {I : } (h : K →ₐ[R] K') [] (hI : I 0) :
0
@[simp]
theorem FractionalIdeal.map_eq_zero_iff {R : Type u_1} [] {K : Type u_3} {K' : Type u_4} [] [Field K'] [Algebra R K] [] [Algebra R K'] [] {I : } (h : K →ₐ[R] K') [] :
= 0 I = 0
theorem FractionalIdeal.coeIdeal_injective {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] :
Function.Injective fun I => I
theorem FractionalIdeal.coeIdeal_inj {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] {I : } {J : } :
I = J I = J
@[simp]
theorem FractionalIdeal.coeIdeal_eq_zero {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] {I : } :
I = 0 I =
theorem FractionalIdeal.coeIdeal_ne_zero {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] {I : } :
I 0 I
@[simp]
theorem FractionalIdeal.coeIdeal_eq_one {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] {I : } :
I = 1 I = 1
theorem FractionalIdeal.coeIdeal_ne_one {R : Type u_1} [] {K : Type u_3} [] [Algebra R K] [] {I : } :
I 1 I 1

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

theorem FractionalIdeal.ne_zero_of_mul_eq_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] (I : ) (J : ) (h : I * J = 1) :
I 0
theorem IsFractional.div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : Submodule R₁ K} {J : Submodule R₁ K} :
J 0IsFractional () (I / J)
theorem FractionalIdeal.fractional_div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } (h : J 0) :
IsFractional () (I / J)
@[simp]
theorem FractionalIdeal.div_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } :
I / 0 = 0
theorem FractionalIdeal.div_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } (h : J 0) :
I / J = { val := I / J, property := (_ : IsFractional () (I / J)) }
@[simp]
theorem FractionalIdeal.coe_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } (hJ : J 0) :
↑(I / J) = I / J
theorem FractionalIdeal.mem_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } (h : J 0) {x : K} :
x I / J ∀ (y : K), y Jx * y I
theorem FractionalIdeal.mul_one_div_le_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } :
I * (1 / I) 1
theorem FractionalIdeal.le_self_mul_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } (hI : I 1) :
I I * (1 / I)
theorem FractionalIdeal.le_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } {J' : } (hJ' : J' 0) :
I J / J' ∀ (x : K), x I∀ (y : K), y J'x * y J
theorem FractionalIdeal.le_div_iff_mul_le {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } {J : } {J' : } (hJ' : J' 0) :
I J / J' I * J' J
@[simp]
theorem FractionalIdeal.div_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } :
I / 1 = I
theorem FractionalIdeal.eq_one_div_of_mul_eq_one_right {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] (I : ) (J : ) (h : I * J = 1) :
J = 1 / I
theorem FractionalIdeal.mul_div_self_cancel_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {I : } :
I * (1 / I) = 1 J, I * J = 1
@[simp]
theorem FractionalIdeal.map_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : ) (J : ) (h : K ≃ₐ[R₁] K') :
theorem FractionalIdeal.map_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : ) (h : K ≃ₐ[R₁] K') :
FractionalIdeal.map (h) (1 / I) = 1 / FractionalIdeal.map (h) I
theorem FractionalIdeal.eq_zero_or_one {K : Type u_4} {L : Type u_5} [] [] [Algebra K L] [] (I : ) :
I = 0 I = 1
theorem FractionalIdeal.eq_zero_or_one_of_isField {R₁ : Type u_3} {K : Type u_4} [CommRing R₁] [] [Algebra R₁ K] [] (hF : IsField R₁) (I : ) :
I = 0 I = 1
def FractionalIdeal.spanFinset (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] {ι : Type u_5} (s : ) (f : ιK) :

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

Instances For
@[simp]
theorem FractionalIdeal.spanFinset_coe (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] {ι : Type u_5} (s : ) (f : ιK) :
↑() = Submodule.span R₁ (f '' s)
@[simp]
theorem FractionalIdeal.spanFinset_eq_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] {ι : Type u_5} {s : } {f : ιK} :
= 0 ∀ (j : ι), j sf j = 0
theorem FractionalIdeal.spanFinset_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] {ι : Type u_5} {s : } {f : ιK} :
0 j, j s f j 0
theorem FractionalIdeal.isFractional_span_singleton {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) :
theorem FractionalIdeal.spanSingleton_def {R : Type u_5} [] (S : ) {P : Type u_6} [] [Algebra R P] [loc : ] (x : P) :
= { val := Submodule.span R {x}, property := (_ : IsFractional S (Submodule.span R {x})) }
@[irreducible]
def FractionalIdeal.spanSingleton {R : Type u_5} [] (S : ) {P : Type u_6} [] [Algebra R P] [loc : ] (x : P) :

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

Instances For
@[simp]
theorem FractionalIdeal.coe_spanSingleton {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) :
@[simp]
theorem FractionalIdeal.mem_spanSingleton {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {y : P} :
z, z y = x
theorem FractionalIdeal.mem_spanSingleton_self {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) :
@[simp]
theorem FractionalIdeal.spanSingleton_le_iff_mem {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {I : } :
x I
theorem FractionalIdeal.spanSingleton_eq_spanSingleton {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] [] {x : P} {y : P} :
z, z x = y
theorem FractionalIdeal.eq_spanSingleton_of_principal {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (I : ) :
theorem FractionalIdeal.isPrincipal_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (I : ) :
x,
@[simp]
theorem FractionalIdeal.spanSingleton_zero {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] :
theorem FractionalIdeal.spanSingleton_eq_zero_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {y : P} :
y = 0
theorem FractionalIdeal.spanSingleton_ne_zero_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {y : P} :
y 0
@[simp]
theorem FractionalIdeal.spanSingleton_one {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] :
@[simp]
theorem FractionalIdeal.spanSingleton_mul_spanSingleton {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) (y : P) :
@[simp]
theorem FractionalIdeal.spanSingleton_pow {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) (n : ) :
=
@[simp]
theorem FractionalIdeal.coeIdeal_span_singleton {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] (x : R) :
@[simp]
theorem FractionalIdeal.canonicalEquiv_spanSingleton {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {P' : Type u_5} [CommRing P'] [Algebra R P'] [] (x : P) :
↑() () = FractionalIdeal.spanSingleton S (↑(IsLocalization.map P' () (_ : ∀ (y : R), y S↑() y S)) x)
theorem FractionalIdeal.mem_singleton_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {y : P} {I : } :
y y', y' I y = x * y'
theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal {R₁ : Type u_3} [CommRing R₁] (K : Type u_4) [] [Algebra R₁ K] [] {I : Ideal R₁} {J : Ideal R₁} {x : R₁} {y : R₁} (hy : y ) :
FractionalIdeal.spanSingleton () (IsLocalization.mk' K x { val := y, property := 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} [] [Algebra R₁ K] [] {I : Ideal R₁} {J : Ideal R₁} {z : K} :
= J Ideal.span {().fst} * I = Ideal.span {().snd} * J
theorem FractionalIdeal.one_div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] [IsDomain R₁] (x : K) :
@[simp]
theorem FractionalIdeal.div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] [IsDomain R₁] (J : ) (d : K) :
theorem FractionalIdeal.exists_eq_spanSingleton_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] [IsDomain R₁] (I : ) :
a aI, a 0 I = FractionalIdeal.spanSingleton () (↑(algebraMap R₁ K) a)⁻¹ * aI
instance FractionalIdeal.isPrincipal {K : Type u_4} [] {R : Type u_5} [] [] [Algebra R K] [] (I : ) :
theorem FractionalIdeal.le_spanSingleton_mul_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {I : } {J : } :
I ∀ (zI : P), zI IzJ, zJ J x * zJ = zI
theorem FractionalIdeal.spanSingleton_mul_le_iff {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {I : } {J : } :
J ∀ (z : P), z Ix * z J
theorem FractionalIdeal.eq_spanSingleton_mul {R : Type u_1} [] {S : } {P : Type u_2} [] [Algebra R P] [loc : ] {x : P} {I : } {J : } :
I = (∀ (zI : P), zI IzJ, zJ J x * zJ = zI) ∀ (z : P), z Jx * z I
theorem FractionalIdeal.isNoetherian_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] :
IsNoetherian R₁ { x // x 0 }
theorem FractionalIdeal.isNoetherian_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] {I : } :
IsNoetherian R₁ { x // x I } ∀ (J : ), J I
theorem FractionalIdeal.isNoetherian_coeIdeal {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [] (I : Ideal R₁) :
IsNoetherian R₁ { x // x I }
theorem FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] (x : R₁) {I : } (hI : IsNoetherian R₁ { x // x I }) :
IsNoetherian R₁ { x // x ↑(FractionalIdeal.spanSingleton () (↑(algebraMap R₁ K) x)⁻¹ * I) }
theorem FractionalIdeal.isNoetherian {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [] [Algebra R₁ K] [frac : ] [IsDomain R₁] [] (I : ) :
IsNoetherian R₁ { x // x I }

Every fractional ideal of a noetherian integral domain is noetherian.

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

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.

Instances For
@[simp]
theorem FractionalIdeal.adjoinIntegral_coe {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) (hx : ) :
↑() = Subalgebra.toSubmodule (Algebra.adjoin R {x})
theorem FractionalIdeal.mem_adjoinIntegral_self {R : Type u_1} [] (S : ) {P : Type u_2} [] [Algebra R P] [loc : ] (x : P) (hx : ) :
x