mathlib3 documentation

ring_theory.fractional_ideal

Fractional ideals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

References #

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

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] [algebra R P] (I : submodule R P) :

Prop

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

Equations

is_fractional S I = ∃ (a : R) (H : a ∈ S), ∀ (b : P), b ∈ I → is_localization.is_integer R (a • b)

def fractional_ideal {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [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.

Equations

fractional_ideal S P = {I // is_fractional S 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] [algebra R P] :

has_coe (fractional_ideal S P) (submodule R 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).

Equations

fractional_ideal.submodule.has_coe = {coe := λ (I : fractional_ideal S P), I.val}

@[protected]

theorem fractional_ideal.is_fractional {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I : fractional_ideal S P) :

is_fractional S ↑I

@[protected, instance]

def fractional_ideal.set_like {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

set_like (fractional_ideal S P) P

Equations

fractional_ideal.set_like = {coe := λ (I : fractional_ideal S P), ↑↑I, coe_injective' := _}

@[simp]

theorem fractional_ideal.mem_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : fractional_ideal S 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] [algebra R P] {I J : fractional_ideal S 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] [algebra R P] (p : fractional_ideal S P) (s : set P) (hs : s = ↑p) :

fractional_ideal S P

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

Equations

p.copy s hs = ⟨↑p.copy s hs, _⟩

@[simp]

theorem fractional_ideal.coe_copy {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (p : fractional_ideal S P) (s : set P) (hs : s = ↑p) :

↑(p.copy s hs) = s

theorem fractional_ideal.coe_eq {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (p : fractional_ideal S P) (s : set P) (hs : s = ↑p) :

p.copy s hs = p

@[simp]

theorem fractional_ideal.val_eq_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I : fractional_ideal S P) :

@[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] [algebra R P] (I : submodule R P) (hI : is_fractional S 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] [algebra R P] (I : fractional_ideal S P) :

add_comm_group ↥I

Equations

I.add_comm_group = ↑I.add_comm_group

@[protected, instance]

def fractional_ideal.module {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I : fractional_ideal S P) :

Equations

I.module = ↑I.module

theorem fractional_ideal.coe_to_submodule_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

function.injective coe

theorem fractional_ideal.coe_to_submodule_inj {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I J : fractional_ideal S P} :

↑I = ↑J ↔ I = J

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] [algebra R P] (I : submodule R P) (h : I ≤ 1) :

is_fractional S I

theorem fractional_ideal.is_fractional_of_le {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : submodule R P} {J : fractional_ideal S P} (hIJ : I ≤ ↑J) :

is_fractional S I

@[protected, instance]

def fractional_ideal.has_coe_t {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

has_coe_t (ideal R) (fractional_ideal S 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

fractional_ideal.has_coe_t = {coe := λ (I : ideal R), ⟨is_localization.coe_submodule P I, _⟩}

@[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] [algebra R P] (I : ideal R) :

↑↑I = is_localization.coe_submodule P I

@[simp]

theorem fractional_ideal.mem_coe_ideal {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [algebra R P] {x : P} {I : ideal R} :

x ∈ ↑I ↔ ∃ (x' : R), x' ∈ I ∧ ⇑(algebra_map R 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] [algebra R P] {x : R} {I : ideal R} (hx : x ∈ I) :

⇑(algebra_map R 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] [algebra R P] [is_localization S P] (h : S ≤ non_zero_divisors R) {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] [algebra R K] [is_fraction_ring R 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] [algebra R P] :

has_zero (fractional_ideal S P)

Equations

fractional_ideal.has_zero S = {zero := ↑0}

@[simp]

theorem fractional_ideal.mem_zero_iff {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [algebra R 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] [algebra R P] :

@[simp, norm_cast]

theorem fractional_ideal.coe_ideal_bot {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R 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] [algebra R P] [loc : is_localization S P] {x : R} {I : ideal R} (h : S ≤ non_zero_divisors R) :

(∃ (x' : R), x' ∈ I ∧ ⇑(algebra_map R P) x' = ⇑(algebra_map R P) x) ↔ x ∈ I

theorem fractional_ideal.coe_ideal_injective' {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (h : S ≤ non_zero_divisors R) :

function.injective coe

theorem fractional_ideal.coe_ideal_inj' {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (h : S ≤ non_zero_divisors R) {I J : ideal R} :

↑I = ↑J ↔ I = J

@[simp]

theorem fractional_ideal.coe_ideal_eq_zero' {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] {I : ideal R} (h : S ≤ non_zero_divisors R) :

↑I = 0 ↔ I = ⊥

theorem fractional_ideal.coe_ideal_ne_zero' {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] {I : ideal R} (h : S ≤ non_zero_divisors R) :

↑I ≠ 0 ↔ I ≠ ⊥

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] [algebra R P] {I : fractional_ideal S 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] [algebra R P] {I : fractional_ideal S P} :

↑I ≠ ⊥ ↔ I ≠ 0

@[protected, instance]

def fractional_ideal.inhabited {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

inhabited (fractional_ideal S P)

Equations

fractional_ideal.inhabited = {default := 0}

@[protected, instance]

def fractional_ideal.has_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

has_one (fractional_ideal S P)

Equations

fractional_ideal.has_one = {one := ↑⊤}

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

theorem fractional_ideal.mem_one_iff {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [algebra R P] {x : P} :

x ∈ 1 ↔ ∃ (x' : R), ⇑(algebra_map 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] [algebra R P] (x : R) :

⇑(algebra_map 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] [algebra R 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] [algebra R P] :

↑1 = is_localization.coe_submodule 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] [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 fractional_ideal.coe_le_coe {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I J : fractional_ideal S 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] [algebra R P] (I : fractional_ideal S 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] [algebra R P] :

order_bot (fractional_ideal S P)

Equations

fractional_ideal.order_bot = {bot := 0, bot_le := _}

@[simp]

theorem fractional_ideal.bot_eq_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

@[simp]

theorem fractional_ideal.le_zero_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : fractional_ideal S 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] [algebra R P] {I : fractional_ideal S P} :

I = 0 ↔ ∀ (x : P), x ∈ I → x = 0

theorem is_fractional.sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I J : submodule R P} :

is_fractional S I → is_fractional S J → is_fractional S (I ⊔ J)

theorem is_fractional.inf_right {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : submodule R P} :

is_fractional S I → ∀ (J : submodule R P), is_fractional S (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] [algebra R P] :

has_inf (fractional_ideal S P)

Equations

fractional_ideal.has_inf = {inf := λ (I J : fractional_ideal S P), ⟨↑I ⊓ ↑J, _⟩}

@[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] [algebra R P] (I J : fractional_ideal S 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] [algebra R P] :

has_sup (fractional_ideal S P)

Equations

fractional_ideal.has_sup = {sup := λ (I J : fractional_ideal S P), ⟨↑I ⊔ ↑J, _⟩}

@[norm_cast]

theorem fractional_ideal.coe_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I J : fractional_ideal S 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] [algebra R P] :

lattice (fractional_ideal S P)

Equations

fractional_ideal.lattice = function.injective.lattice coe fractional_ideal.lattice._proof_1 fractional_ideal.coe_sup fractional_ideal.coe_inf

@[protected, instance]

def fractional_ideal.semilattice_sup {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

semilattice_sup (fractional_ideal S P)

Equations

fractional_ideal.semilattice_sup = {sup := lattice.sup fractional_ideal.lattice, le := lattice.le fractional_ideal.lattice, lt := lattice.lt fractional_ideal.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

@[protected, instance]

def fractional_ideal.has_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

has_add (fractional_ideal S P)

Equations

fractional_ideal.has_add = {add := has_sup.sup fractional_ideal.has_sup}

@[simp]

theorem fractional_ideal.sup_eq_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I J : fractional_ideal S 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] [algebra R P] (I J : fractional_ideal S 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] [algebra R 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] [algebra R P] {I : submodule R P} (n : ℕ) :

is_fractional S I → is_fractional S (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] [algebra R P] :

has_smul ℕ (fractional_ideal S P)

Equations

fractional_ideal.has_smul = {smul := λ (n : ℕ) (I : fractional_ideal S P), ⟨n • ↑I, _⟩}

@[norm_cast]

theorem fractional_ideal.coe_nsmul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (n : ℕ) (I : fractional_ideal S 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] [algebra R P] {I J : submodule R P} :

is_fractional S I → is_fractional S J → is_fractional S (I * J)

theorem is_fractional.pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : submodule R P} (h : is_fractional S I) (n : ℕ) :

is_fractional S (I ^ n)

@[irreducible]

def fractional_ideal.mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I J : fractional_ideal S P) :

fractional_ideal S 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

I.mul J = ⟨↑I * ↑J, _⟩

@[protected, instance]

def fractional_ideal.has_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

has_mul (fractional_ideal S P)

Equations

fractional_ideal.has_mul = {mul := λ (I J : fractional_ideal S P), I.mul J}

@[simp]

theorem fractional_ideal.mul_eq_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I J : fractional_ideal S P) :

I.mul J = I * J

theorem fractional_ideal.mul_def {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I J : fractional_ideal S P) :

I * 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] [algebra R P] (I J : fractional_ideal S 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] [algebra R 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] [algebra R P] (I : fractional_ideal S P) :

monotone (has_mul.mul I)

theorem fractional_ideal.mul_right_mono {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I : fractional_ideal S P) :

monotone (λ (J : fractional_ideal S 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] [algebra R P] {I J : fractional_ideal S 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] [algebra R P] {I J K : fractional_ideal S P} :

I * J ≤ K ↔ ∀ (i : P), i ∈ I → ∀ (j : P), j ∈ J → i * 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] [algebra R P] :

has_pow (fractional_ideal S P) ℕ

Equations

fractional_ideal.nat.has_pow = {pow := λ (I : fractional_ideal S P) (n : ℕ), ⟨↑I ^ n, _⟩}

@[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] [algebra R P] (I : fractional_ideal S 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] [algebra R P] {I J : fractional_ideal S P} {C : P → Prop} {r : P} (hr : r ∈ I * J) (hm : ∀ (i : P), i ∈ I → ∀ (j : P), j ∈ J → C (i * j)) (ha : ∀ (x y : P), C x → C y → C (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] [algebra R P] :

has_nat_cast (fractional_ideal S P)

Equations

fractional_ideal.has_nat_cast = {nat_cast := nat.unary_cast fractional_ideal.has_add}

theorem fractional_ideal.coe_nat_cast {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R 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] [algebra R P] :

comm_semiring (fractional_ideal S P)

Equations

fractional_ideal.comm_semiring = function.injective.comm_semiring coe fractional_ideal.comm_semiring._proof_1 fractional_ideal.coe_zero fractional_ideal.coe_one fractional_ideal.coe_add fractional_ideal.coe_mul fractional_ideal.comm_semiring._proof_2 fractional_ideal.coe_pow fractional_ideal.coe_nat_cast

def fractional_ideal.coe_submodule_hom {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] :

fractional_ideal S P →+* submodule R P

fractional_ideal.submodule.has_coe as a bundled ring_hom.

Equations

fractional_ideal.coe_submodule_hom S P = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem fractional_ideal.coe_submodule_hom_apply {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] (ᾰ : fractional_ideal S P) :

⇑(fractional_ideal.coe_submodule_hom S P) ᾰ = ↑ᾰ

theorem fractional_ideal.add_le_add_left {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I J : fractional_ideal S P} (hIJ : I ≤ J) (J' : fractional_ideal S 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] [algebra R P] {I J : fractional_ideal S P} (hIJ : I ≤ J) (J' : fractional_ideal S 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] [algebra R P] {I : fractional_ideal S 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] [algebra R P] {I : fractional_ideal S 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] [algebra R P] {I : ideal R} :

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] [algebra R P] {J : fractional_ideal S P} :

J ≤ 1 ↔ ∃ (I : ideal R), ↑I = J

@[simp]

theorem fractional_ideal.one_le {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {I : fractional_ideal S P} :

1 ≤ I ↔ 1 ∈ I

@[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] [algebra R P] (ᾰ : ideal R) :

⇑(fractional_ideal.coe_ideal_hom S P) ᾰ = ↑ᾰ

def fractional_ideal.coe_ideal_hom {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] :

ideal R →+* fractional_ideal S P

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

Equations

fractional_ideal.coe_ideal_hom S P = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

theorem fractional_ideal.coe_ideal_pow {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R 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] [algebra R P] [is_localization S P] {α : Sort u_3} {f : α → ideal R} (hS : S ≤ non_zero_divisors R) :

↑(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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') {I : submodule R P} :

is_fractional S I → is_fractional S (submodule.map g.to_linear_map I)

def fractional_ideal.map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') :

fractional_ideal S P → fractional_ideal S P'

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

Equations

fractional_ideal.map g = λ (I : fractional_ideal S P), ⟨submodule.map g.to_linear_map ↑I, _⟩

@[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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') (I : fractional_ideal S P) :

↑(fractional_ideal.map g I) = submodule.map g.to_linear_map ↑I

@[simp]

theorem fractional_ideal.mem_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] {I : fractional_ideal S P} {g : P →ₐ[R] P'} {y : P'} :

y ∈ fractional_ideal.map g I ↔ ∃ (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] [algebra R P] (I : fractional_ideal S P) :

fractional_ideal.map (alg_hom.id R 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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] {P'' : Type u_4} [comm_ring P''] [algebra R P''] (I : fractional_ideal S P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P'') :

fractional_ideal.map (g'.comp g) I = fractional_ideal.map g' (fractional_ideal.map g I)

@[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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') (I : ideal R) :

fractional_ideal.map g ↑I = ↑I

@[simp]

theorem fractional_ideal.map_one {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') :

fractional_ideal.map g 1 = 1

@[simp]

theorem fractional_ideal.map_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P →ₐ[R] P') :

fractional_ideal.map g 0 = 0

@[simp]

theorem fractional_ideal.map_add {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (I J : fractional_ideal S P) (g : P →ₐ[R] P') :

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

@[simp]

theorem fractional_ideal.map_mul {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (I J : fractional_ideal S P) (g : P →ₐ[R] P') :

fractional_ideal.map g (I * J) = fractional_ideal.map g I * fractional_ideal.map g 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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (I : fractional_ideal S P) (g : P ≃ₐ[R] P') :

fractional_ideal.map ↑(g.symm) (fractional_ideal.map ↑g I) = 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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (I : fractional_ideal S P') (g : P ≃ₐ[R] P') :

fractional_ideal.map ↑g (fractional_ideal.map ↑(g.symm) I) = I

theorem fractional_ideal.map_mem_map {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] {f : P →ₐ[R] P'} (h : function.injective ⇑f) {x : P} {I : fractional_ideal S P} :

⇑f x ∈ fractional_ideal.map f I ↔ x ∈ I

theorem fractional_ideal.map_injective {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (f : P →ₐ[R] P') (h : function.injective ⇑f) :

function.injective (fractional_ideal.map f)

def fractional_ideal.map_equiv {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P ≃ₐ[R] P') :

fractional_ideal S P ≃+* fractional_ideal S P'

If g is an equivalence, map g is an isomorphism

Equations

fractional_ideal.map_equiv g = {to_fun := fractional_ideal.map ↑g, inv_fun := fractional_ideal.map ↑(g.symm), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[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] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P ≃ₐ[R] P') :

⇑(fractional_ideal.map_equiv g) = fractional_ideal.map ↑g

@[simp]

theorem fractional_ideal.map_equiv_apply {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P ≃ₐ[R] P') (I : fractional_ideal S P) :

⇑(fractional_ideal.map_equiv g) I = fractional_ideal.map ↑g I

@[simp]

theorem fractional_ideal.map_equiv_symm {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] {P' : Type u_3} [comm_ring P'] [algebra R P'] (g : P ≃ₐ[R] P') :

(fractional_ideal.map_equiv g).symm = fractional_ideal.map_equiv g.symm

@[simp]

theorem fractional_ideal.map_equiv_refl {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] :

fractional_ideal.map_equiv alg_equiv.refl = ring_equiv.refl (fractional_ideal S 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] [algebra R P] {s : set P} :

is_fractional S (submodule.span R s) ↔ ∃ (a : R) (H : a ∈ S), ∀ (b : P), b ∈ s → is_localization.is_integer R (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] [algebra R P] [loc : is_localization S P] {I : submodule R P} (hI : I.fg) :

is_fractional S I

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] [algebra R P] {I J : fractional_ideal S P} {x : P} (hx : x ∈ I * J) :

∃ (T T' : finset P), ↑T ⊆ ↑I ∧ ↑T' ⊆ ↑J ∧ x ∈ submodule.span R (↑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] [algebra R P] (inj : function.injective ⇑(algebra_map R P)) (I : ideal R) :

↑↑I.fg ↔ I.fg

theorem fractional_ideal.fg_unit {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] (I : (fractional_ideal S 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] [algebra R P] (I : fractional_ideal S 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] [algebra R P] (inj : function.injective ⇑(algebra_map R 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] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] :

fractional_ideal S P ≃+* fractional_ideal S P'

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

Equations

fractional_ideal.canonical_equiv S P P' = fractional_ideal.map_equiv {to_fun := (is_localization.ring_equiv_of_ring_equiv P P' (ring_equiv.refl R) _).to_fun, inv_fun := (is_localization.ring_equiv_of_ring_equiv P P' (ring_equiv.refl R) _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[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] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] {I : fractional_ideal S P} {x : P'} :

x ∈ ⇑(fractional_ideal.canonical_equiv S P P') I ↔ ∃ (y : P) (H : y ∈ I), ⇑(is_localization.map P' (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] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] :

(fractional_ideal.canonical_equiv S P P').symm = fractional_ideal.canonical_equiv S P' P

theorem fractional_ideal.canonical_equiv_flip {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] (I : fractional_ideal S P') :

⇑(fractional_ideal.canonical_equiv S P P') (⇑(fractional_ideal.canonical_equiv S P' P) I) = I

@[simp]

theorem fractional_ideal.canonical_equiv_canonical_equiv {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] (P'' : Type u_4) [comm_ring P''] [algebra R P''] [is_localization S P''] (I : fractional_ideal S P) :

⇑(fractional_ideal.canonical_equiv S P' P'') (⇑(fractional_ideal.canonical_equiv S P P') I) = ⇑(fractional_ideal.canonical_equiv S P P'') I

theorem fractional_ideal.canonical_equiv_trans_canonical_equiv {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] (P'' : Type u_4) [comm_ring P''] [algebra R P''] [is_localization S P''] :

(fractional_ideal.canonical_equiv S P P').trans (fractional_ideal.canonical_equiv S P' P'') = fractional_ideal.canonical_equiv S P P''

@[simp]

theorem fractional_ideal.canonical_equiv_coe_ideal {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] [loc : is_localization S P] (P' : Type u_3) [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] (I : ideal R) :

⇑(fractional_ideal.canonical_equiv S P P') ↑I = ↑I

@[simp]

theorem fractional_ideal.canonical_equiv_self {R : Type u_1} [comm_ring R] (S : submonoid R) (P : Type u_2) [comm_ring P] [algebra R P] [loc : is_localization S P] :

fractional_ideal.canonical_equiv S P P = ring_equiv.refl (fractional_ideal S P)

`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] [algebra R K] [is_fraction_ring R K] {I : fractional_ideal (non_zero_divisors R) K} [nontrivial R] (hI : I ≠ 0) :

∃ (x : R) (H : x ≠ 0), ⇑(algebra_map R 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'] [algebra R K] [is_fraction_ring R K] [algebra R K'] [is_fraction_ring R K'] {I : fractional_ideal (non_zero_divisors R) K} (h : K →ₐ[R] K') [nontrivial R] (hI : I ≠ 0) :

fractional_ideal.map h 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'] [algebra R K] [is_fraction_ring R K] [algebra R K'] [is_fraction_ring R K'] {I : fractional_ideal (non_zero_divisors R) K} (h : K →ₐ[R] K') [nontrivial R] :

fractional_ideal.map h I = 0 ↔ I = 0

theorem fractional_ideal.coe_ideal_injective {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R K] :

function.injective coe

theorem fractional_ideal.coe_ideal_inj {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R K] {I J : ideal R} :

↑I = ↑J ↔ I = J

@[simp]

theorem fractional_ideal.coe_ideal_eq_zero {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R K] {I : ideal R} :

↑I = 0 ↔ I = ⊥

theorem fractional_ideal.coe_ideal_ne_zero {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R K] {I : ideal R} :

↑I ≠ 0 ↔ I ≠ ⊥

@[simp]

theorem fractional_ideal.coe_ideal_eq_one {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R K] {I : ideal R} :

↑I = 1 ↔ I = 1

theorem fractional_ideal.coe_ideal_ne_one {R : Type u_1} [comm_ring R] {K : Type u_3} [field K] [algebra R K] [is_fraction_ring R 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] :

nontrivial (fractional_ideal (non_zero_divisors 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 : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J : submodule R₁ K} :

is_fractional (non_zero_divisors R₁) I → is_fractional (non_zero_divisors R₁) J → J ≠ 0 → is_fractional (non_zero_divisors R₁) (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 : is_fraction_ring R₁ K] [is_domain R₁] {I J : fractional_ideal (non_zero_divisors R₁) K} (h : J ≠ 0) :

is_fractional (non_zero_divisors R₁) (↑I / ↑J)

@[protected, instance]

noncomputable def fractional_ideal.has_div {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : is_fraction_ring R₁ K] [is_domain R₁] :

has_div (fractional_ideal (non_zero_divisors R₁) K)

Equations

fractional_ideal.has_div = {div := λ (I J : fractional_ideal (non_zero_divisors R₁) K), dite (J = 0) (λ (h : J = 0), 0) (λ (h : ¬J = 0), ⟨↑I / ↑J, _⟩)}

@[simp]

theorem fractional_ideal.div_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [frac : is_fraction_ring R₁ K] [is_domain R₁] {I : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J : fractional_ideal (non_zero_divisors R₁) K} (h : J ≠ 0) {x : K} :

x ∈ I / J ↔ ∀ (y : K), y ∈ J → x * 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 : is_fraction_ring R₁ K] [is_domain R₁] {I : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J J' : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I J J' : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] (I J : fractional_ideal (non_zero_divisors R₁) 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 : is_fraction_ring R₁ K] [is_domain R₁] {I : fractional_ideal (non_zero_divisors R₁) K} :

I * (1 / I) = 1 ↔ ∃ (J : fractional_ideal (non_zero_divisors R₁) K), 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 : is_fraction_ring R₁ K] [is_domain R₁] {K' : Type u_5} [field K'] [algebra R₁ K'] [is_fraction_ring R₁ K'] (I J : fractional_ideal (non_zero_divisors R₁) K) (h : K ≃ₐ[R₁] K') :

fractional_ideal.map ↑h (I / J) = fractional_ideal.map ↑h I / fractional_ideal.map ↑h 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 : is_fraction_ring R₁ K] [is_domain R₁] {K' : Type u_5} [field K'] [algebra R₁ K'] [is_fraction_ring R₁ K'] (I : fractional_ideal (non_zero_divisors R₁) K) (h : K ≃ₐ[R₁] K') :

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

theorem fractional_ideal.eq_zero_or_one {K : Type u_4} {L : Type u_5} [field K] [field L] [algebra K L] [is_fraction_ring K L] (I : fractional_ideal (non_zero_divisors K) 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] [is_fraction_ring R₁ K] (hF : is_field R₁) (I : fractional_ideal (non_zero_divisors R₁) 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] [is_fraction_ring R₁ K] {ι : Type u_1} (s : finset ι) (f : ι → K) :

fractional_ideal (non_zero_divisors R₁) K

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

Equations

fractional_ideal.span_finset R₁ s f = ⟨submodule.span R₁ (f '' ↑s), _⟩

@[simp]

theorem fractional_ideal.span_finset_coe (R₁ : Type u_3) [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [is_fraction_ring R₁ K] {ι : Type u_1} (s : finset ι) (f : ι → K) :

↑(fractional_ideal.span_finset R₁ s f) = submodule.span R₁ (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] [is_fraction_ring R₁ K] {ι : Type u_1} {s : finset ι} {f : ι → K} :

fractional_ideal.span_finset R₁ s f = 0 ↔ ∀ (j : ι), j ∈ s → f 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] [is_fraction_ring R₁ K] {ι : Type u_1} {s : finset ι} {f : ι → K} :

fractional_ideal.span_finset R₁ s f ≠ 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] [algebra R P] [loc : is_localization S P] (x : P) :

is_fractional S (submodule.span R {x})

@[irreducible]

def fractional_ideal.span_singleton {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (x : P) :

fractional_ideal S P

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

Equations

fractional_ideal.span_singleton S x = ⟨submodule.span R {x}, _⟩

@[simp]

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

↑(fractional_ideal.span_singleton S x) = submodule.span R {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] [algebra R P] [loc : is_localization S P] {x y : P} :

x ∈ fractional_ideal.span_singleton S y ↔ ∃ (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] [algebra R P] [loc : is_localization S P] (x : P) :

x ∈ fractional_ideal.span_singleton S x

@[simp]

theorem fractional_ideal.span_singleton_le_iff_mem {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] {x : P} {I : fractional_ideal S P} :

fractional_ideal.span_singleton S x ≤ I ↔ x ∈ I

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] [algebra R P] [loc : is_localization S P] [no_zero_smul_divisors R P] {x y : P} :

fractional_ideal.span_singleton S x = fractional_ideal.span_singleton S y ↔ ∃ (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] [algebra R P] [loc : is_localization S P] (I : fractional_ideal S P) [↑I.is_principal] :

I = fractional_ideal.span_singleton S (submodule.is_principal.generator ↑I)

theorem fractional_ideal.is_principal_iff {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (I : fractional_ideal S P) :

↑I.is_principal ↔ ∃ (x : P), I = fractional_ideal.span_singleton S x

@[simp]

theorem fractional_ideal.span_singleton_zero {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] :

fractional_ideal.span_singleton S 0 = 0

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] [algebra R P] [loc : is_localization S P] {y : P} :

fractional_ideal.span_singleton S y = 0 ↔ 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] [algebra R P] [loc : is_localization S P] {y : P} :

fractional_ideal.span_singleton S y ≠ 0 ↔ 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] [algebra R P] [loc : is_localization S P] :

fractional_ideal.span_singleton S 1 = 1

@[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] [algebra R P] [loc : is_localization S P] (x y : P) :

fractional_ideal.span_singleton S x * fractional_ideal.span_singleton S y = fractional_ideal.span_singleton S (x * y)

@[simp]

theorem fractional_ideal.span_singleton_pow {R : Type u_1} [comm_ring R] {S : submonoid R} {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (x : P) (n : ℕ) :

fractional_ideal.span_singleton S x ^ n = fractional_ideal.span_singleton S (x ^ 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] [algebra R P] [loc : is_localization S P] (x : R) :

↑(ideal.span {x}) = fractional_ideal.span_singleton S (⇑(algebra_map R 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] [algebra R P] [loc : is_localization S P] {P' : Type u_3} [comm_ring P'] [algebra R P'] [is_localization S P'] (x : P) :

⇑(fractional_ideal.canonical_equiv S P P') (fractional_ideal.span_singleton S x) = fractional_ideal.span_singleton S (⇑(is_localization.map 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] [algebra R P] [loc : is_localization S P] {x y : P} {I : fractional_ideal S P} :

y ∈ fractional_ideal.span_singleton S x * I ↔ ∃ (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] [is_fraction_ring R₁ K] {I J : ideal R₁} {x y : R₁} (hy : y ∈ non_zero_divisors R₁) :

fractional_ideal.span_singleton (non_zero_divisors R₁) (is_localization.mk' K x ⟨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] [is_fraction_ring R₁ K] {I J : ideal R₁} {z : K} :

fractional_ideal.span_singleton (non_zero_divisors R₁) z * ↑I = ↑J ↔ ideal.span {(is_localization.sec (non_zero_divisors R₁) z).fst} * I = ideal.span {↑((is_localization.sec (non_zero_divisors R₁) z).snd)} * J

theorem fractional_ideal.one_div_span_singleton {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [is_fraction_ring R₁ K] [is_domain R₁] (x : K) :

1 / fractional_ideal.span_singleton (non_zero_divisors R₁) x = fractional_ideal.span_singleton (non_zero_divisors R₁) x⁻¹

@[simp]

theorem fractional_ideal.div_span_singleton {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [is_fraction_ring R₁ K] [is_domain R₁] (J : fractional_ideal (non_zero_divisors R₁) K) (d : K) :

J / fractional_ideal.span_singleton (non_zero_divisors R₁) d = fractional_ideal.span_singleton (non_zero_divisors R₁) d⁻¹ * J

theorem fractional_ideal.exists_eq_span_singleton_mul {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [is_fraction_ring R₁ K] [is_domain R₁] (I : fractional_ideal (non_zero_divisors R₁) K) :

∃ (a : R₁) (aI : ideal R₁), a ≠ 0 ∧ I = fractional_ideal.span_singleton (non_zero_divisors R₁) (⇑(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] [is_principal_ideal_ring R] [algebra R K] [is_fraction_ring R K] (I : fractional_ideal (non_zero_divisors R) K) :

↑I.is_principal

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] [algebra R P] [loc : is_localization S P] {x : P} {I J : fractional_ideal S P} :

I ≤ fractional_ideal.span_singleton S x * J ↔ ∀ (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] [algebra R P] [loc : is_localization S P] {x : P} {I J : fractional_ideal S P} :

fractional_ideal.span_singleton S x * I ≤ J ↔ ∀ (z : P), z ∈ I → x * 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] [algebra R P] [loc : is_localization S P] {x : P} {I J : fractional_ideal S P} :

I = fractional_ideal.span_singleton S x * J ↔ (∀ (zI : P), zI ∈ I → (∃ (zJ : P) (H : zJ ∈ J), x * zJ = zI)) ∧ ∀ (z : P), z ∈ J → x * z ∈ I

theorem fractional_ideal.is_noetherian_zero {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] :

is_noetherian R₁ ↥0

theorem fractional_ideal.is_noetherian_iff {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] {I : fractional_ideal (non_zero_divisors R₁) K} :

is_noetherian R₁ ↥I ↔ ∀ (J : fractional_ideal (non_zero_divisors R₁) K), J ≤ I → ↑J.fg

theorem fractional_ideal.is_noetherian_coe_ideal {R₁ : Type u_3} [comm_ring R₁] {K : Type u_4} [field K] [algebra R₁ K] [is_noetherian_ring R₁] (I : ideal R₁) :

is_noetherian R₁ ↥↑I

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 : is_fraction_ring R₁ K] [is_domain R₁] (x : R₁) {I : fractional_ideal (non_zero_divisors R₁) K} (hI : is_noetherian R₁ ↥I) :

is_noetherian R₁ ↥(fractional_ideal.span_singleton (non_zero_divisors R₁) (⇑(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 : is_fraction_ring R₁ K] [is_domain R₁] [is_noetherian_ring R₁] (I : fractional_ideal (non_zero_divisors R₁) K) :

is_noetherian R₁ ↥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] [algebra R P] [loc : is_localization S P] (x : P) (hx : is_integral R x) :

is_fractional S (⇑subalgebra.to_submodule (algebra.adjoin R {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] [algebra R P] [loc : is_localization S P] (x : P) (hx : is_integral R x) :

↑(fractional_ideal.adjoin_integral S x hx) = ⇑subalgebra.to_submodule (algebra.adjoin R {x})

def fractional_ideal.adjoin_integral {R : Type u_1} [comm_ring R] (S : submonoid R) {P : Type u_2} [comm_ring P] [algebra R P] [loc : is_localization S P] (x : P) (hx : is_integral R x) :

fractional_ideal S P

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

fractional_ideal.adjoin_integral S x hx = ⟨⇑subalgebra.to_submodule (algebra.adjoin R {x}), _⟩

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

x ∈ fractional_ideal.adjoin_integral S x hx