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.

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

Main statements #

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 #

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

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

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

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] [algebra R 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] [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) :
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] :
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] [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_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) :
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} :
@[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] :
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] [algebra R 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] [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) :
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

(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] :
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] [algebra R 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] [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} :
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} :
@[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] :
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] [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] :
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] [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] :
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] [algebra R 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] [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 : ) :
@[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] :
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] [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} :
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 : ) :
@[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.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] [algebra R 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] [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) :
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] :
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] [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
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 : ) :
@[simp]
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} :
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] [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) :
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] :

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

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

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

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

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

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) :
@[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] :
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} :
@[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] :
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} :
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) :
@[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₁] :
Equations
@[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') :
@[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') :
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.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] [is_fraction_ring R₁ K] {ι : Type u_1} (s : finset ι) (f : ι K) :
@[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) :
@[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) :

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

Every fractional ideal of a noetherian integral domain is noetherian.

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

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