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.

• 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
• 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).

• FractionalIdeal R⁰ K is the type of fractional ideals in the field of fractions
• Div (FractionalIdeal 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
• mul_div_self_cancel_iff states that 1 / I is the inverse of I if one exists
• isNoetherian 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 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

def IsFractional {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing 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

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

def FractionalIdeal {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing 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

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

def FractionalIdeal.coeToSubmodule {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : Submodule R P

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

instance FractionalIdeal.instCoeOutFractionalIdealSubmoduleToSemiringToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToSemiringToCommSemiring {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : CoeOut (FractionalIdeal 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 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.

theorem FractionalIdeal.isFractional {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : IsFractional S ↑I

instance FractionalIdeal.instSetLikeFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : SetLike (FractionalIdeal S P) P

Equations

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

@[simp]

theorem FractionalIdeal.mem_coe {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {x : P} : x ∈ ↑I ↔ x ∈ I

theorem FractionalIdeal.ext {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} : (∀ (x : P), x ∈ I ↔ x ∈ J) → I = J

def FractionalIdeal.copy {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p) : FractionalIdeal S P

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 := (_ : IsFractional S (Submodule.copy (↑p) s hs)) }

@[simp]

theorem FractionalIdeal.coe_copy {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p) : ↑(FractionalIdeal.copy p s hs) = s

theorem FractionalIdeal.coe_eq {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (p : FractionalIdeal S P) (s : Set P) (hs : s = ↑p) : FractionalIdeal.copy p s hs = p

@[simp]

theorem FractionalIdeal.val_eq_coe {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : ↑I = ↑I

@[simp]

theorem FractionalIdeal.coe_mk {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Submodule R P) (hI : IsFractional S I) : ↑{ val := I, property := hI } = I

theorem FractionalIdeal.coeToSet_coeToSubmodule {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : ↑↑I = ↑I

Transfer instances from Submodule R P to FractionalIdeal S P.

instance FractionalIdeal.instModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToModuleToSemiringToCommSemiringInstMembershipSetLikeCoeToSubmoduleAddCommMonoid {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : Module R ↥↑I

Equations

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

theorem FractionalIdeal.coeToSubmodule_injective {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Function.Injective fun (I : FractionalIdeal S P) => ↑I

theorem FractionalIdeal.coeToSubmodule_inj {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} : ↑I = ↑J ↔ I = J

theorem FractionalIdeal.isFractional_of_le_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Submodule R P) (h : I ≤ 1) : IsFractional S I

theorem FractionalIdeal.isFractional_of_le {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} {J : FractionalIdeal S P} (hIJ : I ≤ ↑J) : IsFractional S I

def FractionalIdeal.coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Ideal R) : FractionalIdeal S P

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 := (_ : IsFractional S (IsLocalization.coeSubmodule P I)) }

instance FractionalIdeal.instCoeTCIdealToSemiringToCommSemiringFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : CoeTC (Ideal R) (FractionalIdeal S P)

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.instCoeTCIdealToSemiringToCommSemiringFractionalIdeal = { coe := fun (I : Ideal R) => ↑I }

@[simp]

theorem FractionalIdeal.coe_coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Ideal R) : ↑↑I = IsLocalization.coeSubmodule P I

@[simp]

theorem FractionalIdeal.mem_coeIdeal {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] {x : P} {I : Ideal R} : x ∈ ↑I ↔ ∃ x' ∈ I, (algebraMap R P) x' = x

theorem FractionalIdeal.mem_coeIdeal_of_mem {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] {x : R} {I : Ideal R} (hx : x ∈ I) : (algebraMap R P) x ∈ ↑I

theorem FractionalIdeal.coeIdeal_le_coeIdeal' {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [IsLocalization S P] (h : S ≤ nonZeroDivisors R) {I : Ideal R} {J : Ideal R} : ↑I ≤ ↑J ↔ I ≤ J

@[simp]

theorem FractionalIdeal.coeIdeal_le_coeIdeal {R : Type u_1} [CommRing R] (K : Type u_3) [CommRing K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} {J : Ideal R} : ↑I ≤ ↑J ↔ I ≤ J

instance FractionalIdeal.instZeroFractionalIdeal {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] : Zero (FractionalIdeal S P)

Equations

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

@[simp]

theorem FractionalIdeal.mem_zero_iff {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] {x : P} : x ∈ 0 ↔ x = 0

@[simp]

theorem FractionalIdeal.coe_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : ↑0 = ⊥

@[simp]

theorem FractionalIdeal.coeIdeal_bot {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : ↑⊥ = 0

@[simp]

theorem FractionalIdeal.exists_mem_algebraMap_eq {R : Type u_1} [CommRing R] {S : Submonoid R} (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : R} {I : Ideal R} (h : S ≤ nonZeroDivisors R) : (∃ x' ∈ I, (algebraMap R P) x' = (algebraMap R P) x) ↔ x ∈ I

theorem FractionalIdeal.coeIdeal_injective' {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (h : S ≤ nonZeroDivisors R) : Function.Injective fun (I : Ideal R) => ↑I

theorem FractionalIdeal.coeIdeal_inj' {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (h : S ≤ nonZeroDivisors R) {I : Ideal R} {J : Ideal R} : ↑I = ↑J ↔ I = J

theorem FractionalIdeal.coeIdeal_eq_zero' {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {I : Ideal R} (h : S ≤ nonZeroDivisors R) : ↑I = 0 ↔ I = ⊥

theorem FractionalIdeal.coeIdeal_ne_zero' {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {I : Ideal R} (h : S ≤ nonZeroDivisors R) : ↑I ≠ 0 ↔ I ≠ ⊥

theorem FractionalIdeal.coeToSubmodule_eq_bot {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} : ↑I = ⊥ ↔ I = 0

theorem FractionalIdeal.coeToSubmodule_ne_bot {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} : ↑I ≠ ⊥ ↔ I ≠ 0

instance FractionalIdeal.instInhabitedFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Inhabited (FractionalIdeal S P)

Equations

• FractionalIdeal.instInhabitedFractionalIdeal = { default := 0 }

instance FractionalIdeal.instOneFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : One (FractionalIdeal S P)

Equations

• FractionalIdeal.instOneFractionalIdeal = { one := ↑⊤ }

@[simp]

theorem FractionalIdeal.coeIdeal_top {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] : ↑⊤ = 1

theorem FractionalIdeal.mem_one_iff {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] {x : P} : x ∈ 1 ↔ ∃ (x' : R), (algebraMap R P) x' = x

theorem FractionalIdeal.coe_mem_one {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] (x : R) : (algebraMap R P) x ∈ 1

theorem FractionalIdeal.one_mem_one {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] : 1 ∈ 1

theorem FractionalIdeal.coe_one_eq_coeSubmodule_top {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : ↑1 = IsLocalization.coeSubmodule P ⊤

(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.

@[simp]

theorem FractionalIdeal.coe_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing 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 FractionalIdeal.coe_le_coe {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} : ↑I ≤ ↑J ↔ I ≤ J

theorem FractionalIdeal.zero_le {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : 0 ≤ I

instance FractionalIdeal.orderBot {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : OrderBot (FractionalIdeal S P)

Equations

• FractionalIdeal.orderBot = OrderBot.mk (_ : ∀ (I : FractionalIdeal S P), 0 ≤ I)

@[simp]

theorem FractionalIdeal.bot_eq_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : ⊥ = 0

@[simp]

theorem FractionalIdeal.le_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} : I ≤ 0 ↔ I = 0

theorem FractionalIdeal.eq_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} : I = 0 ↔ ∀ x ∈ I, x = 0

theorem IsFractional.sup {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} {J : Submodule R P} : IsFractional S I → IsFractional S J → IsFractional S (I ⊔ J)

theorem IsFractional.inf_right {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} : IsFractional S I → ∀ (J : Submodule R P), IsFractional S (I ⊓ J)

instance FractionalIdeal.instInfFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Inf (FractionalIdeal S P)

Equations

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

@[simp]

theorem FractionalIdeal.coe_inf {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : ↑(I ⊓ J) = ↑I ⊓ ↑J

instance FractionalIdeal.instSupFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Sup (FractionalIdeal S P)

Equations

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

theorem FractionalIdeal.coe_sup {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : ↑(I ⊔ J) = ↑I ⊔ ↑J

instance FractionalIdeal.lattice {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Lattice (FractionalIdeal S P)

Equations

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

instance FractionalIdeal.instSemilatticeSupFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : SemilatticeSup (FractionalIdeal S P)

Equations

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

instance FractionalIdeal.instAddFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Add (FractionalIdeal S P)

Equations

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

@[simp]

theorem FractionalIdeal.sup_eq_add {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : I ⊔ J = I + J

@[simp]

theorem FractionalIdeal.coe_add {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : ↑(I + J) = ↑I + ↑J

@[simp]

theorem FractionalIdeal.coeIdeal_sup {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Ideal R) (J : Ideal R) : ↑(I ⊔ J) = ↑I + ↑J

theorem IsFractional.nsmul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} (n : ℕ) : IsFractional S I → IsFractional S (n • I)

instance FractionalIdeal.instSMulNatFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : SMul ℕ (FractionalIdeal S P)

Equations

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

theorem FractionalIdeal.coe_nsmul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (n : ℕ) (I : FractionalIdeal S P) : ↑(n • I) = n • ↑I

theorem IsFractional.mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} {J : Submodule R P} : IsFractional S I → IsFractional S J → IsFractional S (I * J)

theorem IsFractional.pow {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Submodule R P} (h : IsFractional S I) (n : ℕ) : IsFractional S (I ^ n)

theorem FractionalIdeal.mul_def' {R : Type u_3} [CommRing R] {S : Submonoid R} {P : Type u_4} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : FractionalIdeal.mul I J = { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) }

@[irreducible]

def FractionalIdeal.mul {R : Type u_3} [CommRing R] {S : Submonoid R} {P : Type u_4} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : FractionalIdeal S P

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

• @FractionalIdeal.mul = FractionalIdeal.wrapped✝.1

instance FractionalIdeal.instMulFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Mul (FractionalIdeal S P)

Equations

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

@[simp]

theorem FractionalIdeal.mul_eq_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : FractionalIdeal.mul I J = I * J

theorem FractionalIdeal.mul_def {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : I * J = { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) }

@[simp]

theorem FractionalIdeal.coe_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (J : FractionalIdeal S P) : ↑(I * J) = ↑I * ↑J

@[simp]

theorem FractionalIdeal.coeIdeal_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Ideal R) (J : Ideal R) : ↑(I * J) = ↑I * ↑J

theorem FractionalIdeal.mul_left_mono {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : Monotone fun (x : FractionalIdeal S P) => I * x

theorem FractionalIdeal.mul_right_mono {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : Monotone fun (J : FractionalIdeal S P) => J * I

theorem FractionalIdeal.mul_mem_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} {i : P} {j : P} (hi : i ∈ I) (hj : j ∈ J) : i * j ∈ I * J

theorem FractionalIdeal.mul_le {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} {K : FractionalIdeal S P} : I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K

instance FractionalIdeal.instPowFractionalIdealNat {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Pow (FractionalIdeal S P) ℕ

Equations

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

@[simp]

theorem FractionalIdeal.coe_pow {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (n : ℕ) : ↑(I ^ n) = ↑I ^ n

theorem FractionalIdeal.mul_induction_on {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} {C : P → Prop} {r : P} (hr : r ∈ I * J) (hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)) (ha : ∀ (x y : P), C x → C y → C (x + y)) : C r

instance FractionalIdeal.instNatCastFractionalIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : NatCast (FractionalIdeal S P)

Equations

• FractionalIdeal.instNatCastFractionalIdeal = { natCast := Nat.unaryCast }

theorem FractionalIdeal.coe_nat_cast {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (n : ℕ) : ↑↑n = ↑n

instance FractionalIdeal.commSemiring {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : CommSemiring (FractionalIdeal S P)

Equations

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

@[simp]

theorem FractionalIdeal.coeSubmoduleHom_apply {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : (FractionalIdeal.coeSubmoduleHom S P) I = ↑I

def FractionalIdeal.coeSubmoduleHom {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] : FractionalIdeal S P →+* Submodule R P

FractionalIdeal.coeToSubmodule as a bundled RingHom.

Equations

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

theorem FractionalIdeal.add_le_add_left {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} (hIJ : I ≤ J) (J' : FractionalIdeal S P) : J' + I ≤ J' + J

theorem FractionalIdeal.mul_le_mul_left {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} (hIJ : I ≤ J) (J' : FractionalIdeal S P) : J' * I ≤ J' * J

theorem FractionalIdeal.le_self_mul_self {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} (hI : 1 ≤ I) : I ≤ I * I

theorem FractionalIdeal.mul_self_le_self {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} (hI : I ≤ 1) : I * I ≤ I

theorem FractionalIdeal.coeIdeal_le_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : Ideal R} : ↑I ≤ 1

theorem FractionalIdeal.le_one_iff_exists_coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {J : FractionalIdeal S P} : J ≤ 1 ↔ ∃ (I : Ideal R), ↑I = J

@[simp]

theorem FractionalIdeal.one_le {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} : 1 ≤ I ↔ 1 ∈ I

@[simp]

theorem FractionalIdeal.coeIdealHom_apply {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (I : Ideal R) : (FractionalIdeal.coeIdealHom S P) I = ↑I

def FractionalIdeal.coeIdealHom {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] : Ideal R →+* FractionalIdeal S P

coeIdealHom (S : Submonoid R) P is (↑) : Ideal R → FractionalIdeal S P as a ring hom

Equations

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

theorem FractionalIdeal.coeIdeal_pow {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] (I : Ideal R) (n : ℕ) : ↑(I ^ n) = ↑I ^ n

theorem FractionalIdeal.coeIdeal_finprod {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [IsLocalization S P] {α : Sort u_3} {f : α → Ideal R} (hS : S ≤ nonZeroDivisors R) : ↑(finprod fun (a : α) => f a) = finprod fun (a : α) => ↑(f a)

theorem IsFractional.map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') {I : Submodule R P} : IsFractional S I → IsFractional S (Submodule.map (AlgHom.toLinearMap g) I)

def FractionalIdeal.map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : FractionalIdeal S P → FractionalIdeal S P'

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

Equations

• FractionalIdeal.map g I = { val := Submodule.map (AlgHom.toLinearMap g) ↑I, property := (_ : IsFractional S (Submodule.map (AlgHom.toLinearMap g) ↑I)) }

@[simp]

theorem FractionalIdeal.coe_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : FractionalIdeal S P) : ↑(FractionalIdeal.map g I) = Submodule.map (AlgHom.toLinearMap g) ↑I

@[simp]

theorem FractionalIdeal.mem_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {I : FractionalIdeal S P} {g : P →ₐ[R] P'} {y : P'} : y ∈ FractionalIdeal.map g I ↔ ∃ x ∈ I, g x = y

@[simp]

theorem FractionalIdeal.map_id {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : FractionalIdeal.map (AlgHom.id R P) I = I

@[simp]

theorem FractionalIdeal.map_comp {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {P'' : Type u_4} [CommRing P''] [Algebra R P''] (I : FractionalIdeal S P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P'') : FractionalIdeal.map (AlgHom.comp g' g) I = FractionalIdeal.map g' (FractionalIdeal.map g I)

@[simp]

theorem FractionalIdeal.map_coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') (I : Ideal R) : FractionalIdeal.map g ↑I = ↑I

@[simp]

theorem FractionalIdeal.map_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : FractionalIdeal.map g 1 = 1

@[simp]

theorem FractionalIdeal.map_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P →ₐ[R] P') : FractionalIdeal.map g 0 = 0

@[simp]

theorem FractionalIdeal.map_add {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P) (J : FractionalIdeal S P) (g : P →ₐ[R] P') : FractionalIdeal.map g (I + J) = FractionalIdeal.map g I + FractionalIdeal.map g J

@[simp]

theorem FractionalIdeal.map_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P) (J : FractionalIdeal S P) (g : P →ₐ[R] P') : FractionalIdeal.map g (I * J) = FractionalIdeal.map g I * FractionalIdeal.map g J

@[simp]

theorem FractionalIdeal.map_map_symm {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P) (g : P ≃ₐ[R] P') : FractionalIdeal.map (↑(AlgEquiv.symm g)) (FractionalIdeal.map (↑g) I) = I

@[simp]

theorem FractionalIdeal.map_symm_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (I : FractionalIdeal S P') (g : P ≃ₐ[R] P') : FractionalIdeal.map (↑g) (FractionalIdeal.map (↑(AlgEquiv.symm g)) I) = I

theorem FractionalIdeal.map_mem_map {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] {f : P →ₐ[R] P'} (h : Function.Injective ⇑f) {x : P} {I : FractionalIdeal S P} : f x ∈ FractionalIdeal.map f I ↔ x ∈ I

theorem FractionalIdeal.map_injective {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (f : P →ₐ[R] P') (h : Function.Injective ⇑f) : Function.Injective (FractionalIdeal.map f)

def FractionalIdeal.mapEquiv {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : FractionalIdeal S P ≃+* FractionalIdeal S P'

If g is an equivalence, map g is an isomorphism

Equations

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

@[simp]

theorem FractionalIdeal.coeFun_mapEquiv {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : ⇑(FractionalIdeal.mapEquiv g) = FractionalIdeal.map ↑g

@[simp]

theorem FractionalIdeal.mapEquiv_apply {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') (I : FractionalIdeal S P) : (FractionalIdeal.mapEquiv g) I = FractionalIdeal.map (↑g) I

@[simp]

theorem FractionalIdeal.mapEquiv_symm {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {P' : Type u_3} [CommRing P'] [Algebra R P'] (g : P ≃ₐ[R] P') : RingEquiv.symm (FractionalIdeal.mapEquiv g) = FractionalIdeal.mapEquiv (AlgEquiv.symm g)

@[simp]

theorem FractionalIdeal.mapEquiv_refl {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : FractionalIdeal.mapEquiv AlgEquiv.refl = RingEquiv.refl (FractionalIdeal S P)

theorem FractionalIdeal.isFractional_span_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {s : Set P} : IsFractional S (Submodule.span R s) ↔ ∃ a ∈ S, ∀ b ∈ s, IsLocalization.IsInteger R (a • b)

theorem FractionalIdeal.isFractional_of_fg {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {I : Submodule R P} (hI : Submodule.FG I) : IsFractional S I

theorem FractionalIdeal.mem_span_mul_finite_of_mem_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] {I : FractionalIdeal S P} {J : FractionalIdeal S P} {x : P} (hx : x ∈ I * J) : ∃ (T : Finset P) (T' : Finset P), ↑T ⊆ ↑I ∧ ↑T' ⊆ ↑J ∧ x ∈ Submodule.span R (↑T * ↑T')

theorem FractionalIdeal.coeIdeal_fg {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] (inj : Function.Injective ⇑(algebraMap R P)) (I : Ideal R) : Submodule.FG ↑↑I ↔ Ideal.FG I

theorem FractionalIdeal.fg_unit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : (FractionalIdeal S P)ˣ) : Submodule.FG ↑↑I

theorem FractionalIdeal.fg_of_isUnit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) (h : IsUnit I) : Submodule.FG ↑I

theorem Ideal.fg_of_isUnit {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (inj : Function.Injective ⇑(algebraMap R P)) (I : Ideal R) (h : IsUnit ↑I) : Ideal.FG I

theorem FractionalIdeal.canonicalEquiv_def {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] : FractionalIdeal.canonicalEquiv S P P' = FractionalIdeal.mapEquiv (let src := IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S); { toEquiv := src.toEquiv, map_mul' := (_ : ∀ (x y : P), Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv (x * y) = Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv x * Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv y), map_add' := (_ : ∀ (x y : P), Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv (x + y) = Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv x + Equiv.toFun (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)).toEquiv y), commutes' := (_ : ∀ (r : R), (IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) (_ : Submonoid.map (RingEquiv.toMonoidHom (RingEquiv.refl R)) S = S)) ((algebraMap R P) r) = (algebraMap R P') ((RingEquiv.refl R) r)) })

@[irreducible]

noncomputable def FractionalIdeal.canonicalEquiv {R : Type u_5} [CommRing R] (S : Submonoid R) (P : Type u_6) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_7) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] : FractionalIdeal S P ≃+* FractionalIdeal S P'

canonicalEquiv f f' is the canonical equivalence between the fractional ideals in P and in P', which are both localizations of R at S.

Equations

• @FractionalIdeal.canonicalEquiv = FractionalIdeal.wrapped✝.1

@[simp]

theorem FractionalIdeal.mem_canonicalEquiv_apply {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] {I : FractionalIdeal S P} {x : P'} : x ∈ (FractionalIdeal.canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) (_ : ∀ y ∈ S, (RingHom.id R) y ∈ S)) y = x

@[simp]

theorem FractionalIdeal.canonicalEquiv_symm {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] : RingEquiv.symm (FractionalIdeal.canonicalEquiv S P P') = FractionalIdeal.canonicalEquiv S P' P

theorem FractionalIdeal.canonicalEquiv_flip {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] (I : FractionalIdeal S P') : (FractionalIdeal.canonicalEquiv S P P') ((FractionalIdeal.canonicalEquiv S P' P) I) = I

@[simp]

theorem FractionalIdeal.canonicalEquiv_canonicalEquiv {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] (I : FractionalIdeal S P) : (FractionalIdeal.canonicalEquiv S P' P'') ((FractionalIdeal.canonicalEquiv S P P') I) = (FractionalIdeal.canonicalEquiv S P P'') I

theorem FractionalIdeal.canonicalEquiv_trans_canonicalEquiv {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] (P'' : Type u_5) [CommRing P''] [Algebra R P''] [IsLocalization S P''] : RingEquiv.trans (FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.canonicalEquiv S P' P'') = FractionalIdeal.canonicalEquiv S P P''

@[simp]

theorem FractionalIdeal.canonicalEquiv_coeIdeal {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] (P' : Type u_3) [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P'] (I : Ideal R) : (FractionalIdeal.canonicalEquiv S P P') ↑I = ↑I

@[simp]

theorem FractionalIdeal.canonicalEquiv_self {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R P] [loc : IsLocalization S P] : FractionalIdeal.canonicalEquiv S P P = RingEquiv.refl (FractionalIdeal S P)

IsFractionRing section

This section concerns fractional ideals in the field of fractions, i.e. the type FractionalIdeal R⁰ K where IsFractionRing R K.

theorem FractionalIdeal.exists_ne_zero_mem_isInteger {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} [Nontrivial R] (hI : I ≠ 0) : ∃ (x : R), x ≠ 0 ∧ (algebraMap R K) x ∈ I

Nonzero fractional ideals contain a nonzero integer.

theorem FractionalIdeal.map_ne_zero {R : Type u_1} [CommRing R] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R K'] [IsFractionRing R K'] {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R] (hI : I ≠ 0) : FractionalIdeal.map h I ≠ 0

@[simp]

theorem FractionalIdeal.map_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R K'] [IsFractionRing R K'] {I : FractionalIdeal (nonZeroDivisors R) K} (h : K →ₐ[R] K') [Nontrivial R] : FractionalIdeal.map h I = 0 ↔ I = 0

theorem FractionalIdeal.coeIdeal_injective {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] : Function.Injective fun (I : Ideal R) => ↑I

theorem FractionalIdeal.coeIdeal_inj {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} {J : Ideal R} : ↑I = ↑J ↔ I = J

@[simp]

theorem FractionalIdeal.coeIdeal_eq_zero {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I = 0 ↔ I = ⊥

theorem FractionalIdeal.coeIdeal_ne_zero {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I ≠ 0 ↔ I ≠ ⊥

@[simp]

theorem FractionalIdeal.coeIdeal_eq_one {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {I : Ideal R} : ↑I = 1 ↔ I = 1

theorem FractionalIdeal.coeIdeal_ne_one {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing 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 = nonZeroDivisors R, R's localization at which is a field because R is a domain.

instance FractionalIdeal.instNontrivialFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

• (_ : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K)) = (_ : Nontrivial (FractionalIdeal (nonZeroDivisors R₁) K))

theorem FractionalIdeal.ne_zero_of_mul_eq_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] (I : FractionalIdeal (nonZeroDivisors R₁) K) (J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : I ≠ 0

theorem IsFractional.div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : Submodule R₁ K} {J : Submodule R₁ K} : IsFractional (nonZeroDivisors R₁) I → IsFractional (nonZeroDivisors R₁) J → J ≠ 0 → IsFractional (nonZeroDivisors R₁) (I / J)

theorem FractionalIdeal.fractional_div_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : IsFractional (nonZeroDivisors R₁) (↑I / ↑J)

noncomputable instance FractionalIdeal.instDivFractionalIdealNonZeroDivisorsToMonoidWithZeroToSemiringToCommSemiringToCommRingToEuclideanDomain {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] : Div (FractionalIdeal (nonZeroDivisors R₁) K)

Equations

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

@[simp]

theorem FractionalIdeal.div_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I / 0 = 0

theorem FractionalIdeal.div_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) : I / J = { val := ↑I / ↑J, property := (_ : IsFractional (nonZeroDivisors R₁) (↑I / ↑J)) }

@[simp]

theorem FractionalIdeal.coe_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} (hJ : J ≠ 0) : ↑(I / J) = ↑I / ↑J

theorem FractionalIdeal.mem_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0) {x : K} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I

theorem FractionalIdeal.mul_one_div_le_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * (1 / I) ≤ 1

theorem FractionalIdeal.le_self_mul_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : I ≤ 1) : I ≤ I * (1 / I)

theorem FractionalIdeal.le_div_iff_of_nonzero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} {J' : FractionalIdeal (nonZeroDivisors R₁) K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J

theorem FractionalIdeal.le_div_iff_mul_le {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} {J : FractionalIdeal (nonZeroDivisors R₁) K} {J' : FractionalIdeal (nonZeroDivisors R₁) K} (hJ' : J' ≠ 0) : I ≤ J / J' ↔ I * J' ≤ J

@[simp]

theorem FractionalIdeal.div_one {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I / 1 = I

theorem FractionalIdeal.eq_one_div_of_mul_eq_one_right {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) (J : FractionalIdeal (nonZeroDivisors R₁) K) (h : I * J = 1) : J = 1 / I

theorem FractionalIdeal.mul_div_self_cancel_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K} : I * (1 / I) = 1 ↔ ∃ (J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1

@[simp]

theorem FractionalIdeal.map_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (J : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : FractionalIdeal.map (↑h) (I / J) = FractionalIdeal.map (↑h) I / FractionalIdeal.map (↑h) J

theorem FractionalIdeal.map_one_div {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] {K' : Type u_5} [Field K'] [Algebra R₁ K'] [IsFractionRing R₁ K'] (I : FractionalIdeal (nonZeroDivisors R₁) K) (h : K ≃ₐ[R₁] K') : FractionalIdeal.map (↑h) (1 / I) = 1 / FractionalIdeal.map (↑h) I

theorem FractionalIdeal.eq_zero_or_one {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [IsFractionRing K L] (I : FractionalIdeal (nonZeroDivisors K) L) : I = 0 ∨ I = 1

theorem FractionalIdeal.eq_zero_or_one_of_isField {R₁ : Type u_3} {K : Type u_4} [CommRing R₁] [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] (hF : IsField R₁) (I : FractionalIdeal (nonZeroDivisors R₁) K) : I = 0 ∨ I = 1

def FractionalIdeal.spanFinset (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K) : FractionalIdeal (nonZeroDivisors R₁) K

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

Equations

• FractionalIdeal.spanFinset R₁ s f = { val := Submodule.span R₁ (f '' ↑s), property := (_ : IsFractional (nonZeroDivisors R₁) (Submodule.span R₁ (f '' ↑s))) }

@[simp]

theorem FractionalIdeal.spanFinset_coe (R₁ : Type u_3) [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K) : ↑(FractionalIdeal.spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)

@[simp]

theorem FractionalIdeal.spanFinset_eq_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K} : FractionalIdeal.spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0

theorem FractionalIdeal.spanFinset_ne_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {ι : Type u_5} {s : Finset ι} {f : ι → K} : FractionalIdeal.spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0

theorem FractionalIdeal.isFractional_span_singleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) : IsFractional S (Submodule.span R {x})

theorem FractionalIdeal.spanSingleton_def {R : Type u_5} [CommRing R] (S : Submonoid R) {P : Type u_6} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) : FractionalIdeal.spanSingleton S x = { val := Submodule.span R {x}, property := (_ : IsFractional S (Submodule.span R {x})) }

@[irreducible]

def FractionalIdeal.spanSingleton {R : Type u_5} [CommRing R] (S : Submonoid R) {P : Type u_6} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) : FractionalIdeal S P

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

Equations

• @FractionalIdeal.spanSingleton = FractionalIdeal.wrapped✝.1

@[simp]

theorem FractionalIdeal.coe_spanSingleton {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) : ↑(FractionalIdeal.spanSingleton S x) = Submodule.span R {x}

@[simp]

theorem FractionalIdeal.mem_spanSingleton {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {y : P} : x ∈ FractionalIdeal.spanSingleton S y ↔ ∃ (z : R), z • y = x

theorem FractionalIdeal.mem_spanSingleton_self {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) : x ∈ FractionalIdeal.spanSingleton S x

@[simp]

theorem FractionalIdeal.spanSingleton_le_iff_mem {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} : FractionalIdeal.spanSingleton S x ≤ I ↔ x ∈ I

theorem FractionalIdeal.spanSingleton_eq_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] [NoZeroSMulDivisors R P] {x : P} {y : P} : FractionalIdeal.spanSingleton S x = FractionalIdeal.spanSingleton S y ↔ ∃ (z : Rˣ), z • x = y

theorem FractionalIdeal.eq_spanSingleton_of_principal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (I : FractionalIdeal S P) [Submodule.IsPrincipal ↑I] : I = FractionalIdeal.spanSingleton S (Submodule.IsPrincipal.generator ↑I)

theorem FractionalIdeal.isPrincipal_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (I : FractionalIdeal S P) : Submodule.IsPrincipal ↑I ↔ ∃ (x : P), I = FractionalIdeal.spanSingleton S x

@[simp]

theorem FractionalIdeal.spanSingleton_zero {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] : FractionalIdeal.spanSingleton S 0 = 0

theorem FractionalIdeal.spanSingleton_eq_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {y : P} : FractionalIdeal.spanSingleton S y = 0 ↔ y = 0

theorem FractionalIdeal.spanSingleton_ne_zero_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {y : P} : FractionalIdeal.spanSingleton S y ≠ 0 ↔ y ≠ 0

@[simp]

theorem FractionalIdeal.spanSingleton_one {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] : FractionalIdeal.spanSingleton S 1 = 1

@[simp]

theorem FractionalIdeal.spanSingleton_mul_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (y : P) : FractionalIdeal.spanSingleton S x * FractionalIdeal.spanSingleton S y = FractionalIdeal.spanSingleton S (x * y)

@[simp]

theorem FractionalIdeal.spanSingleton_pow {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (n : ℕ) : FractionalIdeal.spanSingleton S x ^ n = FractionalIdeal.spanSingleton S (x ^ n)

@[simp]

theorem FractionalIdeal.coeIdeal_span_singleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : R) : ↑(Ideal.span {x}) = FractionalIdeal.spanSingleton S ((algebraMap R P) x)

@[simp]

theorem FractionalIdeal.canonicalEquiv_spanSingleton {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {P' : Type u_5} [CommRing P'] [Algebra R P'] [IsLocalization S P'] (x : P) : (FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.spanSingleton S x) = FractionalIdeal.spanSingleton S ((IsLocalization.map P' (RingHom.id R) (_ : ∀ y ∈ S, (RingHom.id R) y ∈ S)) x)

theorem FractionalIdeal.mem_singleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {y : P} {I : FractionalIdeal S P} : y ∈ FractionalIdeal.spanSingleton S x * I ↔ ∃ y' ∈ I, y = x * y'

theorem FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal {R₁ : Type u_3} [CommRing R₁] (K : Type u_4) [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {I : Ideal R₁} {J : Ideal R₁} {x : R₁} {y : R₁} (hy : y ∈ nonZeroDivisors R₁) : FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (IsLocalization.mk' K x { val := y, property := hy }) * ↑I = ↑J ↔ Ideal.span {x} * I = Ideal.span {y} * J

theorem FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] {I : Ideal R₁} {J : Ideal R₁} {z : K} : FractionalIdeal.spanSingleton (nonZeroDivisors R₁) z * ↑I = ↑J ↔ Ideal.span {(IsLocalization.sec (nonZeroDivisors R₁) z).1} * I = Ideal.span {↑(IsLocalization.sec (nonZeroDivisors R₁) z).2} * J

theorem FractionalIdeal.one_div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (x : K) : 1 / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x⁻¹

@[simp]

theorem FractionalIdeal.div_spanSingleton {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (J : FractionalIdeal (nonZeroDivisors R₁) K) (d : K) : J / FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) d⁻¹ * J

theorem FractionalIdeal.exists_eq_spanSingleton_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsFractionRing R₁ K] [IsDomain R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) : ∃ (a : R₁) (aI : Ideal R₁), a ≠ 0 ∧ I = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) a)⁻¹ * ↑aI

instance FractionalIdeal.isPrincipal {K : Type u_4} [Field K] {R : Type u_5} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Algebra R K] [IsFractionRing R K] (I : FractionalIdeal (nonZeroDivisors R) K) : Submodule.IsPrincipal ↑I

Equations

• (_ : Submodule.IsPrincipal ↑I) = (_ : Submodule.IsPrincipal ↑I)

theorem FractionalIdeal.le_spanSingleton_mul_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} : I ≤ FractionalIdeal.spanSingleton S x * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

theorem FractionalIdeal.spanSingleton_mul_le_iff {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} : FractionalIdeal.spanSingleton S x * I ≤ J ↔ ∀ z ∈ I, x * z ∈ J

theorem FractionalIdeal.eq_spanSingleton_mul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] {x : P} {I : FractionalIdeal S P} {J : FractionalIdeal S P} : I = FractionalIdeal.spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

theorem FractionalIdeal.isNoetherian_zero {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] : IsNoetherian R₁ ↥↑0

theorem FractionalIdeal.isNoetherian_iff {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] {I : FractionalIdeal (nonZeroDivisors R₁) K} : IsNoetherian R₁ ↥↑I ↔ ∀ J ≤ I, Submodule.FG ↑J

theorem FractionalIdeal.isNoetherian_coeIdeal {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [IsNoetherianRing R₁] (I : Ideal R₁) : IsNoetherian R₁ ↥↑↑I

theorem FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] (x : R₁) {I : FractionalIdeal (nonZeroDivisors R₁) K} (hI : IsNoetherian R₁ ↥↑I) : IsNoetherian R₁ ↥↑(FractionalIdeal.spanSingleton (nonZeroDivisors R₁) ((algebraMap R₁ K) x)⁻¹ * I)

theorem FractionalIdeal.isNoetherian {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] [IsNoetherianRing R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K) : IsNoetherian R₁ ↥↑I

Every fractional ideal of a noetherian integral domain is noetherian.

theorem FractionalIdeal.isFractional_adjoin_integral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (hx : IsIntegral R x) : IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))

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

def FractionalIdeal.adjoinIntegral {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (hx : IsIntegral R x) : FractionalIdeal S P

FractionalIdeal.adjoinIntegral (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

• FractionalIdeal.adjoinIntegral S x hx = { val := Subalgebra.toSubmodule (Algebra.adjoin R {x}), property := (_ : IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))) }

@[simp]

theorem FractionalIdeal.adjoinIntegral_coe {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (hx : IsIntegral R x) : ↑(FractionalIdeal.adjoinIntegral S x hx) = Subalgebra.toSubmodule (Algebra.adjoin R {x})

theorem FractionalIdeal.mem_adjoinIntegral_self {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] [loc : IsLocalization S P] (x : P) (hx : IsIntegral R x) : x ∈ FractionalIdeal.adjoinIntegral S x hx