Documentation

Mathlib.RingTheory.Ideal.Basic

Ideals over a ring #

This file defines Ideal R, the type of (left) ideals over a ring R. Note that over commutative rings, left ideals and two-sided ideals are equivalent.

Implementation notes #

Ideal R is implemented using Submodule R R, where is interpreted as *.

TODO #

Support right ideals, and two-sided ideals over non-commutative rings.

@[reducible, inline]
abbrev Ideal (R : Type u) [Semiring R] :

A (left) ideal in a semiring R is an additive submonoid s such that a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.

Equations
Instances For

    A ring is a principal ideal ring if all (left) ideals are principal.

    Instances
      theorem Ideal.zero_mem {α : Type u} [Semiring α] (I : Ideal α) :
      0 I
      theorem Ideal.add_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} {b : α} :
      a Ib Ia + b I
      theorem Ideal.mul_mem_left {α : Type u} [Semiring α] (I : Ideal α) (a : α) {b : α} :
      b Ia * b I
      theorem Ideal.ext_iff {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} :
      I = J ∀ (x : α), x I x J
      theorem Ideal.ext {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (h : ∀ (x : α), x I x J) :
      I = J
      theorem Ideal.sum_mem {α : Type u} [Semiring α] (I : Ideal α) {ι : Type u_1} {t : Finset ι} {f : ια} :
      (∀ ct, f c I)it, f i I
      theorem Ideal.eq_top_of_unit_mem {α : Type u} [Semiring α] (I : Ideal α) (x : α) (y : α) (hx : x I) (h : y * x = 1) :
      I =
      theorem Ideal.eq_top_of_isUnit_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} (hx : x I) (h : IsUnit x) :
      I =
      theorem Ideal.eq_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) :
      I = 1 I
      theorem Ideal.ne_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) :
      I 1I
      @[simp]
      theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) :
      y * x I x I
      def Ideal.span {α : Type u} [Semiring α] (s : Set α) :

      The ideal generated by a subset of a ring

      Equations
      Instances For
        @[simp]
        theorem Ideal.submodule_span_eq {α : Type u} [Semiring α] {s : Set α} :
        @[simp]
        @[simp]
        theorem Ideal.span_univ {α : Type u} [Semiring α] :
        Ideal.span Set.univ =
        theorem Ideal.span_union {α : Type u} [Semiring α] (s : Set α) (t : Set α) :
        theorem Ideal.span_iUnion {α : Type u} [Semiring α] {ι : Sort u_1} (s : ιSet α) :
        Ideal.span (⋃ (i : ι), s i) = ⨆ (i : ι), Ideal.span (s i)
        theorem Ideal.mem_span {α : Type u} [Semiring α] {s : Set α} (x : α) :
        x Ideal.span s ∀ (p : Ideal α), s px p
        theorem Ideal.subset_span {α : Type u} [Semiring α] {s : Set α} :
        s (Ideal.span s)
        theorem Ideal.span_le {α : Type u} [Semiring α] {s : Set α} {I : Ideal α} :
        Ideal.span s I s I
        theorem Ideal.span_mono {α : Type u} [Semiring α] {s : Set α} {t : Set α} :
        @[simp]
        theorem Ideal.span_eq {α : Type u} [Semiring α] (I : Ideal α) :
        Ideal.span I = I
        @[simp]
        theorem Ideal.mem_span_insert {α : Type u} [Semiring α] {s : Set α} {x : α} {y : α} :
        x Ideal.span (insert y s) ∃ (a : α), zIdeal.span s, x = a * y + z
        theorem Ideal.mem_span_singleton' {α : Type u} [Semiring α] {x : α} {y : α} :
        x Ideal.span {y} ∃ (a : α), a * y = x
        theorem Ideal.mem_span_singleton_self {α : Type u} [Semiring α] (x : α) :
        theorem Ideal.span_singleton_le_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} :
        Ideal.span {x} I x I
        theorem Ideal.span_singleton_mul_left_unit {α : Type u} [Semiring α] {a : α} (h2 : IsUnit a) (x : α) :
        theorem Ideal.span_insert {α : Type u} [Semiring α] (x : α) (s : Set α) :
        theorem Ideal.span_eq_bot {α : Type u} [Semiring α] {s : Set α} :
        Ideal.span s = xs, x = 0
        @[simp]
        theorem Ideal.span_singleton_eq_bot {α : Type u} [Semiring α] {x : α} :
        Ideal.span {x} = x = 0
        theorem Ideal.span_singleton_ne_top {α : Type u_1} [CommSemiring α] {x : α} (hx : ¬IsUnit x) :
        @[simp]
        theorem Ideal.span_zero {α : Type u} [Semiring α] :
        @[simp]
        theorem Ideal.span_one {α : Type u} [Semiring α] :
        theorem Ideal.span_eq_top_iff_finite {α : Type u} [Semiring α] (s : Set α) :
        Ideal.span s = ∃ (s' : Finset α), s' s Ideal.span s' =
        theorem Ideal.mem_span_singleton_sup {α : Type u} [Semiring α] {x : α} {y : α} {I : Ideal α} :
        x Ideal.span {y} I ∃ (a : α), bI, a * y + b = x
        def Ideal.ofRel {α : Type u} [Semiring α] (r : ααProp) :

        The ideal generated by an arbitrary binary relation.

        Equations
        Instances For
          class Ideal.IsPrime {α : Type u} [Semiring α] (I : Ideal α) :

          An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P

          • ne_top' : I

            The prime ideal is not the entire ring.

          • mem_or_mem' : ∀ {x y : α}, x * y Ix I y I

            If a product lies in the prime ideal, then at least one element lies in the prime ideal.

          Instances
            theorem Ideal.IsPrime.ne_top' {α : Type u} :
            ∀ {inst : Semiring α} {I : Ideal α} [self : I.IsPrime], I

            The prime ideal is not the entire ring.

            theorem Ideal.IsPrime.mem_or_mem' {α : Type u} :
            ∀ {inst : Semiring α} {I : Ideal α} [self : I.IsPrime] {x y : α}, x * y Ix I y I

            If a product lies in the prime ideal, then at least one element lies in the prime ideal.

            theorem Ideal.isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} :
            I.IsPrime I ∀ {x y : α}, x * y Ix I y I
            theorem Ideal.IsPrime.ne_top {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) :
            theorem Ideal.IsPrime.mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x : α} {y : α} :
            x * y Ix I y I
            theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {x : α} {y : α} (h : x * y = 0) :
            x I y I
            theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ) (H : r ^ n I) :
            r I
            theorem Ideal.not_isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} :
            ¬I.IsPrime I = ∃ (x : α) (_ : xI) (y : α) (_ : yI), x * y I
            theorem Ideal.zero_ne_one_of_proper {α : Type u} [Semiring α] {I : Ideal α} (h : I ) :
            0 1
            theorem Ideal.bot_prime {α : Type u} [Semiring α] [IsDomain α] :
            .IsPrime
            class Ideal.IsMaximal {α : Type u} [Semiring α] (I : Ideal α) :

            An ideal is maximal if it is maximal in the collection of proper ideals.

            • out : IsCoatom I

              The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.

            Instances
              theorem Ideal.IsMaximal.out {α : Type u} :
              ∀ {inst : Semiring α} {I : Ideal α} [self : I.IsMaximal], IsCoatom I

              The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.

              theorem Ideal.isMaximal_def {α : Type u} [Semiring α] {I : Ideal α} :
              I.IsMaximal IsCoatom I
              theorem Ideal.IsMaximal.ne_top {α : Type u} [Semiring α] {I : Ideal α} (h : I.IsMaximal) :
              theorem Ideal.isMaximal_iff {α : Type u} [Semiring α] {I : Ideal α} :
              I.IsMaximal 1I ∀ (J : Ideal α) (x : α), I JxIx J1 J
              theorem Ideal.IsMaximal.eq_of_le {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (hI : I.IsMaximal) (hJ : J ) (IJ : I J) :
              I = J
              instance Ideal.instIsCoatomic {α : Type u} [Semiring α] :
              Equations
              • =
              theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [Semiring α] {M : Ideal α} {M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M M') :
              M M' =
              theorem Ideal.exists_le_maximal {α : Type u} [Semiring α] (I : Ideal α) (hI : I ) :
              ∃ (M : Ideal α), M.IsMaximal I M

              Krull's theorem: if I is an ideal that is not the whole ring, then it is included in some maximal ideal.

              theorem Ideal.exists_maximal (α : Type u) [Semiring α] [Nontrivial α] :
              ∃ (M : Ideal α), M.IsMaximal

              Krull's theorem: a nontrivial ring has a maximal ideal.

              instance Ideal.instNontrivial {α : Type u} [Semiring α] [Nontrivial α] :
              Equations
              • =
              theorem Ideal.maximal_of_no_maximal {α : Type u} [Semiring α] {P : Ideal α} (hmax : ∀ (m : Ideal α), P < m¬m.IsMaximal) (J : Ideal α) (hPJ : P < J) :
              J =

              If P is not properly contained in any maximal ideal then it is not properly contained in any proper ideal

              theorem Ideal.span_pair_comm {α : Type u} [Semiring α] {x : α} {y : α} :
              Ideal.span {x, y} = Ideal.span {y, x}
              theorem Ideal.mem_span_pair {α : Type u} [Semiring α] {x : α} {y : α} {z : α} :
              z Ideal.span {x, y} ∃ (a : α) (b : α), a * x + b * y = z
              @[simp]
              theorem Ideal.span_pair_add_mul_left {R : Type u} [CommRing R] {x : R} {y : R} (z : R) :
              Ideal.span {x + y * z, y} = Ideal.span {x, y}
              @[simp]
              theorem Ideal.span_pair_add_mul_right {R : Type u} [CommRing R] {x : R} {y : R} (z : R) :
              Ideal.span {x, y + x * z} = Ideal.span {x, y}
              theorem Ideal.IsMaximal.exists_inv {α : Type u} [Semiring α] {I : Ideal α} (hI : I.IsMaximal) {x : α} (hx : xI) :
              ∃ (y : α), iI, y * x + i = 1
              theorem Ideal.mem_sup_left {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} :
              x Sx S T
              theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} :
              x Tx S T
              theorem Ideal.mem_iSup_of_mem {R : Type u} [Semiring R] {ι : Sort u_1} {S : ιIdeal R} (i : ι) {x : R} :
              x S ix iSup S
              theorem Ideal.mem_sSup_of_mem {R : Type u} [Semiring R] {S : Set (Ideal R)} {s : Ideal R} (hs : s S) {x : R} :
              x sx sSup S
              theorem Ideal.mem_sInf {R : Type u} [Semiring R] {s : Set (Ideal R)} {x : R} :
              x sInf s ∀ ⦃I : Ideal R⦄, I sx I
              @[simp]
              theorem Ideal.mem_inf {R : Type u} [Semiring R] {I : Ideal R} {J : Ideal R} {x : R} :
              x I J x I x J
              @[simp]
              theorem Ideal.mem_iInf {R : Type u} [Semiring R] {ι : Sort u_1} {I : ιIdeal R} {x : R} :
              x iInf I ∀ (i : ι), x I i
              @[simp]
              theorem Ideal.mem_bot {R : Type u} [Semiring R] {x : R} :
              x x = 0
              def Ideal.pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) :
              Ideal (ια)

              I^n as an ideal of R^n.

              Equations
              • I.pi ι = { carrier := {x : ια | ∀ (i : ι), x i I}, add_mem' := , zero_mem' := , smul_mem' := }
              Instances For
                theorem Ideal.mem_pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) (x : ια) :
                x I.pi ι ∀ (i : ι), x i I
                theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [Semiring α] {s : Set (Ideal α)} (hs : s.Nonempty) (hs' : IsChain (fun (x1 x2 : Ideal α) => x1 x2) s) (H : ps, p.IsPrime) :
                (sInf s).IsPrime
                @[simp]
                theorem Ideal.mul_unit_mem_iff_mem {α : Type u} [CommSemiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) :
                x * y I x I
                theorem Ideal.mem_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} :
                x Ideal.span {y} y x
                theorem Ideal.span_singleton_le_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} :
                theorem Ideal.span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain α] {x : α} {y : α} :
                theorem Ideal.span_singleton_mul_right_unit {α : Type u} [CommSemiring α] {a : α} (h2 : IsUnit a) (x : α) :
                @[simp]
                theorem Ideal.span_singleton_eq_top {α : Type u} [CommSemiring α] {x : α} :
                theorem Ideal.span_singleton_prime {α : Type u} [CommSemiring α] {p : α} (hp : p 0) :
                (Ideal.span {p}).IsPrime Prime p
                theorem Ideal.IsMaximal.isPrime {α : Type u} [CommSemiring α] {I : Ideal α} (H : I.IsMaximal) :
                I.IsPrime
                @[instance 100]
                instance Ideal.IsMaximal.isPrime' {α : Type u} [CommSemiring α] (I : Ideal α) [_H : I.IsMaximal] :
                I.IsPrime
                Equations
                • =
                theorem Ideal.factors_decreasing {α : Type u} [CommSemiring α] [IsDomain α] (b₁ : α) (b₂ : α) (h₁ : b₁ 0) (h₂ : ¬IsUnit b₂) :
                Ideal.span {b₁ * b₂} < Ideal.span {b₁}
                theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [CommSemiring α] (I : Ideal α) (h : a I) :
                a * b I
                theorem Ideal.mem_of_dvd {α : Type u} {a : α} {b : α} [CommSemiring α] (I : Ideal α) (hab : a b) (ha : a I) :
                b I
                theorem Ideal.pow_mem_of_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) (ha : a I) (n : ) (hn : 0 < n) :
                a ^ n I
                theorem Ideal.pow_mem_of_pow_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) {m : } {n : } (ha : a ^ m I) (h : m n) :
                a ^ n I
                theorem Ideal.add_pow_mem_of_pow_mem_of_le {α : Type u} {a : α} {b : α} [CommSemiring α] (I : Ideal α) {m : } {n : } {k : } (ha : a ^ m I) (hb : b ^ n I) (hk : m + n k + 1) :
                (a + b) ^ k I
                theorem Ideal.add_pow_add_pred_mem_of_pow_mem {α : Type u} {a : α} {b : α} [CommSemiring α] (I : Ideal α) {m : } {n : } (ha : a ^ m I) (hb : b ^ n I) :
                (a + b) ^ (m + n - 1) I
                theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : I.IsPrime) {x : α} {y : α} :
                x * y I x I y I
                theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ) (hn : 0 < n) :
                r ^ n I r I
                theorem Ideal.pow_multiset_sum_mem_span_pow {α : Type u} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ) :
                s.sum ^ (Multiset.card s * n + 1) Ideal.span (Multiset.map (fun (x : α) => x ^ (n + 1)) s).toFinset
                theorem Ideal.sum_pow_mem_span_pow {α : Type u} [CommSemiring α] {ι : Type u_1} (s : Finset ι) (f : ια) (n : ) :
                (∑ is, f i) ^ (s.card * n + 1) Ideal.span ((fun (i : ι) => f i ^ (n + 1)) '' s)
                theorem Ideal.span_pow_eq_top {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ) (n : ) :
                Ideal.span ((fun (x : α) => x ^ n) '' s) =
                theorem Ideal.isPrime_of_maximally_disjoint {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint I S) (maximally_disjoint : ∀ (J : Ideal α), I < J¬Disjoint J S) :
                I.IsPrime
                theorem Ideal.neg_mem_iff {α : Type u} [Ring α] (I : Ideal α) {a : α} :
                -a I a I
                theorem Ideal.add_mem_iff_left {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} :
                b I(a + b I a I)
                theorem Ideal.add_mem_iff_right {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} :
                a I(a + b I b I)
                theorem Ideal.sub_mem {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} :
                a Ib Ia - b I
                theorem Ideal.mem_span_insert' {α : Type u} [Ring α] {s : Set α} {x : α} {y : α} :
                x Ideal.span (insert y s) ∃ (a : α), x + a * y Ideal.span s
                @[simp]
                theorem Ideal.span_singleton_neg {α : Type u} [Ring α] (x : α) :
                theorem Ideal.eq_bot_or_top {K : Type u} [DivisionSemiring K] (I : Ideal K) :
                I = I =

                All ideals in a division (semi)ring are trivial.

                A bijection between (left) ideals of a division ring and {0, 1}, sending to 0 and to 1.

                Equations
                Instances For
                  Equations
                  • =

                  Ideals of a DivisionSemiring are a simple order. Thanks to the way abbreviations work, this automatically gives an IsSimpleModule K instance.

                  Equations
                  • =
                  theorem Ideal.eq_bot_of_prime {K : Type u} [DivisionSemiring K] (I : Ideal K) [h : I.IsPrime] :
                  I =
                  theorem Ideal.bot_isMaximal {K : Type u} [DivisionSemiring K] :
                  .IsMaximal
                  theorem Ideal.mul_sub_mul_mem {R : Type u_1} [CommRing R] (I : Ideal R) {a : R} {b : R} {c : R} {d : R} (h1 : a - b I) (h2 : c - d I) :
                  a * c - b * d I
                  theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] (hf : ¬IsField R) :
                  ∃ (x : R) (_ : x 0), ¬IsUnit x
                  theorem Ring.not_isField_iff_exists_prime {R : Type u_1} [CommSemiring R] [Nontrivial R] :
                  ¬IsField R ∃ (p : Ideal R), p p.IsPrime

                  Also see Ideal.isSimpleOrder for the forward direction as an instance when R is a division (semi)ring.

                  This result actually holds for all division semirings, but we lack the predicate to state it.

                  theorem Ring.ne_bot_of_isMaximal_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] {M : Ideal R} (max : M.IsMaximal) (not_field : ¬IsField R) :

                  When a ring is not a field, the maximal ideals are nontrivial.

                  theorem Ideal.bot_lt_of_maximal {R : Type u} [CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) :
                  < M
                  def nonunits (α : Type u) [Monoid α] :
                  Set α

                  The set of non-invertible elements of a monoid.

                  Equations
                  Instances For
                    @[simp]
                    theorem mem_nonunits_iff {α : Type u} {a : α} [Monoid α] :
                    theorem mul_mem_nonunits_right {α : Type u} {a : α} {b : α} [CommMonoid α] :
                    b nonunits αa * b nonunits α
                    theorem mul_mem_nonunits_left {α : Type u} {a : α} {b : α} [CommMonoid α] :
                    a nonunits αa * b nonunits α
                    theorem zero_mem_nonunits {α : Type u} [Semiring α] :
                    0 nonunits α 0 1
                    @[simp]
                    theorem one_not_mem_nonunits {α : Type u} [Monoid α] :
                    1nonunits α
                    @[simp]
                    theorem map_mem_nonunits_iff {α : Type u} {β : Type v} {F : Type w} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a : α) :
                    theorem coe_subset_nonunits {α : Type u} [Semiring α] {I : Ideal α} (h : I ) :
                    I nonunits α
                    theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [CommSemiring α] (h : a nonunits α) :
                    ∃ (I : Ideal α), I.IsMaximal a I