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

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.instCoeOutSubmodule {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

• FractionalIdeal.instCoeOutSubmodule = { coe := FractionalIdeal.coeToSubmodule }

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

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

An element of S such that I.den • I = I.num, see FractionalIdeal.num and FractionalIdeal.den_mul_self_eq_num.

Equations

• I.den = ⟨Exists.choose ⋯, ⋯⟩

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

An ideal of R such that I.den • I = I.num, see FractionalIdeal.den and FractionalIdeal.den_mul_self_eq_num.

Equations

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

theorem FractionalIdeal.den_mul_self_eq_num {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) : I.den • ↑I = Submodule.map (Algebra.linearMap R P) I.num

noncomputable def FractionalIdeal.equivNum {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P} (h_nz : ↑I.den ≠ 0) : ↥↑I ≃ₗ[R] ↥I.num

The linear equivalence between the fractional ideal I and the integral ideal I.num defined by mapping x to den I • x.

Equations

• FractionalIdeal.equivNum h_nz = (LinearEquiv.ofBijective ((DistribMulAction.toLinearMap R P I.den).restrict ⋯) ⋯).trans (Submodule.equivMapOfInjective (Algebra.linearMap R P) ⋯ I.num).symm

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

Equations

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

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

@[simp]

theorem FractionalIdeal.equivNum_apply {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P} (h_nz : ↑I.den ≠ 0) (x : ↥I) : (algebraMap R P) ↑((FractionalIdeal.equivNum h_nz) x) = I.den • ↑x

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

• p.copy s hs = ⟨(↑p).copy 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) : ↑(p.copy 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) : p.copy 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) : ↑⟨I, 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.instModuleSubtypeMemSubmoduleCoeToSubmodule {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

• I.instModuleSubtypeMemSubmoduleCoeToSubmodule = (↑I).module

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 = ⟨IsLocalization.coeSubmodule P I, ⋯⟩

instance FractionalIdeal.instCoeTCIdeal {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.instCoeTCIdeal = { 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.instZero {R : Type u_1} [CommRing R] (S : Submonoid R) {P : Type u_2} [CommRing P] [Algebra R P] : Zero (FractionalIdeal S P)

Equations

• FractionalIdeal.instZero 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.instInhabited {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Inhabited (FractionalIdeal S P)

Equations

• FractionalIdeal.instInhabited = { default := 0 }

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

Equations

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

theorem FractionalIdeal.zero_of_num_eq_bot {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] [NoZeroSMulDivisors R P] (hS : 0 ∉ S) {I : FractionalIdeal S P} (hI : I.num = ⊥) : I = 0

theorem FractionalIdeal.num_zero_eq {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (h_inj : Function.Injective ⇑(algebraMap R P)) : FractionalIdeal.num 0 = 0

@[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 ⋯

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

Equations

• FractionalIdeal.instInf = { inf := fun (I J : FractionalIdeal S P) => ⟨↑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.instSup {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Sup (FractionalIdeal S P)

Equations

• FractionalIdeal.instSup = { sup := fun (I J : FractionalIdeal S P) => ⟨↑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

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

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

Equations

• FractionalIdeal.instSemilatticeSup = let __src := FractionalIdeal.lattice; SemilatticeSup.mk ⋯ ⋯ ⋯

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

Equations

• FractionalIdeal.instAdd = { 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.instSMulNat {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : SMul ℕ (FractionalIdeal S P)

Equations

• FractionalIdeal.instSMulNat = { smul := fun (n : ℕ) (I : FractionalIdeal S P) => ⟨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) : I.mul J = ⟨↑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.instMul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Mul (FractionalIdeal S P)

Equations

• FractionalIdeal.instMul = { mul := fun (I J : FractionalIdeal S P) => I.mul 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) : I.mul 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 = ⟨↑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.instPowNat {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : Pow (FractionalIdeal S P) ℕ

Equations

• FractionalIdeal.instPowNat = { pow := fun (I : FractionalIdeal S P) (n : ℕ) => ⟨↑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.instNatCast {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] : NatCast (FractionalIdeal S P)

Equations

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

theorem FractionalIdeal.coe_natCast {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

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

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

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

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

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

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)