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

and `P`

the localization of `R`

at `S`

.

`IsFractional`

defines which`R`

-submodules of`P`

are fractional ideals`FractionalIdeal S P`

is the type of fractional ideals in`P`

- a coercion
`coeIdeal : Ideal R → FractionalIdeal S P`

`CommSemiring (FractionalIdeal S P)`

instance: the typical ideal operations generalized to fractional ideals`Lattice (FractionalIdeal S P)`

instance

## Main statements #

`mul_left_mono`

and`mul_right_mono`

state that ideal multiplication is monotone`mul_div_self_cancel_iff`

states that`1 / I`

is the inverse of`I`

if 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 `FractionalIdeal`

to be the subtype of the predicate `IsFractional`

,
instead of having `FractionalIdeal`

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 `IsLocalization`

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

A submodule `I`

is a fractional ideal if `a I ⊆ R`

for some `a ≠ 0`

.

## Equations

- IsFractional S I = ∃ a ∈ S, ∀ b ∈ I, IsLocalization.IsInteger R (a • b)

## Instances For

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

- FractionalIdeal S P = { I : Submodule R P // IsFractional S I }

## Instances For

Map a fractional ideal `I`

to a submodule by forgetting that `∃ a, a I ⊆ R`

.

This implements the coercion `FractionalIdeal S P → Submodule R P`

.

## Equations

- ↑I = ↑I

## Instances For

Map a fractional ideal `I`

to a submodule by forgetting that `∃ a, a I ⊆ R`

.

This coercion is typically called `coeToSubmodule`

in lemma names
(or `coe`

when the coercion is clear from the context),
not to be confused with `IsLocalization.coeSubmodule : Ideal R → Submodule R P`

(which we use to define `coe : Ideal R → FractionalIdeal S P`

).

## Equations

- One or more equations did not get rendered due to their size.

An element of `S`

such that `I.den • I = I.num`

, see `FractionalIdeal.num`

and
`FractionalIdeal.den_mul_self_eq_num`

.

## Equations

- FractionalIdeal.den I = { val := Exists.choose ⋯, property := ⋯ }

## Instances For

An ideal of `R`

such that `I.den • I = I.num`

, see `FractionalIdeal.den`

and
`FractionalIdeal.den_mul_self_eq_num`

.

## Equations

- FractionalIdeal.num I = Submodule.comap (Algebra.linearMap R P) (FractionalIdeal.den I • ↑I)

## Instances For

The linear equivalence between the fractional ideal `I`

and the integral ideal `I.num`

defined by mapping `x`

to `den I • x`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- FractionalIdeal.instSetLikeFractionalIdeal = { coe := fun (I : FractionalIdeal S P) => ↑↑I, coe_injective' := ⋯ }

Copy of a `FractionalIdeal`

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

## Equations

- FractionalIdeal.copy p s hs = { val := Submodule.copy (↑p) s hs, property := ⋯ }

## Instances For

Transfer instances from `Submodule R P`

to `FractionalIdeal S P`

.

## Equations

- One or more equations did not get rendered due to their size.

Map an ideal `I`

to a fractional ideal by forgetting `I`

is integral.

This is the function that implements the coercion `Ideal R → FractionalIdeal S P`

.

## Equations

- ↑I = { val := IsLocalization.coeSubmodule P I, property := ⋯ }

## Instances For

Map an ideal `I`

to a fractional ideal by forgetting `I`

is integral.

This is a bundled version of `IsLocalization.coeSubmodule : Ideal R → Submodule R P`

,
which is not to be confused with the `coe : FractionalIdeal S P → Submodule R P`

,
also called `coeToSubmodule`

in theorem names.

This map is available as a ring hom, called `FractionalIdeal.coeIdealHom`

.

## Equations

- FractionalIdeal.instZeroFractionalIdeal S = { zero := ↑0 }

`(1 : FractionalIdeal 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`

.

`Lattice`

section #

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

## Equations

- FractionalIdeal.orderBot = OrderBot.mk ⋯

## Equations

- FractionalIdeal.instInfFractionalIdeal = { inf := fun (I J : FractionalIdeal S P) => { val := ↑I ⊓ ↑J, property := ⋯ } }

## Equations

- FractionalIdeal.instSupFractionalIdeal = { sup := fun (I J : FractionalIdeal S P) => { val := ↑I ⊔ ↑J, property := ⋯ } }

## Equations

- FractionalIdeal.lattice = Function.Injective.lattice (fun (a : { I : Submodule R P // IsFractional S I }) => ↑a) ⋯ ⋯ ⋯

## Equations

- FractionalIdeal.instSemilatticeSupFractionalIdeal = let __src := FractionalIdeal.lattice; SemilatticeSup.mk ⋯ ⋯ ⋯

## Equations

- FractionalIdeal.instAddFractionalIdeal = { add := fun (x x_1 : FractionalIdeal S P) => x ⊔ x_1 }

## Equations

- FractionalIdeal.instSMulNatFractionalIdeal = { smul := fun (n : ℕ) (I : FractionalIdeal S P) => { val := n • ↑I, property := ⋯ } }

`FractionalIdeal.mul`

is the product of two fractional ideals,
used to define the `Mul`

instance.

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

is `I * J`

.

Elaborated terms involving `FractionalIdeal`

tend to grow quite large,
so by making definitions irreducible, we hope to avoid deep unfolds.

## Equations

## Instances For

## Equations

- FractionalIdeal.instMulFractionalIdeal = { mul := fun (I J : FractionalIdeal S P) => FractionalIdeal.mul I J }

## Equations

- FractionalIdeal.instPowFractionalIdealNat = { pow := fun (I : FractionalIdeal S P) (n : ℕ) => { val := ↑I ^ n, property := ⋯ } }

## Equations

- FractionalIdeal.commSemiring = Function.Injective.commSemiring (fun (a : { I : Submodule R P // IsFractional S I }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

`FractionalIdeal.coeToSubmodule`

as a bundled `RingHom`

.

## Equations

- FractionalIdeal.coeSubmoduleHom S P = { toMonoidHom := { toOneHom := { toFun := FractionalIdeal.coeToSubmodule, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

`coeIdealHom (S : Submonoid R) P`

is `(↑) : Ideal R → FractionalIdeal S P`

as a ring hom

## Equations

- FractionalIdeal.coeIdealHom S P = { toMonoidHom := { toOneHom := { toFun := FractionalIdeal.coeIdeal, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }