mathlib documentation

ring_theory.fractional_ideal

Fractional ideals

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

Main definitions

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

Let K be the localization of R at R \ {0} and g the natural ring hom from R to K.

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.1 + J.1 = (I + J).1 and ⊥.1 = 0.1.

In ring_theory.localization, we define a copy of the localization map f's codomain P (f.codomain) so that the R-algebra instance on P can 'know' the map needed to induce the R-algebra structure.

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 non_zero_divisors R, making the localization a field.

References

Tags

fractional ideal, fractional ideals, invertible ideal

def ring.is_fractional {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] (f : localization_map S P) :
submodule R f.codomain → Prop

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

Equations
def ring.fractional_ideal {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] :
localization_map S PType 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
@[simp]
theorem ring.fractional_ideal.val_eq_coe {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ring.fractional_ideal f) :
I.val = I

@[simp]
theorem ring.fractional_ideal.coe_mk {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : submodule R f.codomain) (hI : ring.is_fractional f I) :
I, hI⟩ = I

@[instance]
def ring.fractional_ideal.has_mem {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

Equations
@[ext]
theorem ring.fractional_ideal.ext {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {I J : ring.fractional_ideal f} :
I = JI = J

Fractional ideals are equal if their submodules are equal.

Combined with submodule.ext this gives that fractional ideals are equal if they have the same elements.

theorem ring.fractional_ideal.fractional_of_subset_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : submodule R f.codomain) :

@[simp]
theorem ring.fractional_ideal.coe_coe_ideal {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ideal R) :

@[simp]
theorem ring.fractional_ideal.mem_coe {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {x : f.codomain} {I : ideal R} :
x I ∃ (x' : R) (H : x' I), (f.to_map) x' = x

@[instance]
def ring.fractional_ideal.has_zero {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

Equations
@[simp]
theorem ring.fractional_ideal.mem_zero_iff {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {x : P} :
x 0 x = 0

@[simp]
theorem ring.fractional_ideal.coe_zero {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

theorem ring.fractional_ideal.coe_ne_bot_iff_nonzero {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {I : ring.fractional_ideal f} :

@[instance]
def ring.fractional_ideal.inhabited {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

Equations
@[instance]
def ring.fractional_ideal.has_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

Equations
theorem ring.fractional_ideal.mem_one_iff {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {x : P} :
x 1 ∃ (x' : R), (f.to_map) x' = x

theorem ring.fractional_ideal.coe_mem_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (x : R) :
(f.to_map) x 1

theorem ring.fractional_ideal.one_mem_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :
1 1

@[simp]
theorem ring.fractional_ideal.coe_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

lattice section

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

@[instance]

Equations
theorem ring.fractional_ideal.le_iff {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {I J : ring.fractional_ideal f} :
I J ∀ (x : P), x Ix J

theorem ring.fractional_ideal.zero_le {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ring.fractional_ideal f) :
0 I

@[simp]
theorem ring.fractional_ideal.bot_eq_zero {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :
= 0

theorem ring.fractional_ideal.eq_zero_iff {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {I : ring.fractional_ideal f} :
I = 0 ∀ (x : P), x Ix = 0

theorem ring.fractional_ideal.fractional_sup {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :

theorem ring.fractional_ideal.fractional_inf {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :

@[simp]
theorem ring.fractional_ideal.sup_eq_add {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :
I J = I + J

@[simp]
theorem ring.fractional_ideal.coe_add {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :
(I + J) = I + J

theorem ring.fractional_ideal.fractional_mul {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :

@[instance]
def ring.fractional_ideal.has_mul {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

Equations
@[simp]
theorem ring.fractional_ideal.coe_mul {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I J : ring.fractional_ideal f) :
I * J = (I) * J

theorem ring.fractional_ideal.mul_left_mono {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ring.fractional_ideal f) :

theorem ring.fractional_ideal.mul_right_mono {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ring.fractional_ideal f) :
monotone (λ (J : ring.fractional_ideal f), J * I)

theorem ring.fractional_ideal.fractional_map {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (g : f.codomain →ₐ[R] f'.codomain) (I : ring.fractional_ideal f) :

def ring.fractional_ideal.map {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} :

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

Equations
@[simp]
theorem ring.fractional_ideal.coe_map {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (g : f.codomain →ₐ[R] f'.codomain) (I : ring.fractional_ideal f) :

@[simp]
theorem ring.fractional_ideal.mem_map {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} {I : ring.fractional_ideal f} {g : f.codomain →ₐ[R] f'.codomain} {y : f'.codomain} :
y ring.fractional_ideal.map g I ∃ (x : f.codomain), x I g x = y

@[simp]
theorem ring.fractional_ideal.map_id {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (I : ring.fractional_ideal f) :

@[simp]
theorem ring.fractional_ideal.map_comp {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} {P'' : Type u_4} [comm_ring P''] {f'' : localization_map S P''} (I : ring.fractional_ideal f) (g : f.codomain →ₐ[R] f'.codomain) (g' : f'.codomain →ₐ[R] f''.codomain) :

@[simp]
theorem ring.fractional_ideal.map_coe_ideal {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (g : f.codomain →ₐ[R] f'.codomain) (I : ideal R) :

@[simp]
theorem ring.fractional_ideal.map_one {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (g : f.codomain →ₐ[R] f'.codomain) :

@[simp]
theorem ring.fractional_ideal.map_zero {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (g : f.codomain →ₐ[R] f'.codomain) :

@[simp]
theorem ring.fractional_ideal.map_add {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (I J : ring.fractional_ideal f) (g : f.codomain →ₐ[R] f'.codomain) :

@[simp]
theorem ring.fractional_ideal.map_mul {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (I J : ring.fractional_ideal f) (g : f.codomain →ₐ[R] f'.codomain) :

@[simp]
theorem ring.fractional_ideal.map_map_symm {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (I : ring.fractional_ideal f) (g : f.codomain ≃ₐ[R] f'.codomain) :

@[simp]
theorem ring.fractional_ideal.map_symm_map {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} (I : ring.fractional_ideal f') (g : f.codomain ≃ₐ[R] f'.codomain) :

def ring.fractional_ideal.map_equiv {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {P' : Type u_3} [comm_ring P'] {f' : localization_map S P'} :

If g is an equivalence, map g is an isomorphism

Equations
@[simp]

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

Equations

fraction_map section

This section concerns fractional ideals in the field of fractions, i.e. the type fractional_ideal g when g is a fraction_map R K.

theorem ring.fractional_ideal.exists_ne_zero_mem_is_integer {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} :
I 0(∃ (x : R) (H : x 0), (localization_map.to_map g) x I)

Nonzero fractional ideals contain a nonzero integer.

theorem ring.fractional_ideal.map_ne_zero {R : Type u_1} [integral_domain R] {K : Type u_3} {K' : Type u_4} [field K] [field K'] {g : fraction_map R K} {g' : fraction_map R K'} {I : ring.fractional_ideal g} (h : localization_map.codomain g →ₐ[R] localization_map.codomain g') :

@[simp]
theorem ring.fractional_ideal.map_eq_zero_iff {R : Type u_1} [integral_domain R] {K : Type u_3} {K' : Type u_4} [field K] [field K'] {g : fraction_map R K} {g' : fraction_map R K'} {I : ring.fractional_ideal g} (h : localization_map.codomain g →ₐ[R] localization_map.codomain g') :

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.

@[instance]
def ring.fractional_ideal.nontrivial {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} :

theorem ring.fractional_ideal.fractional_div_of_nonzero {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I J : ring.fractional_ideal g} :
J 0ring.is_fractional g (I.val / J.val)

@[instance]

Equations
@[instance]
def ring.fractional_ideal.has_inv {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} :

Equations
theorem ring.fractional_ideal.inv_eq {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} :
I⁻¹ = 1 / I

@[simp]
theorem ring.fractional_ideal.div_zero {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} :
I / 0 = 0

theorem ring.fractional_ideal.div_nonzero {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I J : ring.fractional_ideal g} (h : J 0) :
I / J = I.val / J.val, _⟩

theorem ring.fractional_ideal.inv_zero {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} :
0⁻¹ = 0

theorem ring.fractional_ideal.inv_nonzero {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} (h : I 0) :
I⁻¹ = 1 / I, _⟩

@[simp]
theorem ring.fractional_ideal.div_one {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} :
I / 1 = I

theorem ring.fractional_ideal.ne_zero_of_mul_eq_one {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} (I J : ring.fractional_ideal g) :
I * J = 1I 0

theorem ring.fractional_ideal.right_inverse_eq {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} (I J : ring.fractional_ideal g) :
I * J = 1J = I⁻¹

I⁻¹ is the inverse of I if I has an inverse.

theorem ring.fractional_ideal.mul_inv_cancel_iff {R : Type u_1} [integral_domain R] {K : Type u_3} [field K] {g : fraction_map R K} {I : ring.fractional_ideal g} :
I * I⁻¹ = 1 ∃ (J : ring.fractional_ideal g), I * J = 1

theorem ring.fractional_ideal.span_fractional_iff {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {s : set f.codomain} :
ring.is_fractional f (submodule.span R s) ∃ (a : R) (H : a S), ∀ (b : P), b sf.is_integer (((f.to_map) a) * b)

theorem ring.fractional_ideal.span_singleton_fractional {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} (x : f.codomain) :

def ring.fractional_ideal.span_singleton {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} :

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

Equations
@[simp]

@[simp]

theorem ring.fractional_ideal.mem_singleton_mul {R : Type u_1} [integral_domain R] {S : submonoid R} {P : Type u_2} [comm_ring P] {f : localization_map S P} {x y : f.codomain} {I : ring.fractional_ideal f} :
y (ring.fractional_ideal.span_singleton x) * I ∃ (y' : f.codomain) (H : y' I), y = x * y'

@[instance]