Documentation

Mathlib.RingTheory.Ideal.Defs

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
      class Ideal.IsTwoSided {α : Type u} [Semiring α] (I : Ideal α) :

      A left ideal I : Ideal R is two-sided if it is also a right ideal.

      • mul_mem_of_left {a : α} (b : α) : a Ia * b I
      Instances
        theorem Ideal.isTwoSided_iff {α : Type u} [Semiring α] (I : Ideal α) :
        I.IsTwoSided ∀ {a : α} (b : α), a Ia * b I
        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.mul_mem_right {α : Type u_1} {a : α} (b : α) [Semiring α] (I : Ideal α) [I.IsTwoSided] (h : a I) :
        a * b I
        theorem Ideal.ext {α : Type u} [Semiring α] {I J : Ideal α} (h : ∀ (x : α), x I x J) :
        I = J
        theorem Ideal.ext_iff {α : Type u} [Semiring α] {I J : Ideal α} :
        I = J ∀ (x : α), x I x J
        @[simp]
        theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x y : α} (hy : IsUnit y) :
        y * x I x I
        theorem Ideal.pow_mem_of_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} (ha : a I) (n : ) (hn : 0 < n) :
        a ^ n I
        theorem Ideal.pow_mem_of_pow_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} {m n : } (ha : a ^ m I) (h : m n) :
        a ^ n I
        def Module.eqIdeal (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (m m' : M) :

        For two elements m and m' in an R-module M, the set of elements r : R with equal scalar product with m and m' is an ideal of R. If M is a group, this coincides with the kernel of LinearMap.toSpanSingleton R M (m - m').

        Equations
          Instances For
            instance Ideal.instIsTwoSided {α : Type u} [CommSemiring α] (I : Ideal α) :
            instance Ideal.instIsTwoSided_1 {α : Type u_1} [CommRing α] (I : Ideal α) :
            @[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_of_dvd {α : Type u} {a b : α} [CommSemiring α] (I : Ideal α) (hab : a b) (ha : a I) :
            b I
            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.mul_sub_mul_mem {α : Type u} [Ring α] (I : Ideal α) {a b c d : α} [I.IsTwoSided] (h1 : a - b I) (h2 : c - d I) :
            a * c - b * d I