Mathlib.Algebra.Module.Submodule.Equiv

LinearEquiv.ofEq definition

(h : p = q) : p ≃ₗ[R] q

Full source

/-- Linear equivalence between two equal submodules. -/
def ofEq (h : p = q) : p ≃ₗ[R] q :=
  { Equiv.setCongr (congr_arg _ h) with
    map_smul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

Linear equivalence between equal submodules

Informal description

Given a semiring $R$ and two equal submodules $p$ and $q$ of an $R$-module $M$, the linear equivalence $\text{ofEq}\, p\, q\, h$ is the canonical linear isomorphism between $p$ and $q$ induced by their equality $h : p = q$. This equivalence maps each element $x \in p$ to the corresponding element in $q$ (which is the same as $x$ since $p = q$), and preserves both the additive and scalar multiplicative structures. The inverse of this equivalence is simply the same map in the opposite direction.

LinearEquiv.coe_ofEq_apply theorem

(h : p = q) (x : p) : (ofEq p q h x : M) = x

Full source

@[simp]
theorem coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : M) = x :=
  rfl

Image under Linear Equivalence of Equal Submodules is Identity

Informal description

For any submodules $p$ and $q$ of an $R$-module $M$ with $h : p = q$, and for any element $x \in p$, the image of $x$ under the linear equivalence $\text{ofEq}\, p\, q\, h$ is equal to $x$ when viewed as an element of $M$.

LinearEquiv.ofEq_symm theorem

(h : p = q) : (ofEq p q h).symm = ofEq q p h.symm

Full source

@[simp]
theorem ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm :=
  rfl

Inverse of Linear Equivalence Between Equal Submodules

Informal description

Given a semiring $R$ and two equal submodules $p$ and $q$ of an $R$-module $M$, the inverse of the linear equivalence $\text{ofEq}\, p\, q\, h$ (induced by the equality $h : p = q$) is equal to the linear equivalence $\text{ofEq}\, q\, p\, h^{-1}$ (induced by the symmetric equality $h^{-1} : q = p$).

LinearEquiv.ofEq_rfl theorem

: ofEq p p rfl = LinearEquiv.refl R p

Full source

@[simp]
theorem ofEq_rfl : ofEq p p rfl = LinearEquiv.refl R p := by ext; rfl

Linear Equivalence of Reflexive Equality is Identity

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the linear equivalence $\text{ofEq}\, p\, p\, \text{rfl}$ induced by the reflexivity proof $\text{rfl} : p = p$ is equal to the identity linear equivalence $\text{refl}\, R\, p$ on $p$.

LinearEquiv.ofSubmodules definition

 (p : Submodule R M) (q : Submodule R₂ M₂) (h : p.map (e : M →ₛₗ[σ₁₂] M₂) = q) : p ≃ₛₗ[σ₁₂] q

Full source

/-- A linear equivalence which maps a submodule of one module onto another, restricts to a linear
equivalence of the two submodules. -/
def ofSubmodules (p : Submodule R M) (q : Submodule R₂ M₂) (h : p.map (e : M →ₛₗ[σ₁₂] M₂) = q) :
    p ≃ₛₗ[σ₁₂] q :=
  (e.submoduleMap p).trans (LinearEquiv.ofEq _ _ h)

Linear equivalence between submodules with matching image

Informal description

Given a linear equivalence $e \colon M \simeq_{\sigma_{12}} M₂$ between modules over semirings $R$ and $R₂$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$), and submodules $p \subseteq M$ and $q \subseteq M₂$ such that the image of $p$ under $e$ equals $q$, the linear equivalence restricts to a linear equivalence between $p$ and $q$. More precisely, if $h \colon e(p) = q$ is a proof that the image of $p$ under $e$ equals $q$, then $\text{ofSubmodules}\, e\, p\, q\, h$ is the induced linear equivalence $p \simeq_{\sigma_{12}} q$.

LinearEquiv.ofSubmodules_apply theorem

{p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q) (x : p) : ↑(e.ofSubmodules p q h x) = e x

Full source

@[simp]
theorem ofSubmodules_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q) (x : p) :
    ↑(e.ofSubmodules p q h x) = e x :=
  rfl

Image under Induced Submodule Equivalence Matches Original Map

Informal description

Let $e \colon M \simeq_{\sigma_{12}} M₂$ be a linear equivalence between modules $M$ and $M₂$ over semirings $R$ and $R₂$ respectively, with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$. Let $p \subseteq M$ and $q \subseteq M₂$ be submodules such that the image of $p$ under $e$ equals $q$, i.e., $e(p) = q$. Then for any $x \in p$, the image of $x$ under the induced linear equivalence $e.ofSubmodules\, p\, q\, h \colon p \simeq_{\sigma_{12}} q$ is equal to $e(x)$ when viewed as an element of $M₂$.

LinearEquiv.ofSubmodules_symm_apply theorem

 {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q) (x : q) : ↑((e.ofSubmodules p q h).symm x) = e.symm x

Full source

@[simp]
theorem ofSubmodules_symm_apply {p : Submodule R M} {q : Submodule R₂ M₂} (h : p.map ↑e = q)
    (x : q) : ↑((e.ofSubmodules p q h).symm x) = e.symm x :=
  rfl

Inverse of Restricted Linear Equivalence Commutes with Global Inverse

Informal description

Let $e \colon M \simeq_{\sigma_{12}} M₂$ be a linear equivalence between modules over semirings $R$ and $R₂$ with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$. Let $p \subseteq M$ and $q \subseteq M₂$ be submodules such that the image of $p$ under $e$ equals $q$ (i.e., $e(p) = q$). Then for any $x \in q$, the underlying element of $M$ corresponding to the inverse equivalence $(e|_{p,q})^{-1}(x)$ is equal to $e^{-1}(x)$. In other words, the following diagram commutes: \[ \begin{CD} p @>{e|_{p,q}}>> q \\ @V{\text{incl}}VV @VV{\text{incl}}V \\ M @>{e}>> M₂ \end{CD} \] where the vertical maps are the inclusion maps, and the inverse satisfies $\text{incl} \circ (e|_{p,q})^{-1} = e^{-1} \circ \text{incl}$ on $q$.

LinearEquiv.ofSubmodule' definition

 [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) : U.comap (f : M →ₛₗ[σ₁₂] M₂) ≃ₛₗ[σ₁₂] U

Full source

/-- A linear equivalence of two modules restricts to a linear equivalence from the preimage of any
submodule to that submodule.

This is `LinearEquiv.ofSubmodule` but with `comap` on the left instead of `map` on the right. -/
def ofSubmodule' [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
    U.comap (f : M →ₛₗ[σ₁₂] M₂) ≃ₛₗ[σ₁₂] U :=
  (f.symm.ofSubmodules _ _ f.symm.map_eq_comap).symm

Linear equivalence between submodule preimage and submodule

Informal description

Given a linear equivalence $f \colon M \simeq_{\sigma_{12}} M₂$ between modules over semirings $R$ and $R₂$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$), and a submodule $U \subseteq M₂$, the linear equivalence restricts to a linear equivalence between the preimage of $U$ under $f$ and $U$ itself. More precisely, $\text{ofSubmodule'}\, f\, U$ is the induced linear equivalence $f^{-1}(U) \simeq_{\sigma_{12}} U$, where $f^{-1}(U) = \{x \in M \mid f(x) \in U\}$ is the preimage submodule.

LinearEquiv.ofSubmodule'_toLinearMap theorem

 [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
  (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop

Full source

theorem ofSubmodule'_toLinearMap [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂)
    (U : Submodule R₂ M₂) :
    (f.ofSubmodule' U).toLinearMap = (f.toLinearMap.domRestrict _).codRestrict _ Subtype.prop := by
  ext
  rfl

Underlying Linear Map of Submodule Equivalence as Restricted Map

Informal description

Given a linear equivalence $f \colon M \simeq_{\sigma_{12}} M₂$ between modules over semirings $R$ and $R₂$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$), and a submodule $U \subseteq M₂$, the underlying linear map of the induced equivalence $f^{-1}(U) \simeq_{\sigma_{12}} U$ is equal to the codomain restriction to $U$ of the domain restriction of $f$ to $f^{-1}(U)$. More precisely, for any $x \in f^{-1}(U)$, the linear map sends $x$ to $\langle f(x), \text{Subtype.prop}(x) \rangle \in U$, where $\text{Subtype.prop}(x)$ is the proof that $f(x) \in U$.

LinearEquiv.ofSubmodule'_apply theorem

 [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : U.comap (f : M →ₛₗ[σ₁₂] M₂)) :
  (f.ofSubmodule' U x : M₂) = f (x : M)

Full source

@[simp]
theorem ofSubmodule'_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂)
    (x : U.comap (f : M →ₛₗ[σ₁₂] M₂)) : (f.ofSubmodule' U x : M₂) = f (x : M) :=
  rfl

Image under restricted linear equivalence equals original image

Informal description

Let $R$ and $R_2$ be semirings, $M$ an $R$-module, $M_2$ an $R_2$-module, and $\sigma_{12} \colon R \to R_2$ a ring homomorphism. Given a linear equivalence $f \colon M \simeq_{\sigma_{12}} M_2$ and a submodule $U \subseteq M_2$, for any element $x$ in the preimage submodule $f^{-1}(U) \subseteq M$, the image of $x$ under the induced linear equivalence $f|_{f^{-1}(U)} \colon f^{-1}(U) \simeq_{\sigma_{12}} U$ equals $f(x)$ as an element of $M_2$.

LinearEquiv.ofSubmodule'_symm_apply theorem

 [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : U) :
  ((f.ofSubmodule' U).symm x : M) = f.symm (x : M₂)

Full source

@[simp]
theorem ofSubmodule'_symm_apply [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂)
    (U : Submodule R₂ M₂) (x : U) : ((f.ofSubmodule' U).symm x : M) = f.symm (x : M₂) :=
  rfl

Inverse Image Formula for Linear Equivalence of Submodules

Informal description

Given a linear equivalence $f \colon M \simeq_{\sigma_{12}} M_2$ between modules over semirings $R$ and $R_2$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R_2$), and a submodule $U \subseteq M_2$, the inverse of the induced linear equivalence $f.\text{ofSubmodule'}\, U$ satisfies the following: for any $x \in U$, the image under the inverse equivalence is equal to the inverse image of $x$ under $f$, i.e., $$(f.\text{ofSubmodule'}\, U)^{-1}(x) = f^{-1}(x).$$

LinearEquiv.ofTop definition

(h : p = ⊤) : p ≃ₗ[R] M

Full source

/-- The top submodule of `M` is linearly equivalent to `M`. -/
def ofTop (h : p = ⊤) : p ≃ₗ[R] M :=
  { p.subtype with
    invFun := fun x => ⟨x, h.symm ▸ trivial⟩
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }

Linear equivalence between a submodule and the ambient module when the submodule is the whole space

Informal description

Given a submodule $p$ of a module $M$ over a semiring $R$, if $p$ is equal to the top submodule (i.e., $p = M$), then there exists a linear equivalence between $p$ and $M$. More precisely, the linear equivalence is constructed as follows: - The forward map is the canonical inclusion $p \hookrightarrow M$ (given by the submodule subtype). - The inverse map sends any $x \in M$ to $\langle x, \text{trivial}\rangle \in p$, where the trivial proof comes from the assumption $p = M$. - Both compositions are identity maps.

LinearEquiv.ofTop_apply theorem

{h} (x : p) : ofTop p h x = x

Full source

@[simp]
theorem ofTop_apply {h} (x : p) : ofTop p h x = x :=
  rfl

Identity Mapping in Linear Equivalence Between Submodule and Ambient Module

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, if $p$ is equal to the entire module $M$ (i.e., $p = M$), then the linear equivalence `ofTop p h` maps any element $x \in p$ to itself in $M$.

LinearEquiv.coe_ofTop_symm_apply theorem

{h} (x : M) : ((ofTop p h).symm x : M) = x

Full source

@[simp]
theorem coe_ofTop_symm_apply {h} (x : M) : ((ofTop p h).symm x : M) = x :=
  rfl

Inverse of Top Submodule Linear Equivalence Acts as Identity on $M$

Informal description

For any module $M$ over a semiring $R$ and submodule $p$ of $M$ such that $p = M$, the application of the inverse linear equivalence $(p \simeq_{\sigma} M)^{-1}$ to an element $x \in M$ yields $x$ when viewed as an element of $M$. More precisely, if $e : p \simeq_{\sigma} M$ is the linear equivalence given by $p = M$, then for any $x \in M$, we have $e^{-1}(x) = x$ (where the equality holds in $M$ after applying the coercion from $p$ to $M$).

LinearEquiv.ofTop_symm_apply theorem

{h} (x : M) : (ofTop p h).symm x = ⟨x, h.symm ▸ trivial⟩

Full source

theorem ofTop_symm_apply {h} (x : M) : (ofTop p h).symm x = ⟨x, h.symm ▸ trivial⟩ :=
  rfl

Inverse of the Linear Equivalence Between a Submodule and the Ambient Module

Informal description

Let $M$ be a module over a semiring $R$, and let $p$ be a submodule of $M$ such that $p = M$ (i.e., $p$ is the entire module). For any element $x \in M$, the inverse of the linear equivalence $\text{ofTop}~p~h$ maps $x$ to the pair $\langle x, \text{trivial}\rangle \in p$, where the second component is trivial due to the assumption $p = M$.

LinearEquiv.range theorem

: LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤

Full source

@[simp]
protected theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤ :=
  LinearMap.range_eq_top.2 e.toEquiv.surjective

Range of a Linear Equivalence is the Entire Codomain

Informal description

For any linear equivalence (semilinear isomorphism) $e \colon M \to_{\sigma_{12}} M_2$ between modules $M$ and $M_2$ over semirings $R$ and $R_2$ respectively, with respect to a ring homomorphism $\sigma_{12} \colon R \to R_2$, the range of $e$ is equal to the entire module $M_2$. That is, \[ \text{range}(e) = M_2. \]

LinearEquivClass.range theorem

 [Module R M] [Module R₂ M₂] {F : Type*} [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂] (e : F) :
  LinearMap.range e = ⊤

Full source

@[simp]
protected theorem _root_.LinearEquivClass.range [Module R M] [Module R₂ M₂] {F : Type*}
    [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂] (e : F) : LinearMap.range e = ⊤ :=
  LinearMap.range_eq_top.2 (EquivLike.surjective e)

Range of a Semilinear Equivalence is the Entire Codomain

Informal description

For any semilinear equivalence $e \colon M \to M₂$ between modules $M$ over a semiring $R$ and $M₂$ over a semiring $R₂$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$), the range of $e$ is equal to the entire module $M₂$. That is, \[ \text{range}(e) = M₂. \]

LinearEquiv.range_comp theorem

 [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] :
  LinearMap.range (h.comp (e : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = LinearMap.range h

Full source

@[simp]
theorem range_comp [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] :
    LinearMap.range (h.comp (e : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = LinearMap.range h :=
  LinearMap.range_comp_of_range_eq_top _ e.range

Range of Composition with Linear Equivalence Equals Range of Second Map

Informal description

Let $R$, $S$, and $T$ be semirings with surjective ring homomorphisms $\sigma_{12} \colon R \to S$, $\sigma_{23} \colon S \to T$, and $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Given a linear equivalence $e \colon M \to_{\sigma_{12}} M_2$ and a semilinear map $h \colon M_2 \to_{\sigma_{23}} M_3$, the range of their composition equals the range of $h$, i.e., \[ \mathrm{range}(h \circ e) = \mathrm{range}(h). \]

LinearEquiv.ofLeftInverse definition

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂ → M} (h : Function.LeftInverse g f) :
  M ≃ₛₗ[σ₁₂] (LinearMap.range f)

Full source

/-- A linear map `f : M →ₗ[R] M₂` with a left-inverse `g : M₂ →ₗ[R] M` defines a linear
equivalence between `M` and `f.range`.

This is a computable alternative to `LinearEquiv.ofInjective`, and a bidirectional version of
`LinearMap.rangeRestrict`. -/
def ofLeftInverse [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂ → M}
    (h : Function.LeftInverse g f) : M ≃ₛₗ[σ₁₂] (LinearMap.range f) :=
  { LinearMap.rangeRestrict f with
    toFun := LinearMap.rangeRestrict f
    invFun := g ∘ (LinearMap.range f).subtype
    left_inv := h
    right_inv := fun x =>
      Subtype.ext <|
        let ⟨x', hx'⟩ := LinearMap.mem_range.mp x.prop
        show f (g x) = x by rw [← hx', h x'] }

Linear equivalence between a module and the range of a map with left inverse

Informal description

Given a semilinear map $f \colon M \to M₂$ between modules over semirings $R$ and $R₂$ (with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$), and a left inverse $g \colon M₂ \to M$ of $f$ (i.e., $g \circ f = \text{id}_M$), the linear equivalence $\text{ofLeftInverse}\ h$ establishes an isomorphism between $M$ and the range of $f$ as an $R₂$-submodule of $M₂$. More precisely, this equivalence: 1. Maps $x \in M$ to $f(x) \in \text{range}(f)$ via the range restriction of $f$ 2. Has inverse map given by composing $g$ with the submodule inclusion $\text{range}(f) \hookrightarrow M₂$ This provides a computable alternative to constructing a linear equivalence from an injective linear map, while also giving a bidirectional version of range restriction.

LinearEquiv.ofLeftInverse_apply theorem

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f) (x : M) : ↑(ofLeftInverse h x) = f x

Full source

@[simp]
theorem ofLeftInverse_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
    (h : Function.LeftInverse g f) (x : M) : ↑(ofLeftInverse h x) = f x :=
  rfl

Application of Linear Equivalence from Left Inverse Maps to Range

Informal description

Given a semilinear map $f \colon M \to M₂$ between modules over semirings $R$ and $R₂$ with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$, and a left inverse $g \colon M₂ \to M$ of $f$ (i.e., $g \circ f = \text{id}_M$), the application of the linear equivalence $\text{ofLeftInverse}\ h$ to an element $x \in M$ satisfies $\text{ofLeftInverse}\ h\ x = f(x)$, where the equality holds in the range submodule of $f$.

LinearEquiv.ofLeftInverse_symm_apply theorem

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f) (x : LinearMap.range f) :
  (ofLeftInverse h).symm x = g x

Full source

@[simp]
theorem ofLeftInverse_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
    (h : Function.LeftInverse g f) (x : LinearMap.range f) : (ofLeftInverse h).symm x = g x :=
  rfl

Inverse of Linear Equivalence from Left Inverse Evaluates as Left Inverse

Informal description

Let $R$ and $R_2$ be semirings with compatible ring homomorphisms $\sigma_{12} \colon R \to R_2$ and $\sigma_{21} \colon R_2 \to R$. Let $M$ be an $R$-module and $M_2$ an $R_2$-module. Given a semilinear map $f \colon M \to M_2$ with respect to $\sigma_{12}$, and a left inverse $g \colon M_2 \to M$ of $f$ (i.e., $g \circ f = \text{id}_M$), then for any $x$ in the range submodule $\text{range}(f) \subseteq M_2$, the inverse of the linear equivalence $\text{ofLeftInverse}\ h$ satisfies $(\text{ofLeftInverse}\ h)^{-1}(x) = g(x)$.

LinearEquiv.ofInjective definition

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Injective f) : M ≃ₛₗ[σ₁₂] LinearMap.range f

Full source

/-- An `Injective` linear map `f : M →ₗ[R] M₂` defines a linear equivalence
between `M` and `f.range`. See also `LinearMap.ofLeftInverse`. -/
noncomputable def ofInjective [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Injective f) :
    M ≃ₛₗ[σ₁₂] LinearMap.range f :=
  ofLeftInverse <| Classical.choose_spec h.hasLeftInverse

Linear equivalence between a module and the range of an injective linear map

Informal description

Given an injective semilinear map $ f : M \to M₂ $ between modules over semirings $ R $ and $ R₂ $ (with respect to ring homomorphisms $ \sigma_{12} : R \to R₂ $ and $ \sigma_{21} : R₂ \to R $ forming inverse pairs), the linear equivalence $ \text{ofInjective}\ f\ h $ establishes an isomorphism between $ M $ and the range of $ f $ as an $ R₂ $-submodule of $ M₂ $. More precisely, this equivalence: 1. Maps $ x \in M $ to $ f(x) \in \text{range}(f) $ 2. Has an inverse map that recovers $ x $ from $ f(x) $ using the injectivity of $ f $ This provides a canonical way to view an injective linear map as an isomorphism onto its range.

LinearEquiv.ofInjective_apply theorem

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f} (x : M) : ↑(ofInjective f h x) = f x

Full source

@[simp]
theorem ofInjective_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f}
    (x : M) : ↑(ofInjective f h x) = f x :=
  rfl

Image under injective linear equivalence equals original map value

Informal description

Let $R$ and $R_2$ be semirings with compatible ring homomorphisms $\sigma_{12} \colon R \to R_2$ and $\sigma_{21} \colon R_2 \to R$. Let $M$ be an $R$-module and $M_2$ an $R_2$-module. Given an injective semilinear map $f \colon M \to M_2$ with respect to $\sigma_{12}$, then for any $x \in M$, the image of $x$ under the linear equivalence $\text{ofInjective}\ f\ h$ equals $f(x)$ when viewed as an element of $M_2$.

LinearEquiv.ofInjective_symm_apply theorem

 [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f} (x : LinearMap.range f) :
  f ((ofInjective f h).symm x) = x

Full source

@[simp]
lemma ofInjective_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Injective f}
    (x : LinearMap.range f) :
    f ((ofInjective f h).symm x) = x := by
  obtain ⟨-, ⟨y, rfl⟩⟩ := x
  have : ⟨f y, LinearMap.mem_range_self f y⟩ = LinearEquiv.ofInjective f h y := rfl
  simp [this]

Inverse of injective linear equivalence preserves application: $f(e^{-1}(x)) = x$ for $x \in \text{range}(f)$

Informal description

Let $R$ and $R_2$ be semirings with ring homomorphisms $\sigma_{12} : R \to R_2$ and $\sigma_{21} : R_2 \to R$ forming inverse pairs. Let $f : M \to M_2$ be an injective $\sigma_{12}$-semilinear map between $R$-module $M$ and $R_2$-module $M_2$. For any element $x$ in the range submodule $\text{range}(f) \subseteq M_2$, we have $f(e^{-1}(x)) = x$, where $e^{-1}$ is the inverse of the linear equivalence $e : M \simeq_{\sigma_{12}} \text{range}(f)$ induced by $f$.

LinearEquiv.ofBijective definition

[RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : Bijective f) : M ≃ₛₗ[σ₁₂] M₂

Full source

/-- A bijective linear map is a linear equivalence. -/
noncomputable def ofBijective [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : Bijective f) :
    M ≃ₛₗ[σ₁₂] M₂ :=
  (ofInjective f hf.injective).trans <| ofTop _ <|
    LinearMap.range_eq_top.2 hf.surjective

Linear isomorphism from a bijective semilinear map

Informal description

Given a bijective semilinear map $ f : M \to M₂ $ between modules over semirings $ R $ and $ R₂ $ (with respect to ring homomorphisms $ \sigma_{12} : R \to R₂ $ and $ \sigma_{21} : R₂ \to R $ forming inverse pairs), the linear equivalence $ \text{ofBijective}\ f\ hf $ establishes an isomorphism between $ M $ and $ M₂ $. More precisely: 1. The forward map sends $ x \in M $ to $ f(x) \in M₂ $ 2. The inverse map is constructed using the bijectivity of $ f $ 3. The composition of these maps yields the identity in both directions This provides a canonical way to view a bijective linear map as a linear isomorphism between the modules.

LinearEquiv.ofBijective_apply theorem

[RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf} (x : M) : ofBijective f hf x = f x

Full source

@[simp]
theorem ofBijective_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf} (x : M) :
    ofBijective f hf x = f x :=
  rfl

Application of bijective semilinear map equals its linear equivalence

Informal description

Let $R$ and $R_2$ be semirings with ring homomorphisms $\sigma_{12} \colon R \to R_2$ and $\sigma_{21} \colon R_2 \to R$ forming inverse pairs. Let $f \colon M \to M_2$ be a bijective $\sigma_{12}$-semilinear map between an $R$-module $M$ and an $R_2$-module $M_2$. Then for any $x \in M$, the linear equivalence $\text{ofBijective}\ f\ \text{hf}$ satisfies $(\text{ofBijective}\ f\ \text{hf})(x) = f(x)$.

LinearEquiv.ofBijective_symm_apply_apply theorem

[RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h} (x : M) : (ofBijective f h).symm (f x) = x

Full source

@[simp]
theorem ofBijective_symm_apply_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h} (x : M) :
    (ofBijective f h).symm (f x) = x := by
  simp [LinearEquiv.symm_apply_eq]

Inverse of Bijective Semilinear Equivalence Acts as Left Inverse

Informal description

Let $R$ and $R_2$ be semirings with ring homomorphisms $\sigma_{12}: R \to R_2$ and $\sigma_{21}: R_2 \to R$ forming inverse pairs. Given a bijective semilinear map $f: M \to M_2$ between modules $M$ and $M_2$ over $R$ and $R_2$ respectively, and letting $h$ be the proof of bijectivity, then for any $x \in M$, the inverse of the linear equivalence $\text{ofBijective}(f, h)$ satisfies $(\text{ofBijective}(f, h))^{-1}(f(x)) = x$.

LinearEquiv.apply_ofBijective_symm_apply theorem

[RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h} (x : M₂) : f ((ofBijective f h).symm x) = x

Full source

@[simp]
theorem apply_ofBijective_symm_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h}
    (x : M₂) : f ((ofBijective f h).symm x) = x := by
  rw [← ofBijective_apply f ((ofBijective f h).symm x), apply_symm_apply]

Bijective semilinear map acts as right inverse through its linear equivalence

Informal description

Let $R$ and $R_2$ be semirings with ring homomorphisms $\sigma_{12}: R \to R_2$ and $\sigma_{21}: R_2 \to R$ forming inverse pairs. Given a bijective semilinear map $f: M \to M_2$ between modules $M$ and $M_2$ over $R$ and $R_2$ respectively, and letting $h$ be the proof of bijectivity, then for any $x \in M_2$, we have $f(f^{-1}(x)) = x$, where $f^{-1}$ is the inverse of the linear equivalence $\text{ofBijective}(f, h)$.

Submodule.equivSubtypeMap definition

(p : Submodule R M) (q : Submodule R p) : q ≃ₗ[R] q.map p.subtype

Full source

/-- Given `p` a submodule of the module `M` and `q` a submodule of `p`, `p.equivSubtypeMap q`
is the natural `LinearEquiv` between `q` and `q.map p.subtype`. -/
def equivSubtypeMap (p : Submodule R M) (q : Submodule R p) : q ≃ₗ[R] q.map p.subtype :=
  { (p.subtype.domRestrict q).codRestrict _ (by rintro ⟨x, hx⟩; exact ⟨x, hx, rfl⟩) with
    invFun := by
      rintro ⟨x, hx⟩
      refine ⟨⟨x, ?_⟩, ?_⟩ <;> rcases hx with ⟨⟨_, h⟩, _, rfl⟩ <;> assumption
    left_inv := fun ⟨⟨_, _⟩, _⟩ => rfl
    right_inv := fun ⟨x, ⟨_, h⟩, _, rfl⟩ => by ext; rfl }

Natural linear equivalence between a submodule and its inclusion image

Informal description

Given a submodule $p$ of a module $M$ over a semiring $R$ and a submodule $q$ of $p$, the linear equivalence $\text{equivSubtypeMap}$ between $q$ and the image of $q$ under the inclusion map $p \hookrightarrow M$ is defined as follows: 1. The forward map sends an element $\langle x, h_x \rangle \in q$ (where $x \in p$ and $h_x$ is a proof that $x \in q$) to $\langle x, h_x, \text{rfl} \rangle \in q.\text{map}(p.\text{subtype})$, where $\text{rfl}$ is the proof that $x = x$ under the inclusion. 2. The inverse map sends an element $\langle x, \langle \langle y, h_y \rangle, h, \text{rfl} \rangle \rangle \in q.\text{map}(p.\text{subtype})$ back to $\langle \langle y, h_y \rangle, h \rangle \in q$. This equivalence establishes a natural isomorphism between the submodule $q$ and its image under the inclusion map into $M$.

Submodule.equivSubtypeMap_apply theorem

{p : Submodule R M} {q : Submodule R p} (x : q) : (p.equivSubtypeMap q x : M) = p.subtype.domRestrict q x

Full source

@[simp]
theorem equivSubtypeMap_apply {p : Submodule R M} {q : Submodule R p} (x : q) :
    (p.equivSubtypeMap q x : M) = p.subtype.domRestrict q x :=
  rfl

Image of Submodule Element under Natural Equivalence Equals Restricted Inclusion

Informal description

Let $M$ be a module over a semiring $R$, $p$ a submodule of $M$, and $q$ a submodule of $p$. For any element $x \in q$, the image of $x$ under the linear equivalence $\text{equivSubtypeMap}$ from $q$ to $q.\text{map}(p.\text{subtype})$ (when viewed in $M$) equals the restriction of the inclusion map $p \hookrightarrow M$ to $q$ applied to $x$. In symbols: $(p.\text{equivSubtypeMap} q)(x) = (p.\text{subtype} \restriction q)(x)$ as elements of $M$.

Submodule.equivSubtypeMap_symm_apply theorem

{p : Submodule R M} {q : Submodule R p} (x : q.map p.subtype) : ((p.equivSubtypeMap q).symm x : M) = x

Full source

@[simp]
theorem equivSubtypeMap_symm_apply {p : Submodule R M} {q : Submodule R p} (x : q.map p.subtype) :
    ((p.equivSubtypeMap q).symm x : M) = x := by
  cases x
  rfl

Inverse of Submodule Equivalence Acts as Identity on Inclusion Image

Informal description

Let $M$ be a module over a semiring $R$, $p$ a submodule of $M$, and $q$ a submodule of $p$. For any element $x$ in the image of $q$ under the inclusion map $p \hookrightarrow M$, the evaluation of the inverse of the linear equivalence $\text{equivSubtypeMap}$ at $x$ (when viewed as an element of $M$) equals $x$ itself. In other words, if $e : q \simeq_{\text{id}} q.\text{map}(p.\text{subtype})$ is the natural linear equivalence, then for any $x \in q.\text{map}(p.\text{subtype})$, we have $e^{-1}(x) = x$ as elements of $M$.

Submodule.comap_equiv_self_of_inj_of_le definition

{f : M →ₗ[R] N} {p : Submodule R N} (hf : Injective f) (h : p ≤ LinearMap.range f) : p.comap f ≃ₗ[R] p

Full source

/-- A linear injection `M ↪ N` restricts to an equivalence `f⁻¹ p ≃ p` for any submodule `p`
contained in its range. -/
@[simps! apply]
noncomputable def comap_equiv_self_of_inj_of_le {f : M →ₗ[R] N} {p : Submodule R N}
    (hf : Injective f) (h : p ≤ LinearMap.range f) :
    p.comap f ≃ₗ[R] p :=
  LinearEquiv.ofBijective
  ((f ∘ₗ (p.comap f).subtype).codRestrict p <| fun ⟨_, hx⟩ ↦ mem_comap.mp hx)
  (⟨fun x y hxy ↦ by simpa using hf (Subtype.ext_iff.mp hxy),
    fun ⟨x, hx⟩ ↦ by obtain ⟨y, rfl⟩ := h hx; exact ⟨⟨y, hx⟩, by simp [Subtype.ext_iff]⟩⟩)

Linear equivalence between pullback and submodule for injective maps

Informal description

Given an injective linear map $ f : M \to N $ between modules over a semiring $ R $ and a submodule $ p \subseteq N $ contained in the range of $ f $, there exists a linear equivalence between the pullback submodule $ f^{-1}(p) $ and $ p $ itself. More precisely: 1. The forward map sends $ x \in f^{-1}(p) $ to $ f(x) \in p $ 2. The inverse map is constructed using the injectivity of $ f $ and the condition $ p \subseteq \text{range}(f) $ 3. The composition of these maps yields the identity in both directions This establishes that $ f $ restricts to an isomorphism between $ f^{-1}(p) $ and $ p $.

LinearMap.codRestrictOfInjective definition

: M₁ →ₗ[R] M₃

Full source

/-- The restriction of a linear map on the target to a submodule of the target given by
an inclusion. -/
noncomputable def codRestrictOfInjective : M₁ →ₗ[R] M₃ :=
  (LinearEquiv.ofInjective i hi).symm ∘ₗ f.codRestrict (LinearMap.range i) hf

Linear map factorization through an injective map

Informal description

Given an injective linear map $ i : M_2 \to M_3 $ between modules over a semiring $ R $, and a linear map $ f : M_1 \to M_3 $ such that the image of $ f $ is contained in the range of $ i $, the function constructs a linear map from $ M_1 $ to $ M_2 $ by first restricting the codomain of $ f $ to the range of $ i $ and then applying the inverse of the linear equivalence between $ M_2 $ and the range of $ i $. More precisely, the map is defined as the composition: \[ \text{codRestrictOfInjective}\ f\ i\ hi\ hf = e^{-1} \circ (\text{codRestrict}\ f\ (\text{range}\ i)\ hf) \] where $ e : M_2 \simeq \text{range}\ i $ is the linear equivalence induced by the injectivity of $ i $, and $ hf $ is the proof that $ \text{range}\ f \subseteq \text{range}\ i $.

LinearMap.codRestrictOfInjective_comp_apply theorem

(x : M₁) : i (LinearMap.codRestrictOfInjective f i hi hf x) = f x

Full source

@[simp]
lemma codRestrictOfInjective_comp_apply (x : M₁) :
    i (LinearMap.codRestrictOfInjective f i hi hf x) = f x := by
  simp [LinearMap.codRestrictOfInjective]

Commutativity of codomain restriction through an injective linear map: $i \circ g = f$

Informal description

Let $R$ be a semiring, and let $M_1$, $M_2$, $M_3$ be modules over $R$. Given an injective linear map $i \colon M_2 \to M_3$ and a linear map $f \colon M_1 \to M_3$ such that the range of $f$ is contained in the range of $i$, then for any $x \in M_1$, we have $i(g(x)) = f(x)$, where $g \colon M_1 \to M_2$ is the linear map obtained by restricting the codomain of $f$ through $i$.

LinearMap.codRestrictOfInjective_comp theorem

: i ∘ₗ LinearMap.codRestrictOfInjective f i hi hf = f

Full source

@[simp]
lemma codRestrictOfInjective_comp :
    i ∘ₗ LinearMap.codRestrictOfInjective f i hi hf = f := by
  ext
  simp

Composition of injective linear map with codomain restriction equals original map

Informal description

Let $R$ be a semiring, and let $M_1$, $M_2$, $M_3$ be modules over $R$. Given an injective linear map $i \colon M_2 \to M_3$ and a linear map $f \colon M_1 \to M_3$ such that the range of $f$ is contained in the range of $i$, the composition of $i$ with the codomain-restricted map $g \colon M_1 \to M_2$ equals $f$, i.e., $i \circ g = f$.

LinearMap.codRestrict₂ definition

: M₁ →ₗ[R] M₂ →ₗ[R] M₃

Full source

/-- The restriction of a bilinear map to a submodule in which it takes values. -/
noncomputable def codRestrict₂ :
    M₁ →ₗ[R] M₂ →ₗ[R] M₃ :=
  let e : LinearMap.rangeLinearMap.range i ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
  { toFun := fun x ↦ e.comp <| (f x).codRestrict (p := LinearMap.range i) (hf x)
    map_add' := by intro x₁ x₂; ext y; simp [f.map_add, ← e.map_add, codRestrict]
    map_smul' := by intro t x; ext y; simp [f.map_smul, ← e.map_smul, codRestrict] }

Restriction of a bilinear map to a submodule in its codomain

Informal description

Given a bilinear map $f : M_1 \times M_2 \to M_3$ between modules over a semiring $R$, and a submodule $i : M_3' \hookrightarrow M_3$ such that $f(x, y) \in \text{range}(i)$ for all $x \in M_1$ and $y \in M_2$, the function restricts $f$ to a bilinear map from $M_1 \times M_2$ to $M_3'$. More precisely, the restricted bilinear map $\text{codRestrict}_2\ f\ i\ hi\ hf$ satisfies: 1. For all $x \in M_1$ and $y \in M_2$, the value $(\text{codRestrict}_2\ f\ i\ hi\ hf)(x, y)$ is the unique element of $M_3'$ that maps to $f(x, y)$ under $i$. 2. The restriction preserves bilinearity: it is linear in each argument separately.

LinearMap.codRestrict₂_apply theorem

(x : M₁) (y : M₂) : i (codRestrict₂ f i hi hf x y) = f x y

Full source

@[simp]
lemma codRestrict₂_apply (x : M₁) (y : M₂) :
    i (codRestrict₂ f i hi hf x y) = f x y := by
  simp [codRestrict₂]

Codomain restriction of bilinear map preserves evaluation: $i(f'(x,y)) = f(x,y)$

Informal description

Let $R$ be a semiring, and let $M_1$, $M_2$, $M_3$ be modules over $R$. Given a bilinear map $f : M_1 \times M_2 \to M_3$, a submodule inclusion $i : M_3' \hookrightarrow M_3$ with $i$ injective, and proofs $hi$ that $i$ is injective and $hf$ that $f(x,y) \in \text{range}(i)$ for all $x \in M_1$ and $y \in M_2$, then for any $x \in M_1$ and $y \in M_2$, we have $i\big((\text{codRestrict}_2\ f\ i\ hi\ hf)(x, y)\big) = f(x, y)$.