Documentation

Mathlib.RingTheory.Ideal.Colon

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
def Submodule.colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (N P : 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 = { carrier := {r : R | r • ↑P ⊆ ↑N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
    source
    theorem Submodule.mem_colon {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N P : Submodule R M} {r : R} :
    r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N
    source
    theorem Submodule.mem_colon' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N P : Submodule R M} {r : R} :
    r ∈ N.colon P ↔ P ≤ Submodule.comap (r • LinearMap.id) N
    source
    @[simp]
    theorem Submodule.colon_top {R : Type u_1} [CommSemiring R] {I : Ideal R} :
    Submodule.colon I ⊤ = I
    source
    @[simp]
    theorem Submodule.colon_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
    ⊥.colon N = N.annihilator
    source
    theorem Submodule.colon_mono {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N₁ N₂ P₁ P₂ : Submodule R M} (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) :
    N₁.colon P₂ ≤ N₂.colon P₁
    source
    theorem Submodule.iInf_colon_iSup {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (ι₁ : Sort u_6) (f : ι₁ → Submodule R M) (ι₂ : Sort u_7) (g : ι₂ → Submodule R M) :
    (⨅ (i : ι₁), f i).colon (⨆ (j : ι₂), g j) = ⨅ (i : ι₁), ⨅ (j : ι₂), (f i).colon (g j)
    source
    @[simp]
    theorem Submodule.mem_colon_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 (Submodule.span R {x}) ↔ r • x ∈ N
    source
    @[simp]
    theorem Ideal.mem_colon_singleton {R : Type u_1} [CommSemiring R] {I : Ideal R} {x r : R} :
    r ∈ Submodule.colon I (Ideal.span {x}) ↔ r * x ∈ I
    source
    @[simp]
    theorem Submodule.annihilator_map_mkQ_eq_colon {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N P : Submodule R M} :
    (Submodule.map N.mkQ P).annihilator = N.colon P
    source
    theorem Submodule.annihilator_quotient {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Submodule R M} :
    Module.annihilator R (M ⧸ N) = N.colon ⊤
    source
    theorem Ideal.annihilator_quotient {R : Type u_1} [CommRing R] {I : Ideal R} :
    Module.annihilator R (R ⧸ I) = I