Documentation

Mathlib.RingTheory.FractionalIdeal.Basic

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.

Main statements #

Implementation notes #

Fractional ideals are considered equal when they contain the same elements, independent of the denominator a : R such that a I ⊆ R. Thus, we define 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 #

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) :

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

Equations
Instances For
    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
    Instances For
      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) :

      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
        instance FractionalIdeal.instCoeOutSubmodule {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra 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) :
        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
        Instances For
          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) :

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

          Equations
          Instances For
            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
            Instances For
              instance FractionalIdeal.instSetLike {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R 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) :

              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,
              Instances For
                @[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
                theorem FractionalIdeal.zero_mem {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : FractionalIdeal S P) :
                0 I
                @[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) :
                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) :
                def FractionalIdeal.coeIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] (I : Ideal R) :

                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
                Instances For
                  instance FractionalIdeal.instCoeTCIdeal {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R 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) :
                  @[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] :
                  Equations
                  @[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] :
                  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] :
                  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 : 0S) {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)) :
                  @[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

                  (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] :
                  Equations
                  @[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 xI, 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 IIsFractional S JIsFractional 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] :
                  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] :
                  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] :
                  Equations
                  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] :
                  Equations
                  @[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 IIsFractional S (n I)
                  instance FractionalIdeal.instSMulNat {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] :
                  Equations
                  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 IIsFractional S JIsFractional 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.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
                    instance FractionalIdeal.instMul {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] :
                    Equations
                    @[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 iI, jJ, i * j K
                    instance FractionalIdeal.instPowNat {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R 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 : PProp} {r : P} (hr : r I * J) (hm : iI, jJ, C (i * j)) (ha : ∀ (x y : P), C xC yC (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] :
                    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
                    @[deprecated FractionalIdeal.coe_natCast]
                    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

                    Alias of FractionalIdeal.coe_natCast.

                    instance FractionalIdeal.commSemiring {R : Type u_1} [CommRing R] {S : Submonoid R} {P : Type u_2} [CommRing P] [Algebra R P] :
                    Equations
                    @[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.coeToSubmodule as a bundled RingHom.

                    Equations
                    Instances For
                      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) :
                      def FractionalIdeal.coeIdealHom {R : Type u_1} [CommRing R] (S : Submonoid R) (P : Type u_2) [CommRing P] [Algebra R 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' := }
                      Instances For
                        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) :
                        (∏ᶠ (a : α), f a) = ∏ᶠ (a : α), (f a)
                        theorem FractionalIdeal.fg_of_isNoetherianRing {R : Type u_3} [CommRing R] [Nontrivial R] {S : Submonoid R} {P : Type u_4} [Nontrivial P] [CommRing P] [Algebra R P] [NoZeroSMulDivisors R P] [hR : IsNoetherianRing R] (hS : S nonZeroDivisors R) (I : FractionalIdeal S P) :
                        (I).FG

                        The fractional ideals of a Noetherian ring are finitely generated.