Ideals over a ring
This file defines ideal R, the type of ideals over a commutative ring R.
Implementation notes
ideal R is implemented using submodule R R, where • is interpreted as *.
TODO
Support one-sided ideals, and ideals over non-commutative rings
The ideal generated by a subset of a ring
Equations
- ideal.span s = submodule.span α s
theorem
ideal.span_le
{α : Type u}
[comm_ring α]
{s : set α}
{I : ideal α} :
ideal.span s ≤ I ↔ s ⊆ ↑I
theorem
ideal.span_mono
{α : Type u}
[comm_ring α]
{s t : set α} :
s ⊆ t → ideal.span s ≤ ideal.span t
theorem
ideal.mem_span_insert
{α : Type u}
[comm_ring α]
{s : set α}
{x y : α} :
x ∈ ideal.span (has_insert.insert y s) ↔ ∃ (a z : α) (H : z ∈ ideal.span s), x = a * y + z
theorem
ideal.mem_span_insert'
{α : Type u}
[comm_ring α]
{s : set α}
{x y : α} :
x ∈ ideal.span (has_insert.insert y s) ↔ ∃ (a : α), x + a * y ∈ ideal.span s
theorem
ideal.mem_span_singleton'
{α : Type u}
[comm_ring α]
{x y : α} :
x ∈ ideal.span {y} ↔ ∃ (a : α), a * y = x
theorem
ideal.span_singleton_le_span_singleton
{α : Type u}
[comm_ring α]
{x y : α} :
ideal.span {x} ≤ ideal.span {y} ↔ y ∣ x
theorem
ideal.span_singleton_eq_span_singleton
{α : Type u}
[integral_domain α]
{x y : α} :
ideal.span {x} = ideal.span {y} ↔ associated x y
@[simp]
theorem
ideal.span_singleton_eq_bot
{α : Type u}
[comm_ring α]
{x : α} :
ideal.span {x} = ⊥ ↔ x = 0
theorem
ideal.span_singleton_eq_top
{α : Type u}
[comm_ring α]
{x : α} :
ideal.span {x} = ⊤ ↔ is_unit x
theorem
ideal.span_singleton_mul_right_unit
{α : Type u}
[comm_ring α]
{a : α}
(h2 : is_unit a)
(x : α) :
ideal.span {x * a} = ideal.span {x}
theorem
ideal.span_singleton_mul_left_unit
{α : Type u}
[comm_ring α]
{a : α}
(h2 : is_unit a)
(x : α) :
ideal.span {a * x} = ideal.span {x}
@[class]
An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P
theorem
ideal.span_singleton_prime
{α : Type u}
[comm_ring α]
{p : α} :
p ≠ 0 → ((ideal.span {p}).is_prime ↔ prime p)
@[class]
An ideal is maximal if it is maximal in the collection of proper ideals.
theorem
ideal.is_maximal.eq_of_le
{α : Type u}
[comm_ring α]
{I J : ideal α} :
I.is_maximal → J ≠ ⊤ → I ≤ J → I = J
theorem
ideal.is_maximal.exists_inv
{α : Type u}
[comm_ring α]
{I : ideal α}
(hI : I.is_maximal)
{x : α} :
theorem
ideal.is_maximal.is_prime
{α : Type u}
[comm_ring α]
{I : ideal α} :
I.is_maximal → I.is_prime
@[instance]
def
ideal.is_maximal.is_prime'
{α : Type u}
[comm_ring α]
(I : ideal α)
[H : I.is_maximal] :
I.is_prime
Equations
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}
[comm_ring α]
[nontrivial α] :
∃ (M : ideal α), M.is_maximal
Krull's theorem: a nontrivial ring has a maximal ideal.
theorem
ideal.factors_decreasing
{β : Type v}
[integral_domain β]
(b₁ b₂ : β) :
b₁ ≠ 0 → ¬is_unit b₂ → ideal.span {b₁ * b₂} < ideal.span {b₁}
The quotient R/I of a ring R by an ideal I.
Equations
@[instance]
Equations
@[instance]
Equations
- ideal.quotient.has_mul I = {mul := λ (a b : I.quotient), quotient.lift_on₂' a b (λ (a b : α), submodule.quotient.mk (a * b)) _}
@[instance]
Equations
- ideal.quotient.comm_ring I = {add := add_comm_group.add (submodule.quotient.add_comm_group I), add_assoc := _, zero := add_comm_group.zero (submodule.quotient.add_comm_group I), zero_add := _, add_zero := _, neg := add_comm_group.neg (submodule.quotient.add_comm_group I), add_left_neg := _, add_comm := _, mul := has_mul.mul (ideal.quotient.has_mul I), mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
The ring homomorphism from a ring R to a quotient ring R/I.
Equations
- ideal.quotient.mk I = {to_fun := λ (a : α), submodule.quotient.mk a, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[instance]
Equations
- ideal.quotient.inhabited = {default := ⇑(ideal.quotient.mk I) 37}
theorem
ideal.quotient.eq
{α : Type u}
[comm_ring α]
{I : ideal α}
{x y : α} :
⇑(ideal.quotient.mk I) x = ⇑(ideal.quotient.mk I) y ↔ x - y ∈ I
@[simp]
theorem
ideal.quotient.mk_eq_mk
{α : Type u}
[comm_ring α]
{I : ideal α}
(x : α) :
submodule.quotient.mk x = ⇑(ideal.quotient.mk I) x
theorem
ideal.quotient.eq_zero_iff_mem
{α : Type u}
{a : α}
[comm_ring α]
{I : ideal α} :
⇑(ideal.quotient.mk I) a = 0 ↔ a ∈ I
theorem
ideal.quotient.nontrivial
{α : Type u}
[comm_ring α]
{I : ideal α} :
I ≠ ⊤ → nontrivial I.quotient
@[instance]
Equations
- ideal.quotient.integral_domain I = {add := comm_ring.add (ideal.quotient.comm_ring I), add_assoc := _, zero := comm_ring.zero (ideal.quotient.comm_ring I), zero_add := _, add_zero := _, neg := comm_ring.neg (ideal.quotient.comm_ring I), add_left_neg := _, add_comm := _, mul := comm_ring.mul (ideal.quotient.comm_ring I), mul_assoc := _, one := comm_ring.one (ideal.quotient.comm_ring I), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
theorem
ideal.quotient.exists_inv
{α : Type u}
[comm_ring α]
{I : ideal α}
[hI : I.is_maximal]
{a : I.quotient} :
quotient by maximal ideal is a field. def rather than instance, since users will have computable inverses in some applications
Equations
- ideal.quotient.field I = {add := integral_domain.add (ideal.quotient.integral_domain I), add_assoc := _, zero := integral_domain.zero (ideal.quotient.integral_domain I), zero_add := _, add_zero := _, neg := integral_domain.neg (ideal.quotient.integral_domain I), add_left_neg := _, add_comm := _, mul := integral_domain.mul (ideal.quotient.integral_domain I), mul_assoc := _, one := integral_domain.one (ideal.quotient.integral_domain I), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (a : I.quotient), dite (a = 0) (λ (ha : a = 0), 0) (λ (ha : ¬a = 0), classical.some _), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
def
ideal.quotient.lift
{α : Type u}
{β : Type v}
[comm_ring α]
[comm_ring β]
(S : ideal α)
(f : α →+* β) :
Given a ring homomorphism f : α →+* β sending all elements of an ideal to zero,
lift it to the quotient by this ideal.
@[simp]
theorem
ideal.quotient.lift_mk
{α : Type u}
{β : Type v}
{a : α}
[comm_ring α]
[comm_ring β]
(S : ideal α)
(f : α →+* β)
(H : ∀ (a : α), a ∈ S → ⇑f a = 0) :
⇑(ideal.quotient.lift S f H) (⇑(ideal.quotient.mk S) a) = ⇑f a
theorem
ideal.mem_Sup_of_mem
{R : Type u}
[comm_ring R]
{S : set (ideal R)}
{s : ideal R}
(hs : s ∈ S)
{x : R} :
x ∈ s → x ∈ has_Sup.Sup S
@[instance]
R^n/I^n is a R/I-module.
Equations
- I.module_pi ι = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (c : I.quotient) (m : (I.pi ι).quotient), quotient.lift_on₂' c m (λ (r : α) (m : ι → α), submodule.quotient.mk (r • m)) _}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
R^n/I^n is isomorphic to (R/I)^n as an R/I-module.
Equations
- I.pi_quot_equiv ι = {to_fun := λ (x : (I.pi ι).quotient), quotient.lift_on' x (λ (f : ι → α) (i : ι), ⇑(ideal.quotient.mk I) (f i)) _, map_add' := _, map_smul' := _, inv_fun := λ (x : ι → I.quotient), ⇑(ideal.quotient.mk (I.pi ι)) (λ (i : ι), quotient.out' (x i)), left_inv := _, right_inv := _}
@[simp]
@[class]
- to_nontrivial : nontrivial α
- is_local : ∀ (a : α), is_unit a ∨ is_unit (1 - a)
A commutative ring is local if it has a unique maximal ideal. Note that
local_ring is a predicate.
theorem
local_ring.is_unit_or_is_unit_one_sub_self
{α : Type u}
[comm_ring α]
[local_ring α]
(a : α) :
theorem
local_ring.is_unit_of_mem_nonunits_one_sub_self
{α : Type u}
[comm_ring α]
[local_ring α]
(a : α) :
theorem
local_ring.is_unit_one_sub_self_of_mem_nonunits
{α : Type u}
[comm_ring α]
[local_ring α]
(a : α) :
The ideal of elements that are not units.
Equations
- local_ring.maximal_ideal α = {carrier := nonunits α (ring.to_monoid α), zero_mem' := _, add_mem' := _, smul_mem' := _}
@[instance]
Equations
- _ = _
theorem
local_ring.maximal_ideal_unique
(α : Type u)
[comm_ring α]
[local_ring α] :
∃! (I : ideal α), I.is_maximal
theorem
local_ring.eq_maximal_ideal
{α : Type u}
[comm_ring α]
[local_ring α]
{I : ideal α} :
I.is_maximal → I = local_ring.maximal_ideal α
theorem
local_ring.le_maximal_ideal
{α : Type u}
[comm_ring α]
[local_ring α]
{J : ideal α} :
J ≠ ⊤ → J ≤ local_ring.maximal_ideal α
@[simp]
theorem
local_ring.mem_maximal_ideal
{α : Type u}
[comm_ring α]
[local_ring α]
(x : α) :
x ∈ local_ring.maximal_ideal α ↔ x ∈ nonunits α
theorem
local_of_unique_max_ideal
{α : Type u}
[comm_ring α] :
(∃! (I : ideal α), I.is_maximal) → local_ring α
@[class]
A local ring homomorphism is a homomorphism between local rings such that the image of the maximal ideal of the source is contained within the maximal ideal of the target.
@[simp]
theorem
is_unit_of_map_unit
{α : Type u}
{β : Type v}
[semiring α]
[semiring β]
(f : α →+* β)
[is_local_ring_hom f]
(a : α) :
theorem
of_irreducible_map
{α : Type u}
{β : Type v}
[semiring α]
[semiring β]
(f : α →+* β)
[h : is_local_ring_hom f]
{x : α} :
irreducible (⇑f x) → irreducible x
theorem
map_nonunit
{α : Type u}
{β : Type v}
[comm_ring α]
[local_ring α]
[comm_ring β]
[local_ring β]
(f : α →+* β)
[is_local_ring_hom f]
(a : α) :
a ∈ local_ring.maximal_ideal α → ⇑f a ∈ local_ring.maximal_ideal β
The residue field of a local ring is the quotient of the ring by its maximal ideal.
Equations
@[instance]
Equations
@[instance]
Equations
- local_ring.inhabited α = {default := 37}
The quotient map from a local ring to its residue field.
Equations
def
local_ring.residue_field.map
{α : Type u}
{β : Type v}
[comm_ring α]
[local_ring α]
[comm_ring β]
[local_ring β]
(f : α →+* β)
[is_local_ring_hom f] :
The map on residue fields induced by a local homomorphism between local rings
Equations
@[instance]