Documentation

Mathlib.RingTheory.Ideal.Basic

Ideals over a ring #

This file contains an assortment of definitions and results for 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.

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.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.pow_multiset_sum_mem_span_pow {α : Type u} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ) :
    s.sum ^ (s.card * 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.span_range_pow_eq_top {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ) (n : s) :
    Ideal.span (Set.range fun (x : s) => x ^ n x) =

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

    Equations
    Instances For

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

      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