Mathlib.LinearAlgebra.Quotient.Basic

Submodule.Quotient.restrictScalarsEquiv definition

 [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) : (M ⧸ P.restrictScalars S) ≃ₗ[S] M ⧸ P

Full source

/-- The quotient of `P` as an `S`-submodule is the same as the quotient of `P` as an `R`-submodule,
where `P : Submodule R M`.
-/
def restrictScalarsEquiv [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M]
    (P : Submodule R M) : (M ⧸ P.restrictScalars S) ≃ₗ[S] M ⧸ P :=
  { Quotient.congrRight fun _ _ => Iff.rfl with
    map_add' := fun x y => Quotient.inductionOn₂' x y fun _x' _y' => rfl
    map_smul' := fun _c x => Submodule.Quotient.induction_on _ x fun _x' => rfl }

Equivalence of Quotient Modules under Restriction of Scalars

Informal description

Given a ring $S$ with a scalar multiplication action on a ring $R$, a module $M$ over $R$ with a compatible $S$-module structure (via `IsScalarTower S R M`), and a submodule $P$ of $M$, there is a linear equivalence between the quotient of $M$ by $P$ as an $S$-submodule and the quotient of $M$ by $P$ as an $R$-submodule. More precisely, the equivalence is given by the identity map on equivalence classes, and it preserves both addition and scalar multiplication by elements of $S$.

Submodule.Quotient.restrictScalarsEquiv_mk theorem

 [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) (x : M) :
  restrictScalarsEquiv S P (mk x) = mk x

Full source

@[simp]
theorem restrictScalarsEquiv_mk [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M]
    (P : Submodule R M) (x : M) :
    restrictScalarsEquiv S P (mk x) = mk x :=
  rfl

Commutativity of Restriction of Scalars Equivalence with Quotient Map

Informal description

Let $S$ be a ring with a scalar multiplication action on a ring $R$, $M$ a module over $R$ with a compatible $S$-module structure (via `IsScalarTower S R M`), and $P$ a submodule of $M$. For any element $x \in M$, the linear equivalence `restrictScalarsEquiv S P` maps the equivalence class of $x$ in $M ⧸ P.\text{restrictScalars }S$ to the equivalence class of $x$ in $M ⧸ P$. In other words, the following diagram commutes: \[ \text{restrictScalarsEquiv }S\, P\, ([x]_{M ⧸ P.\text{restrictScalars }S}) = [x]_{M ⧸ P} \]

Submodule.Quotient.restrictScalarsEquiv_symm_mk theorem

 [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) (x : M) :
  (restrictScalarsEquiv S P).symm (mk x) = mk x

Full source

@[simp]
theorem restrictScalarsEquiv_symm_mk [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M]
    (P : Submodule R M) (x : M) :
    (restrictScalarsEquiv S P).symm (mk x) = mk x :=
  rfl

Inverse of Restriction of Scalars Equivalence Preserves Quotient Classes

Informal description

Let $S$ be a ring with a scalar multiplication action on a ring $R$, $M$ a module over $R$ with a compatible $S$-module structure (via `IsScalarTower S R M`), and $P$ a submodule of $M$. Then the inverse of the linear equivalence `restrictScalarsEquiv S P` maps the equivalence class of $x$ in $M ⧸ P$ to the equivalence class of $x$ in $M ⧸ P.\text{restrictScalars } S$. In other words, for any $x \in M$, we have $(restrictScalarsEquiv\, S\, P)^{-1}([x]) = [x]$, where $[x]$ denotes the equivalence class of $x$ in the respective quotient module.

Submodule.Quotient.nontrivial_of_lt_top theorem

(h : p < ⊤) : Nontrivial (M ⧸ p)

Full source

theorem nontrivial_of_lt_top (h : p < ⊤) : Nontrivial (M ⧸ p) := by
  obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
  refine ⟨⟨mk x, 0, ?_⟩⟩
  simpa using not_mem_s

Nontriviality of Quotient Module by Proper Submodule

Informal description

If $p$ is a proper submodule of a module $M$ (i.e., $p < \top$), then the quotient module $M ⧸ p$ is nontrivial (i.e., it contains at least two distinct elements).

Submodule.QuotientBot.infinite instance

[Infinite M] : Infinite (M ⧸ (⊥ : Submodule R M))

Full source

instance QuotientBot.infinite [Infinite M] : Infinite (M ⧸ (⊥ : Submodule R M)) :=
  Infinite.of_injective Submodule.Quotient.mk fun _x _y h =>
    sub_eq_zero.mp <| (Submodule.Quotient.eq ⊥).mp h

Infinite Quotient of Infinite Module by Zero Submodule

Informal description

For any infinite module $M$ over a ring $R$, the quotient module $M ⧸ \{0\}$ is infinite.

Submodule.QuotientTop.unique instance

: Unique (M ⧸ (⊤ : Submodule R M))

Full source

instance QuotientTop.unique : Unique (M ⧸ (⊤ : Submodule R M)) where
  default := 0
  uniq x := Submodule.Quotient.induction_on _ x fun _x =>
    (Submodule.Quotient.eq ⊤).mpr Submodule.mem_top

Uniqueness of the Quotient by the Top Submodule

Informal description

The quotient module $M ⧸ \top$ has exactly one element, where $\top$ denotes the top submodule of $M$ (i.e., $M$ itself).

Submodule.QuotientTop.fintype instance

: Fintype (M ⧸ (⊤ : Submodule R M))

Full source

instance QuotientTop.fintype : Fintype (M ⧸ (⊤ : Submodule R M)) :=
  Fintype.ofSubsingleton 0

Finiteness of the Quotient Module by the Top Submodule

Informal description

For any module $M$ over a ring $R$, the quotient module $M ⧸ \top$ is finite, where $\top$ denotes the top submodule of $M$ (i.e., $M$ itself).

Submodule.subsingleton_quotient_iff_eq_top theorem

: Subsingleton (M ⧸ p) ↔ p = ⊤

Full source

theorem subsingleton_quotient_iff_eq_top : SubsingletonSubsingleton (M ⧸ p) ↔ p = ⊤ := by
  constructor
  · rintro h
    refine eq_top_iff.mpr fun x _ => ?_
    have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)
    rwa [sub_zero] at this
  · rintro rfl
    infer_instance

Quotient Module is Subsingleton iff Submodule is Entire Module

Informal description

The quotient module $M ⧸ p$ is a subsingleton (has at most one element) if and only if the submodule $p$ is equal to the top submodule $\top$ (i.e., $p = M$).

Submodule.unique_quotient_iff_eq_top theorem

: Nonempty (Unique (M ⧸ p)) ↔ p = ⊤

Full source

theorem unique_quotient_iff_eq_top : NonemptyNonempty (Unique (M ⧸ p)) ↔ p = ⊤ :=
  ⟨fun ⟨h⟩ => subsingleton_quotient_iff_eq_top.mp (@Unique.instSubsingleton _ h),
    by rintro rfl; exact ⟨QuotientTop.unique⟩⟩

Quotient Module is Unique iff Submodule is Entire Module

Informal description

The quotient module $M ⧸ p$ has a unique element if and only if the submodule $p$ is equal to the entire module $M$ (i.e., $p = \top$).

Submodule.Quotient.fintype instance

[Fintype M] (S : Submodule R M) : Fintype (M ⧸ S)

Full source

noncomputable instance Quotient.fintype [Fintype M] (S : Submodule R M) : Fintype (M ⧸ S) :=
  @_root_.Quotient.fintype _ _ _ fun _ _ => Classical.dec _

Finiteness of Quotient Modules for Finite Modules

Informal description

For any finite module $M$ over a ring $R$ and any submodule $S$ of $M$, the quotient module $M ⧸ S$ is also finite.

Submodule.card_eq_card_quotient_mul_card theorem

(S : Submodule R M) : Nat.card M = Nat.card S * Nat.card (M ⧸ S)

Full source

theorem card_eq_card_quotient_mul_card (S : Submodule R M) :
    Nat.card M = Nat.card S * Nat.card (M ⧸ S) := by
  rw [mul_comm, ← Nat.card_prod]
  exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

Cardinality Product Formula for Modules and Quotients

Informal description

For any submodule $S$ of a module $M$ over a ring $R$, the cardinality of $M$ is equal to the product of the cardinalities of $S$ and the quotient module $M ⧸ S$, i.e., $$|M| = |S| \cdot |M ⧸ S|.$$

Submodule.strictMono_comap_prod_map theorem

: StrictMono fun m : Submodule R M ↦ (m.comap p.subtype, m.map p.mkQ)

Full source

theorem strictMono_comap_prod_map :
    StrictMono fun m : Submodule R M ↦ (m.comap p.subtype, m.map p.mkQ) :=
  fun m₁ m₂ ↦ QuotientAddGroup.strictMono_comap_prod_map
    p.toAddSubgroup (a := m₁.toAddSubgroup) (b := m₂.toAddSubgroup)

Strict Monotonicity of Submodule Restriction and Quotient Map Pair

Informal description

The function that maps a submodule $m$ of $M$ to the pair $(m \cap p, \pi(m))$, where $\pi \colon M \to M ⧸ p$ is the quotient map, is strictly monotone with respect to the submodule inclusion order.

Submodule.liftQ definition

(f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ ker f) : M ⧸ p →ₛₗ[τ₁₂] M₂

Full source

/-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
vanishing on `p`, as a linear map. -/
def liftQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ ker f) : M ⧸ pM ⧸ p →ₛₗ[τ₁₂] M₂ :=
  { QuotientAddGroup.lift p.toAddSubgroup f.toAddMonoidHom h with
    map_smul' := by rintro a ⟨x⟩; exact f.map_smulₛₗ a x }

Induced linear map on quotient module

Informal description

Given a linear map $f \colon M \to M₂$ between modules and a submodule $p$ of $M$ such that $p$ is contained in the kernel of $f$, the function `Submodule.liftQ` constructs the induced linear map from the quotient module $M ⧸ p$ to $M₂$. This map sends an equivalence class $[x]$ in $M ⧸ p$ to $f(x)$ in $M₂$.

Submodule.liftQ_apply theorem

(f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) : p.liftQ f h (Quotient.mk x) = f x

Full source

@[simp]
theorem liftQ_apply (f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) : p.liftQ f h (Quotient.mk x) = f x :=
  rfl

Evaluation of Induced Linear Map on Quotient Module

Informal description

Let $M$ and $M₂$ be modules over a ring $R$, $p$ a submodule of $M$, and $f \colon M \to M₂$ a linear map such that $p$ is contained in the kernel of $f$. Then for any $x \in M$, the induced linear map $\text{liftQ}(f, h)$ from the quotient module $M ⧸ p$ to $M₂$ satisfies $\text{liftQ}(f, h)([x]) = f(x)$, where $[x]$ denotes the equivalence class of $x$ in $M ⧸ p$.

Submodule.liftQ_mkQ theorem

(f : M →ₛₗ[τ₁₂] M₂) (h) : (p.liftQ f h).comp p.mkQ = f

Full source

@[simp]
theorem liftQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) (h) : (p.liftQ f h).comp p.mkQ = f := by ext; rfl

Composition of Quotient Lift with Quotient Map Recovers Original Linear Map

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau_{12} \colon R \to S$. Given a linear map $f \colon M \to M₂$ and a submodule $p$ of $M$ such that $p$ is contained in the kernel of $f$, the composition of the induced linear map $\operatorname{liftQ}(f, h) \colon M ⧸ p \to M₂$ with the quotient map $\operatorname{mkQ} \colon M \to M ⧸ p$ equals $f$. That is, $\operatorname{liftQ}(f, h) \circ \operatorname{mkQ} = f$.

Submodule.pi_liftQ_eq_liftQ_pi theorem

 {ι : Type*} {N : ι → Type*} [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)] (f : (i : ι) → M →ₗ[R] (N i))
  {p : Submodule R M} (h : ∀ i, p ≤ ker (f i)) :
  LinearMap.pi (fun i ↦ p.liftQ (f i) (h i)) = p.liftQ (LinearMap.pi f) (LinearMap.ker_pi f ▸ le_iInf h)

Full source

theorem pi_liftQ_eq_liftQ_pi {ι : Type*} {N : ι → Type*}
    [∀ i, AddCommGroup (N i)] [∀ i, Module R (N i)]
    (f : (i : ι) → M →ₗ[R] (N i)) {p : Submodule R M} (h : ∀ i, p ≤ ker (f i)) :
    LinearMap.pi (fun i ↦ p.liftQ (f i) (h i)) =
      p.liftQ (LinearMap.pi f) (LinearMap.ker_pi f ▸ le_iInf h) := by
  ext x i
  simp

Equality of Product Lift and Lift of Product Maps on Quotient Module

Informal description

Let $M$ be a module over a ring $R$, $p$ a submodule of $M$, and $\{N_i\}_{i \in \iota}$ a family of modules over $R$. Given a family of linear maps $f_i \colon M \to N_i$ such that $p$ is contained in the kernel of each $f_i$, the linear map $\pi$ from $M ⧸ p$ to the product $\prod_{i \in \iota} N_i$ induced by the family $\{\text{liftQ}(f_i, h_i)\}_{i \in \iota}$ is equal to the linear map induced by $\pi f$ on $M ⧸ p$, where $\pi f \colon M \to \prod_{i \in \iota} N_i$ is the product map $(f_i)_{i \in \iota}$. In other words, the following diagram commutes: \[ \begin{tikzcd} M \arrow[r, "\pi f"] \arrow[d, "\text{mkQ}"'] & \prod_{i \in \iota} N_i \\ M ⧸ p \arrow[ru, "\text{liftQ}(\pi f, \cdot)"'] \arrow[r, "\pi (\text{liftQ}(f_i, h_i))"'] & \prod_{i \in \iota} N_i \end{tikzcd} \]

Submodule.liftQSpanSingleton definition

(x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) : (M ⧸ R ∙ x) →ₛₗ[τ₁₂] M₂

Full source

/-- Special case of `submodule.liftQ` when `p` is the span of `x`. In this case, the condition on
`f` simply becomes vanishing at `x`. -/
def liftQSpanSingleton (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) : (M ⧸ R ∙ x) →ₛₗ[τ₁₂] M₂ :=
  (R ∙ x).liftQ f <| by rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]

Induced linear map on quotient by span of a single element

Informal description

Given a module $M$ over a ring $R$, an element $x \in M$, a linear map $f \colon M \to M₂$ that vanishes at $x$ (i.e., $f(x) = 0$), the function `Submodule.liftQSpanSingleton` constructs the induced linear map from the quotient module $M ⧸ (R \cdot x)$ to $M₂$. Here, $R \cdot x$ denotes the submodule spanned by $x$. The map sends an equivalence class $[y]$ in $M ⧸ (R \cdot x)$ to $f(y)$ in $M₂$.

Submodule.liftQSpanSingleton_apply theorem

(x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M) : liftQSpanSingleton x f h (Quotient.mk y) = f y

Full source

@[simp]
theorem liftQSpanSingleton_apply (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M) :
    liftQSpanSingleton x f h (Quotient.mk y) = f y :=
  rfl

Evaluation of Induced Linear Map on Quotient by Span of a Single Element

Informal description

Given a module $M$ over a ring $R$, an element $x \in M$, a linear map $f \colon M \to M₂$ such that $f(x) = 0$, and an element $y \in M$, the induced linear map $\overline{f} \colon M ⧸ (R \cdot x) \to M₂$ satisfies $\overline{f}([y]) = f(y)$, where $[y]$ denotes the equivalence class of $y$ in the quotient module $M ⧸ (R \cdot x)$.

Submodule.range_mkQ theorem

: range p.mkQ = ⊤

Full source

@[simp]
theorem range_mkQ : range p.mkQ = ⊤ :=
  eq_top_iff'.2 <| by rintro ⟨x⟩; exact ⟨x, rfl⟩

Range of Quotient Map is Entire Quotient Module

Informal description

The range of the quotient map $\pi : M \to M ⧸ p$ is the entire quotient module $M ⧸ p$, i.e., $\text{range}(\pi) = \top$.

Submodule.ker_mkQ theorem

: ker p.mkQ = p

Full source

@[simp]
theorem ker_mkQ : ker p.mkQ = p := by ext; simp

Kernel of Quotient Map Equals Submodule

Informal description

The kernel of the quotient linear map $\pi : M \to M ⧸ p$ is equal to the submodule $p$ itself, i.e., $\ker(\pi) = p$.

Submodule.le_comap_mkQ theorem

(p' : Submodule R (M ⧸ p)) : p ≤ comap p.mkQ p'

Full source

theorem le_comap_mkQ (p' : Submodule R (M ⧸ p)) : p ≤ comap p.mkQ p' := by
  simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

Submodule Containment in Preimage of Quotient Map

Informal description

For any submodule $p'$ of the quotient module $M ⧸ p$, the submodule $p$ is contained in the preimage of $p'$ under the quotient map $\pi : M \to M ⧸ p$, i.e., $p \leq \pi^{-1}(p')$.

Submodule.mkQ_map_self theorem

: map p.mkQ p = ⊥

Full source

@[simp]
theorem mkQ_map_self : map p.mkQ p = ⊥ := by
  rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]

Quotient Map Annihilates Submodule: $\pi(p) = 0$

Informal description

For a submodule $p$ of a module $M$ over a ring $R$, the image of $p$ under the quotient map $\pi : M \to M ⧸ p$ is the zero submodule, i.e., $\pi(p) = 0$.

Submodule.comap_map_mkQ theorem

: comap p.mkQ (map p.mkQ p') = p ⊔ p'

Full source

@[simp]
theorem comap_map_mkQ : comap p.mkQ (map p.mkQ p') = p ⊔ p' := by simp [comap_map_eq, sup_comm]

Preimage-Image Identity for Quotient Modules: $\pi^{-1}(\pi(p')) = p \sqcup p'$

Informal description

For any submodules $p$ and $p'$ of a module $M$ over a ring $R$, the preimage under the quotient map $\pi : M \to M ⧸ p$ of the image of $p'$ under $\pi$ is equal to the supremum of $p$ and $p'$, i.e., \[ \pi^{-1}(\pi(p')) = p \sqcup p'. \]

Submodule.map_mkQ_eq_top theorem

: map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

Full source

@[simp]
theorem map_mkQ_eq_top : mapmap p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤ := by
  simp only [LinearMap.map_eq_top_iff p.range_mkQ, sup_comm, ker_mkQ]

Quotient Map Image Equals Top iff Join Equals Top

Informal description

For a module $M$ over a ring $R$ with submodules $p$ and $p'$, the image of $p'$ under the quotient map $\pi \colon M \to M ⧸ p$ is the entire quotient module $M ⧸ p$ if and only if the join of $p$ and $p'$ is the entire module $M$, i.e., $\pi(p') = M ⧸ p \leftrightarrow p \sqcup p' = M$.

Submodule.mapQ definition

(f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : M ⧸ p →ₛₗ[τ₁₂] M₂ ⧸ q

Full source

/-- The map from the quotient of `M` by submodule `p` to the quotient of `M₂` by submodule `q` along
`f : M → M₂` is linear. -/
def mapQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ comap f q) : M ⧸ pM ⧸ p →ₛₗ[τ₁₂] M₂ ⧸ q :=
  p.liftQ (q.mkQ.comp f) <| by simpa [ker_comp] using h

Induced linear map between quotient modules

Informal description

Given a linear map $f \colon M \to M₂$ between modules and submodules $p \subseteq M$, $q \subseteq M₂$ such that $p$ is contained in the preimage of $q$ under $f$, the function `Submodule.mapQ` constructs the induced linear map from the quotient module $M ⧸ p$ to $M₂ ⧸ q$. This map sends an equivalence class $[x] \in M ⧸ p$ to $[f(x)] \in M₂ ⧸ q$.

Submodule.mapQ_apply theorem

(f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) : mapQ p q f h (Quotient.mk x) = Quotient.mk (f x)

Full source

@[simp]
theorem mapQ_apply (f : M →ₛₗ[τ₁₂] M₂) {h} (x : M) :
    mapQ p q f h (Quotient.mk x) = Quotient.mk (f x) :=
  rfl

Action of Induced Quotient Map on Equivalence Classes

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with submodules $p \subseteq M$ and $q \subseteq M₂$. Given a linear map $f \colon M \to M₂$ and a condition $h$ ensuring $p \leq f^{-1}(q)$, the induced map $\text{mapQ}_p^q f h \colon M ⧸ p \to M₂ ⧸ q$ satisfies \[ \text{mapQ}_p^q f h ([x]) = [f(x)] \] for any $x \in M$, where $[x]$ denotes the equivalence class of $x$ in $M ⧸ p$.

Submodule.mapQ_mkQ theorem

(f : M →ₛₗ[τ₁₂] M₂) {h} : (mapQ p q f h).comp p.mkQ = q.mkQ.comp f

Full source

theorem mapQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) {h} : (mapQ p q f h).comp p.mkQ = q.mkQ.comp f := by
  ext x; rfl

Commutativity of Induced Quotient Map with Quotient Projections

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau₁₂ \colon R \to S$. Let $p$ be a submodule of $M$ and $q$ be a submodule of $M₂$, and let $f \colon M \to M₂$ be a linear map such that $p$ is contained in the preimage of $q$ under $f$. Then the composition of the induced quotient map $\text{mapQ}(f, h) \colon M ⧸ p \to M₂ ⧸ q$ with the quotient map $\text{mkQ} \colon M \to M ⧸ p$ is equal to the composition of the quotient map $\text{mkQ} \colon M₂ \to M₂ ⧸ q$ with $f$. In symbols: $$(\text{mapQ}(f, h)) \circ \text{mkQ} = \text{mkQ} \circ f$$

Submodule.comap_liftQ theorem

(f : M →ₛₗ[τ₁₂] M₂) (h) : q.comap (p.liftQ f h) = (q.comap f).map (mkQ p)

Full source

theorem comap_liftQ (f : M →ₛₗ[τ₁₂] M₂) (h) : q.comap (p.liftQ f h) = (q.comap f).map (mkQ p) :=
  le_antisymm (by rintro ⟨x⟩ hx; exact ⟨_, hx, rfl⟩)
    (by rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ])

Preimage of Submodule under Induced Quotient Map Equals Quotient of Preimage under Original Map

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau_{12} \colon R \to S$. Let $p$ be a submodule of $M$ and $f \colon M \to M₂$ be a linear map such that $p$ is contained in the kernel of $f$. For any submodule $q$ of $M₂$, the preimage of $q$ under the induced linear map $\operatorname{liftQ}(f, h) \colon M ⧸ p \to M₂$ is equal to the image under the quotient map $\operatorname{mkQ} \colon M \to M ⧸ p$ of the preimage of $q$ under $f$. In symbols: $$(\operatorname{liftQ}(f, h))^{-1}(q) = \operatorname{mkQ}(f^{-1}(q))$$

Submodule.map_liftQ theorem

 [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) (q : Submodule R (M ⧸ p)) : q.map (p.liftQ f h) = (q.comap p.mkQ).map f

Full source

theorem map_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) (q : Submodule R (M ⧸ p)) :
    q.map (p.liftQ f h) = (q.comap p.mkQ).map f :=
  le_antisymm (by rintro _ ⟨⟨x⟩, hxq, rfl⟩; exact ⟨x, hxq, rfl⟩)
    (by rintro _ ⟨x, hxq, rfl⟩; exact ⟨Quotient.mk x, hxq, rfl⟩)

Image of Submodule under Induced Quotient Map Equals Image of Preimage under Original Map

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau₁₂ \colon R \to S$. Let $p$ be a submodule of $M$ and $f \colon M \to M₂$ be a linear map such that $p$ is contained in the kernel of $f$. For any submodule $q$ of the quotient module $M ⧸ p$, the image of $q$ under the induced linear map $\text{liftQ}(f, h) \colon M ⧸ p \to M₂$ equals the image under $f$ of the preimage of $q$ under the quotient map $\text{mkQ} \colon M \to M ⧸ p$. In symbols: $$q.\text{map}(\text{liftQ}(f, h)) = (q.\text{comap}(\text{mkQ})).\text{map}(f)$$

Submodule.ker_liftQ theorem

(f : M →ₛₗ[τ₁₂] M₂) (h) : ker (p.liftQ f h) = (ker f).map (mkQ p)

Full source

theorem ker_liftQ (f : M →ₛₗ[τ₁₂] M₂) (h) : ker (p.liftQ f h) = (ker f).map (mkQ p) :=
  comap_liftQ _ _ _ _

Kernel of Induced Quotient Map Equals Quotient of Kernel of Original Map

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau_{12} \colon R \to S$. Let $p$ be a submodule of $M$ and $f \colon M \to M₂$ be a linear map such that $p$ is contained in the kernel of $f$. Then the kernel of the induced linear map $\operatorname{liftQ}(f, h) \colon M ⧸ p \to M₂$ is equal to the image under the quotient map $\operatorname{mkQ} \colon M \to M ⧸ p$ of the kernel of $f$. In symbols: $$\ker(\operatorname{liftQ}(f, h)) = \operatorname{mkQ}(\ker f)$$

Submodule.range_liftQ theorem

[RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) : range (p.liftQ f h) = range f

Full source

theorem range_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) :
    range (p.liftQ f h) = range f := by simpa only [range_eq_map] using map_liftQ _ _ _ _

Range of Induced Quotient Map Equals Range of Original Linear Map

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau₁₂ \colon R \to S$. Let $p$ be a submodule of $M$ and $f \colon M \to M₂$ be a linear map such that $p$ is contained in the kernel of $f$. Then the range of the induced linear map $\text{liftQ}(f, h) \colon M ⧸ p \to M₂$ equals the range of $f$. In symbols: $$\text{range}(\text{liftQ}(f, h)) = \text{range}(f)$$

Submodule.ker_liftQ_eq_bot theorem

(f : M →ₛₗ[τ₁₂] M₂) (h) (h' : ker f ≤ p) : ker (p.liftQ f h) = ⊥

Full source

theorem ker_liftQ_eq_bot (f : M →ₛₗ[τ₁₂] M₂) (h) (h' : ker f ≤ p) : ker (p.liftQ f h) = ⊥ := by
  rw [ker_liftQ, le_antisymm h h', mkQ_map_self]

Trivial Kernel of Induced Quotient Map When Kernel Equals Submodule

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau_{12} \colon R \to S$. Let $p$ be a submodule of $M$ and $f \colon M \to M₂$ be a linear map such that: 1. $p$ is contained in the kernel of $f$ (i.e., $p \leq \ker f$), and 2. The kernel of $f$ is contained in $p$ (i.e., $\ker f \leq p$). Then the kernel of the induced linear map $\operatorname{liftQ}(f, h) \colon M ⧸ p \to M₂$ is trivial, i.e., $\ker(\operatorname{liftQ}(f, h)) = \{0\}$.

Submodule.ker_liftQ_eq_bot' theorem

(f : M →ₛₗ[τ₁₂] M₂) (h : p = ker f) : ker (p.liftQ f (le_of_eq h)) = ⊥

Full source

theorem ker_liftQ_eq_bot' (f : M →ₛₗ[τ₁₂] M₂) (h : p = ker f) :
    ker (p.liftQ f (le_of_eq h)) = ⊥ :=
  ker_liftQ_eq_bot p f h.le h.ge

Trivial Kernel of Quotient Map When Submodule Equals Kernel

Informal description

Let $M$ and $M₂$ be modules over rings $R$ and $S$ respectively, with a ring homomorphism $\tau_{12} \colon R \to S$. Let $f \colon M \to M₂$ be a linear map and $p$ be a submodule of $M$ such that $p = \ker f$. Then the kernel of the induced linear map $\operatorname{liftQ}(f, \text{le\_of\_eq } h) \colon M ⧸ p \to M₂$ is trivial, i.e., $\ker(\operatorname{liftQ}(f, \text{le\_of\_eq } h)) = \{0\}$.

Submodule.factor abbrev

(H : p ≤ p') : M ⧸ p →ₗ[R] M ⧸ p'

Full source

/-- The linear map from the quotient by a smaller submodule to the quotient by a larger submodule.

This is the `Submodule.Quotient` version of `Quot.Factor`

When the two submodules are of the form `I ^ m • ⊤` and `I ^ n • ⊤` and `n ≤ m`,
please refer to the dedicated version `Submodule.factorPow`. -/
abbrev factor (H : p ≤ p') : M ⧸ pM ⧸ p →ₗ[R] M ⧸ p' :=
  mapQ _ _ LinearMap.id H

Canonical Linear Map Between Quotient Modules Induced by Submodule Inclusion

Informal description

Given a module $M$ over a ring $R$ and two submodules $p \subseteq p'$ of $M$, there exists a canonical linear map $\text{factor} \colon M ⧸ p \to M ⧸ p'$ induced by the inclusion $p \subseteq p'$. This map sends the equivalence class $[x]_p \in M ⧸ p$ to $[x]_{p'} \in M ⧸ p'$.

Submodule.factor_mk theorem

(H : p ≤ p') (x : M) : factor H (mkQ p x) = mkQ p' x

Full source

@[simp]
theorem factor_mk (H : p ≤ p') (x : M) : factor H (mkQ p x) = mkQ p' x :=
  rfl

Canonical Quotient Map Preserves Equivalence Classes

Informal description

Given a module $M$ over a ring $R$ and two submodules $p \subseteq p'$ of $M$, the canonical linear map $\text{factor} \colon M ⧸ p \to M ⧸ p'$ satisfies $\text{factor}([x]_p) = [x]_{p'}$ for any $x \in M$, where $[x]_p$ denotes the equivalence class of $x$ in $M ⧸ p$.

Submodule.factor_comp_mk theorem

(H : p ≤ p') : (factor H).comp (mkQ p) = mkQ p'

Full source

@[simp]
theorem factor_comp_mk (H : p ≤ p') : (factor H).comp (mkQ p) = mkQ p' := by
  ext x
  rw [LinearMap.comp_apply, factor_mk]

Commutativity of Quotient Maps via Submodule Inclusion

Informal description

For any module $M$ over a ring $R$ and submodules $p \subseteq p'$ of $M$, the composition of the canonical linear map $\text{factor} \colon M ⧸ p \to M ⧸ p'$ with the quotient map $\text{mkQ} \colon M \to M ⧸ p$ equals the quotient map $\text{mkQ} \colon M \to M ⧸ p'$. In other words, the following diagram commutes: \[ \begin{CD} M @>{\text{mkQ}_p}>> M ⧸ p \\ @| @VV{\text{factor}}V \\ M @>{\text{mkQ}_{p'}}>> M ⧸ p' \end{CD} \]

Submodule.factor_comp theorem

(H1 : p ≤ p') (H2 : p' ≤ p'') : (factor H2).comp (factor H1) = factor (H1.trans H2)

Full source

@[simp]
theorem factor_comp (H1 : p ≤ p') (H2 : p' ≤ p'') :
    (factor H2).comp (factor H1) = factor (H1.trans H2) := by
  ext
  simp

Composition of Canonical Quotient Maps for Nested Submodules

Informal description

Given a module $M$ over a ring $R$ and submodules $p \subseteq p' \subseteq p''$ of $M$, the composition of the canonical linear maps $M ⧸ p \to M ⧸ p'$ and $M ⧸ p' \to M ⧸ p''$ equals the canonical linear map $M ⧸ p \to M ⧸ p''$ induced by the inclusion $p \subseteq p''$. In other words, the following diagram commutes: \[ \begin{CD} M ⧸ p @>{\text{factor}_{p \subseteq p'}}>> M ⧸ p' \\ @VV{\text{factor}_{p \subseteq p''}}V @VV{\text{factor}_{p' \subseteq p''}}V \\ M ⧸ p'' @= M ⧸ p'' \end{CD} \]

Submodule.factor_comp_apply theorem

(H1 : p ≤ p') (H2 : p' ≤ p'') (x : M ⧸ p) : factor H2 (factor H1 x) = factor (H1.trans H2) x

Full source

@[simp]
theorem factor_comp_apply (H1 : p ≤ p') (H2 : p' ≤ p'') (x : M ⧸ p) :
    factor H2 (factor H1 x) = factor (H1.trans H2) x := by
  rw [← comp_apply]
  simp

Composition of Quotient Maps for Nested Submodules

Informal description

For any module $M$ over a ring $R$ and submodules $p \subseteq p' \subseteq p''$ of $M$, given an element $x \in M ⧸ p$, applying the canonical linear maps $M ⧸ p \to M ⧸ p'$ and then $M ⧸ p' \to M ⧸ p''$ to $x$ is equal to applying the canonical linear map $M ⧸ p \to M ⧸ p''$ directly to $x$.

Submodule.factor_surjective theorem

(H : p ≤ p') : Function.Surjective (factor H)

Full source

lemma factor_surjective (H : p ≤ p') : Function.Surjective (factor H) := by
  intro x
  use Quotient.mk x.out
  exact Quotient.out_eq x

Surjectivity of the Canonical Quotient Map Between Nested Submodule Quotients

Informal description

For any module $M$ over a ring $R$ and submodules $p \subseteq p'$ of $M$, the canonical linear map $\text{factor} \colon M ⧸ p \to M ⧸ p'$ induced by the inclusion $p \subseteq p'$ is surjective.

Submodule.comapMkQRelIso definition

: Submodule R (M ⧸ p) ≃o Set.Ici p

Full source

/-- The correspondence theorem for modules: there is an order isomorphism between submodules of the
quotient of `M` by `p`, and submodules of `M` larger than `p`. -/
def comapMkQRelIso : SubmoduleSubmodule R (M ⧸ p) ≃o Set.Ici p where
  toFun p' := ⟨comap p.mkQ p', le_comap_mkQ p _⟩
  invFun q := map p.mkQ q
  left_inv p' := map_comap_eq_self <| by simp
  right_inv := fun ⟨q, hq⟩ => Subtype.ext_val <| by simpa [comap_map_mkQ p]
  map_rel_iff' := comap_le_comap_iff <| range_mkQ _

Correspondence theorem for submodules via quotient map

Informal description

The order isomorphism between the submodules of the quotient module $M ⧸ p$ and the submodules of $M$ containing $p$. Specifically, it maps a submodule $p'$ of $M ⧸ p$ to its preimage under the quotient map $\pi : M \to M ⧸ p$, and conversely maps a submodule $q$ of $M$ containing $p$ to its image under $\pi$.

Submodule.comapMkQOrderEmbedding definition

: Submodule R (M ⧸ p) ↪o Submodule R M

Full source

/-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
of `M`. -/
def comapMkQOrderEmbedding : SubmoduleSubmodule R (M ⧸ p) ↪o Submodule R M :=
  (RelIso.toRelEmbedding <| comapMkQRelIso p).trans (Subtype.relEmbedding (· ≤ ·) _)

Order embedding of submodules via quotient map

Informal description

The order embedding from the submodules of the quotient module $M ⧸ p$ to the submodules of $M$ containing $p$. Specifically, it maps a submodule $p'$ of $M ⧸ p$ to its preimage under the quotient map $\pi : M \to M ⧸ p$, preserving the order structure.

Submodule.comapMkQOrderEmbedding_eq theorem

(p' : Submodule R (M ⧸ p)) : comapMkQOrderEmbedding p p' = comap p.mkQ p'

Full source

@[simp]
theorem comapMkQOrderEmbedding_eq (p' : Submodule R (M ⧸ p)) :
    comapMkQOrderEmbedding p p' = comap p.mkQ p' :=
  rfl

Equality of Order Embedding and Preimage under Quotient Map

Informal description

For any submodule $p'$ of the quotient module $M ⧸ p$, the image of $p'$ under the order embedding `comapMkQOrderEmbedding` is equal to the preimage of $p'$ under the quotient map $\pi : M \to M ⧸ p$.

Submodule.span_preimage_eq theorem

 [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty) (h₁ : s ⊆ range f) :
  span R (f ⁻¹' s) = (span R₂ s).comap f

Full source

theorem span_preimage_eq [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty)
    (h₁ : s ⊆ range f) : span R (f ⁻¹' s) = (span R₂ s).comap f := by
  suffices (span R₂ s).comap f ≤ span R (f ⁻¹' s) by exact le_antisymm (span_preimage_le f s) this
  have hk : ker f ≤ span R (f ⁻¹' s) := by
    let y := Classical.choose h₀
    have hy : y ∈ s := Classical.choose_spec h₀
    rw [ker_le_iff]
    use y, h₁ hy
    rw [← Set.singleton_subset_iff] at hy
    exact Set.Subset.trans subset_span (span_mono (Set.preimage_mono hy))
  rw [← left_eq_sup] at hk
  rw [range_coe f] at h₁
  rw [hk, ← LinearMap.map_le_map_iff, map_span, map_comap_eq, Set.image_preimage_eq_of_subset h₁]
  exact inf_le_right

Equality of Span and Preimage under Linear Map: $\text{span}_R(f^{-1}(s)) = f^{-1}(\text{span}_{R_2}(s))$ for $s \subseteq \text{range}(f)$

Informal description

Let $R$ and $R_2$ be rings, $M$ and $M_2$ be modules over $R$ and $R_2$ respectively, and $\tau_{12}: R \to R_2$ be a ring homomorphism. Given a surjective linear map $f: M \to M_2$ (with respect to $\tau_{12}$), and a nonempty subset $s \subseteq M_2$ contained in the range of $f$, the span of the preimage $f^{-1}(s)$ in $M$ equals the preimage under $f$ of the span of $s$ in $M_2$. That is, $$\text{span}_R(f^{-1}(s)) = f^{-1}(\text{span}_{R_2}(s)).$$

Submodule.Quotient.equiv definition

 {N : Type*} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : P.map f = Q) :
  (M ⧸ P) ≃ₗ[R] N ⧸ Q

Full source

/-- If `P` is a submodule of `M` and `Q` a submodule of `N`,
and `f : M ≃ₗ N` maps `P` to `Q`, then `M ⧸ P` is equivalent to `N ⧸ Q`. -/
@[simps]
def Quotient.equiv {N : Type*} [AddCommGroup N] [Module R N] (P : Submodule R M)
    (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : P.map f = Q) : (M ⧸ P) ≃ₗ[R] N ⧸ Q :=
  { P.mapQ Q (f : M →ₗ[R] N) fun _ hx => hf ▸ Submodule.mem_map_of_mem hx with
    toFun := P.mapQ Q (f : M →ₗ[R] N) fun _ hx => hf ▸ Submodule.mem_map_of_mem hx
    invFun :=
      Q.mapQ P (f.symm : N →ₗ[R] M) fun x hx => by
        rw [← hf, Submodule.mem_map] at hx
        obtain ⟨y, hy, rfl⟩ := hx
        simpa
    left_inv := fun x => Submodule.Quotient.induction_on _ x (by simp)
    right_inv := fun x => Submodule.Quotient.induction_on _ x (by simp) }

Linear equivalence of quotient modules induced by a linear equivalence of modules

Informal description

Given modules $M$ and $N$ over a ring $R$, with submodules $P \subseteq M$ and $Q \subseteq N$, and a linear equivalence $f \colon M \simeq N$ that maps $P$ to $Q$ (i.e., $f(P) = Q$), there is an induced linear equivalence between the quotient modules $M ⧸ P$ and $N ⧸ Q$.

Submodule.Quotient.equiv_symm theorem

 {R M N : Type*} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : Submodule R M)
  (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : P.map f = Q) :
  (Quotient.equiv P Q f hf).symm = Quotient.equiv Q P f.symm ((Submodule.map_symm_eq_iff f).mpr hf)

Full source

@[simp]
theorem Quotient.equiv_symm {R M N : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N)
    (hf : P.map f = Q) :
    (Quotient.equiv P Q f hf).symm =
      Quotient.equiv Q P f.symm ((Submodule.map_symm_eq_iff f).mpr hf) :=
  rfl

Inverse of Quotient Module Equivalence Induced by Linear Equivalence

Informal description

Let $R$ be a ring, and let $M$ and $N$ be modules over $R$ with submodules $P \subseteq M$ and $Q \subseteq N$. Given a linear equivalence $f \colon M \simeq N$ such that $f(P) = Q$, the inverse of the induced linear equivalence $\text{Quotient.equiv} \colon M ⧸ P \simeq N ⧸ Q$ is equal to the linear equivalence induced by the inverse map $f^{-1} \colon N \simeq M$ and the condition $f^{-1}(Q) = P$.

Submodule.Quotient.equiv_trans theorem

 {N O : Type*} [AddCommGroup N] [Module R N] [AddCommGroup O] [Module R O] (P : Submodule R M) (Q : Submodule R N)
  (S : Submodule R O) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O) (he : P.map e = Q) (hf : Q.map f = S)
  (hef : P.map (e.trans f) = S) :
  Quotient.equiv P S (e.trans f) hef = (Quotient.equiv P Q e he).trans (Quotient.equiv Q S f hf)

Full source

@[simp]
theorem Quotient.equiv_trans {N O : Type*} [AddCommGroup N] [Module R N] [AddCommGroup O]
    [Module R O] (P : Submodule R M) (Q : Submodule R N) (S : Submodule R O) (e : M ≃ₗ[R] N)
    (f : N ≃ₗ[R] O) (he : P.map e = Q) (hf : Q.map f = S) (hef : P.map (e.trans f) = S) :
    Quotient.equiv P S (e.trans f) hef =
      (Quotient.equiv P Q e he).trans (Quotient.equiv Q S f hf) := by
  ext
  -- `simp` can deal with `hef` depending on `e` and `f`
  simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]
  -- `rw` can deal with `mapQ_comp` needing extra hypotheses coming from the RHS
  rw [mapQ_comp, LinearMap.comp_apply]

Transitivity of Induced Linear Equivalences on Quotient Modules

Informal description

Let $M$, $N$, and $O$ be modules over a ring $R$, with submodules $P \subseteq M$, $Q \subseteq N$, and $S \subseteq O$. Given linear equivalences $e \colon M \simeq N$ and $f \colon N \simeq O$ such that $e$ maps $P$ to $Q$ (i.e., $e(P) = Q$) and $f$ maps $Q$ to $S$ (i.e., $f(Q) = S$), the induced linear equivalence between the quotient modules $M ⧸ P$ and $O ⧸ S$ via the composition $e \circ f$ is equal to the composition of the induced linear equivalences $M ⧸ P \simeq N ⧸ Q$ and $N ⧸ Q \simeq O ⧸ S$.

LinearMap.range_mkQ_comp theorem

(f : M →ₛₗ[τ₁₂] M₂) : (range f).mkQ.comp f = 0

Full source

theorem range_mkQ_comp (f : M →ₛₗ[τ₁₂] M₂) : (range f).mkQ.comp f = 0 :=
  LinearMap.ext fun x => by simp

Composition of Quotient Map with Linear Map Yields Zero Map

Informal description

For any linear map $f \colon M \to M₂$ between modules over appropriate rings, the composition of the quotient map $(M₂ ⧸ \text{range } f).\text{mkQ}$ with $f$ is the zero map, i.e., $(\text{range } f).\text{mkQ} \circ f = 0$.

LinearMap.ker_le_range_iff theorem

 {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} : ker g ≤ range f ↔ (range f).mkQ.comp (ker g).subtype = 0

Full source

theorem ker_le_range_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
    kerker g ≤ range f ↔ (range f).mkQ.comp (ker g).subtype = 0 := by
  rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]

Kernel-Range Containment Criterion via Quotient Map Composition

Informal description

For any linear maps $f \colon M \to M_2$ and $g \colon M_2 \to M_3$ between modules over appropriate rings, the kernel of $g$ is contained in the range of $f$ if and only if the composition of the quotient map $(M_2 ⧸ \text{range } f).\text{mkQ}$ with the inclusion map $\text{ker } g \hookrightarrow M_2$ is the zero map, i.e., $(\text{range } f).\text{mkQ} \circ (\text{ker } g).\text{subtype} = 0$.

LinearMap.range_eq_top_of_cancel theorem

 {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ u v : M₂ →ₗ[R₂] M₂ ⧸ (range f), u.comp f = v.comp f → u = v) : range f = ⊤

Full source

/-- An epimorphism is surjective. -/
theorem range_eq_top_of_cancel {f : M →ₛₗ[τ₁₂] M₂}
    (h : ∀ u v : M₂ →ₗ[R₂] M₂ ⧸ (range f), u.comp f = v.comp f → u = v) : range f = ⊤ := by
  have h₁ : (0 : M₂ →ₗ[R₂] M₂ ⧸ (range f)).comp f = 0 := zero_comp _
  rw [← Submodule.ker_mkQ (range f), ← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)]
  exact ker_zero

Surjectivity of Linear Map via Cancellation Property

Informal description

Let $f \colon M \to M₂$ be a linear map between modules over appropriate rings. If for any two linear maps $u, v \colon M₂ \to M₂ ⧸ \text{range } f$, the condition $u \circ f = v \circ f$ implies $u = v$, then the range of $f$ is the entire module $M₂$, i.e., $\text{range } f = \top$.

Submodule.quotEquivOfEqBot definition

(hp : p = ⊥) : (M ⧸ p) ≃ₗ[R] M

Full source

/-- If `p = ⊥`, then `M / p ≃ₗ[R] M`. -/
def quotEquivOfEqBot (hp : p = ⊥) : (M ⧸ p) ≃ₗ[R] M :=
  LinearEquiv.ofLinear (p.liftQ id <| hp.symm ▸ bot_le) p.mkQ (liftQ_mkQ _ _ _) <|
    p.quot_hom_ext _ LinearMap.id fun _ => rfl

Linear equivalence between quotient by zero submodule and original module

Informal description

Given a module $M$ over a ring $R$ and a submodule $p$ of $M$ that is equal to the zero submodule $\bot$, there exists a linear equivalence between the quotient module $M ⧸ p$ and $M$ itself. This equivalence maps each equivalence class $[x] \in M ⧸ p$ to its representative $x \in M$, and conversely, each $x \in M$ to its equivalence class $[x] \in M ⧸ p$.

Submodule.quotEquivOfEqBot_apply_mk theorem

(hp : p = ⊥) (x : M) : p.quotEquivOfEqBot hp (Quotient.mk x) = x

Full source

@[simp]
theorem quotEquivOfEqBot_apply_mk (hp : p = ⊥) (x : M) :
    p.quotEquivOfEqBot hp (Quotient.mk x) = x :=
  rfl

Linear equivalence $\text{quotEquivOfEqBot}$ maps equivalence class to representative when quotienting by zero submodule

Informal description

Let $M$ be a module over a ring $R$ and $p$ a submodule of $M$ such that $p = \bot$ (the zero submodule). For any element $x \in M$, the linear equivalence $\text{quotEquivOfEqBot}$ applied to the equivalence class $[x] \in M ⧸ p$ returns $x$ itself, i.e., $\text{quotEquivOfEqBot}([x]) = x$.

Submodule.quotEquivOfEqBot_symm_apply theorem

(hp : p = ⊥) (x : M) : (p.quotEquivOfEqBot hp).symm x = (Quotient.mk x)

Full source

@[simp]
theorem quotEquivOfEqBot_symm_apply (hp : p = ⊥) (x : M) :
    (p.quotEquivOfEqBot hp).symm x = (Quotient.mk x) :=
  rfl

Inverse of Quotient Equivalence by Zero Submodule Maps Elements to Their Equivalence Classes

Informal description

Given a module $M$ over a ring $R$ and a submodule $p$ of $M$ such that $p$ is the zero submodule (i.e., $p = \bot$), the inverse of the linear equivalence $\text{quotEquivOfEqBot}$ maps any element $x \in M$ to its equivalence class $[x] \in M ⧸ p$.

Submodule.coe_quotEquivOfEqBot_symm theorem

(hp : p = ⊥) : ((p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ

Full source

@[simp]
theorem coe_quotEquivOfEqBot_symm (hp : p = ⊥) :
    ((p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ :=
  rfl

Inverse of Quotient Equivalence by Zero Submodule Equals Quotient Map

Informal description

For a module $M$ over a ring $R$ and a submodule $p$ of $M$ such that $p$ is the zero submodule (i.e., $p = \bot$), the inverse of the linear equivalence $\text{quotEquivOfEqBot}$ from $M$ to $M ⧸ p$ is equal to the quotient map $\text{mkQ} : M → M ⧸ p$ as linear maps.

Submodule.Quotient.equiv_refl theorem

 (P : Submodule R M) (Q : Submodule R M) (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :
  Quotient.equiv P Q (LinearEquiv.refl R M) hf = quotEquivOfEq _ _ (by simpa using hf)

Full source

@[simp]
theorem Quotient.equiv_refl (P : Submodule R M) (Q : Submodule R M)
    (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :
    Quotient.equiv P Q (LinearEquiv.refl R M) hf = quotEquivOfEq _ _ (by simpa using hf) :=
  rfl

Identity Linear Equivalence Induces Identity on Quotient Modules

Informal description

Given a module $M$ over a ring $R$ and submodules $P, Q \subseteq M$ such that the image of $P$ under the identity linear equivalence $\text{id}_M$ equals $Q$, the induced linear equivalence $\text{Quotient.equiv}$ between the quotient modules $M ⧸ P$ and $M ⧸ Q$ is equal to the linear equivalence $\text{quotEquivOfEq}$ induced by the equality $P = Q$.

Submodule.mapQLinear definition

: compatibleMaps p q →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q

Full source

/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
the natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear. -/
def mapQLinear : compatibleMapscompatibleMaps p q →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q where
  toFun f := mapQ _ _ f.val f.property
  map_add' x y := by
    ext
    rfl
  map_smul' c f := by
    ext
    rfl

Linear map between spaces of compatible linear maps and quotient maps

Informal description

Given modules $M$ and $M₂$ over a commutative ring $R$, with submodules $p \subseteq M$ and $q \subseteq M₂$, the natural linear map from the space of linear maps $\{f \in \text{Hom}(M, M₂) \mid f(p) \subseteq q\}$ to $\text{Hom}(M/p, M₂/q)$ is defined. This map takes a linear map $f$ satisfying $f(p) \subseteq q$ to the induced map $\overline{f} \colon M/p \to M₂/q$ that sends $[x]$ to $[f(x)]$.

Main definitions