# mathlibdocumentation

ring_theory.fractional_ideal

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

• `is_fractional` defines which `R`-submodules of `P` are fractional ideals
• `fractional_ideal S P` is the type of fractional ideals in `P`
• `has_coe_t (ideal R) (fractional_ideal S P)` instance
• `comm_semiring (fractional_ideal S P)` instance: the typical ideal operations generalized to fractional ideals
• `lattice (fractional_ideal 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).

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

## Main statements #

• `mul_left_mono` and `mul_right_mono` state that ideal multiplication is monotone
• `prod_one_self_div_eq` states that `1 / I` is the inverse of `I` if one exists
• `is_noetherian` states that every fractional ideal of a noetherian integral domain is noetherian

## 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 `fractional_ideal` to be the subtype of the predicate `is_fractional`, instead of having `fractional_ideal` 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 `is_localization` 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.

## Tags #

fractional ideal, fractional ideals, invertible ideal

def is_fractional {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] (I : P) :
Prop

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

Equations
• = ∃ (a : R) (H : a S), ∀ (b : P), b I (a b)
def fractional_ideal {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ 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`.

Equations
• = {I // I}
Instances for `fractional_ideal`
@[protected, instance]
def fractional_ideal.submodule.has_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
has_coe P) P)

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

This coercion is typically called `coe_to_submodule` in lemma names (or `coe` when the coercion is clear from the context), not to be confused with `is_localization.coe_submodule : ideal R → submodule R P` (which we use to define `coe : ideal R → fractional_ideal S P`, referred to as `coe_ideal` in theorem names).

Equations
@[protected]
theorem fractional_ideal.is_fractional {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
@[protected, instance]
def fractional_ideal.set_like {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp]
theorem fractional_ideal.mem_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} {x : P} :
x I x I
@[ext]
theorem fractional_ideal.ext {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} :
(∀ (x : P), x I x J)I = J
@[protected]
def fractional_ideal.copy {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (p : P) (s : set P) (hs : s = p) :

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

Equations
@[simp]
theorem fractional_ideal.val_eq_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
I.val = I
@[simp, norm_cast]
theorem fractional_ideal.coe_mk {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) (hI : I) :
I, hI⟩ = I

Transfer instances from `submodule R P` to `fractional_ideal S P`. -

@[protected, instance]
def fractional_ideal.add_comm_group {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
Equations
@[protected, instance]
def fractional_ideal.module {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
I
Equations
theorem fractional_ideal.coe_to_submodule_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
theorem fractional_ideal.is_fractional_of_le_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) (h : I 1) :
theorem fractional_ideal.is_fractional_of_le {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} {J : P} (hIJ : I J) :
@[protected, instance]
def fractional_ideal.coe_to_fractional_ideal {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :

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

This is a bundled version of `is_localization.coe_submodule : ideal R → submodule R P`, which is not to be confused with the `coe : fractional_ideal S P → submodule R P`, also called `coe_to_submodule` in theorem names.

This map is available as a ring hom, called `fractional_ideal.coe_ideal_hom`.

Equations
@[simp, norm_cast]
theorem fractional_ideal.coe_coe_ideal {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : ideal R) :
@[simp]
theorem fractional_ideal.mem_coe_ideal {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] {x : P} {I : ideal R} :
x I ∃ (x' : R), x' I P) x' = x
theorem fractional_ideal.mem_coe_ideal_of_mem {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] {x : R} {I : ideal R} (hx : x I) :
P) x I
theorem fractional_ideal.coe_ideal_le_coe_ideal' {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [ P] (h : S ) {I J : ideal R} :
I J I J
@[simp]
theorem fractional_ideal.coe_ideal_le_coe_ideal {R : Type u_1} [comm_ring R] (K : Type u_2) [comm_ring K] [ K] [ K] {I J : ideal R} :
I J I J
@[protected, instance]
def fractional_ideal.has_zero {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp]
theorem fractional_ideal.mem_zero_iff {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] {x : P} :
x 0 x = 0
@[simp, norm_cast]
theorem fractional_ideal.coe_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
@[simp, norm_cast]
theorem fractional_ideal.coe_to_fractional_ideal_bot {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
@[simp]
theorem fractional_ideal.exists_mem_to_map_eq {R : Type u_1} [comm_ring R] {S : submonoid R} (P : Type u_2) [comm_ring P] [ P] [loc : P] {x : R} {I : ideal R} (h : S ) :
(∃ (x' : R), x' I P) x' = P) x) x I
theorem fractional_ideal.coe_to_fractional_ideal_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (h : S ) :
theorem fractional_ideal.coe_to_fractional_ideal_eq_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {I : ideal R} (hS : S ) :
I = 0 I =
theorem fractional_ideal.coe_to_fractional_ideal_ne_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {I : ideal R} (hS : S ) :
theorem fractional_ideal.coe_to_submodule_eq_bot {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} :
I = I = 0
theorem fractional_ideal.coe_to_submodule_ne_bot {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} :
@[protected, instance]
def fractional_ideal.inhabited {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[protected, instance]
def fractional_ideal.has_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp, norm_cast]
theorem fractional_ideal.coe_ideal_top {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] :
theorem fractional_ideal.mem_one_iff {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] {x : P} :
x 1 ∃ (x' : R), P) x' = x
theorem fractional_ideal.coe_mem_one {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] (x : R) :
P) x 1
theorem fractional_ideal.one_mem_one {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] :
1 1
theorem fractional_ideal.coe_one_eq_coe_submodule_top {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :

`(1 : fractional_ideal 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, norm_cast]
theorem fractional_ideal.coe_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ 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 fractional_ideal.coe_le_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} :
I J I J
theorem fractional_ideal.zero_le {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
0 I
@[protected, instance]
def fractional_ideal.order_bot {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp]
theorem fractional_ideal.bot_eq_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
= 0
@[simp]
theorem fractional_ideal.le_zero_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} :
I 0 I = 0
theorem fractional_ideal.eq_zero_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} :
I = 0 ∀ (x : P), x Ix = 0
theorem is_fractional.sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} :
(I J)
theorem is_fractional.inf_right {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} :
∀ (J : P), (I J)
@[protected, instance]
def fractional_ideal.has_inf {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp, norm_cast]
theorem fractional_ideal.coe_inf {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
(I J) = I J
@[protected, instance]
def fractional_ideal.has_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[norm_cast]
theorem fractional_ideal.coe_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
(I J) = I J
@[protected, instance]
def fractional_ideal.lattice {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[protected, instance]
def fractional_ideal.semilattice_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[protected, instance]
def fractional_ideal.has_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp]
theorem fractional_ideal.sup_eq_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
I J = I + J
@[simp, norm_cast]
theorem fractional_ideal.coe_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
(I + J) = I + J
@[simp, norm_cast]
theorem fractional_ideal.coe_ideal_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : ideal R) :
(I J) = I + J
theorem is_fractional.nsmul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} (n : ) :
(n I)
@[protected, instance]
def fractional_ideal.has_smul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
P)
Equations
@[norm_cast]
theorem fractional_ideal.coe_nsmul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (n : ) (I : P) :
(n I) = n I
theorem is_fractional.mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} :
(I * J)
theorem is_fractional.pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} (h : I) (n : ) :
(I ^ n)
@[irreducible]
def fractional_ideal.mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :

`fractional_ideal.mul` is the product of two fractional ideals, used to define the `has_mul` instance.

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

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

Equations
@[protected, instance]
def fractional_ideal.has_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp]
theorem fractional_ideal.mul_eq_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
I.mul J = I * J
@[simp, norm_cast]
theorem fractional_ideal.coe_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : P) :
(I * J) = I * J
@[simp, norm_cast]
theorem fractional_ideal.coe_ideal_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I J : ideal R) :
(I * J) = I * J
theorem fractional_ideal.mul_left_mono {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
theorem fractional_ideal.mul_right_mono {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
monotone (λ (J : P), J * I)
theorem fractional_ideal.mul_mem_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} {i j : P} (hi : i I) (hj : j J) :
i * j I * J
theorem fractional_ideal.mul_le {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J K : P} :
I * J K ∀ (i : P), i I∀ (j : P), j Ji * j K
@[protected, instance]
def fractional_ideal.nat.has_pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
@[simp, norm_cast]
theorem fractional_ideal.coe_pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) (n : ) :
(I ^ n) = I ^ n
@[protected]
theorem fractional_ideal.mul_induction_on {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} {C : P → Prop} {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
@[protected, instance]
def fractional_ideal.has_nat_cast {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
theorem fractional_ideal.coe_nat_cast {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (n : ) :
@[protected, instance]
def fractional_ideal.comm_semiring {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
Equations
theorem fractional_ideal.add_le_add_left {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} (hIJ : I J) (J' : P) :
J' + I J' + J
theorem fractional_ideal.mul_le_mul_left {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} (hIJ : I J) (J' : P) :
J' * I J' * J
theorem fractional_ideal.le_self_mul_self {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} (hI : 1 I) :
I I * I
theorem fractional_ideal.mul_self_le_self {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : P} (hI : I 1) :
I * I I
theorem fractional_ideal.coe_ideal_le_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I : ideal R} :
I 1
theorem fractional_ideal.le_one_iff_exists_coe_ideal {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {J : P} :
J 1 ∃ (I : ideal R), I = J
@[simp]
theorem fractional_ideal.coe_ideal_hom_apply {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] (ᾰ : ideal R) :
=
def fractional_ideal.coe_ideal_hom {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] :

`coe_ideal_hom (S : submonoid R) P` is `coe : ideal R → fractional_ideal S P` as a ring hom

Equations
theorem fractional_ideal.coe_ideal_pow {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] (I : ideal R) (n : ) :
(I ^ n) = I ^ n
theorem fractional_ideal.coe_ideal_finprod {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] [ P] {α : Sort u_3} {f : α → } (hS : S ) :
(finprod (λ (a : α), f a)) = finprod (λ (a : α), (f a))
theorem is_fractional.map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') {I : P} :
def fractional_ideal.map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') :
P'

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

Equations
• = λ (I : P), , _⟩
@[simp, norm_cast]
theorem fractional_ideal.coe_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') (I : P) :
@[simp]
theorem fractional_ideal.mem_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] {I : P} {g : P →ₐ[R] P'} {y : P'} :
∃ (x : P), x I g x = y
@[simp]
theorem fractional_ideal.map_id {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) :
I = I
@[simp]
theorem fractional_ideal.map_comp {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] {P'' : Type u_4} [comm_ring P''] [ P''] (I : P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P'') :
@[simp, norm_cast]
theorem fractional_ideal.map_coe_ideal {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') (I : ideal R) :
@[simp]
theorem fractional_ideal.map_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') :
@[simp]
theorem fractional_ideal.map_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P →ₐ[R] P') :
@[simp]
theorem fractional_ideal.map_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (I J : P) (g : P →ₐ[R] P') :
(I + J) =
@[simp]
theorem fractional_ideal.map_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (I J : P) (g : P →ₐ[R] P') :
(I * J) =
@[simp]
theorem fractional_ideal.map_map_symm {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (I : P) (g : P ≃ₐ[R] P') :
= I
@[simp]
theorem fractional_ideal.map_symm_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (I : P') (g : P ≃ₐ[R] P') :
= I
theorem fractional_ideal.map_mem_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] {f : P →ₐ[R] P'} (h : function.injective f) {x : P} {I : P} :
f x x I
theorem fractional_ideal.map_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (f : P →ₐ[R] P') (h : function.injective f) :
def fractional_ideal.map_equiv {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P ≃ₐ[R] P') :
≃+* P'

If `g` is an equivalence, `map g` is an isomorphism

Equations
@[simp]
theorem fractional_ideal.coe_fun_map_equiv {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P ≃ₐ[R] P') :
@[simp]
theorem fractional_ideal.map_equiv_apply {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P ≃ₐ[R] P') (I : P) :
@[simp]
theorem fractional_ideal.map_equiv_symm {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {P' : Type u_3} [comm_ring P'] [ P'] (g : P ≃ₐ[R] P') :
@[simp]
theorem fractional_ideal.map_equiv_refl {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] :
theorem fractional_ideal.is_fractional_span_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {s : set P} :
s) ∃ (a : R) (H : a S), ∀ (b : P), b s (a b)
theorem fractional_ideal.is_fractional_of_fg {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {I : P} (hI : I.fg) :
theorem fractional_ideal.mem_span_mul_finite_of_mem_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] {I J : P} {x : P} (hx : x I * J) :
∃ (T T' : finset P), T I T' J x (T * T')
theorem fractional_ideal.coe_ideal_fg {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] (inj : function.injective P)) (I : ideal R) :
theorem fractional_ideal.fg_unit {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P)ˣ) :
theorem fractional_ideal.fg_of_is_unit {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (I : P) (h : is_unit I) :
theorem ideal.fg_of_is_unit {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] (inj : function.injective P)) (I : ideal R) (h : is_unit I) :
I.fg
@[irreducible]
noncomputable def fractional_ideal.canonical_equiv {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] [loc : P] (P' : Type u_3) [comm_ring P'] [ P'] [loc' : P'] :
≃+* P'

`canonical_equiv f f'` is the canonical equivalence between the fractional ideals in `P` and in `P'`

Equations
@[simp]
theorem fractional_ideal.mem_canonical_equiv_apply {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] [loc : P] (P' : Type u_3) [comm_ring P'] [ P'] [loc' : P'] {I : P} {x : P'} :
x P') I ∃ (y : P) (H : y I), (ring_hom.id R) _) y = x
@[simp]
theorem fractional_ideal.canonical_equiv_symm {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] [loc : P] (P' : Type u_3) [comm_ring P'] [ P'] [loc' : P'] :
@[simp]
theorem fractional_ideal.canonical_equiv_flip {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [ P] [loc : P] (P' : Type u_3) [comm_ring P'] [ P'] [loc' : P'] (I : P') :
P') ( P) I) = I

### `is_fraction_ring` section #

This section concerns fractional ideals in the field of fractions, i.e. the type `fractional_ideal R⁰ K` where `is_fraction_ring R K`.

theorem fractional_ideal.exists_ne_zero_mem_is_integer {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] {I : K} [nontrivial R] (hI : I 0) :
∃ (x : R) (H : x 0), K) x I

Nonzero fractional ideals contain a nonzero integer.

theorem fractional_ideal.map_ne_zero {R : Type u_1} [comm_ring R] {K : Type u_3} {K' : Type u_4} [field K] [field K'] [ K] [ K] [ K'] [ K'] {I : K} (h : K →ₐ[R] K') [nontrivial R] (hI : I 0) :
@[simp]
theorem fractional_ideal.map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_3} {K' : Type u_4} [field K] [field K'] [ K] [ K] [ K'] [ K'] {I : K} (h : K →ₐ[R] K') [nontrivial R] :
I = 0
theorem fractional_ideal.coe_ideal_injective {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] :
@[simp]
theorem fractional_ideal.coe_ideal_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] {I : ideal R} :
I = 0 I =
theorem fractional_ideal.coe_ideal_ne_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] {I : ideal R} :
theorem fractional_ideal.coe_ideal_ne_zero {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] {I : ideal R} (hI : I ) :
I 0
@[simp]
theorem fractional_ideal.coe_ideal_eq_one_iff {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [ K] [ K] {I : ideal R} :
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 = non_zero_divisors R`, `R`'s localization at which is a field because `R` is a domain.

@[protected, instance]
def fractional_ideal.nontrivial {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] :
theorem fractional_ideal.ne_zero_of_mul_eq_one {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] (I J : K) (h : I * J = 1) :
I 0
theorem is_fractional.div_of_nonzero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J : K} :
J 0 (I / J)
theorem fractional_ideal.fractional_div_of_nonzero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J : K} (h : J 0) :
(I / J)
@[protected, instance]
noncomputable def fractional_ideal.fractional_ideal_has_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] :
Equations
@[simp]
theorem fractional_ideal.div_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I : K} :
I / 0 = 0
theorem fractional_ideal.div_nonzero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J : K} (h : J 0) :
I / J = I / J, _⟩
@[simp]
theorem fractional_ideal.coe_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J : K} (hJ : J 0) :
(I / J) = I / J
theorem fractional_ideal.mem_div_iff_of_nonzero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J : K} (h : J 0) {x : K} :
x I / J ∀ (y : K), y Jx * y I
theorem fractional_ideal.mul_one_div_le_one {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I : K} :
I * (1 / I) 1
theorem fractional_ideal.le_self_mul_one_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I : K} (hI : I 1) :
I I * (1 / I)
theorem fractional_ideal.le_div_iff_of_nonzero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J J' : K} (hJ' : J' 0) :
I J / J' ∀ (x : K), x I∀ (y : K), y J'x * y J
theorem fractional_ideal.le_div_iff_mul_le {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I J J' : K} (hJ' : J' 0) :
I J / J' I * J' J
@[simp]
theorem fractional_ideal.div_one {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I : K} :
I / 1 = I
theorem fractional_ideal.eq_one_div_of_mul_eq_one_right {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] (I J : K) (h : I * J = 1) :
J = 1 / I
theorem fractional_ideal.mul_div_self_cancel_iff {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {I : K} :
I * (1 / I) = 1 ∃ (J : , I * J = 1
@[simp]
theorem fractional_ideal.map_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {K' : Type u_5} [field K'] [algebra R₁ K'] [ K'] (I J : K) (h : K ≃ₐ[R₁] K') :
(I / J) =
@[simp]
theorem fractional_ideal.map_one_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] {K' : Type u_5} [field K'] [algebra R₁ K'] [ K'] (I : K) (h : K ≃ₐ[R₁] K') :
(1 / I) =
theorem fractional_ideal.eq_zero_or_one {K : Type u_4} {L : Type u_5} [field K] [field L] [ L] [ L] (I : L) :
I = 0 I = 1
theorem fractional_ideal.eq_zero_or_one_of_is_field {R₁ : Type u_3} {K : Type u_4} [comm_ring R₁] [field K] [algebra R₁ K] [ K] (hF : is_field R₁) (I : K) :
I = 0 I = 1
def fractional_ideal.span_finset (R₁ : Type u_3) [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] {ι : Type u_1} (s : finset ι) (f : ι → K) :

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

Equations
@[simp]
theorem fractional_ideal.span_finset_coe (R₁ : Type u_3) [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] {ι : Type u_1} (s : finset ι) (f : ι → K) :
f) = (f '' s)
@[simp]
theorem fractional_ideal.span_finset_eq_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] {ι : Type u_1} {s : finset ι} {f : ι → K} :
= 0 ∀ (j : ι), j sf j = 0
theorem fractional_ideal.span_finset_ne_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] {ι : Type u_1} {s : finset ι} {f : ι → K} :
0 ∃ (j : ι) (H : j s), f j 0
theorem fractional_ideal.is_fractional_span_singleton {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) :
{x})
@[irreducible]
def fractional_ideal.span_singleton {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) :

`span_singleton x` is the fractional ideal generated by `x` if `0 ∉ S`

Equations
@[simp]
theorem fractional_ideal.coe_span_singleton {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) :
= {x}
@[simp]
theorem fractional_ideal.mem_span_singleton {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] {x y : P} :
∃ (z : R), z y = x
theorem fractional_ideal.mem_span_singleton_self {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) :
theorem fractional_ideal.span_singleton_eq_span_singleton {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {x y : P} :
∃ (z : Rˣ), z x = y
theorem fractional_ideal.eq_span_singleton_of_principal {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (I : P) [I.is_principal] :
theorem fractional_ideal.is_principal_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (I : P) :
I.is_principal ∃ (x : P),
@[simp]
theorem fractional_ideal.span_singleton_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] :
theorem fractional_ideal.span_singleton_eq_zero_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {y : P} :
y = 0
theorem fractional_ideal.span_singleton_ne_zero_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {y : P} :
y 0
@[simp]
theorem fractional_ideal.span_singleton_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] :
@[simp]
theorem fractional_ideal.span_singleton_mul_span_singleton {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (x y : P) :
@[simp]
theorem fractional_ideal.span_singleton_pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) (n : ) :
@[simp]
theorem fractional_ideal.coe_ideal_span_singleton {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : R) :
(ideal.span {x}) = ( P) x)
@[simp]
theorem fractional_ideal.canonical_equiv_span_singleton {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {P' : Type u_3} [comm_ring P'] [ P'] [ P'] (x : P) :
= ( (ring_hom.id R) _) x)
theorem fractional_ideal.mem_singleton_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {x y : P} {I : P} :
∃ (y' : P) (H : y' I), y = x * y'
theorem fractional_ideal.mk'_mul_coe_ideal_eq_coe_ideal {R₁ : Type u_3} [comm_ring R₁] (K : Type u_4) [field K] [algebra R₁ K] [ K] {I J : ideal R₁} {x y : R₁} (hy : y ) :
y, hy⟩) * I = J ideal.span {x} * I = ideal.span {y} * J
theorem fractional_ideal.span_singleton_mul_coe_ideal_eq_coe_ideal {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] {I J : ideal R₁} {z : K} :
theorem fractional_ideal.one_div_span_singleton {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] [is_domain R₁] (x : K) :
@[simp]
theorem fractional_ideal.div_span_singleton {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] [is_domain R₁] (J : K) (d : K) :
theorem fractional_ideal.exists_eq_span_singleton_mul {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [ K] [is_domain R₁] (I : K) :
∃ (a : R₁) (aI : ideal R₁), a 0 I = ((algebra_map R₁ K) a)⁻¹ * aI
@[protected, instance]
def fractional_ideal.is_principal {K : Type u_4} [field K] {R : Type u_1} [comm_ring R] [is_domain R] [ K] [ K] (I : K) :
theorem fractional_ideal.le_span_singleton_mul_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {x : P} {I J : P} :
∀ (zI : P), zI I(∃ (zJ : P) (H : zJ J), x * zJ = zI)
theorem fractional_ideal.span_singleton_mul_le_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {x : P} {I J : P} :
∀ (z : P), z Ix * z J
theorem fractional_ideal.eq_span_singleton_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [ P] [loc : P] {x : P} {I J : P} :
(∀ (zI : P), zI I(∃ (zJ : P) (H : zJ J), x * zJ = zI)) ∀ (z : P), z Jx * z I
theorem fractional_ideal.is_noetherian_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] :
0
theorem fractional_ideal.is_noetherian_iff {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] {I : K} :
I ∀ (J : , J IJ.fg
theorem fractional_ideal.is_noetherian_coe_to_fractional_ideal {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] (I : ideal R₁) :
theorem fractional_ideal.is_noetherian_span_singleton_inv_to_map_mul {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] (x : R₁) {I : K} (hI : I) :
((algebra_map R₁ K) x)⁻¹ * I)
theorem fractional_ideal.is_noetherian {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : K] [is_domain R₁] (I : K) :
I

Every fractional ideal of a noetherian integral domain is noetherian.

theorem fractional_ideal.is_fractional_adjoin_integral {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) (hx : x) :

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

@[simp]
theorem fractional_ideal.adjoin_integral_coe {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) (hx : x) :
hx) = {x}).to_submodule
def fractional_ideal.adjoin_integral {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) (hx : x) :

`fractional_ideal.adjoin_integral (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
theorem fractional_ideal.mem_adjoin_integral_self {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [ P] [loc : P] (x : P) (hx : x) :