mathlib docs: ring_theory.ideal.operations

source

@[instance]

def submodule.has_scalar' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

has_scalar (ideal R) (submodule R M)

Equations

submodule.has_scalar' = {smul := λ (I : ideal R) (N : submodule R M), ⨆ (r : ↥I), submodule.map (r.val • linear_map.id) N}

source

def submodule.annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

submodule R M → ideal R

N.annihilator is the ideal of all elements r : R such that r • N = 0.

Equations

N.annihilator = (linear_map.lsmul R ↥N).ker

source

def submodule.colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

submodule R M → submodule R M → ideal R

N.colon P is the ideal of all elements r : R such that r • P ⊆ N.

Equations

N.colon P = (submodule.map N.mkq P).annihilator

source

theorem submodule.mem_annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} {r : R} :

r ∈ N.annihilator ↔ ∀ (n : M), n ∈ N → r • n = 0

source

theorem submodule.mem_annihilator' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} {r : R} :

r ∈ N.annihilator ↔ N ≤ submodule.comap (r • linear_map.id) ⊥

source

theorem submodule.annihilator_bot {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

⊥.annihilator = ⊤

source

theorem submodule.annihilator_eq_top_iff {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N : submodule R M} :

N.annihilator = ⊤ ↔ N = ⊥

source

theorem submodule.annihilator_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} :

N ≤ P → P.annihilator ≤ N.annihilator

source

theorem submodule.annihilator_supr {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (ι : Sort w) (f : ι → submodule R M) :

(⨆ (i : ι), f i).annihilator = ⨅ (i : ι), (f i).annihilator

source

theorem submodule.mem_colon {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} {r : R} :

r ∈ N.colon P ↔ ∀ (p : M), p ∈ P → r • p ∈ N

source

theorem submodule.mem_colon' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N P : submodule R M} {r : R} :

r ∈ N.colon P ↔ P ≤ submodule.comap (r • linear_map.id) N

source

theorem submodule.colon_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {N₁ N₂ P₁ P₂ : submodule R M} :

N₁ ≤ N₂ → P₁ ≤ P₂ → N₁.colon P₂ ≤ N₂.colon P₁

source

theorem submodule.infi_colon_supr {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (ι₁ : Sort w) (f : ι₁ → submodule R M) (ι₂ : Sort x) (g : ι₂ → submodule R M) :

(⨅ (i : ι₁), f i).colon (⨆ (j : ι₂), g j) = ⨅ (i : ι₁) (j : ι₂), (f i).colon (g j)

source

theorem submodule.smul_mem_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} {r : R} {n : M} :

r ∈ I → n ∈ N → r • n ∈ I • N

source

theorem submodule.smul_le {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N P : submodule R M} :

I • N ≤ P ↔ ∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → r • n ∈ P

source

theorem submodule.smul_induction_on {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} {p : M → Prop} {x : M} :

x ∈ I • N → (∀ (r : R), r ∈ I → ∀ (n : M), n ∈ N → p (r • n)) → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → (∀ (c : R) (n : M), p n → p (c • n)) → p x

source

theorem submodule.mem_smul_span_singleton {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {m x : M} :

x ∈ I • submodule.span R {m} ↔ ∃ (y : R) (H : y ∈ I), y • m = x

source

theorem submodule.smul_le_right {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N : submodule R M} :

I • N ≤ N

source

theorem submodule.smul_mono {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I J : ideal R} {N P : submodule R M} :

I ≤ J → N ≤ P → I • N ≤ J • P

source

theorem submodule.smul_mono_left {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I J : ideal R} {N : submodule R M} :

I ≤ J → I • N ≤ J • N

source

theorem submodule.smul_mono_right {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N P : submodule R M} :

N ≤ P → I • N ≤ I • P

source

@[simp]

theorem submodule.smul_bot {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) :

I • ⊥ = ⊥

source

@[simp]

theorem submodule.bot_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N : submodule R M) :

⊥ • N = ⊥

source

@[simp]

theorem submodule.top_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (N : submodule R M) :

⊤ • N = N

source

theorem submodule.smul_sup {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N P : submodule R M) :

I • (N ⊔ P) = I • N ⊔ I • P

source

theorem submodule.sup_smul {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I J : ideal R) (N : submodule R M) :

(I ⊔ J) • N = I • N ⊔ J • N

source

theorem submodule.smul_assoc {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I J : ideal R) (N : submodule R M) :

(I • J) • N = I • J • N

source

theorem submodule.span_smul_span {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (S : set R) (T : set M) :

ideal.span S • submodule.span R T = submodule.span R (⋃ (s : R) (H : s ∈ S) (t : M) (H : t ∈ T), {s • t})

source

theorem submodule.map_smul'' {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) {M' : Type w} [add_comm_group M'] [module R M'] (f : M →ₗ[R] M') :

submodule.map f (I • N) = I • submodule.map f N

source

theorem ideal.exists_sub_one_mem_and_mem {R : Type u} [comm_ring R] {ι : Type v} (s : finset ι) {f : ι → ideal R} (hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤) (i : ι) :

i ∈ s → (∃ (r : R), r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j)

source

theorem ideal.exists_sub_mem {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] {f : ι → ideal R} (hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) (g : ι → R) :

∃ (r : R), ∀ (i : ι), r - g i ∈ f i

source

def ideal.quotient_inf_to_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} (f : ι → ideal R) :

(⨅ (i : ι), f i).quotient →+* Π (i : ι), (f i).quotient

The homomorphism from R/(⋂ i, f i) to ∏ i, (R / f i) featured in the Chinese Remainder Theorem. It is bijective if the ideals f i are comaximal.

Equations

ideal.quotient_inf_to_pi_quotient f = ideal.quotient.lift (⨅ (i : ι), f i) (_.mpr (pi.ring_hom (λ (i : ι), ideal.quotient.mk (f i)))) _

source

theorem ideal.quotient_inf_to_pi_quotient_bijective {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] {f : ι → ideal R} :

(∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) → function.bijective ⇑(ideal.quotient_inf_to_pi_quotient f)

source

def ideal.quotient_inf_ring_equiv_pi_quotient {R : Type u} [comm_ring R] {ι : Type v} [fintype ι] (f : ι → ideal R) :

(∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤) → ((⨅ (i : ι), f i).quotient ≃+* Π (i : ι), (f i).quotient)

Chinese Remainder Theorem. Eisenbud Ex.2.6. Similar to Atiyah-Macdonald 1.10 and Stacks 00DT

Equations

ideal.quotient_inf_ring_equiv_pi_quotient f hf = {to_fun := (equiv.of_bijective ⇑(ideal.quotient_inf_to_pi_quotient (λ (i : ι), f i)) _).to_fun, inv_fun := (equiv.of_bijective ⇑(ideal.quotient_inf_to_pi_quotient (λ (i : ι), f i)) _).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[instance]

def ideal.has_mul {R : Type u} [comm_ring R] :

has_mul (ideal R)

Equations

ideal.has_mul = {mul := has_scalar.smul submodule.has_scalar'}

source

theorem ideal.mul_mem_mul {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} :

r ∈ I → s ∈ J → r * s ∈ I * J

source

theorem ideal.mul_mem_mul_rev {R : Type u} [comm_ring R] {I J : ideal R} {r s : R} :

r ∈ I → s ∈ J → s * r ∈ I * J

source

theorem ideal.mul_le {R : Type u} [comm_ring R] {I J K : ideal R} :

I * J ≤ K ↔ ∀ (r : R), r ∈ I → ∀ (s : R), s ∈ J → r * s ∈ K

source

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

I * J ≤ J

source

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

I * J ≤ I

source

@[simp]

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

I ⊔ I * J = I

source

@[simp]

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

I ⊔ J * I = I

source

@[simp]

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

I * J ⊔ I = I

source

@[simp]

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

J * I ⊔ I = I

source

theorem ideal.mul_comm {R : Type u} [comm_ring R] (I J : ideal R) :

I * J = J * I

source

theorem ideal.mul_assoc {R : Type u} [comm_ring R] (I J K : ideal R) :

(I * J) * K = I * J * K

source

theorem ideal.span_mul_span {R : Type u} [comm_ring R] (S T : set R) :

(ideal.span S) * ideal.span T = ideal.span (⋃ (s : R) (H : s ∈ S) (t : R) (H : t ∈ T), {s * t})

source

theorem ideal.span_mul_span' {R : Type u} [comm_ring R] (S T : set R) :

(ideal.span S) * ideal.span T = ideal.span (S * T)

source

theorem ideal.span_singleton_mul_span_singleton {R : Type u} [comm_ring R] (r s : R) :

(ideal.span {r}) * ideal.span {s} = ideal.span {r * s}

source

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

I * J ≤ I ⊓ J

source

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

I ⊔ J = ⊤ → I * J = I ⊓ J

source

theorem ideal.mul_bot {R : Type u} [comm_ring R] (I : ideal R) :

I * ⊥ = ⊥

source

theorem ideal.bot_mul {R : Type u} [comm_ring R] (I : ideal R) :

⊥ * I = ⊥

source

theorem ideal.mul_top {R : Type u} [comm_ring R] (I : ideal R) :

I * ⊤ = I

source

theorem ideal.top_mul {R : Type u} [comm_ring R] (I : ideal R) :

⊤ * I = I

source

theorem ideal.mul_mono {R : Type u} [comm_ring R] {I J K L : ideal R} :

I ≤ K → J ≤ L → I * J ≤ K * L

source

theorem ideal.mul_mono_left {R : Type u} [comm_ring R] {I J K : ideal R} :

I ≤ J → I * K ≤ J * K

source

theorem ideal.mul_mono_right {R : Type u} [comm_ring R] {I J K : ideal R} :

J ≤ K → I * J ≤ I * K

source

theorem ideal.mul_sup {R : Type u} [comm_ring R] (I J K : ideal R) :

I * (J ⊔ K) = I * J ⊔ I * K

source

theorem ideal.sup_mul {R : Type u} [comm_ring R] (I J K : ideal R) :

(I ⊔ J) * K = I * K ⊔ J * K

source

theorem ideal.pow_le_pow {R : Type u} [comm_ring R] {I : ideal R} {m n : ℕ} :

m ≤ n → I ^ n ≤ I ^ m

source

theorem ideal.mul_eq_bot {R : Type u_1} [integral_domain R] {I J : ideal R} :

I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥

source

def ideal.radical {R : Type u} [comm_ring R] :

ideal R → ideal R

The radical of an ideal I consists of the elements r such that r^n ∈ I for some n.

Equations

I.radical = {carrier := {r : R | ∃ (n : ℕ), r ^ n ∈ I}, zero_mem' := _, add_mem' := _, smul_mem' := _}

source

theorem ideal.le_radical {R : Type u} [comm_ring R] {I : ideal R} :

I ≤ I.radical

source

theorem ideal.radical_top (R : Type u) [comm_ring R] :

⊤.radical = ⊤

source

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

I ≤ J → I.radical ≤ J.radical

source

theorem ideal.radical_idem {R : Type u} [comm_ring R] (I : ideal R) :

I.radical.radical = I.radical

source

theorem ideal.radical_eq_top {R : Type u} [comm_ring R] {I : ideal R} :

I.radical = ⊤ ↔ I = ⊤

source

theorem ideal.is_prime.radical {R : Type u} [comm_ring R] {I : ideal R} :

I.is_prime → I.radical = I

source

theorem ideal.radical_sup {R : Type u} [comm_ring R] (I J : ideal R) :

(I ⊔ J).radical = (I.radical ⊔ J.radical).radical

source

theorem ideal.radical_inf {R : Type u} [comm_ring R] (I J : ideal R) :

(I ⊓ J).radical = I.radical ⊓ J.radical

source

theorem ideal.radical_mul {R : Type u} [comm_ring R] (I J : ideal R) :

(I * J).radical = I.radical ⊓ J.radical

source

theorem ideal.is_prime.radical_le_iff {R : Type u} [comm_ring R] {I J : ideal R} :

J.is_prime → (I.radical ≤ J ↔ I ≤ J)

source

theorem ideal.radical_eq_Inf {R : Type u} [comm_ring R] (I : ideal R) :

I.radical = Inf {J : ideal R | I ≤ J ∧ J.is_prime}

source

@[instance]

def ideal.comm_semiring {R : Type u} [comm_ring R] :

comm_semiring (ideal R)

Equations

ideal.comm_semiring = submodule.comm_semiring

source

@[simp]

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

I + J = I ⊔ J

source

@[simp]

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

0 = ⊥

source

@[simp]

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

1 = ⊤

source

theorem ideal.top_pow (R : Type u) [comm_ring R] (n : ℕ) :

⊤ ^ n = ⊤

source

theorem ideal.radical_pow {R : Type u} [comm_ring R] (I : ideal R) (n : ℕ) :

n > 0 → (I ^ n).radical = I.radical

source

def ideal.map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :

(R →+* S) → ideal R → ideal S

I.map f is the span of the image of the ideal I under f, which may be bigger than the image itself.

Equations

ideal.map f I = ideal.span (⇑f '' ↑I)

source

def ideal.comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :

(R →+* S) → ideal S → ideal R

I.comap f is the preimage of I under f.

Equations

ideal.comap f I = {carrier := ⇑f ⁻¹' ↑I, zero_mem' := _, add_mem' := _, smul_mem' := _}

source

theorem ideal.map_mono {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I J : ideal R} :

I ≤ J → ideal.map f I ≤ ideal.map f J

source

theorem ideal.mem_map_of_mem {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {x : R} :

x ∈ I → ⇑f x ∈ ideal.map f I

source

theorem ideal.map_le_iff_le_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :

ideal.map f I ≤ K ↔ I ≤ ideal.comap f K

source

@[simp]

theorem ideal.mem_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K : ideal S} {x : R} :

x ∈ ideal.comap f K ↔ ⇑f x ∈ K

source

theorem ideal.comap_mono {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K L : ideal S} :

K ≤ L → ideal.comap f K ≤ ideal.comap f L

source

theorem ideal.comap_ne_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} :

K ≠ ⊤ → ideal.comap f K ≠ ⊤

source

theorem ideal.is_prime.comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} [hK : K.is_prime] :

(ideal.comap f K).is_prime

source

theorem ideal.map_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

ideal.map f ⊤ = ⊤

source

theorem ideal.map_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I J : ideal R) :

ideal.map f (I * J) = (ideal.map f I) * ideal.map f J

source

theorem ideal.gc_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

galois_connection (ideal.map f) (ideal.comap f)

source

@[simp]

theorem ideal.comap_id {R : Type u} [comm_ring R] (I : ideal R) :

ideal.comap (ring_hom.id R) I = I

source

@[simp]

theorem ideal.map_id {R : Type u} [comm_ring R] (I : ideal R) :

ideal.map (ring_hom.id R) I = I

source

theorem ideal.comap_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {T : Type u_1} [comm_ring T] {I : ideal T} (f : R →+* S) (g : S →+* T) :

ideal.comap f (ideal.comap g I) = ideal.comap (g.comp f) I

source

theorem ideal.map_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {T : Type u_1} [comm_ring T] {I : ideal R} (f : R →+* S) (g : S →+* T) :

ideal.map g (ideal.map f I) = ideal.map (g.comp f) I

source

theorem ideal.map_le_of_le_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :

I ≤ ideal.comap f K → ideal.map f I ≤ K

source

theorem ideal.le_comap_of_map_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} {K : ideal S} :

ideal.map f I ≤ K → I ≤ ideal.comap f K

source

theorem ideal.le_comap_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal R} :

I ≤ ideal.comap f (ideal.map f I)

source

theorem ideal.map_comap_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {K : ideal S} :

ideal.map f (ideal.comap f K) ≤ K

source

@[simp]

theorem ideal.comap_top {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} :

ideal.comap f ⊤ = ⊤

source

@[simp]

theorem ideal.comap_eq_top_iff {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} {I : ideal S} :

ideal.comap f I = ⊤ ↔ I = ⊤

source

@[simp]

theorem ideal.map_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] {f : R →+* S} :

ideal.map f ⊥ = ⊥

source

@[simp]

theorem ideal.map_comap_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I : ideal R) :

ideal.map f (ideal.comap f (ideal.map f I)) = ideal.map f I

source

@[simp]

theorem ideal.comap_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) :

ideal.comap f (ideal.map f (ideal.comap f K)) = ideal.comap f K

source

theorem ideal.map_sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (I J : ideal R) :

ideal.map f (I ⊔ J) = ideal.map f I ⊔ ideal.map f J

source

theorem ideal.comap_inf {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K L : ideal S) :

ideal.comap f (K ⊓ L) = ideal.comap f K ⊓ ideal.comap f L

source

theorem ideal.map_supr {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ideal R) :

ideal.map f (supr K) = ⨆ (i : ι), ideal.map f (K i)

source

theorem ideal.comap_infi {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (K : ι → ideal S) :

ideal.comap f (infi K) = ⨅ (i : ι), ideal.comap f (K i)

source

theorem ideal.map_Sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal R)) :

ideal.map f (Sup s) = ⨆ (I : ideal R) (H : I ∈ s), ideal.map f I

source

theorem ideal.comap_Inf {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal S)) :

ideal.comap f (Inf s) = ⨅ (I : ideal S) (H : I ∈ s), ideal.comap f I

source

theorem ideal.comap_Inf' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (s : set (ideal S)) :

ideal.comap f (Inf s) = ⨅ (I : ideal R) (H : I ∈ ideal.comap f '' s), I

source

theorem ideal.comap_radical {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) :

ideal.comap f K.radical = (ideal.comap f K).radical

source

theorem ideal.comap_is_prime {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (K : ideal S) [H : K.is_prime] :

(ideal.comap f K).is_prime

source

@[simp]

theorem ideal.map_quotient_self {R : Type u} [comm_ring R] (I : ideal R) :

ideal.map (ideal.quotient.mk I) I = ⊥

source

theorem ideal.map_inf_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I J : ideal R} :

ideal.map f (I ⊓ J) ≤ ideal.map f I ⊓ ideal.map f J

source

theorem ideal.map_radical_le {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

ideal.map f I.radical ≤ (ideal.map f I).radical

source

theorem ideal.le_comap_sup {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K L : ideal S} :

ideal.comap f K ⊔ ideal.comap f L ≤ ideal.comap f (K ⊔ L)

source

theorem ideal.le_comap_mul {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K L : ideal S} :

(ideal.comap f K) * ideal.comap f L ≤ ideal.comap f (K * L)

source

theorem ideal.map_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) (I : ideal S) :

ideal.map f (ideal.comap f I) = I

source

def ideal.gi_map_comap {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.surjective ⇑f → galois_insertion (ideal.map f) (ideal.comap f)

map and comap are adjoint, and the composition map f ∘ comap f is the identity

Equations

ideal.gi_map_comap f hf = galois_insertion.monotone_intro _ _ _ _

source

theorem ideal.map_surjective_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.surjective ⇑f → function.surjective (ideal.map f)

source

theorem ideal.comap_injective_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.surjective ⇑f → function.injective (ideal.comap f)

source

theorem ideal.map_sup_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) (I J : ideal S) :

ideal.map f (ideal.comap f I ⊔ ideal.comap f J) = I ⊔ J

source

theorem ideal.map_supr_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective ⇑f) (K : ι → ideal S) :

ideal.map f (⨆ (i : ι), ideal.comap f (K i)) = supr K

source

theorem ideal.map_inf_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) (I J : ideal S) :

ideal.map f (ideal.comap f I ⊓ ideal.comap f J) = I ⊓ J

source

theorem ideal.map_infi_comap_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {ι : Sort u_1} (hf : function.surjective ⇑f) (K : ι → ideal S) :

ideal.map f (⨅ (i : ι), ideal.comap f (K i)) = infi K

source

theorem ideal.mem_image_of_mem_map_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) {I : ideal R} {y : S} :

y ∈ ideal.map f I → y ∈ ⇑f '' ↑I

source

theorem ideal.mem_map_iff_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) {I : ideal R} {y : S} :

y ∈ ideal.map f I ↔ ∃ (x : R), x ∈ I ∧ ⇑f x = y

source

theorem ideal.comap_map_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) (I : ideal R) :

ideal.comap f (ideal.map f I) = I ⊔ ideal.comap f ⊥

source

theorem ideal.le_map_of_comap_le_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} {K : ideal S} :

function.surjective ⇑f → ideal.comap f K ≤ I → K ≤ ideal.map f I

source

def ideal.rel_iso_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.surjective ⇑f → ideal S ≃o {p // ideal.comap f ⊥ ≤ p}

Correspondence theorem

Equations

ideal.rel_iso_of_surjective f hf = {to_equiv := {to_fun := λ (J : ideal S), ⟨ideal.comap f J, _⟩, inv_fun := λ (I : {p // ideal.comap f ⊥ ≤ p}), ideal.map f I.val, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

def ideal.order_embedding_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.surjective ⇑f → ideal S ↪o ideal R

The map on ideals induced by a surjective map preserves inclusion.

Equations

ideal.order_embedding_of_surjective f hf = (rel_iso.to_rel_embedding (ideal.rel_iso_of_surjective f hf)).trans (subtype.rel_embedding has_le.le (λ (p : ideal R), ideal.comap f ⊥ ≤ p))

source

theorem ideal.map_eq_top_or_is_maximal_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

function.surjective ⇑f → I.is_maximal → ideal.map f I = ⊤ ∨ (ideal.map f I).is_maximal

source

theorem ideal.comap_is_maximal_of_surjective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {K : ideal S} (hf : function.surjective ⇑f) [H : K.is_maximal] :

(ideal.comap f K).is_maximal

source

theorem ideal.mem_quotient_iff_mem {R : Type u} [comm_ring R] {I J : ideal R} (hIJ : I ≤ J) {x : R} :

⇑(ideal.quotient.mk I) x ∈ ideal.map (ideal.quotient.mk I) J ↔ x ∈ J

source

theorem ideal.comap_bot_le_of_injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

function.injective ⇑f → ideal.comap f ⊥ ≤ I

source

def ideal.rel_iso_of_bijective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.bijective ⇑f → ideal S ≃o ideal R

Special case of the correspondence theorem for isomorphic rings

Equations

ideal.rel_iso_of_bijective f hf = {to_equiv := {to_fun := ideal.comap f, inv_fun := ideal.map f, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

theorem ideal.comap_le_iff_le_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} {K : ideal S} :

function.bijective ⇑f → (ideal.comap f K ≤ I ↔ K ≤ ideal.map f I)

source

theorem ideal.map.is_maximal {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal R} :

function.bijective ⇑f → I.is_maximal → (ideal.map f I).is_maximal

source

def ideal.is_primary {R : Type u} [comm_ring R] :

ideal R → Prop

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

Equations

I.is_primary = (I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical)

source

theorem ideal.is_primary.to_is_prime {R : Type u} [comm_ring R] (I : ideal R) :

I.is_prime → I.is_primary

source

theorem ideal.mem_radical_of_pow_mem {R : Type u} [comm_ring R] {I : ideal R} {x : R} {m : ℕ} :

x ^ m ∈ I.radical → x ∈ I.radical

source

theorem ideal.is_prime_radical {R : Type u} [comm_ring R] {I : ideal R} :

I.is_primary → I.radical.is_prime

source

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

I.is_primary → J.is_primary → I.radical = J.radical → (I ⊓ J).is_primary

source

def ring_hom.ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] :

(R →+* S) → ideal R

Kernel of a ring homomorphism as an ideal of the domain.

Equations

f.ker = ideal.comap f ⊥

source

theorem ring_hom.mem_ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) {r : R} :

r ∈ f.ker ↔ ⇑f r = 0

An element is in the kernel if and only if it maps to zero.

source

theorem ring_hom.ker_eq {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

↑(f.ker) = is_add_group_hom.ker ⇑f

source

theorem ring_hom.ker_eq_comap_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

f.ker = ideal.comap f ⊥

source

theorem ring_hom.injective_iff_ker_eq_bot {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

function.injective ⇑f ↔ f.ker = ⊥

source

theorem ring_hom.ker_eq_bot_iff_eq_zero {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :

f.ker = ⊥ ↔ ∀ (x : R), ⇑f x = 0 → x = 0

source

theorem ring_hom.not_one_mem_ker {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [nontrivial S] (f : R →+* S) :

1 ∉ f.ker

If the target is not the zero ring, then one is not in the kernel.

source

@[simp]

theorem ring_hom.ker_coe_equiv {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (f : R ≃+* S) :

↑f.ker = ⊥

source

theorem ring_hom.ker_is_prime {R : Type u} {S : Type v} [comm_ring R] [integral_domain S] (f : R →+* S) :

f.ker.is_prime

The kernel of a homomorphism to an integral domain is a prime ideal.

source

theorem ideal.map_eq_bot_iff_le_ker {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal R} (f : R →+* S) :

ideal.map f I = ⊥ ↔ I ≤ f.ker

source

@[simp]

theorem ideal.mk_ker {R : Type u_1} [comm_ring R] {I : ideal R} :

(ideal.quotient.mk I).ker = I

source

theorem ideal.ker_le_comap {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {K : ideal S} (f : R →+* S) :

f.ker ≤ ideal.comap f K

source

theorem ideal.map_Inf {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {A : set (ideal R)} {f : R →+* S} :

function.surjective ⇑f → (∀ (J : ideal R), J ∈ A → f.ker ≤ J) → ideal.map f (Inf A) = Inf (ideal.map f '' A)

source

theorem ideal.map_is_prime_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective ⇑f) {I : ideal R} [H : I.is_prime] :

f.ker ≤ I → (ideal.map f I).is_prime

source

theorem ideal.map_is_prime_of_equiv {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (f : R ≃+* S) {I : ideal R} [I.is_prime] :

(ideal.map ↑f I).is_prime

source

theorem ideal.map_radical_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective ⇑f) {I : ideal R} :

f.ker ≤ I → ideal.map f I.radical = (ideal.map f I).radical

source

def ideal.quotient_map {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal R} (J : ideal S) (f : R →+* S) :

I ≤ ideal.comap f J → I.quotient →+* J.quotient

The ring hom R/f⁻¹(I) →+* S/I induced by a ring hom f : R →+* S

Equations

J.quotient_map f hIJ = ideal.quotient.lift I ((ideal.quotient.mk J).comp f) _

source

@[instance]

def ideal.quotient_algebra {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal S} [algebra R S] :

algebra (ideal.comap (algebra_map R S) J).quotient J.quotient

Equations

ideal.quotient_algebra = (J.quotient_map (algebra_map R S) ideal.quotient_algebra._proof_1).to_algebra

source

theorem ideal.algebra_map_quotient_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {J : ideal S} [algebra R S] :

function.injective ⇑(algebra_map (ideal.comap (algebra_map R S) J).quotient J.quotient)

source

@[instance]

def submodule.semimodule_submodule {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :

semimodule (ideal R) (submodule R M)

Equations

submodule.semimodule_submodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := submodule.has_scalar' _inst_3, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

source

def ring_hom.lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective ⇑f) (g : A →+* C) :

f.ker ≤ g.ker → B →+* C

lift_of_surjective f hf g hg is the unique ring homomorphism φ

such that φ.comp f = g (lift_of_surjective_comp),
where f : A →+* B is surjective (hf),
and g : B →+* C satisfies hg : f.ker ≤ g.ker.

See lift_of_surjective_eq for the uniqueness lemma.

   A .
   |  \
 f |   \ g
   |    \
   v     \⌟
   B ----> C
      ∃!φ

Equations

f.lift_of_surjective hf g hg = {to_fun := λ (b : B), ⇑g (classical.some _), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem ring_hom.lift_of_surjective_comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective ⇑f) (g : A →+* C) (hg : f.ker ≤ g.ker) (a : A) :

⇑(f.lift_of_surjective hf g hg) (⇑f a) = ⇑g a

source

@[simp]

theorem ring_hom.lift_of_surjective_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective ⇑f) (g : A →+* C) (hg : f.ker ≤ g.ker) :

(f.lift_of_surjective hf g hg).comp f = g

source

theorem ring_hom.eq_lift_of_surjective {A : Type u_1} {B : Type u_2} {C : Type u_3} [comm_ring A] [comm_ring B] [comm_ring C] (f : A →+* B) (hf : function.surjective ⇑f) (g : A →+* C) (hg : f.ker ≤ g.ker) (h : B →+* C) :

h.comp f = g → h = f.lift_of_surjective hf g hg

mathlib documentation

More operations on modules and ideals