The colon ideal #

This file defines Submodule.colon N P as the ideal of all elements r : R such that r • P ⊆ N. The normal notation for this would be N : P which has already been taken by type theory.

source

🔸 coverage

def Submodule.colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (S : Set M) :

Ideal R

N.colon P is the ideal of all elements r : R such that r • P ⊆ N. We treat it as an infix in lemma names.

Equations

Instances For

source

📐 coverage

theorem Submodule.mem_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {S : Set M} {r : R} :

r ∈ N.colon S ↔ ∀ s ∈ S, r • s ∈ N

source

📐 coverage

@[simp]

theorem Submodule.mem_colon_singleton {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {x : M} {r : R} :

r ∈ N.colon {x} ↔ r • x ∈ N

source

📐 coverage

@[instance 100]

instance Submodule.instIsTwoSidedColonCoe {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} (P : Submodule R M) :

(N.colon ↑P).IsTwoSided

source

📐 coverage

@[simp]

theorem Submodule.colon_univ {R : Type u_1} [Semiring R] {I : Ideal R} [I.IsTwoSided] :

colon I Set.univ = I

source

📐 coverage

@[deprecated Submodule.colon_univ (since := "2026-01-11")]

theorem Submodule.colon_top {R : Type u_1} [Semiring R] {I : Ideal R} [I.IsTwoSided] :

colon I Set.univ = I

Alias of Submodule.colon_univ.

source

📐 coverage

@[simp]

theorem Submodule.bot_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

⊥.colon ↑N = N.annihilator

source

📐 coverage

theorem Submodule.colon_mono {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N₁ N₂ : Submodule R M} {S₁ S₂ : Set M} (hn : N₁ ≤ N₂) (hs : S₁ ⊆ S₂) :

N₁.colon S₂ ≤ N₂.colon S₁

source

📐 coverage

theorem Ideal.le_colon {R : Type u_1} [Semiring R] {I : Ideal R} {S : Set R} [I.IsTwoSided] :

I ≤ Submodule.colon I S

source

📐 coverage

theorem Submodule.iInf_colon_iUnion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (ι₁ : Sort u_3) (f : ι₁ → Submodule R M) (ι₂ : Sort u_4) (g : ι₂ → Set M) :

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

source

📐 coverage

@[deprecated Submodule.iInf_colon_iUnion (since := "2026-01-11")]

theorem Submodule.iInf_colon_iSup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (ι₁ : Sort u_3) (f : ι₁ → Submodule R M) (ι₂ : Sort u_4) (g : ι₂ → Set M) :

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

Alias of Submodule.iInf_colon_iUnion.

source

📐 coverage

theorem Submodule.colon_inf_eq_left_of_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N₁ N₂ : Submodule R M} {S : Set M} (h : S ⊆ ↑N₂) :

(N₁ ⊓ N₂).colon S = N₁.colon S

If S ⊆ N₂, then intersecting with N₂ does not change the colon ideal.

source

📐 coverage

@[simp]

theorem Submodule.colon_eq_top_iff_subset {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} (S : Set M) :

N.colon S = ⊤ ↔ S ⊆ ↑N

source

📐 coverage

@[simp]

theorem Submodule.inf_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N₁ N₂ : Submodule R M} {S : Set M} :

(N₁ ⊓ N₂).colon S = N₁.colon S ⊓ N₂.colon S

source

📐 coverage

@[simp]

theorem Submodule.iInf_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} {ι : Sort u_3} (f : ι → Submodule R M) :

(⨅ (i : ι), f i).colon S = ⨅ (i : ι), (f i).colon S

source

📐 coverage

@[simp]

theorem Submodule.colon_finsetInf {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} {ι : Type u_3} (s : Finset ι) (f : ι → Submodule R M) :

(s.inf f).colon S = s.inf fun (i : ι) => (f i).colon S

source

📐 coverage

@[simp]

theorem Submodule.top_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} :

⊤.colon S = ⊤

source

📐 coverage

@[simp]

theorem Submodule.colon_union {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {S₁ S₂ : Set M} :

N.colon (S₁ ∪ S₂) = N.colon S₁ ⊓ N.colon S₂

source

📐 coverage

@[simp]

theorem Submodule.colon_iUnion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {ι : Sort u_3} (f : ι → Set M) :

N.colon (⋃ (i : ι), f i) = ⨅ (i : ι), N.colon (f i)

source

📐 coverage

@[simp]

theorem Submodule.colon_empty {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

N.colon ∅ = ⊤

source

📐 coverage

theorem Submodule.colon_singleton_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

N.colon {0} = ⊤

source

📐 coverage

theorem Submodule.colon_bot {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

N.colon ↑⊥ = ⊤

source

📐 coverage

@[deprecated Submodule.mem_colon (since := "2026-01-15")]

theorem Submodule.mem_colon' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {S : Set M} {r : R} :

r ∈ N.colon S ↔ S ≤ ↑(comap (r • LinearMap.id) N)

source

📐 coverage

theorem Submodule.mem_colon_iff_le {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N N' : Submodule R M} {r : R} :

r ∈ N.colon ↑N' ↔ r • N' ≤ N

source

📐 coverage

theorem Submodule.bot_colon' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Set M} :

⊥.colon S = (span R S).annihilator

A variant for arbitrary sets in commutative semirings

source

📐 coverage

@[simp]

theorem Submodule.colon_span {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {S : Set M} :

N.colon ↑(span R S) = N.colon S

source

📐 coverage

@[simp]

theorem Ideal.colon_span {R : Type u_1} [CommSemiring R] {I : Ideal R} {S : Set R} :

Submodule.colon I ↑(span S) = Submodule.colon I S

source

📐 coverage

theorem Submodule.mem_colon_span_singleton {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {x : M} {r : R} :

r ∈ N.colon ↑(R ∙ x) ↔ r • x ∈ N

source

📐 coverage

theorem Ideal.mem_colon_span_singleton {R : Type u_1} [CommSemiring R] {I : Ideal R} {x r : R} :

r ∈ Submodule.colon I ↑(span {x}) ↔ r * x ∈ I

source

📐 coverage

@[simp]

theorem Submodule.annihilator_map_mkQ_eq_colon {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N P : Submodule R M} :

(map N.mkQ P).annihilator = N.colon ↑P

source

📐 coverage

theorem Submodule.annihilator_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} :

Module.annihilator R (M ⧸ N) = N.colon Set.univ

source

📐 coverage

theorem Ideal.annihilator_quotient {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] :

Module.annihilator R (R ⧸ I) = I

Documentation

Mathlib.RingTheory.Ideal.Colon

The colon ideal #