Fractional ideals
This file defines fractional ideals of an integral domain and proves basic facts about them.
Main definitions
Let S be a submonoid of an integral domain R, P the localization of R at S, and f the
natural ring hom from R to P.
is_fractionaldefines whichR-submodules ofPare fractional idealsfractional_ideal fis the type of fractional ideals inPhas_coe (ideal R) (fractional_ideal f)instancecomm_semiring (fractional_ideal f)instance: the typical ideal operations generalized to fractional idealslattice (fractional_ideal f)instancemapis the pushforward of a fractional ideal along an algebra morphism
Let K be the localization of R at R \ {0} and g the natural ring hom from R to K.
has_div (fractional_ideal g)instance: the ideal quotientI / J(typically written $I : J$, but a:operator cannot be defined)
Main statements
mul_left_monoandmul_right_monostate that ideal multiplication is monotoneright_inverse_eqstates that1 / Iis the inverse ofIif one exists
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
- https://en.wikipedia.org/wiki/Fractional_ideal
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) :
A submodule I is a fractional ideal if a I ⊆ R for some a ≠ 0.
Equations
- ring.is_fractional f I = ∃ (a : R) (H : a ∈ S), ∀ (b : P), b ∈ I → f.is_integer (⇑(f.to_map) a * b)
def
ring.fractional_ideal
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P] :
localization_map S 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
- ring.fractional_ideal f = {I // ring.is_fractional f I}
@[instance]
def
ring.fractional_ideal.has_coe
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
has_coe (ring.fractional_ideal f) (submodule R f.codomain)
Equations
- ring.fractional_ideal.has_coe = {coe := λ (I : ring.fractional_ideal f), I.val}
@[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) :
@[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} :
has_mem P (ring.fractional_ideal f)
Equations
- ring.fractional_ideal.has_mem = {mem := λ (x : P) (I : ring.fractional_ideal f), x ∈ ↑I}
@[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} :
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) :
I ≤ submodule.span R {1} → ring.is_fractional f I
@[instance]
def
ring.fractional_ideal.coe_to_fractional_ideal
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
has_coe (ideal R) (ring.fractional_ideal f)
Equations
- ring.fractional_ideal.coe_to_fractional_ideal = {coe := λ (I : ideal R), ⟨f.coe_submodule I, _⟩}
@[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) :
↑↑I = f.coe_submodule I
@[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} :
@[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} :
@[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} :
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) :
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} :
↑1 = f.coe_submodule 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.
@[instance]
def
ring.fractional_ideal.partial_order
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.partial_order = {le := λ (I J : ring.fractional_ideal f), I.val ≤ J.val, lt := preorder.lt._default (λ (I J : ring.fractional_ideal f), I.val ≤ J.val), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
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} :
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
@[instance]
def
ring.fractional_ideal.order_bot
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.order_bot = {bot := 0, le := partial_order.le ring.fractional_ideal.partial_order, lt := partial_order.lt ring.fractional_ideal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[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} :
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} :
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) :
ring.is_fractional f (I.val ⊔ J.val)
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) :
ring.is_fractional f (I.val ⊓ J.val)
@[instance]
def
ring.fractional_ideal.lattice
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.lattice = {sup := λ (I J : ring.fractional_ideal f), ⟨I.val ⊔ J.val, _⟩, le := partial_order.le ring.fractional_ideal.partial_order, lt := partial_order.lt ring.fractional_ideal.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (I J : ring.fractional_ideal f), ⟨I.val ⊓ J.val, _⟩, inf_le_left := _, inf_le_right := _, le_inf := _}
@[instance]
def
ring.fractional_ideal.semilattice_sup_bot
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.semilattice_sup_bot = {bot := order_bot.bot ring.fractional_ideal.order_bot, le := order_bot.le ring.fractional_ideal.order_bot, lt := order_bot.lt ring.fractional_ideal.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := lattice.sup ring.fractional_ideal.lattice, le_sup_left := _, le_sup_right := _, sup_le := _}
@[instance]
def
ring.fractional_ideal.has_add
{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.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) :
@[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) :
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) :
ring.is_fractional f (I.val * J.val)
@[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
- ring.fractional_ideal.has_mul = {mul := λ (I J : ring.fractional_ideal f), ⟨I.val * J.val, _⟩}
@[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) :
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) :
monotone (has_mul.mul I)
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)
@[instance]
def
ring.fractional_ideal.add_comm_monoid
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.add_comm_monoid = {add := has_add.add ring.fractional_ideal.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _}
@[instance]
def
ring.fractional_ideal.comm_monoid
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.comm_monoid = {mul := has_mul.mul ring.fractional_ideal.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, mul_comm := _}
@[instance]
def
ring.fractional_ideal.comm_semiring
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
Equations
- ring.fractional_ideal.comm_semiring = {add := add_comm_monoid.add ring.fractional_ideal.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero ring.fractional_ideal.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := comm_monoid.mul ring.fractional_ideal.comm_monoid, mul_assoc := _, one := comm_monoid.one ring.fractional_ideal.comm_monoid, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
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) :
ring.is_fractional f' (submodule.map g.to_linear_map I.val)
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'} :
(f.codomain →ₐ[R] f'.codomain) → ring.fractional_ideal f → ring.fractional_ideal f'
I.map g is the pushforward of the fractional ideal I along the algebra morphism g
Equations
- ring.fractional_ideal.map g = λ (I : ring.fractional_ideal f), ⟨submodule.map g.to_linear_map I.val, _⟩
@[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.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) :
ring.fractional_ideal.map (alg_hom.id R f.codomain) I = I
@[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''}
(g : f.codomain →ₐ[R] f'.codomain)
(g' : f'.codomain →ₐ[R] f''.codomain)
(I : ring.fractional_ideal f) :
ring.fractional_ideal.map (g'.comp g) I = ring.fractional_ideal.map g' (ring.fractional_ideal.map g I)
@[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) :
ring.fractional_ideal.map g (I + J) = ring.fractional_ideal.map g I + ring.fractional_ideal.map g J
@[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) :
ring.fractional_ideal.map g (I * J) = ring.fractional_ideal.map g I * ring.fractional_ideal.map g J
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'} :
(f.codomain ≃ₐ[R] f'.codomain) → ring.fractional_ideal f ≃+* ring.fractional_ideal f'
If g is an equivalence, map g is an isomorphism
Equations
- ring.fractional_ideal.map_equiv g = {to_fun := ring.fractional_ideal.map ↑g, inv_fun := ring.fractional_ideal.map ↑(g.symm), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
ring.fractional_ideal.map_equiv_apply
{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.map_equiv_refl
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
def
ring.fractional_ideal.canonical_equiv
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
(f f' : localization_map S P) :
canonical_equiv f f' is the canonical equivalence between the fractional
ideals in f.codomain and in f'.codomain
Equations
- ring.fractional_ideal.canonical_equiv f f' = ring.fractional_ideal.map_equiv {to_fun := (f.ring_equiv_of_ring_equiv f' (ring_equiv.refl R) ring.fractional_ideal.canonical_equiv._proof_1).to_fun, inv_fun := (f.ring_equiv_of_ring_equiv f' (ring_equiv.refl R) ring.fractional_ideal.canonical_equiv._proof_1).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
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} :
Equations
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 ≠ 0 → ring.is_fractional g (I.val / J.val)
@[instance]
def
ring.fractional_ideal.fractional_ideal_has_div
{R : Type u_1}
[integral_domain R]
{K : Type u_3}
[field K]
{g : fraction_map R K} :
@[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
- ring.fractional_ideal.has_inv = {inv := λ (I : ring.fractional_ideal g), 1 / I}
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) :
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) :
theorem
ring.fractional_ideal.coe_inv_of_nonzero
{R : Type u_1}
[integral_domain R]
{K : Type u_3}
[field K]
{g : fraction_map R K}
{I : ring.fractional_ideal g} :
@[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} :
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) :
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⁻¹ 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} :
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 ∈ s → f.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) :
ring.is_fractional f (submodule.span R {x})
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
- ring.fractional_ideal.span_singleton x = ⟨submodule.span R {x}, _⟩
@[simp]
theorem
ring.fractional_ideal.coe_span_singleton
{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) :
theorem
ring.fractional_ideal.eq_span_singleton_of_principal
{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.is_principal] :
theorem
ring.fractional_ideal.is_principal_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.val.is_principal ↔ ∃ (x : f.codomain), I = ring.fractional_ideal.span_singleton x
@[simp]
theorem
ring.fractional_ideal.span_singleton_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.span_singleton_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}
{y : f.codomain} :
ring.fractional_ideal.span_singleton y = 0 ↔ y = 0
@[simp]
theorem
ring.fractional_ideal.span_singleton_one
{R : Type u_1}
[integral_domain R]
{S : submonoid R}
{P : Type u_2}
[comm_ring P]
{f : localization_map S P} :
@[simp]
theorem
ring.fractional_ideal.span_singleton_mul_span_singleton
{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) :
@[simp]
theorem
ring.fractional_ideal.coe_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}
(x : R) :
↑(submodule.span R {x}) = ring.fractional_ideal.span_singleton (⇑(f.to_map) x)
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} :
theorem
ring.fractional_ideal.mul_generator_self_inv
{R : Type u_1}
[integral_domain R]
{K : Type u_3}
[field K]
{g : fraction_map R K}
(I : ring.fractional_ideal g)
[I.val.is_principal] :
I ≠ 0 → I * ring.fractional_ideal.span_singleton (submodule.is_principal.generator I.val)⁻¹ = 1
theorem
ring.fractional_ideal.exists_eq_span_singleton_mul
{R : Type u_1}
[integral_domain R]
{K : Type u_3}
[field K]
{g : fraction_map R K}
(I : ring.fractional_ideal g) :
∃ (a : K) (aI : ideal R), I = ring.fractional_ideal.span_singleton a * ↑aI
@[instance]
def
ring.fractional_ideal.is_principal
{K : Type u_3}
[field K]
{R : Type u_1}
[integral_domain R]
[is_principal_ideal_ring R]
{f : fraction_map R K}
(I : ring.fractional_ideal f) :
Equations
- _ = _