mathlib docs: ring_theory.ideal.basic

source

def ideal (R : Type u) [comm_ring R] :

Type u

Ideal in a commutative ring is an additive subgroup s such that a * b ∈ s whenever b ∈ s.

Equations

ideal R = submodule R R

source

theorem ideal.zero_mem {α : Type u} [comm_ring α] (I : ideal α) :

0 ∈ I

source

theorem ideal.add_mem {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (a_1 : a ∈ I) (a_2 : b ∈ I) :

a + b ∈ I

source

theorem ideal.neg_mem_iff {α : Type u} [comm_ring α] (I : ideal α) {a : α} :

-a ∈ I ↔ a ∈ I

source

theorem ideal.add_mem_iff_left {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (a_1 : b ∈ I) :

a + b ∈ I ↔ a ∈ I

source

theorem ideal.add_mem_iff_right {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (a_1 : a ∈ I) :

a + b ∈ I ↔ b ∈ I

source

theorem ideal.sub_mem {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (a_1 : a ∈ I) (a_2 : b ∈ I) :

a - b ∈ I

source

theorem ideal.mul_mem_left {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (a_1 : b ∈ I) :

a * b ∈ I

source

theorem ideal.mul_mem_right {α : Type u} [comm_ring α] (I : ideal α) {a b : α} (h : a ∈ I) :

a * b ∈ I

source

@[ext]

theorem ideal.ext {α : Type u} [comm_ring α] {I J : ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) :

I = J

source

theorem ideal.eq_top_of_unit_mem {α : Type u} [comm_ring α] (I : ideal α) (x y : α) (hx : x ∈ I) (h : y * x = 1) :

I = ⊤

source

theorem ideal.eq_top_of_is_unit_mem {α : Type u} [comm_ring α] (I : ideal α) {x : α} (hx : x ∈ I) (h : is_unit x) :

I = ⊤

source

theorem ideal.eq_top_iff_one {α : Type u} [comm_ring α] (I : ideal α) :

I = ⊤ ↔ 1 ∈ I

source

theorem ideal.ne_top_iff_one {α : Type u} [comm_ring α] (I : ideal α) :

I ≠ ⊤ ↔ 1 ∉ I

source

@[simp]

theorem ideal.unit_mul_mem_iff_mem {α : Type u} [comm_ring α] (I : ideal α) {x y : α} (hy : is_unit y) :

y * x ∈ I ↔ x ∈ I

source

@[simp]

theorem ideal.mul_unit_mem_iff_mem {α : Type u} [comm_ring α] (I : ideal α) {x y : α} (hy : is_unit y) :

x * y ∈ I ↔ x ∈ I

source

def ideal.span {α : Type u} [comm_ring α] (s : set α) :

ideal α

The ideal generated by a subset of a ring

Equations

ideal.span s = submodule.span α s

source

theorem ideal.subset_span {α : Type u} [comm_ring α] {s : set α} :

s ⊆ ↑(ideal.span s)

source

theorem ideal.span_le {α : Type u} [comm_ring α] {s : set α} {I : ideal α} :

ideal.span s ≤ I ↔ s ⊆ ↑I

source

theorem ideal.span_mono {α : Type u} [comm_ring α] {s t : set α} (a : s ⊆ t) :

ideal.span s ≤ ideal.span t

source

@[simp]

theorem ideal.span_eq {α : Type u} [comm_ring α] (I : ideal α) :

ideal.span ↑I = I

source

@[simp]

theorem ideal.span_singleton_one {α : Type u} [comm_ring α] :

ideal.span 1 = ⊤

source

theorem ideal.mem_span_insert {α : Type u} [comm_ring α] {s : set α} {x y : α} :

x ∈ ideal.span (insert y s) ↔ ∃ (a z : α) (H : z ∈ ideal.span s), x = a * y + z

source

theorem ideal.mem_span_insert' {α : Type u} [comm_ring α] {s : set α} {x y : α} :

x ∈ ideal.span (insert y s) ↔ ∃ (a : α), x + a * y ∈ ideal.span s

source

theorem ideal.mem_span_singleton' {α : Type u} [comm_ring α] {x y : α} :

x ∈ ideal.span {y} ↔ ∃ (a : α), a * y = x

source

theorem ideal.mem_span_singleton {α : Type u} [comm_ring α] {x y : α} :

x ∈ ideal.span {y} ↔ y ∣ x

source

theorem ideal.span_singleton_le_span_singleton {α : Type u} [comm_ring α] {x y : α} :

ideal.span {x} ≤ ideal.span {y} ↔ y ∣ x

source

theorem ideal.span_singleton_eq_span_singleton {α : Type u} [integral_domain α] {x y : α} :

ideal.span {x} = ideal.span {y} ↔ associated x y

source

theorem ideal.span_eq_bot {α : Type u} [comm_ring α] {s : set α} :

ideal.span s = ⊥ ↔ ∀ (x : α), x ∈ s → x = 0

source

@[simp]

theorem ideal.span_singleton_eq_bot {α : Type u} [comm_ring α] {x : α} :

ideal.span {x} = ⊥ ↔ x = 0

source

@[simp]

theorem ideal.span_zero {α : Type u} [comm_ring α] :

ideal.span 0 = ⊥

source

theorem ideal.span_singleton_eq_top {α : Type u} [comm_ring α] {x : α} :

ideal.span {x} = ⊤ ↔ is_unit x

source

theorem ideal.span_singleton_mul_right_unit {α : Type u} [comm_ring α] {a : α} (h2 : is_unit a) (x : α) :

ideal.span {x * a} = ideal.span {x}

source

theorem ideal.span_singleton_mul_left_unit {α : Type u} [comm_ring α] {a : α} (h2 : is_unit a) (x : α) :

ideal.span {a * x} = ideal.span {x}

source

def ideal.of_rel {α : Type u} [comm_ring α] (r : α → α → Prop) :

ideal α

The ideal generated by an arbitrary binary relation.

Equations

ideal.of_rel r = submodule.span α {x : α | ∃ (a b : α) (h : r a b), x = a - b}

source

@[class]

def ideal.is_prime {α : Type u} [comm_ring α] (I : ideal α) :

Prop

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

Equations

I.is_prime = (I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I)

Instances

source

theorem ideal.is_prime.mem_or_mem {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_prime) {x y : α} (a : x * y ∈ I) :

x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.mem_or_mem_of_mul_eq_zero {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_prime) {x y : α} (h : x * y = 0) :

x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.mem_of_pow_mem {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_prime) {r : α} (n : ℕ) (H : r ^ n ∈ I) :

r ∈ I

source

theorem ideal.zero_ne_one_of_proper {α : Type u} [comm_ring α] {I : ideal α} (h : I ≠ ⊤) :

0 ≠ 1

source

theorem ideal.span_singleton_prime {α : Type u} [comm_ring α] {p : α} (hp : p ≠ 0) :

(ideal.span {p}).is_prime ↔ prime p

source

theorem ideal.bot_prime {R : Type u_1} [integral_domain R] :

⊥.is_prime

source

@[class]

def ideal.is_maximal {α : Type u} [comm_ring α] (I : ideal α) :

Prop

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

Equations

I.is_maximal = (I ≠ ⊤ ∧ ∀ (J : ideal α), I < J → J = ⊤)

Instances

source

theorem ideal.is_maximal_iff {α : Type u} [comm_ring α] {I : ideal α} :

I.is_maximal ↔ 1 ∉ I ∧ ∀ (J : ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

source

theorem ideal.is_maximal.eq_of_le {α : Type u} [comm_ring α] {I J : ideal α} (hI : I.is_maximal) (hJ : J ≠ ⊤) (IJ : I ≤ J) :

I = J

source

theorem ideal.is_maximal.exists_inv {α : Type u} [comm_ring α] {I : ideal α} (hI : I.is_maximal) {x : α} (hx : x ∉ I) :

∃ (y : α), y * x - 1 ∈ I

source

theorem ideal.is_maximal.is_prime {α : Type u} [comm_ring α] {I : ideal α} (H : I.is_maximal) :

I.is_prime

source

@[instance]

def ideal.is_maximal.is_prime' {α : Type u} [comm_ring α] (I : ideal α) [H : I.is_maximal] :

I.is_prime

source

theorem ideal.exists_le_maximal {α : Type u} [comm_ring α] (I : ideal α) (hI : I ≠ ⊤) :

∃ (M : ideal α), M.is_maximal ∧ I ≤ M

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

source

theorem ideal.exists_maximal {α : Type u} [comm_ring α] [nontrivial α] :

∃ (M : ideal α), M.is_maximal

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

source

theorem ideal.maximal_of_no_maximal {R : Type u} [comm_ring R] {P : ideal R} (hmax : ∀ (m : ideal R), P < m → ¬m.is_maximal) (J : ideal R) (hPJ : P < J) :

J = ⊤

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

source

theorem ideal.mem_span_pair {α : Type u} [comm_ring α] {x y z : α} :

z ∈ ideal.span {x, y} ↔ ∃ (a b : α), a * x + b * y = z

source

theorem ideal.span_singleton_lt_span_singleton {β : Type v} [integral_domain β] {x y : β} :

ideal.span {x} < ideal.span {y} ↔ dvd_not_unit y x

source

theorem ideal.factors_decreasing {β : Type v} [integral_domain β] (b₁ b₂ : β) (h₁ : b₁ ≠ 0) (h₂ : ¬is_unit b₂) :

ideal.span {b₁ * b₂} < ideal.span {b₁}

source

def ideal.quotient {α : Type u} [comm_ring α] (I : ideal α) :

Type u

The quotient R/I of a ring R by an ideal I.

Equations

I.quotient = submodule.quotient I

source

@[instance]

def ideal.quotient.has_one {α : Type u} [comm_ring α] (I : ideal α) :

has_one I.quotient

Equations

ideal.quotient.has_one I = {one := submodule.quotient.mk 1}

source

@[instance]

def ideal.quotient.has_mul {α : Type u} [comm_ring α] (I : ideal α) :

has_mul I.quotient

Equations

ideal.quotient.has_mul I = {mul := λ (a b : I.quotient), quotient.lift_on₂' a b (λ (a b : α), submodule.quotient.mk (a * b)) _}

source

@[instance]

def ideal.quotient.comm_ring {α : Type u} [comm_ring α] (I : ideal α) :

comm_ring I.quotient

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 := _}

source

def ideal.quotient.mk {α : Type u} [comm_ring α] (I : ideal α) :

α →+* I.quotient

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' := _}

source

@[instance]

def ideal.quotient.inhabited {α : Type u} [comm_ring α] {I : ideal α} :

inhabited I.quotient

Equations

ideal.quotient.inhabited = {default := ⇑(ideal.quotient.mk I) 37}

source

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

source

@[simp]

theorem ideal.quotient.mk_eq_mk {α : Type u} [comm_ring α] {I : ideal α} (x : α) :

submodule.quotient.mk x = ⇑(ideal.quotient.mk I) x

source

theorem ideal.quotient.eq_zero_iff_mem {α : Type u} {a : α} [comm_ring α] {I : ideal α} :

⇑(ideal.quotient.mk I) a = 0 ↔ a ∈ I

source

theorem ideal.quotient.zero_eq_one_iff {α : Type u} [comm_ring α] {I : ideal α} :

0 = 1 ↔ I = ⊤

source

theorem ideal.quotient.zero_ne_one_iff {α : Type u} [comm_ring α] {I : ideal α} :

0 ≠ 1 ↔ I ≠ ⊤

source

theorem ideal.quotient.nontrivial {α : Type u} [comm_ring α] {I : ideal α} (hI : I ≠ ⊤) :

nontrivial I.quotient

source

theorem ideal.quotient.mk_surjective {α : Type u} [comm_ring α] {I : ideal α} :

function.surjective ⇑(ideal.quotient.mk I)

source

@[instance]

def ideal.quotient.integral_domain {α : Type u} [comm_ring α] (I : ideal α) [hI : I.is_prime] :

integral_domain I.quotient

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 := _}

source

theorem ideal.quotient.is_integral_domain_iff_prime {α : Type u} [comm_ring α] (I : ideal α) :

is_integral_domain I.quotient ↔ I.is_prime

source

theorem ideal.quotient.exists_inv {α : Type u} [comm_ring α] {I : ideal α} [hI : I.is_maximal] {a : I.quotient} (a_1 : a ≠ 0) :

∃ (b : I.quotient), a * b = 1

source

def ideal.quotient.field {α : Type u} [comm_ring α] (I : ideal α) [hI : I.is_maximal] :

field 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 := _}

source

theorem ideal.quotient.maximal_of_is_field {α : Type u} [comm_ring α] (I : ideal α) (hqf : is_field I.quotient) :

I.is_maximal

If the quotient by an ideal is a field, then the ideal is maximal.

source

theorem ideal.quotient.maximal_ideal_iff_is_field_quotient {α : Type u} [comm_ring α] (I : ideal α) :

I.is_maximal ↔ is_field I.quotient

The quotient of a ring by an ideal is a field iff the ideal is maximal.

source

def ideal.quotient.lift {α : Type u} {β : Type v} [comm_ring α] [comm_ring β] (S : ideal α) (f : α →+* β) (H : ∀ (a : α), a ∈ S → ⇑f a = 0) :

S.quotient →+* β

Given a ring homomorphism f : α →+* β sending all elements of an ideal to zero, lift it to the quotient by this ideal.

Equations

ideal.quotient.lift S f H = {to_fun := λ (x : S.quotient), quotient.lift_on' x ⇑f _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[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

source

theorem ideal.mem_sup_left {R : Type u} [comm_ring R] {S T : ideal R} {x : R} (a : x ∈ S) :

x ∈ S ⊔ T

source

theorem ideal.mem_sup_right {R : Type u} [comm_ring R] {S T : ideal R} {x : R} (a : x ∈ T) :

x ∈ S ⊔ T

source

theorem ideal.mem_supr_of_mem {R : Type u} [comm_ring R] {ι : Type u_1} {S : ι → ideal R} (i : ι) {x : R} (a : x ∈ S i) :

x ∈ supr S

source

theorem ideal.mem_Sup_of_mem {R : Type u} [comm_ring R] {S : set (ideal R)} {s : ideal R} (hs : s ∈ S) {x : R} (a : x ∈ s) :

x ∈ Sup S

source

theorem ideal.mem_Inf {R : Type u} [comm_ring R] {s : set (ideal R)} {x : R} :

x ∈ Inf s ↔ ∀ ⦃I : ideal R⦄, I ∈ s → x ∈ I

source

@[simp]

theorem ideal.mem_inf {R : Type u} [comm_ring R] {I J : ideal R} {x : R} :

x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

source

@[simp]

theorem ideal.mem_infi {R : Type u} [comm_ring R] {ι : Type u_1} {I : ι → ideal R} {x : R} :

x ∈ infi I ↔ ∀ (i : ι), x ∈ I i

source

@[simp]

theorem ideal.mem_bot {R : Type u} [comm_ring R] {x : R} :

x ∈ ⊥ ↔ x = 0

source

theorem ideal.eq_bot_or_top {K : Type u} [field K] (I : ideal K) :

I = ⊥ ∨ I = ⊤

All ideals in a field are trivial.

source

theorem ideal.eq_bot_of_prime {K : Type u} [field K] (I : ideal K) [h : I.is_prime] :

I = ⊥

source

theorem ideal.bot_is_maximal {K : Type u} [field K] :

⊥.is_maximal

source

def ideal.pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :

ideal (ι → α)

I^n as an ideal of R^n.

Equations

I.pi ι = {carrier := {x : ι → α | ∀ (i : ι), x i ∈ I}, zero_mem' := _, add_mem' := _, smul_mem' := _}

source

theorem ideal.mem_pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) (x : ι → α) :

x ∈ I.pi ι ↔ ∀ (i : ι), x i ∈ I

source

@[instance]

def ideal.module_pi {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :

module I.quotient (I.pi ι).quotient

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 := _}

source

def ideal.pi_quot_equiv {α : Type u} [comm_ring α] (I : ideal α) (ι : Type v) :

(I.pi ι).quotient ≃ₗ[I.quotient ] ι → I.quotient

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 := _}

source

theorem ideal.map_pi {α : Type u} [comm_ring α] (I : ideal α) {ι : Type u_1} [fintype ι] {ι' : Type w} (x : ι → α) (hi : ∀ (i : ι), x i ∈ I) (f : (ι → α) →ₗ[α] ι' → α) (i : ι') :

⇑f x i ∈ I

If f : R^n → R^m is an R-linear map and I ⊆ R is an ideal, then the image of I^n is contained in I^m.

source

theorem ring.not_is_field_of_subsingleton {R : Type u_1} [ring R] [subsingleton R] :

¬is_field R

source

theorem ring.exists_not_is_unit_of_not_is_field {R : Type u_1} [comm_ring R] [nontrivial R] (hf : ¬is_field R) :

∃ (x : R) (H : x ≠ 0), ¬is_unit x

source

theorem ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top {R : Type u_1} [comm_ring R] [nontrivial R] :

¬is_field R ↔ ∃ (I : ideal R), ⊥ < I ∧ I < ⊤

source

theorem ring.not_is_field_iff_exists_prime {R : Type u_1} [comm_ring R] [nontrivial R] :

¬is_field R ↔ ∃ (p : ideal R), p ≠ ⊥ ∧ p.is_prime

source

theorem ideal.bot_lt_of_maximal {R : Type u} [comm_ring R] [nontrivial R] (M : ideal R) [hm : M.is_maximal] (non_field : ¬is_field R) :

⊥ < M

source

def nonunits (α : Type u) [monoid α] :

set α

The set of non-invertible elements of a monoid.

Equations

nonunits α = {a : α | ¬is_unit a}

source

@[simp]

theorem mem_nonunits_iff {α : Type u} {a : α} [comm_monoid α] :

a ∈ nonunits α ↔ ¬is_unit a

source

theorem mul_mem_nonunits_right {α : Type u} {a b : α} [comm_monoid α] (a_1 : b ∈ nonunits α) :

a * b ∈ nonunits α

source

theorem mul_mem_nonunits_left {α : Type u} {a b : α} [comm_monoid α] (a_1 : a ∈ nonunits α) :

a * b ∈ nonunits α

source

theorem zero_mem_nonunits {α : Type u} [semiring α] :

0 ∈ nonunits α ↔ 0 ≠ 1

source

@[simp]

theorem one_not_mem_nonunits {α : Type u} [monoid α] :

1 ∉ nonunits α

source

theorem coe_subset_nonunits {α : Type u} [comm_ring α] {I : ideal α} (h : I ≠ ⊤) :

↑I ⊆ nonunits α

source

theorem exists_max_ideal_of_mem_nonunits {α : Type u} {a : α} [comm_ring α] (h : a ∈ nonunits α) :

∃ (I : ideal α), I.is_maximal ∧ a ∈ I

source

@[class]

structure local_ring (α : Type u) [comm_ring α] :

Prop

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.

Instances

source

theorem local_ring.is_unit_or_is_unit_one_sub_self {α : Type u} [comm_ring α] [local_ring α] (a : α) :

is_unit a ∨ is_unit (1 - a)

source

theorem local_ring.is_unit_of_mem_nonunits_one_sub_self {α : Type u} [comm_ring α] [local_ring α] (a : α) (h : 1 - a ∈ nonunits α) :

is_unit a

source

theorem local_ring.is_unit_one_sub_self_of_mem_nonunits {α : Type u} [comm_ring α] [local_ring α] (a : α) (h : a ∈ nonunits α) :

is_unit (1 - a)

source

theorem local_ring.nonunits_add {α : Type u} [comm_ring α] [local_ring α] {x y : α} (hx : x ∈ nonunits α) (hy : y ∈ nonunits α) :

x + y ∈ nonunits α

source

def local_ring.maximal_ideal (α : Type u) [comm_ring α] [local_ring α] :

ideal α

The ideal of elements that are not units.

Equations

local_ring.maximal_ideal α = {carrier := nonunits α (ring.to_monoid α), zero_mem' := _, add_mem' := _, smul_mem' := _}

source

@[instance]

def local_ring.maximal_ideal.is_maximal (α : Type u) [comm_ring α] [local_ring α] :

(local_ring.maximal_ideal α).is_maximal

source

theorem local_ring.maximal_ideal_unique (α : Type u) [comm_ring α] [local_ring α] :

∃! (I : ideal α), I.is_maximal

source

theorem local_ring.eq_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] {I : ideal α} (hI : I.is_maximal) :

I = local_ring.maximal_ideal α

source

theorem local_ring.le_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] {J : ideal α} (hJ : J ≠ ⊤) :

J ≤ local_ring.maximal_ideal α

source

@[simp]

theorem local_ring.mem_maximal_ideal {α : Type u} [comm_ring α] [local_ring α] (x : α) :

x ∈ local_ring.maximal_ideal α ↔ x ∈ nonunits α

source

theorem local_of_nonunits_ideal {α : Type u} [comm_ring α] (hnze : 0 ≠ 1) (h : ∀ (x y : α), x ∈ nonunits α → y ∈ nonunits α → x + y ∈ nonunits α) :

local_ring α

source

theorem local_of_unique_max_ideal {α : Type u} [comm_ring α] (h : ∃! (I : ideal α), I.is_maximal) :

local_ring α

source

theorem local_of_unique_nonzero_prime (R : Type u) [comm_ring R] (h : ∃! (P : ideal R), P ≠ ⊥ ∧ P.is_prime) :

local_ring R

source

theorem local_of_surjective {A : Type u_1} {B : Type u_2} [comm_ring A] [local_ring A] [comm_ring B] [nontrivial B] (f : A →+* B) (hf : function.surjective ⇑f) :

local_ring B

source

@[class]

structure is_local_ring_hom {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) :

Prop

map_nonunit : ∀ (a : α), is_unit (⇑f a) → is_unit a

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.

Instances

source

@[instance]

def is_local_ring_hom_id (A : Type u_1) [semiring A] :

is_local_ring_hom (ring_hom.id A)

source

@[simp]

theorem is_unit_map_iff {A : Type u_1} {B : Type u_2} [semiring A] [semiring B] (f : A →+* B) [is_local_ring_hom f] (a : A) :

is_unit (⇑f a) ↔ is_unit a

source

@[instance]

def is_local_ring_hom_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [semiring A] [semiring B] [semiring C] (g : B →+* C) (f : A →+* B) [is_local_ring_hom g] [is_local_ring_hom f] :

is_local_ring_hom (g.comp f)

source

@[simp]

theorem is_unit_of_map_unit {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) [is_local_ring_hom f] (a : α) (h : is_unit (⇑f a)) :

is_unit a

source

theorem of_irreducible_map {α : Type u} {β : Type v} [semiring α] [semiring β] (f : α →+* β) [h : is_local_ring_hom f] {x : α} (hfx : irreducible (⇑f x)) :

irreducible x

source

theorem map_nonunit {α : Type u} {β : Type v} [comm_ring α] [local_ring α] [comm_ring β] [local_ring β] (f : α →+* β) [is_local_ring_hom f] (a : α) (h : a ∈ local_ring.maximal_ideal α) :

⇑f a ∈ local_ring.maximal_ideal β

source