Mathlib.LinearAlgebra.Isomorphisms

LinearMap.quotKerEquivRange definition

: (M ⧸ LinearMap.ker f) ≃ₗ[R] LinearMap.range f

Full source

/-- The **first isomorphism law for modules**. The quotient of `M` by the kernel of `f` is linearly
equivalent to the range of `f`. -/
noncomputable def quotKerEquivRange : (M ⧸ LinearMap.ker f) ≃ₗ[R] LinearMap.range f :=
  (LinearEquiv.ofInjective ((LinearMap.ker f).liftQ f <| le_rfl) <|
        ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ (le_refl (LinearMap.ker f))).trans
    (LinearEquiv.ofEq _ _ <| Submodule.range_liftQ _ _ _)

First Isomorphism Theorem for Modules (Quotient by Kernel Isomorphic to Range)

Informal description

The **first isomorphism theorem for modules** states that for a linear map $ f: M \to M₂ $ over a ring $ R $, the quotient module $ M / \ker f $ is linearly isomorphic to the range of $ f $. More precisely, there exists a linear equivalence $ (M / \ker f) \simeq \text{range } f $, where $ \ker f $ is the kernel of $ f $ and $ \text{range } f $ is the submodule of $ M₂ $ consisting of all elements of the form $ f(x) $ for $ x \in M $.

LinearMap.quotKerEquivOfSurjective definition

(f : M →ₗ[R] M₂) (hf : Function.Surjective f) : (M ⧸ LinearMap.ker f) ≃ₗ[R] M₂

Full source

/-- The **first isomorphism theorem for surjective linear maps**. -/
noncomputable def quotKerEquivOfSurjective (f : M →ₗ[R] M₂) (hf : Function.Surjective f) :
    (M ⧸ LinearMap.ker f) ≃ₗ[R] M₂ :=
  f.quotKerEquivRange.trans <| .ofTop (LinearMap.range f) <| range_eq_top.2 hf

First Isomorphism Theorem for Surjective Linear Maps

Informal description

The **first isomorphism theorem for surjective linear maps** states that for a surjective linear map $ f: M \to M₂ $ over a ring $ R $, the quotient module $ M / \ker f $ is linearly isomorphic to $ M₂ $. More precisely, there exists a linear equivalence $ (M / \ker f) \simeq M₂ $, where $ \ker f $ is the kernel of $ f $.

LinearMap.quotKerEquivRange_apply_mk theorem

(x : M) : (f.quotKerEquivRange (Submodule.Quotient.mk x) : M₂) = f x

Full source

@[simp]
theorem quotKerEquivRange_apply_mk (x : M) :
    (f.quotKerEquivRange (Submodule.Quotient.mk x) : M₂) = f x :=
  rfl

First Isomorphism Theorem: Image of Quotient Class Equals Value of Linear Map

Informal description

For any element $x$ in the module $M$, the image of the equivalence class of $x$ under the first isomorphism theorem equivalence $f.\text{quotKerEquivRange}$ equals the value of the linear map $f$ at $x$. In symbols: \[ f.\text{quotKerEquivRange}(\overline{x}) = f(x) \] where $\overline{x}$ denotes the equivalence class of $x$ in the quotient module $M / \ker f$.

LinearMap.quotKerEquivRange_symm_apply_image theorem

(x : M) (h : f x ∈ LinearMap.range f) : f.quotKerEquivRange.symm ⟨f x, h⟩ = (LinearMap.ker f).mkQ x

Full source

@[simp]
theorem quotKerEquivRange_symm_apply_image (x : M) (h : f x ∈ LinearMap.range f) :
    f.quotKerEquivRange.symm ⟨f x, h⟩ = (LinearMap.ker f).mkQ x :=
  f.quotKerEquivRange.symm_apply_apply ((LinearMap.ker f).mkQ x)

Inverse of First Isomorphism Theorem Equivalence Applied to Image Element

Informal description

For any linear map $ f: M \to M₂ $ over a ring $ R $, if $ x \in M $ and $ f(x) $ is in the range of $ f $, then the inverse of the first isomorphism theorem equivalence applied to $ \langle f(x), h \rangle $ (where $ h $ is the proof that $ f(x) $ is in the range) equals the canonical quotient map of $ x $ modulo the kernel of $ f $. In symbols: \[ f.\text{quotKerEquivRange}^{-1}(\langle f(x), h \rangle) = \text{ker}(f).\text{mkQ}(x) \]

LinearMap.subToSupQuotient abbrev

(p p' : Submodule R M) : { x // x ∈ p } →ₗ[R] { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'

Full source

/-- Linear map from `p` to `p+p'/p'` where `p p'` are submodules of `R` -/
abbrev subToSupQuotient (p p' : Submodule R M) :
    { x // x ∈ p }{ x // x ∈ p } →ₗ[R] { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p' :=
  (comap (p ⊔ p').subtype p').mkQ.comp (Submodule.inclusion le_sup_left)

Canonical Linear Map from Submodule to Supremum Quotient

Informal description

Given submodules $p$ and $p'$ of an $R$-module $M$, there exists a linear map from the submodule $p$ to the quotient module $(p + p')/p'$, where $p + p'$ denotes the supremum of $p$ and $p'$.

LinearMap.comap_leq_ker_subToSupQuotient theorem

(p p' : Submodule R M) : comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')

Full source

theorem comap_leq_ker_subToSupQuotient (p p' : Submodule R M) :
    comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p') := by
  rw [LinearMap.ker_comp, Submodule.inclusion, comap_codRestrict, ker_mkQ, map_comap_subtype]
  exact comap_mono (inf_le_inf_right _ le_sup_left)

Inclusion of Intersection in Kernel of Submodule-to-Quotient Map

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$, the preimage of the intersection $p \cap p'$ under the inclusion map of $p$ is contained in the kernel of the canonical linear map from $p$ to the quotient module $(p + p')/p'$. In symbols: \[ \text{comap}(p.\text{subtype})(p \cap p') \leq \text{ker}(\text{subToSupQuotient}(p, p')) \]

LinearMap.quotientInfToSupQuotient definition

 (p p' : Submodule R M) :
  (↥p) ⧸ (comap p.subtype p ⊓ comap p.subtype p') →ₗ[R] (↥(p ⊔ p')) ⧸ (comap (p ⊔ p').subtype p')

Full source

/-- Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')`
to `x + p'`, where `p` and `p'` are submodules of an ambient module.

Note that in the following declaration the type of the domain is expressed using
``comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`). -/
def quotientInfToSupQuotient (p p' : Submodule R M) :
    (↥p) ⧸ (comap p.subtype p ⊓ comap p.subtype p')(↥p) ⧸ (comap p.subtype p ⊓ comap p.subtype p') →ₗ[R]
      (↥(p ⊔ p')) ⧸ (comap (p ⊔ p').subtype p') :=
   (comap p.subtype (p ⊓ p')).liftQ (subToSupQuotient p p') (comap_leq_ker_subToSupQuotient p p')

Canonical quotient map from $p/(p \cap p')$ to $(p + p')/p'$

Informal description

Given submodules $p$ and $p'$ of an $R$-module $M$, the canonical linear map from the quotient module $p/(p \cap p')$ to the quotient module $(p + p')/p'$ sends $x + (p \cap p')$ to $x + p'$ for any $x \in p$. Here, $p \cap p'$ denotes the intersection of $p$ and $p'$, and $p + p'$ denotes their sum (supremum as submodules). The map is well-defined and linear over $R$.

LinearMap.quotientInfEquivSupQuotient_injective theorem

(p p' : Submodule R M) : Function.Injective (quotientInfToSupQuotient p p')

Full source

theorem quotientInfEquivSupQuotient_injective (p p' : Submodule R M) :
    Function.Injective (quotientInfToSupQuotient p p') := by
  rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
  rw [ker_comp, ker_mkQ]
  exact fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩

Injectivity of the Second Isomorphism Theorem for Modules

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$, the canonical linear map from $p/(p \cap p')$ to $(p + p')/p'$ is injective. Here, $p \cap p'$ denotes the intersection of $p$ and $p'$, and $p + p'$ denotes their sum as submodules.

LinearMap.quotientInfEquivSupQuotient_surjective theorem

(p p' : Submodule R M) : Function.Surjective (quotientInfToSupQuotient p p')

Full source

theorem quotientInfEquivSupQuotient_surjective (p p' : Submodule R M) :
    Function.Surjective (quotientInfToSupQuotient p p') := by
  rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
  rintro ⟨x, hx⟩; rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
  use ⟨y, hy⟩; apply (Submodule.Quotient.eq _).2
  simp only [mem_comap, map_sub, coe_subtype, coe_inclusion, sub_add_cancel_left, neg_mem_iff, hz]

Surjectivity of the Second Isomorphism Theorem Map for Modules

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$, the canonical linear map $\varphi: p/(p \cap p') \to (p + p')/p'$ is surjective. Here: - $p \cap p'$ denotes the intersection of submodules - $p + p'$ denotes their sum (supremum as submodules) - The map $\varphi$ sends $x + (p \cap p')$ to $x + p'$ for any $x \in p$

LinearMap.quotientInfEquivSupQuotient definition

(p p' : Submodule R M) : (p ⧸ comap p.subtype p ⊓ comap p.subtype p') ≃ₗ[R] _ ⧸ comap (p ⊔ p').subtype p'

Full source

/--
Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism.

Note that in the following declaration the type of the domain is expressed using
``comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`). -/
noncomputable def quotientInfEquivSupQuotient (p p' : Submodule R M) :
    (p ⧸ comap p.subtype p ⊓ comap p.subtype p') ≃ₗ[R] _ ⧸ comap (p ⊔ p').subtype p' :=
  LinearEquiv.ofBijective (quotientInfToSupQuotient p p')
    ⟨quotientInfEquivSupQuotient_injective p p', quotientInfEquivSupQuotient_surjective p p'⟩

Second Isomorphism Theorem for Modules

Informal description

Given submodules $p$ and $p'$ of an $R$-module $M$, there is a canonical linear isomorphism between the quotient module $p/(p \cap p')$ and the quotient module $(p + p')/p'$. Here: - $p \cap p'$ denotes the intersection of submodules $p$ and $p'$ - $p + p'$ denotes their sum (supremum as submodules) - The isomorphism maps $x + (p \cap p')$ to $x + p'$ for any $x \in p$

LinearMap.coe_quotientInfToSupQuotient theorem

(p p' : Submodule R M) : ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p'

Full source

@[simp]
theorem coe_quotientInfToSupQuotient (p p' : Submodule R M) :
    ⇑(quotientInfToSupQuotient p p') = quotientInfEquivSupQuotient p p' :=
  rfl

Canonical Quotient Map Coincides with Second Isomorphism Theorem Map

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$, the underlying function of the canonical linear map $\varphi: p/(p \cap p') \to (p + p')/p'$ coincides with the linear isomorphism given by the second isomorphism theorem. Here: - $p \cap p'$ denotes the intersection of submodules - $p + p'$ denotes their sum (supremum as submodules) - The map $\varphi$ sends $x + (p \cap p')$ to $x + p'$ for any $x \in p$

LinearMap.quotientInfEquivSupQuotient_apply_mk theorem

 (p p' : Submodule R M) (x : p) :
  let map := inclusion (le_sup_left : p ≤ p ⊔ p')
  quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) =
    @Submodule.Quotient.mk R (p ⊔ p' : Submodule R M) _ _ _ (comap (p ⊔ p').subtype p') (map x)

Full source

theorem quotientInfEquivSupQuotient_apply_mk (p p' : Submodule R M) (x : p) :
    let map := inclusion (le_sup_left : p ≤ p ⊔ p')
    quotientInfEquivSupQuotient p p' (Submodule.Quotient.mk x) =
      @Submodule.Quotient.mk R (p ⊔ p' : Submodule R M) _ _ _ (comap (p ⊔ p').subtype p') (map x) :=
  rfl

Image of Coset under Second Isomorphism Theorem for Modules

Informal description

Let $p$ and $p'$ be submodules of an $R$-module $M$, and let $x \in p$. Under the second isomorphism theorem's canonical linear isomorphism $\varphi: p/(p \cap p') \to (p + p')/p'$, the image of the coset $x + (p \cap p')$ is equal to the coset $x + p'$ in $(p + p')/p'$. Here: - $p \cap p'$ denotes the intersection of submodules $p$ and $p'$ - $p + p'$ denotes their sum (supremum as submodules) - The isomorphism $\varphi$ maps $x + (p \cap p')$ to $x + p'$ for any $x \in p$

LinearMap.quotientInfEquivSupQuotient_symm_apply_left theorem

 (p p' : Submodule R M) (x : ↥(p ⊔ p')) (hx : (x : M) ∈ p) :
  (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨x, hx⟩

Full source

theorem quotientInfEquivSupQuotient_symm_apply_left (p p' : Submodule R M) (x : ↥(p ⊔ p'))
    (hx : (x : M) ∈ p) :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨x, hx⟩ :=
  (LinearEquiv.symm_apply_eq _).2 <| by
    rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

Inverse Image of Coset under Second Isomorphism Theorem for Modules when $x \in p$

Informal description

Let $p$ and $p'$ be submodules of an $R$-module $M$, and let $x \in p + p'$ with $x \in p$. Then the inverse of the canonical isomorphism from the second isomorphism theorem maps the coset $x + p'$ to the coset $x + (p \cap p')$ in $p/(p \cap p')$. More precisely, for the canonical linear isomorphism $\varphi: p/(p \cap p') \to (p + p')/p'$ from the second isomorphism theorem, we have: \[ \varphi^{-1}(x + p') = x + (p \cap p') \] when $x \in p$.

LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff theorem

 {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
  (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p'

Full source

theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
  (LinearEquiv.symm_apply_eq _).trans <| by simp

Characterization of Zero Preimage in Second Isomorphism Theorem for Modules

Informal description

Let $p$ and $p'$ be submodules of an $R$-module $M$, and let $x \in p + p'$. The preimage of the coset $x + p'$ under the inverse of the second isomorphism theorem's canonical isomorphism is zero in $p/(p \cap p')$ if and only if $x$ belongs to $p'$. More precisely, for the canonical linear isomorphism $\varphi: p/(p \cap p') \to (p + p')/p'$ from the second isomorphism theorem, we have: \[ \varphi^{-1}(x + p') = 0 \iff x \in p' \]

LinearMap.quotientInfEquivSupQuotient_symm_apply_right theorem

 (p p' : Submodule R M) {x : ↥(p ⊔ p')} (hx : (x : M) ∈ p') :
  (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0

Full source

theorem quotientInfEquivSupQuotient_symm_apply_right (p p' : Submodule R M) {x : ↥(p ⊔ p')}
    (hx : (x : M) ∈ p') : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x)
    = 0 :=
  quotientInfEquivSupQuotient_symm_apply_eq_zero_iff.2 hx

Vanishing of Preimage for Elements in $p'$ under Second Isomorphism Theorem

Informal description

Let $p$ and $p'$ be submodules of an $R$-module $M$, and let $x \in p + p'$ such that $x \in p'$. Then the preimage of the coset $x + p'$ under the inverse of the canonical isomorphism from the second isomorphism theorem is zero in $p/(p \cap p')$. More precisely, for the canonical linear isomorphism $\varphi: p/(p \cap p') \to (p + p')/p'$, we have: \[ \varphi^{-1}(x + p') = 0 \] whenever $x \in p'$.

Submodule.quotientQuotientEquivQuotientAux definition

(h : S ≤ T) : (M ⧸ S) ⧸ T.map S.mkQ →ₗ[R] M ⧸ T

Full source

/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/
def quotientQuotientEquivQuotientAux (h : S ≤ T) : (M ⧸ S) ⧸ T.map S.mkQ(M ⧸ S) ⧸ T.map S.mkQ →ₗ[R] M ⧸ T :=
  liftQ _ (mapQ S T LinearMap.id h)
    (by
      rintro _ ⟨x, hx, rfl⟩
      rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
      exact (Quotient.mk_eq_zero _).mpr hx)

Auxiliary map for the third isomorphism theorem of modules

Informal description

Given a ring $R$ and an $R$-module $M$ with submodules $S \leq T \leq M$, the auxiliary linear map $(M / S) / (T / S) \to M / T$ is defined as the lift of the quotient map $M/S \to M/T$ through the natural projection. This map sends a double coset $[[x]]$ in $(M/S)/(T/S)$ to the coset $[x]$ in $M/T$, where $x \in M$.

Submodule.quotientQuotientEquivQuotientAux_mk theorem

(x : M ⧸ S) : quotientQuotientEquivQuotientAux S T h (Quotient.mk x) = mapQ S T LinearMap.id h x

Full source

@[simp]
theorem quotientQuotientEquivQuotientAux_mk (x : M ⧸ S) :
    quotientQuotientEquivQuotientAux S T h (Quotient.mk x) = mapQ S T LinearMap.id h x :=
  liftQ_apply _ _ _

Auxiliary Map Evaluation on Coset Equals Quotient Map

Informal description

For any coset $x \in M/S$, the auxiliary linear map $\text{quotientQuotientEquivQuotientAux}$ applied to the coset $\text{Quotient.mk}(x)$ equals the map $\text{mapQ}$ applied to $x$ with the identity linear map and the inclusion $S \leq T$.

Submodule.quotientQuotientEquivQuotientAux_mk_mk theorem

(x : M) : quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x

Full source

@[simp]
theorem quotientQuotientEquivQuotientAux_mk_mk (x : M) :
    quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x := by simp

Auxiliary Map Evaluation on Double Coset Equals Single Coset

Informal description

For any element $x$ of the $R$-module $M$, the auxiliary linear map $\text{quotientQuotientEquivQuotientAux}$ applied to the double coset $[[x]]$ in $(M/S)/(T/S)$ equals the coset $[x]$ in $M/T$.

Submodule.quotientQuotientEquivQuotient definition

: ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ T

Full source

/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`. -/
def quotientQuotientEquivQuotient : ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ T :=
  { quotientQuotientEquivQuotientAux S T h with
    toFun := quotientQuotientEquivQuotientAux S T h
    invFun := mapQ _ _ (mkQ S) (le_comap_map _ _)
    left_inv := fun x => Submodule.Quotient.induction_on _
     x fun x => Submodule.Quotient.induction_on _ x fun x =>
      by simp
    right_inv := fun x => Submodule.Quotient.induction_on _ x
      fun x => by simp }

Noether's third isomorphism theorem for modules

Informal description

Given a ring $R$ and an $R$-module $M$ with submodules $S \leq T \leq M$, there is a natural linear isomorphism $(M / S) / (T / S) \cong M / T$. This is known as Noether's third isomorphism theorem for modules.

Submodule.quotientQuotientEquivQuotientSup definition

: ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ S ⊔ T

Full source

/-- Essentially the same equivalence as in the third isomorphism theorem,
except restated in terms of suprema/addition of submodules instead of `≤`. -/
def quotientQuotientEquivQuotientSup : ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ S ⊔ T :=
  quotEquivOfEqquotEquivOfEq _ _ (by rw [map_sup, mkQ_map_self, bot_sup_eq]) ≪≫ₗ
    quotientQuotientEquivQuotient S (S ⊔ T) le_sup_left

Third isomorphism theorem for modules (supremum version)

Informal description

Given a ring $R$ and an $R$-module $M$ with submodules $S$ and $T$, there is a natural linear isomorphism $(M / S) / (T / S) \cong M / (S \sqcup T)$, where $S \sqcup T$ denotes the supremum (sum) of $S$ and $T$.

Submodule.card_quotient_mul_card_quotient theorem

(S T : Submodule R M) (hST : T ≤ S) : Nat.card (S.map T.mkQ) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)

Full source

/-- Corollary of the third isomorphism theorem: `[S : T] [M : S] = [M : T]` -/
theorem card_quotient_mul_card_quotient (S T : Submodule R M) (hST : T ≤ S) :
    Nat.card (S.map T.mkQ) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T) := by
  rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
    Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]

Cardinality Relation in Third Isomorphism Theorem for Modules

Informal description

Let $R$ be a ring and $M$ an $R$-module with submodules $T \leq S \leq M$. Then the cardinality of the quotient module $S/(T \cdot \text{mkQ})$ multiplied by the cardinality of $M/S$ equals the cardinality of $M/T$, i.e., $$|S/(T \cdot \text{mkQ})| \cdot |M/S| = |M/T|.$$