Mathlib.LinearAlgebra.SModEq

SModEq definition

(x y : M) : Prop

Full source

/-- A predicate saying two elements of a module are equivalent modulo a submodule. -/
def SModEq (x y : M) : Prop :=
  (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y

Modular equivalence in a module

Informal description

Two elements $x$ and $y$ of a module $M$ are said to be equivalent modulo a submodule $U$ (denoted $x \equiv y \ [SMOD\ U]$) if their images in the quotient module $M/U$ are equal.

term_≡_[SMOD_] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] notation:50 x " ≡ " y " [SMOD " N "]" => SModEq N x y

Modular equivalence modulo a submodule

Informal description

The notation $x \equiv y \ [\text{SMOD}\ N]$ denotes modular equivalence of elements $x$ and $y$ modulo a submodule $N$, meaning that $x - y \in N$.

SModEq.def theorem

: x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y

Full source

protected theorem SModEq.def :
    x ≡ y [SMOD U]x ≡ y [SMOD U] ↔ (Submodule.Quotient.mk x : M ⧸ U) = Submodule.Quotient.mk y :=
  Iff.rfl

Modular Equivalence Characterization via Quotient Module

Informal description

For elements $x$ and $y$ in a module $M$ and a submodule $U$ of $M$, the modular equivalence $x \equiv y \ [SMOD\ U]$ holds if and only if the images of $x$ and $y$ in the quotient module $M/U$ are equal, i.e., $\overline{x} = \overline{y}$ where $\overline{x}, \overline{y}$ denote the equivalence classes of $x$ and $y$ in $M/U$.

SModEq.sub_mem theorem

: x ≡ y [SMOD U] ↔ x - y ∈ U

Full source

theorem sub_mem : x ≡ y [SMOD U]x ≡ y [SMOD U] ↔ x - y ∈ U := by rw [SModEq.def, Submodule.Quotient.eq]

Modular Equivalence via Submodule Membership: $x \equiv y \ [SMOD\ U] \leftrightarrow x - y \in U$

Informal description

For elements $x$ and $y$ in a module $M$ and a submodule $U$ of $M$, the modular equivalence $x \equiv y \ [SMOD\ U]$ holds if and only if their difference $x - y$ belongs to $U$.

SModEq.top theorem

: x ≡ y [SMOD (⊤ : Submodule R M)]

Full source

@[simp]
theorem top : x ≡ y [SMOD (⊤ : Submodule R M)] :=
  (Submodule.Quotient.eq ⊤).2 mem_top

Modular equivalence modulo the top submodule

Informal description

Two elements $x$ and $y$ of a module $M$ are equivalent modulo the top submodule $\top$ of $M$, i.e., $x \equiv y \ [SMOD\ \top]$.

SModEq.bot theorem

: x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y

Full source

@[simp]
theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)]x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by
  rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]

Modular Equivalence Modulo Trivial Submodule Characterizes Equality

Informal description

For any elements $x$ and $y$ in a module $M$ over a ring $R$, the modular equivalence $x \equiv y \ [SMOD\ \bot]$ holds if and only if $x = y$, where $\bot$ denotes the trivial submodule of $M$.

SModEq.mono theorem

(HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂]

Full source

@[mono]
theorem mono (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) : x ≡ y [SMOD U₂] :=
  (Submodule.Quotient.eq U₂).2 <| HU <| (Submodule.Quotient.eq U₁).1 hxy

Monotonicity of Modular Equivalence in Submodules

Informal description

Let $U_1$ and $U_2$ be submodules of a module $M$ over a ring $R$ such that $U_1 \leq U_2$. If two elements $x, y \in M$ are equivalent modulo $U_1$ (i.e., $x \equiv y \ [SMOD\ U_1]$), then they are also equivalent modulo $U_2$ (i.e., $x \equiv y \ [SMOD\ U_2]$).

SModEq.refl theorem

(x : M) : x ≡ x [SMOD U]

Full source

@[refl]
protected theorem refl (x : M) : x ≡ x [SMOD U] :=
  @rfl _ _

Reflexivity of Modular Equivalence in a Module

Informal description

For any element $x$ in a module $M$ and any submodule $U$ of $M$, we have $x \equiv x \ [SMOD\ U]$.

SModEq.rfl theorem

: x ≡ x [SMOD U]

Full source

protected theorem rfl : x ≡ x [SMOD U] :=
  SModEq.refl _

Reflexivity of Modular Equivalence ($x \equiv x \pmod{U}$)

Informal description

For any element $x$ in a module $M$ and any submodule $U$ of $M$, we have $x \equiv x \pmod{U}$.

SModEq.instIsRefl instance

: IsRefl _ (SModEq U)

Full source

instance : IsRefl _ (SModEq U) :=
  ⟨SModEq.refl⟩

Reflexivity of Modular Equivalence Relation

Informal description

The modular equivalence relation $x \equiv y \pmod{U}$ on a module $M$ with respect to a submodule $U$ is reflexive.

SModEq.symm theorem

(hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U]

Full source

@[symm]
nonrec theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] :=
  hxy.symm

Symmetry of Modular Equivalence in a Module

Informal description

For any elements $x$ and $y$ in a module $M$, if $x \equiv y \pmod{U}$ for a submodule $U$ of $M$, then $y \equiv x \pmod{U}$.

SModEq.trans theorem

(hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U]

Full source

@[trans]
nonrec theorem trans (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U] :=
  hxy.trans hyz

Transitivity of Modular Equivalence in a Module

Informal description

For any elements $x$, $y$, and $z$ in a module $M$ and a submodule $U$ of $M$, if $x \equiv y \pmod{U}$ and $y \equiv z \pmod{U}$, then $x \equiv z \pmod{U}$.

SModEq.instTrans instance

: Trans (SModEq U) (SModEq U) (SModEq U)

Full source

instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where
  trans := trans

Transitivity of Modular Equivalence

Informal description

The modular equivalence relation $\equiv$ modulo a submodule $U$ of a module $M$ is transitive. That is, for any elements $x, y, z \in M$, if $x \equiv y \pmod{U}$ and $y \equiv z \pmod{U}$, then $x \equiv z \pmod{U}$.

SModEq.add theorem

(hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U]

Full source

theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] := by
  rw [SModEq.def] at hxy₁ hxy₂ ⊢
  simp_rw [Quotient.mk_add, hxy₁, hxy₂]

Addition Preserves Modular Equivalence in a Module

Informal description

For any elements $x₁, y₁, x₂, y₂$ in a module $M$ and a submodule $U$ of $M$, if $x₁ \equiv y₁ \pmod{U}$ and $x₂ \equiv y₂ \pmod{U}$, then $x₁ + x₂ \equiv y₁ + y₂ \pmod{U}$.

SModEq.smul theorem

(hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U]

Full source

theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] := by
  rw [SModEq.def] at hxy ⊢
  simp_rw [Quotient.mk_smul, hxy]

Scalar Multiplication Preserves Modular Equivalence in a Module

Informal description

For elements $x$ and $y$ in a module $M$ over a ring $R$, and a submodule $U$ of $M$, if $x \equiv y \pmod{U}$, then for any scalar $c \in R$, we have $c \cdot x \equiv c \cdot y \pmod{U}$.

SModEq.nsmul theorem

(hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U]

Full source

lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U] := by
  rw [SModEq.def] at hxy ⊢
  simp_rw [Quotient.mk_smul, hxy]

Natural Scalar Multiplication Preserves Modular Equivalence in a Module

Informal description

For elements $x$ and $y$ in a module $M$ over a ring $R$, and a submodule $U$ of $M$, if $x \equiv y \pmod{U}$, then for any natural number $n$, we have $n \cdot x \equiv n \cdot y \pmod{U}$.

SModEq.zsmul theorem

(hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U]

Full source

lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U] := by
  rw [SModEq.def] at hxy ⊢
  simp_rw [Quotient.mk_smul, hxy]

Integer Scalar Multiplication Preserves Modular Equivalence in a Module

Informal description

For elements $x$ and $y$ in a module $M$ over a ring $R$, and a submodule $U$ of $M$, if $x \equiv y \pmod{U}$, then for any integer $n$, we have $n \cdot x \equiv n \cdot y \pmod{U}$.

SModEq.mul theorem

 {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I]) (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

Full source

theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
    (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I] := by
  simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
  rw [hxy₁, hxy₂]

Multiplication Preserves Modular Equivalence in a Commutative Ring

Informal description

Let $A$ be a commutative ring with an ideal $I$. For any elements $x_1, x_2, y_1, y_2 \in A$ such that $x_1 \equiv y_1 \pmod{I}$ and $x_2 \equiv y_2 \pmod{I}$, we have $x_1 \cdot x_2 \equiv y_1 \cdot y_2 \pmod{I}$.

SModEq.pow theorem

{I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) : x ^ n ≡ y ^ n [SMOD I]

Full source

lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
    x ^ n ≡ y ^ n [SMOD I] := by
  simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
  rw [hxy]

Power Preservation of Modular Equivalence in a Commutative Ring

Informal description

For any elements $x$ and $y$ in a commutative ring $A$ and an ideal $I$ of $A$, if $x \equiv y \pmod{I}$, then for any natural number $n$, we have $x^n \equiv y^n \pmod{I}$.

SModEq.neg theorem

(hxy : x ≡ y [SMOD U]) : -x ≡ -y [SMOD U]

Full source

lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U] := by
  simpa only [SModEq.def, Quotient.mk_neg, neg_inj]

Negation Preserves Modular Equivalence in a Module

Informal description

For any elements $x$ and $y$ of a module $M$ that are equivalent modulo a submodule $U$ (i.e., $x \equiv y \ [SMOD\ U]$), their additive inverses $-x$ and $-y$ are also equivalent modulo $U$ (i.e., $-x \equiv -y \ [SMOD\ U]$).

SModEq.sub theorem

(hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

Full source

lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U] := by
  rw [SModEq.def] at hxy₁ hxy₂ ⊢
  simp_rw [Quotient.mk_sub, hxy₁, hxy₂]

Subtraction Preserves Modular Equivalence in a Module

Informal description

For any elements $x₁, y₁, x₂, y₂$ in a module $M$ with submodule $U$, if $x₁ \equiv y₁ \pmod{U}$ and $x₂ \equiv y₂ \pmod{U}$, then $x₁ - x₂ \equiv y₁ - y₂ \pmod{U}$.

SModEq.zero theorem

: x ≡ 0 [SMOD U] ↔ x ∈ U

Full source

theorem zero : x ≡ 0 [SMOD U]x ≡ 0 [SMOD U] ↔ x ∈ U := by rw [SModEq.def, Submodule.Quotient.eq, sub_zero]

Characterization of Zero Congruence Modulo Submodule: $x \equiv 0 \pmod{U} \iff x \in U$

Informal description

For any element $x$ in a module $M$ and a submodule $U$ of $M$, the modular equivalence $x \equiv 0 \pmod{U}$ holds if and only if $x$ belongs to $U$.

sub_smodEq_zero theorem

: x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U]

Full source

theorem _root_.sub_smodEq_zero : x - y ≡ 0 [SMOD U]x - y ≡ 0 [SMOD U] ↔ x ≡ y [SMOD U] := by
  simp only [SModEq.sub_mem, sub_zero]

Difference Congruent to Zero iff Elements Congruent Modulo Submodule

Informal description

For any elements $x$ and $y$ in a module $M$ and a submodule $U$ of $M$, the difference $x - y$ is congruent to $0$ modulo $U$ if and only if $x$ is congruent to $y$ modulo $U$. In other words, $x - y \equiv 0 \pmod{U} \leftrightarrow x \equiv y \pmod{U}$.

SModEq.map theorem

(hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f]

Full source

theorem map (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) : f x ≡ f y [SMOD U.map f] :=
  (Submodule.Quotient.eq _).2 <| f.map_sub x y ▸ mem_map_of_mem <| (Submodule.Quotient.eq _).1 hxy

Congruence Preservation under Linear Map Image: $x \equiv y \pmod{U} \Rightarrow f(x) \equiv f(y) \pmod{f(U)}$

Informal description

Given a linear map $f : M \to N$ between modules over a commutative ring $R$, and elements $x, y \in M$ such that $x \equiv y \pmod{U}$, then $f(x) \equiv f(y) \pmod{U \text{.map } f}$, where $U \text{.map } f$ is the image of the submodule $U$ under $f$.

SModEq.comap theorem

{f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f]

Full source

theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V.comap f] :=
  (Submodule.Quotient.eq _).2 <|
    show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy

Congruence Preservation under Linear Map Preimage: $f(x) \equiv f(y) \pmod{V} \Rightarrow x \equiv y \pmod{f^{-1}(V)}$

Informal description

Let $f : M \to N$ be a linear map between modules over a commutative ring $R$, and let $V$ be a submodule of $N$. If $f(x) \equiv f(y) \pmod{V}$, then $x \equiv y \pmod{V \text{.comap } f}$, where $V \text{.comap } f$ is the preimage of $V$ under $f$.

SModEq.eval theorem

{R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) : f.eval x ≡ f.eval y [SMOD I]

Full source

theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
    f.eval x ≡ f.eval y [SMOD I] := by
  rw [SModEq.def] at h ⊢
  show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)
  replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h
  rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]

Polynomial Evaluation Preserves Modular Equivalence

Informal description

Let $R$ be a commutative ring, $I$ an ideal of $R$, and $x, y \in R$ such that $x \equiv y \pmod{I}$. Then for any polynomial $f \in R[X]$, the evaluations satisfy $f(x) \equiv f(y) \pmod{I}$.