Documentation

Mathlib.RingTheory.FractionalIdeal.Operations

More operations on fractional ideals #

Main definitions #

Let K be the localization of R at R⁰ = R \ {0} (i.e. the field of fractions).

Main statement #

References #

Tags #

fractional ideal, fractional ideals, invertible ideal

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 IIsFractional S (Submodule.map g.toLinearMap 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') :

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

Equations
Instances For
    @[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 g.toLinearMap 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 xI, 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) :
    @[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'') :
    @[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) :
    @[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') :
    @[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') :
    @[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') :
    @[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') :
    @[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 (g.symm) (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 (g.symm) 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} :
    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) :
    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') :

    If g is an equivalence, map g is an isomorphism

    Equations
    Instances For
      @[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') :
      @[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) :
      @[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') :
      @[simp]
      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) aS, bs, 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 : I.FG) :
      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) :
      (I).FG I.FG
      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)ˣ) :
      (I).FG
      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) :
      (I).FG
      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) :
      I.FG
      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) ; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := })
      @[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'] :

      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
      Instances For
        @[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 yI, (IsLocalization.map P' (RingHom.id R) ) 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'] :
        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') :
        @[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) :
        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''] :
        @[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) :

        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) :
        @[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] :
        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
        theorem FractionalIdeal.num_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] {I : FractionalIdeal (nonZeroDivisors R) K} :
        I.num = 0 I = 0

        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.

        Equations
        • =
        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} :
        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.instDivNonZeroDivisors {R₁ : Type u_3} [CommRing R₁] {K : Type u_4} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K] [IsDomain R₁] :
        Equations
        @[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 = 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 yJ, 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' xI, yJ', 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') :
        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.span_finset R₁ s f is the fractional ideal of R₁ generated by f '' s.

        Equations
        Instances For
          @[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 js, 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 js, 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) :
          @[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) :

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

          Equations
          Instances For
            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) :
            @[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) :
            @[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.den_mul_self_eq_num' {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) :
            FractionalIdeal.spanSingleton S ((algebraMap R P) I.den) * I = I.num

            A version of FractionalIdeal.den_mul_self_eq_num in terms of fractional ideals.

            @[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} :
            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) :
            (I).IsPrincipal ∃ (x : P), I = FractionalIdeal.spanSingleton S x
            @[simp]
            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} :
            @[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] :
            @[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 : ) :
            @[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) :
            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₁) :
            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} :
            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
            theorem FractionalIdeal.ideal_factor_ne_zero {R : Type u_6} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) {a : R} {J : Ideal R} (haJ : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * J) :
            J 0

            If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then J is nonzero.

            theorem FractionalIdeal.constant_factor_ne_zero {R : Type u_6} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} (hI : I 0) {a : R} {J : Ideal R} (haJ : I = FractionalIdeal.spanSingleton (nonZeroDivisors R) ((algebraMap R K) a)⁻¹ * J) :

            If I is a nonzero fractional ideal, a ∈ R, and J is an ideal of R such that I = a⁻¹J, then a is nonzero.

            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) :
            (I).IsPrincipal
            Equations
            • =
            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 zII, zJJ, 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 zI, 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 (zII, zJJ, x * zJ = zI) zJ, x * z I
            theorem FractionalIdeal.num_le {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) :
            I.num 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 JI, (J).FG
            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) :
            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.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
            Instances For
              @[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) :