Mathlib.RingTheory.Ideal.Colon

Submodule.colon definition

(N P : Submodule R M) : Ideal R

Full source

/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`. -/
def colon (N P : Submodule R M) : Ideal R where
  carrier := {r : R | (r • P : Set M) ⊆ N}
  add_mem' ha hb :=
    (Set.add_smul_subset _ _ _).trans ((Set.add_subset_add ha hb).trans_eq (by simp [← coe_sup]))
  zero_mem' := by simp [Set.zero_smul_set P.nonempty]
  smul_mem' r := by
    simp only [Set.mem_setOf_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]
    intro x hx y hy
    exact N.smul_mem _ (hx hy)

Colon ideal of submodules $ N $ and $ P $

Informal description

Given two submodules $ N $ and $ P $ of a module $ M $ over a semiring $ R $, the colon ideal $ N \colon P $ is the ideal of all elements $ r \in R $ such that the scalar multiplication $ r \cdot P $ is contained in $ N $. In other words, $ r \in N \colon P $ if and only if for every $ p \in P $, the element $ r \cdot p $ belongs to $ N $.

Submodule.mem_colon theorem

{r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N

Full source

theorem mem_colon {r} : r ∈ N.colon Pr ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N := Set.smul_set_subset_iff

Characterization of Elements in the Colon Ideal $N \colon P$

Informal description

For any element $r$ in a semiring $R$ and submodules $N$ and $P$ of an $R$-module $M$, we have $r \in N \colon P$ if and only if for every $p \in P$, the scalar product $r \cdot p$ belongs to $N$.

Submodule.instIsTwoSidedColon instance

: (N.colon P).IsTwoSided

Full source

instance (priority := low) : (N.colon P).IsTwoSided where
  mul_mem_of_left {r} s hr p hp := by
    obtain ⟨p, hp, rfl⟩ := hp
    exact hr ⟨_, P.smul_mem _ hp, (mul_smul ..).symm⟩

Colon Ideal is Two-Sided

Informal description

For any submodules $ N $ and $ P $ of a module $ M $ over a semiring $ R $, the colon ideal $ N \colon P $ is a two-sided ideal of $ R $.

Submodule.colon_top theorem

{I : Ideal R} [I.IsTwoSided] : I.colon ⊤ = I

Full source

@[simp]
theorem colon_top {I : Ideal R} [I.IsTwoSided] : I.colon ⊤ = I := by
  simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
  exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩

Colon Ideal of Top Submodule Equals Original Ideal

Informal description

Let $I$ be a two-sided ideal in a semiring $R$. Then the colon ideal $I \colon \top$ is equal to $I$ itself, where $\top$ denotes the top submodule of $R$ (i.e., the entire module $R$).

Submodule.colon_bot theorem

: colon ⊥ N = N.annihilator

Full source

@[simp]
theorem colon_bot : colon ⊥ N = N.annihilator := by
  simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]

Colon Ideal of Zero Submodule Equals Annihilator

Informal description

For any submodule $N$ of a module $M$ over a semiring $R$, the colon ideal of the zero submodule $\bot$ with respect to $N$ is equal to the annihilator ideal of $N$. That is, $\bot \colon N = \text{ann}_R(N)$.

Submodule.colon_mono theorem

(hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁

Full source

theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ := fun _ hrnp =>
  mem_colon.2 fun p₁ hp₁ => hn <| mem_colon.1 hrnp p₁ <| hp hp₁

Monotonicity of Colon Ideal with Respect to Submodule Inclusion

Informal description

Let $N_1, N_2$ and $P_1, P_2$ be submodules of an $R$-module $M$ such that $N_1 \subseteq N_2$ and $P_1 \subseteq P_2$. Then the colon ideal $N_1 \colon P_2$ is contained in the colon ideal $N_2 \colon P_1$.

Submodule.mem_colon' theorem

{r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N

Full source

theorem mem_colon' {r} : r ∈ N.colon Pr ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=
  mem_colon

Characterization of Colon Ideal via Linear Map Preimage

Informal description

For any element $r$ in a semiring $R$ and submodules $N$ and $P$ of an $R$-module $M$, we have $r \in N \colon P$ if and only if $P$ is contained in the preimage of $N$ under the linear map $m \mapsto r \cdot m$.

Submodule.iInf_colon_iSup theorem

 (ι₁ : Sort*) (f : ι₁ → Submodule R M) (ι₂ : Sort*) (g : ι₂ → Submodule R M) :
  (⨅ i, f i).colon (⨆ j, g j) = ⨅ (i) (j), (f i).colon (g j)

Full source

theorem iInf_colon_iSup (ι₁ : Sort*) (f : ι₁ → Submodule R M) (ι₂ : Sort*)
    (g : ι₂ → Submodule R M) : (⨅ i, f i).colon (⨆ j, g j) = ⨅ (i) (j), (f i).colon (g j) :=
  le_antisymm (le_iInf fun _ => le_iInf fun _ => colon_mono (iInf_le _ _) (le_iSup _ _)) fun _ H =>
    mem_colon'.2 <|
      iSup_le fun j =>
        map_le_iff_le_comap.1 <|
          le_iInf fun i =>
            map_le_iff_le_comap.2 <|
              mem_colon'.1 <|
                have := (mem_iInf _).1 H i
                have := (mem_iInf _).1 this j
                this

Inf-Sup Colon Ideal Decomposition: $(\bigcap_i f_i) \colon (\bigcup_j g_j) = \bigcap_{i,j} (f_i \colon g_j)$

Informal description

Let $R$ be a semiring and $M$ an $R$-module. For any family of submodules $(f_i)_{i \in \iota_1}$ and $(g_j)_{j \in \iota_2}$ of $M$, the colon ideal of the infimum of $(f_i)$ and the supremum of $(g_j)$ equals the infimum of all colon ideals $(f_i) \colon (g_j)$. That is, $$(\bigcap_i f_i) \colon (\bigcup_j g_j) = \bigcap_{i,j} (f_i \colon g_j).$$

Submodule.mem_colon_singleton theorem

{N : Submodule R M} {x : M} {r : R} : r ∈ N.colon (Submodule.span R { x }) ↔ r • x ∈ N

Full source

@[simp]
theorem mem_colon_singleton {N : Submodule R M} {x : M} {r : R} :
    r ∈ N.colon (Submodule.span R {x})r ∈ N.colon (Submodule.span R {x}) ↔ r • x ∈ N :=
  calc
    r ∈ N.colon (Submodule.span R {x}) ↔ ∀ a : R, r • a • x ∈ N := by
      simp [Submodule.mem_colon, Submodule.mem_span_singleton]
    _ ↔ r • x ∈ N := by simp_rw [fun (a : R) ↦ smul_comm r a x]; exact SetLike.forall_smul_mem_iff

Characterization of Colon Ideal Membership for a Single Generator: $r \in N \colon \text{span}_R\{x\} \leftrightarrow r \cdot x \in N$

Informal description

Let $R$ be a semiring, $M$ an $R$-module, $N$ a submodule of $M$, and $x$ an element of $M$. For any element $r \in R$, we have $r$ belongs to the colon ideal $N \colon \text{span}_R\{x\}$ if and only if the scalar multiple $r \cdot x$ belongs to $N$.

Ideal.mem_colon_singleton theorem

{I : Ideal R} {x r : R} : r ∈ I.colon (Ideal.span { x }) ↔ r * x ∈ I

Full source

@[simp]
theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} :
    r ∈ I.colon (Ideal.span {x})r ∈ I.colon (Ideal.span {x}) ↔ r * x ∈ I := by
  simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]

Characterization of Colon Ideal Membership for a Single Generator: $r \in I \colon \text{span}_R\{x\} \leftrightarrow r \cdot x \in I$

Informal description

Let $R$ be a semiring, $I$ an ideal of $R$, and $x, r \in R$. Then $r$ belongs to the colon ideal $I \colon \text{span}_R\{x\}$ if and only if the product $r \cdot x$ belongs to $I$.

Submodule.annihilator_map_mkQ_eq_colon theorem

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

Full source

@[simp]
lemma annihilator_map_mkQ_eq_colon : annihilator (P.map N.mkQ) = N.colon P := by
  ext
  rw [mem_annihilator, mem_colon]
  exact ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
    fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

Annihilator of Quotient Image Equals Colon Ideal

Informal description

For submodules $N$ and $P$ of an $R$-module $M$, the annihilator of the image of $P$ under the quotient map $M \to M ⧸ N$ is equal to the colon ideal $N \colon P$. In other words, $$\text{ann}_R(N.mkQ(P)) = N \colon P.$$

Submodule.annihilator_quotient theorem

{N : Submodule R M} : Module.annihilator R (M ⧸ N) = N.colon ⊤

Full source

theorem annihilator_quotient {N : Submodule R M} :
    Module.annihilator R (M ⧸ N) = N.colon ⊤ := by
  simp_rw [SetLike.ext_iff, Module.mem_annihilator, ← annihilator_map_mkQ_eq_colon, mem_annihilator,
    map_top, LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left,
    forall_const]

Annihilator of Quotient Module Equals Colon Ideal $N \colon M$

Informal description

For a submodule $N$ of an $R$-module $M$, the annihilator of the quotient module $M ⧸ N$ is equal to the colon ideal $N \colon M$. That is, $$\text{ann}_R(M ⧸ N) = \{ r \in R \mid r \cdot M \subseteq N \}.$$

Ideal.annihilator_quotient theorem

{I : Ideal R} [I.IsTwoSided] : Module.annihilator R (R ⧸ I) = I

Full source

theorem _root_.Ideal.annihilator_quotient {I : Ideal R} [I.IsTwoSided] :
    Module.annihilator R (R ⧸ I) = I := by
  rw [Submodule.annihilator_quotient, colon_top]

Annihilator of Quotient Ring by Two-Sided Ideal Equals Original Ideal

Informal description

For any two-sided ideal $I$ in a semiring $R$, the annihilator of the quotient module $R ⧸ I$ is equal to $I$ itself. That is, $$\text{ann}_R(R ⧸ I) = I.$$