Mathlib.Algebra.Module.Equiv.Basic

LinearEquiv.restrictScalars definition

(f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂

Full source

/-- If `M` and `M₂` are both `R`-semimodules and `S`-semimodules and `R`-semimodule structures
are defined by an action of `R` on `S` (formally, we have two scalar towers), then any `S`-linear
equivalence from `M` to `M₂` is also an `R`-linear equivalence.

See also `LinearMap.restrictScalars`. -/
@[simps]
def restrictScalars (f : M ≃ₗ[S] M₂) : M ≃ₗ[R] M₂ :=
  { f.toLinearMap.restrictScalars R with
    toFun := f
    invFun := f.symm
    left_inv := f.left_inv
    right_inv := f.right_inv }

Restriction of scalars for linear equivalences

Informal description

Given modules $M$ and $M₂$ over both a semiring $R$ and a semiring $S$, where the $R$-module structure is defined via an action of $R$ on $S$ (forming a scalar tower), any $S$-linear equivalence $f : M \simeq_{S} M₂$ can be restricted to an $R$-linear equivalence $M \simeq_{R} M₂$. This is constructed by restricting the scalar action of $f$ from $S$ to $R$ while preserving the underlying function and its inverse.

LinearEquiv.restrictScalars_injective theorem

: Function.Injective (restrictScalars R : (M ≃ₗ[S] M₂) → M ≃ₗ[R] M₂)

Full source

theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : (M ≃ₗ[S] M₂) → M ≃ₗ[R] M₂) := fun _ _ h ↦
  ext (LinearEquiv.congr_fun h :)

Injectivity of Scalar Restriction for Linear Equivalences

Informal description

The function that restricts scalars from $S$ to $R$ for linear equivalences between modules $M$ and $M₂$ is injective. That is, if two $S$-linear equivalences $f, g \colon M \simeq_S M₂$ have the same restriction to $R$-linear equivalences, then $f = g$.

LinearEquiv.restrictScalars_inj theorem

(f g : M ≃ₗ[S] M₂) : f.restrictScalars R = g.restrictScalars R ↔ f = g

Full source

@[simp]
theorem restrictScalars_inj (f g : M ≃ₗ[S] M₂) :
    f.restrictScalars R = g.restrictScalars R ↔ f = g :=
  (restrictScalars_injective R).eq_iff

Equality of Linear Equivalences Under Scalar Restriction

Informal description

For any two $S$-linear equivalences $f, g \colon M \simeq_S M₂$ between modules $M$ and $M₂$ over semirings $R$ and $S$ (where $R$ acts on $S$), the restrictions of $f$ and $g$ to $R$-linear equivalences are equal if and only if $f = g$ as $S$-linear equivalences. In other words, the restriction of scalars preserves equality of linear equivalences.

Module.End.isUnit_iff theorem

[Module R M] (f : Module.End R M) : IsUnit f ↔ Function.Bijective f

Full source

theorem _root_.Module.End.isUnit_iff [Module R M] (f : Module.End R M) :
    IsUnitIsUnit f ↔ Function.Bijective f :=
  ⟨fun h ↦
    Function.bijective_iff_has_inverse.mpr <|
      ⟨h.unit.inv,
        ⟨Module.End.isUnit_inv_apply_apply_of_isUnit h,
        Module.End.isUnit_apply_inv_apply_of_isUnit h⟩⟩,
    fun H ↦
    let e : M ≃ₗ[R] M := { f, Equiv.ofBijective f H with }
    ⟨⟨_, e.symm, LinearMap.ext e.right_inv, LinearMap.ext e.left_inv⟩, rfl⟩⟩

Characterization of invertible endomorphisms via bijectivity

Informal description

Let $M$ be a module over a ring $R$ and let $f$ be an $R$-linear endomorphism of $M$. Then $f$ is a unit in the endomorphism ring $\text{End}_R(M)$ if and only if $f$ is bijective as a function from $M$ to itself.

LinearEquiv.automorphismGroup instance

: Group (M ≃ₗ[R] M)

Full source

instance automorphismGroup : Group (M ≃ₗ[R] M) where
  mul f g := g.trans f
  one := LinearEquiv.refl R M
  inv f := f.symm
  mul_assoc _ _ _ := rfl
  mul_one _ := ext fun _ ↦ rfl
  one_mul _ := ext fun _ ↦ rfl
  inv_mul_cancel f := ext <| f.left_inv

Group Structure on Linear Automorphisms

Informal description

For any module $M$ over a ring $R$, the set of linear automorphisms $M \simeq_{R} M$ forms a group under composition of linear maps.

LinearEquiv.one_eq_refl theorem

: (1 : M ≃ₗ[R] M) = refl R M

Full source

lemma one_eq_refl : (1 : M ≃ₗ[R] M) = refl R M := rfl

Identity Element of Linear Automorphism Group is Reflexive Equivalence

Informal description

The identity element of the group of linear automorphisms of a module $M$ over a ring $R$ is equal to the reflexive linear equivalence on $M$, i.e., $1 = \text{refl}_R M$.

LinearEquiv.mul_eq_trans theorem

(f g : M ≃ₗ[R] M) : f * g = g.trans f

Full source

lemma mul_eq_trans (f g : M ≃ₗ[R] M) : f * g = g.trans f := rfl

Composition of Linear Automorphisms as Group Multiplication

Informal description

For any two linear automorphisms $f$ and $g$ of a module $M$ over a ring $R$, the group multiplication $f * g$ is equal to the composition of $g$ followed by $f$ (denoted as $g \circ f$ in standard mathematical notation).

LinearEquiv.coe_one theorem

: ↑(1 : M ≃ₗ[R] M) = id

Full source

@[simp]
lemma coe_one : ↑(1 : M ≃ₗ[R] M) = id := rfl

Identity Linear Automorphism Coerces to Identity Function

Informal description

The identity element of the group of linear automorphisms of a module $M$ over a ring $R$, when coerced to a function, is equal to the identity function $\text{id} \colon M \to M$.

LinearEquiv.coe_toLinearMap_one theorem

: (↑(1 : M ≃ₗ[R] M) : M →ₗ[R] M) = LinearMap.id

Full source

@[simp]
lemma coe_toLinearMap_one : (↑(1 : M ≃ₗ[R] M) : M →ₗ[R] M) = LinearMap.id := rfl

Identity Linear Equivalence Coerces to Identity Linear Map

Informal description

The coercion of the identity linear equivalence $1 : M \simeq_{R} M$ to a linear map is equal to the identity linear map $\text{id} : M \to_{R} M$.

LinearEquiv.coe_toLinearMap_mul theorem

{e₁ e₂ : M ≃ₗ[R] M} : (↑(e₁ * e₂) : M →ₗ[R] M) = (e₁ : M →ₗ[R] M) * (e₂ : M →ₗ[R] M)

Full source

@[simp]
lemma coe_toLinearMap_mul {e₁ e₂ : M ≃ₗ[R] M} :
    (↑(e₁ * e₂) : M →ₗ[R] M) = (e₁ : M →ₗ[R] M) * (e₂ : M →ₗ[R] M) :=
  rfl

Composition of Linear Automorphisms as Linear Maps

Informal description

For any two linear automorphisms $e₁, e₂$ of a module $M$ over a ring $R$, the underlying linear map of their composition $e₁ \circ e₂$ is equal to the composition of their underlying linear maps, i.e., $(e₁ \circ e₂) = e₁ \circ e₂$ as linear maps from $M$ to $M$.

LinearEquiv.coe_pow theorem

(e : M ≃ₗ[R] M) (n : ℕ) : ⇑(e ^ n) = e^[n]

Full source

theorem coe_pow (e : M ≃ₗ[R] M) (n : ℕ) : ⇑(e ^ n) = e^[n] := hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Iteration of Linear Automorphism Powers: $\operatorname{id}(e^n) = e^{[n]}$

Informal description

Let $M$ be a module over a ring $R$ and let $e \colon M \simeq_{R} M$ be a linear automorphism. For any natural number $n$, the $n$-th power of $e$ (under composition in the automorphism group) satisfies $\operatorname{id}(e^n) = e^{[n]}$, where $e^{[n]}$ denotes the $n$-th iterate of $e$ as a function.

LinearEquiv.pow_apply theorem

(e : M ≃ₗ[R] M) (n : ℕ) (m : M) : (e ^ n) m = e^[n] m

Full source

theorem pow_apply (e : M ≃ₗ[R] M) (n : ℕ) (m : M) : (e ^ n) m = e^[n] m := congr_fun (coe_pow e n) m

Iterated Application of Linear Automorphism Powers: $(e^n)(m) = e^{[n]}(m)$

Informal description

Let $M$ be a module over a ring $R$ and let $e \colon M \simeq_{R} M$ be a linear automorphism. For any natural number $n$ and any element $m \in M$, the application of the $n$-th power of $e$ to $m$ equals the $n$-th iterate of $e$ applied to $m$, i.e., $(e^n)(m) = e^{[n]}(m)$.

LinearEquiv.mul_apply theorem

(f : M ≃ₗ[R] M) (g : M ≃ₗ[R] M) (x : M) : (f * g) x = f (g x)

Full source

@[simp] lemma mul_apply (f : M ≃ₗ[R] M) (g : M ≃ₗ[R] M) (x : M) : (f * g) x = f (g x) := rfl

Composition of Linear Automorphisms Preserves Application

Informal description

For any linear automorphisms $f, g$ of a module $M$ over a ring $R$, and for any element $x \in M$, the composition of $f$ and $g$ applied to $x$ equals $f$ applied to $g$ applied to $x$, i.e., $(f \circ g)(x) = f(g(x))$.

LinearEquiv.automorphismGroup.toLinearMapMonoidHom definition

: (M ≃ₗ[R] M) →* M →ₗ[R] M

Full source

/-- Restriction from `R`-linear automorphisms of `M` to `R`-linear endomorphisms of `M`,
promoted to a monoid hom. -/
@[simps]
def automorphismGroup.toLinearMapMonoidHom : (M ≃ₗ[R] M) →* M →ₗ[R] M where
  toFun e := e.toLinearMap
  map_one' := rfl
  map_mul' _ _ := rfl

Restriction from linear automorphisms to linear endomorphisms as a monoid homomorphism

Informal description

The monoid homomorphism that maps each $R$-linear automorphism $e$ of a module $M$ to its underlying $R$-linear endomorphism, viewed as an element of the monoid of $R$-linear endomorphisms of $M$.

LinearEquiv.applyDistribMulAction instance

: DistribMulAction (M ≃ₗ[R] M) M

Full source

/-- The tautological action by `M ≃ₗ[R] M` on `M`.

This generalizes `Function.End.applyMulAction`. -/
instance applyDistribMulAction : DistribMulAction (M ≃ₗ[R] M) M where
  smul := (· <| ·)
  smul_zero := LinearEquiv.map_zero
  smul_add := LinearEquiv.map_add
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Tautological Action of Linear Automorphisms on a Module

Informal description

For any module $M$ over a ring $R$, the group of linear automorphisms $M \simeq_{R} M$ acts on $M$ via the tautological action $(f, x) \mapsto f(x)$. This action is distributive over addition in $M$ and compatible with scalar multiplication by $R$.

LinearEquiv.smul_def theorem

(f : M ≃ₗ[R] M) (a : M) : f • a = f a

Full source

@[simp]
protected theorem smul_def (f : M ≃ₗ[R] M) (a : M) : f • a = f a :=
  rfl

Scalar Action of Linear Automorphisms Equals Function Application

Informal description

For any $R$-linear automorphism $f$ of a module $M$ and any element $a \in M$, the action of $f$ on $a$ via scalar multiplication is equal to the application of $f$ to $a$, i.e., $f \bullet a = f(a)$.

LinearEquiv.apply_faithfulSMul instance

: FaithfulSMul (M ≃ₗ[R] M) M

Full source

/-- `LinearEquiv.applyDistribMulAction` is faithful. -/
instance apply_faithfulSMul : FaithfulSMul (M ≃ₗ[R] M) M :=
  ⟨LinearEquiv.ext⟩

Faithfulness of the Tautological Action of Linear Automorphisms

Informal description

For any module $M$ over a ring $R$, the tautological action of the group of linear automorphisms $M \simeq_{R} M$ on $M$ is faithful. That is, distinct linear automorphisms act differently on $M$.

LinearEquiv.apply_smulCommClass instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (M ≃ₗ[R] M) M

Full source

instance apply_smulCommClass [SMul S R] [SMul S M] [IsScalarTower S R M] :
    SMulCommClass S (M ≃ₗ[R] M) M where
  smul_comm r e m := (e.map_smul_of_tower r m).symm

Commutativity of Scalar Multiplication with Linear Automorphisms in a Module

Informal description

For a module $M$ over a semiring $R$ and a type $S$ with compatible scalar multiplications $S \to R \to M$ forming a scalar tower, the scalar multiplications by $S$ and by linear automorphisms $M \simeq_{R} M$ on $M$ commute. That is, for any $s \in S$, $f \in M \simeq_{R} M$, and $x \in M$, we have $s \cdot (f \cdot x) = f \cdot (s \cdot x)$.

LinearEquiv.apply_smulCommClass' instance

[SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (M ≃ₗ[R] M) S M

Full source

instance apply_smulCommClass' [SMul S R] [SMul S M] [IsScalarTower S R M] :
    SMulCommClass (M ≃ₗ[R] M) S M :=
  SMulCommClass.symm _ _ _

Commutativity of Linear Automorphisms with Scalar Multiplication in a Module

Informal description

For a module $M$ over a semiring $R$ and a type $S$ with compatible scalar multiplications $S \to R \to M$ forming a scalar tower, the scalar multiplications by linear automorphisms $M \simeq_{R} M$ and by $S$ on $M$ commute. That is, for any $f \in M \simeq_{R} M$, $s \in S$, and $x \in M$, we have $f \cdot (s \cdot x) = s \cdot (f \cdot x)$.

LinearEquiv.ofSubsingleton definition

: M ≃ₗ[R] M₂

Full source

/-- Any two modules that are subsingletons are isomorphic. -/
@[simps]
def ofSubsingleton : M ≃ₗ[R] M₂ :=
  { (0 : M →ₗ[R] M₂) with
    toFun := fun _ ↦ 0
    invFun := fun _ ↦ 0
    left_inv := fun _ ↦ Subsingleton.elim _ _
    right_inv := fun _ ↦ Subsingleton.elim _ _ }

Linear equivalence between subsingleton modules

Informal description

Given two modules $M$ and $M_2$ over a semiring $R$, if both $M$ and $M_2$ are subsingletons (i.e., have at most one element), then there exists a linear equivalence (isomorphism) between them. The isomorphism maps every element of $M$ to the zero element of $M_2$ and vice versa.

LinearEquiv.ofSubsingleton_self theorem

: ofSubsingleton M M = refl R M

Full source

@[simp]
theorem ofSubsingleton_self : ofSubsingleton M M = refl R M := by
  ext
  simp [eq_iff_true_of_subsingleton]

Subsingleton Module Self-Equivalence is Identity

Informal description

For any subsingleton module $M$ over a semiring $R$, the linear equivalence $\text{ofSubsingleton}$ from $M$ to itself is equal to the identity linear equivalence $\text{refl}_R M$.

Module.compHom.toLinearEquiv definition

 {R S : Type*} [Semiring R] [Semiring S] (g : R ≃+* S) :
  haveI := compHom S (↑g : R →+* S)
  R ≃ₗ[R] S

Full source

/-- `g : R ≃+* S` is `R`-linear when the module structure on `S` is `Module.compHom S g` . -/
@[simps]
def compHom.toLinearEquiv {R S : Type*} [Semiring R] [Semiring S] (g : R ≃+* S) :
    haveI := compHom S (↑g : R →+* S)
    R ≃ₗ[R] S :=
  letI := compHom S (↑g : R →+* S)
  { g with
    toFun := (g : R → S)
    invFun := (g.symm : S → R)
    map_smul' := g.map_mul }

Linear equivalence induced by ring isomorphism via composition

Informal description

Given semirings $R$ and $S$, and a ring isomorphism $g: R \simeq+* S$, the function constructs a linear equivalence $R \simeq_{R} S$ where $S$ is viewed as an $R$-module via the composition with $g$. Specifically: - The forward map is $g: R → S$ - The inverse map is $g^{-1}: S → R$ - The scalar multiplication is preserved through $g$'s multiplicative property

DistribMulAction.toLinearEquiv definition

(s : S) : M ≃ₗ[R] M

Full source

/-- Each element of the group defines a linear equivalence.

This is a stronger version of `DistribMulAction.toAddEquiv`. -/
@[simps!]
def toLinearEquiv (s : S) : M ≃ₗ[R] M :=
  { toAddEquiv M s, toLinearMap R M s with }

Linear equivalence induced by group action on a module

Informal description

For any element $ s $ of the group $ S $, the function $ \text{DistribMulAction.toLinearEquiv} $ constructs a linear equivalence $ M \simeq_{R} M $ that represents the action of $ s $ on the module $ M $ over the semiring $ R $. This extends the additive equivalence defined by the group action to a linear equivalence, preserving both the additive and scalar multiplicative structures.

DistribMulAction.toModuleAut definition

: S →* M ≃ₗ[R] M

Full source

/-- Each element of the group defines a module automorphism.

This is a stronger version of `DistribMulAction.toAddAut`. -/
@[simps]
def toModuleAut : S →* M ≃ₗ[R] M where
  toFun := toLinearEquiv R M
  map_one' := LinearEquiv.ext <| one_smul _
  map_mul' _ _ := LinearEquiv.ext <| mul_smul _ _

Group action as module automorphisms

Informal description

The function maps each element $ s $ of the group $ S $ to a module automorphism $ M \simeq_{R} M $ (a linear equivalence from $ M $ to itself over the semiring $ R $), forming a group homomorphism from $ S $ to the group of linear automorphisms of $ M $. This extends the additive automorphism defined by the group action to a linear automorphism, preserving both the additive and scalar multiplicative structures.

AddEquiv.toLinearEquiv definition

(h : ∀ (c : R) (x), e (c • x) = c • e x) : M ≃ₗ[R] M₂

Full source

/-- An additive equivalence whose underlying function preserves `smul` is a linear equivalence. -/
def toLinearEquiv (h : ∀ (c : R) (x), e (c • x) = c • e x) : M ≃ₗ[R] M₂ :=
  { e with map_smul' := h }

Linear equivalence induced by an additive equivalence preserving scalar multiplication

Informal description

Given an additive equivalence $e : M \simeq M₂$ between modules $M$ and $M₂$ over a semiring $R$, if $e$ preserves scalar multiplication (i.e., $e(c \bullet x) = c \bullet e(x)$ for all $c \in R$ and $x \in M$), then $e$ can be extended to a linear equivalence between $M$ and $M₂$.

AddEquiv.coe_toLinearEquiv theorem

(h : ∀ (c : R) (x), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h) = e

Full source

@[simp]
theorem coe_toLinearEquiv (h : ∀ (c : R) (x), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h) = e :=
  rfl

Underlying Function of Induced Linear Equivalence Equals Original Additive Equivalence

Informal description

Given an additive equivalence $e : M \simeq M₂$ between modules $M$ and $M₂$ over a semiring $R$, if $e$ preserves scalar multiplication (i.e., $e(c \bullet x) = c \bullet e(x)$ for all $c \in R$ and $x \in M$), then the underlying function of the induced linear equivalence $e.toLinearEquiv(h)$ is equal to $e$ itself.

AddEquiv.coe_toLinearEquiv_symm theorem

(h : ∀ (c : R) (x), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h).symm = e.symm

Full source

@[simp]
theorem coe_toLinearEquiv_symm (h : ∀ (c : R) (x), e (c • x) = c • e x) :
    ⇑(e.toLinearEquiv h).symm = e.symm :=
  rfl

Inverse of Induced Linear Equivalence Equals Inverse of Additive Equivalence

Informal description

Given an additive equivalence $e : M \simeq M₂$ between modules $M$ and $M₂$ over a semiring $R$, if $e$ preserves scalar multiplication (i.e., $e(c \bullet x) = c \bullet e(x)$ for all $c \in R$ and $x \in M$), then the underlying function of the inverse of the induced linear equivalence $(e.toLinearEquiv(h))^{-1}$ is equal to the inverse $e^{-1}$ of the original additive equivalence.

AddEquiv.toNatLinearEquiv definition

: M ≃ₗ[ℕ] M₂

Full source

/-- An additive equivalence between commutative additive monoids is a linear equivalence between
ℕ-modules -/
def toNatLinearEquiv : M ≃ₗ[ℕ] M₂ :=
  e.toLinearEquiv fun c a ↦ by rw [map_nsmul]

Natural number linear equivalence induced by an additive equivalence

Informal description

Given an additive equivalence $e : M \simeq M₂$ between two additive commutative monoids $M$ and $M₂$, the structure `AddEquiv.toNatLinearEquiv` extends $e$ to a linear equivalence between $M$ and $M₂$ viewed as $\mathbb{N}$-modules, where the scalar multiplication is given by repeated addition. This is achieved by verifying that $e$ preserves natural number scalar multiplication (i.e., $e(n \cdot x) = n \cdot e(x)$ for all $n \in \mathbb{N}$ and $x \in M$).

AddEquiv.coe_toNatLinearEquiv theorem

: ⇑e.toNatLinearEquiv = e

Full source

@[simp]
theorem coe_toNatLinearEquiv : ⇑e.toNatLinearEquiv = e :=
  rfl

Equality of Underlying Functions in Natural Number Linear Equivalence Induced by Additive Equivalence

Informal description

For any additive equivalence $e$ between two additive commutative monoids $M$ and $M₂$, the underlying function of the induced $\mathbb{N}$-linear equivalence $e.toNatLinearEquiv$ is equal to $e$ itself. In other words, the map $e.toNatLinearEquiv$ and $e$ coincide as functions from $M$ to $M₂$.

AddEquiv.toNatLinearEquiv_toAddEquiv theorem

: ↑e.toNatLinearEquiv = e

Full source

@[simp]
theorem toNatLinearEquiv_toAddEquiv : ↑e.toNatLinearEquiv = e :=
  rfl

Natural Number Linear Equivalence Coincides with Original Additive Equivalence

Informal description

For any additive equivalence $e$ between two additive commutative monoids $M$ and $M₂$, the underlying additive equivalence of the induced $\mathbb{N}$-linear equivalence $e.toNatLinearEquiv$ is equal to $e$ itself.

LinearEquiv.toAddEquiv_toNatLinearEquiv theorem

(e : M ≃ₗ[ℕ] M₂) : AddEquiv.toNatLinearEquiv ↑e = e

Full source

@[simp]
theorem _root_.LinearEquiv.toAddEquiv_toNatLinearEquiv (e : M ≃ₗ[ℕ] M₂) :
    AddEquiv.toNatLinearEquiv ↑e = e :=
  DFunLike.coe_injective rfl

Natural Linear Equivalence Induced by Additive Equivalence is Identity

Informal description

For any $\mathbb{N}$-linear equivalence $e : M \simeq_{\mathbb{N}} M₂$ between two additive commutative monoids $M$ and $M₂$, the natural number linear equivalence induced by the underlying additive equivalence of $e$ is equal to $e$ itself. In other words, the composition of the operations "forget the linear structure" and "induce the linear structure" is the identity on $\mathbb{N}$-linear equivalences.

AddEquiv.toNatLinearEquiv_symm theorem

: e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv

Full source

@[simp]
theorem toNatLinearEquiv_symm : e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv :=
  rfl

Inverse of Natural Number Linear Equivalence Induced by Additive Equivalence

Informal description

For any additive equivalence $e$ between two additive commutative monoids $M$ and $M₂$, the inverse of the induced $\mathbb{N}$-linear equivalence $e.toNatLinearEquiv$ is equal to the $\mathbb{N}$-linear equivalence induced by the inverse additive equivalence $e.symm$.

AddEquiv.toNatLinearEquiv_refl theorem

: (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M

Full source

@[simp]
theorem toNatLinearEquiv_refl : (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M :=
  rfl

Identity Additive Equivalence Induces Identity $\mathbb{N}$-Linear Equivalence

Informal description

For any additive commutative monoid $M$, the natural number linear equivalence induced by the additive identity equivalence $\text{AddEquiv.refl } M$ is equal to the identity $\mathbb{N}$-linear equivalence $\text{LinearEquiv.refl } \mathbb{N} M$.

AddEquiv.toNatLinearEquiv_trans theorem

(e₂ : M₂ ≃+ M₃) : e.toNatLinearEquiv.trans e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv

Full source

@[simp]
theorem toNatLinearEquiv_trans (e₂ : M₂ ≃+ M₃) :
    e.toNatLinearEquiv.trans e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv :=
  rfl

Composition of $\mathbb{N}$-linear equivalences induced by additive equivalences

Informal description

Let $e : M \simeq M₂$ and $e₂ : M₂ \simeq M₃$ be additive equivalences between additive commutative monoids. Then the composition of the induced $\mathbb{N}$-linear equivalences $e.toNatLinearEquiv$ and $e₂.toNatLinearEquiv$ is equal to the $\mathbb{N}$-linear equivalence induced by the composition $e \circ e₂$.

AddEquiv.toIntLinearEquiv definition

: M ≃ₗ[ℤ] M₂

Full source

/-- An additive equivalence between commutative additive groups is a linear
equivalence between ℤ-modules -/
def toIntLinearEquiv : M ≃ₗ[ℤ] M₂ :=
  e.toLinearEquiv fun c a ↦ e.toAddMonoidHom.map_zsmul a c

$\mathbb{Z}$-linear equivalence induced by an additive equivalence

Informal description

Given an additive equivalence $e : M \simeq M₂$ between two commutative additive groups $M$ and $M₂$, the map $e$ induces a linear equivalence between $M$ and $M₂$ when viewed as $\mathbb{Z}$-modules. This means $e$ preserves both the additive structure and integer scalar multiplication.

AddEquiv.coe_toIntLinearEquiv theorem

: ⇑e.toIntLinearEquiv = e

Full source

@[simp]
theorem coe_toIntLinearEquiv : ⇑e.toIntLinearEquiv = e :=
  rfl

Equality of Underlying Functions in $\mathbb{Z}$-Linear Equivalence Induced by Additive Equivalence

Informal description

For any additive equivalence $e$ between two commutative additive groups $M$ and $M₂$, the underlying function of the induced $\mathbb{Z}$-linear equivalence $e.toIntLinearEquiv$ is equal to $e$ itself.

AddEquiv.toIntLinearEquiv_toAddEquiv theorem

: ↑e.toIntLinearEquiv = e

Full source

@[simp]
theorem toIntLinearEquiv_toAddEquiv : ↑e.toIntLinearEquiv = e := by
  ext
  rfl

Coercion of $\mathbb{Z}$-linear equivalence recovers original additive equivalence

Informal description

For any additive equivalence $e$ between two commutative additive groups $M$ and $M₂$, the underlying additive equivalence of the induced $\mathbb{Z}$-linear equivalence $e.toIntLinearEquiv$ is equal to $e$ itself. In other words, the coercion of $e.toIntLinearEquiv$ back to an additive equivalence recovers $e$.

LinearEquiv.toAddEquiv_toIntLinearEquiv theorem

(e : M ≃ₗ[ℤ] M₂) : AddEquiv.toIntLinearEquiv (e : M ≃+ M₂) = e

Full source

@[simp]
theorem _root_.LinearEquiv.toAddEquiv_toIntLinearEquiv (e : M ≃ₗ[ℤ] M₂) :
    AddEquiv.toIntLinearEquiv (e : M ≃+ M₂) = e :=
  DFunLike.coe_injective rfl

$\mathbb{Z}$-linear equivalence equals its induced additive equivalence's linearization

Informal description

For any $\mathbb{Z}$-linear equivalence $e : M \simeq_{\mathbb{Z}} M₂$ between $\mathbb{Z}$-modules $M$ and $M₂$, the $\mathbb{Z}$-linear equivalence induced by the underlying additive equivalence of $e$ is equal to $e$ itself. In other words, the diagram commutes when converting $e$ to an additive equivalence and back to a $\mathbb{Z}$-linear equivalence.

AddEquiv.toIntLinearEquiv_symm theorem

: e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv

Full source

@[simp]
theorem toIntLinearEquiv_symm : e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv :=
  rfl

Inverse of $\mathbb{Z}$-linear equivalence equals $\mathbb{Z}$-linear equivalence of inverse

Informal description

For any additive equivalence $e$ between two commutative additive groups $M$ and $M₂$, the inverse of the induced $\mathbb{Z}$-linear equivalence $e.toIntLinearEquiv$ is equal to the $\mathbb{Z}$-linear equivalence induced by the inverse additive equivalence $e.symm$. That is, $$(e.toIntLinearEquiv)^{-1} = e.symm.toIntLinearEquiv.$$

AddEquiv.toIntLinearEquiv_refl theorem

: (AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M

Full source

@[simp]
theorem toIntLinearEquiv_refl : (AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M :=
  rfl

Identity Additive Equivalence Induces Identity $\mathbb{Z}$-Linear Equivalence

Informal description

The $\mathbb{Z}$-linear equivalence induced by the additive identity equivalence $\text{AddEquiv.refl } M$ is equal to the identity $\mathbb{Z}$-linear equivalence $\text{LinearEquiv.refl } \mathbb{Z} M$.

AddEquiv.toIntLinearEquiv_trans theorem

(e₂ : M₂ ≃+ M₃) : e.toIntLinearEquiv.trans e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv

Full source

@[simp]
theorem toIntLinearEquiv_trans (e₂ : M₂ ≃+ M₃) :
    e.toIntLinearEquiv.trans e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv :=
  rfl

Compatibility of $\mathbb{Z}$-Linear Equivalence with Composition of Additive Equivalences

Informal description

Given additive equivalences $e : M \simeq M₂$ and $e₂ : M₂ \simeq M₃$ between commutative additive groups, the composition of their induced $\mathbb{Z}$-linear equivalences is equal to the $\mathbb{Z}$-linear equivalence induced by the composition of $e$ and $e₂$. In other words, $(e \to \mathbb{Z}\text{-LinearEquiv}) \circ (e₂ \to \mathbb{Z}\text{-LinearEquiv}) = (e \circ e₂) \to \mathbb{Z}\text{-LinearEquiv}$.

LinearMap.ringLmapEquivSelf definition

[Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M

Full source

/-- The equivalence between R-linear maps from `R` to `M`, and points of `M` itself.
This says that the forgetful functor from `R`-modules to types is representable, by `R`.

This is an `S`-linear equivalence, under the assumption that `S` acts on `M` commuting with `R`.
When `R` is commutative, we can take this to be the usual action with `S = R`.
Otherwise, `S = ℕ` shows that the equivalence is additive.
See note [bundled maps over different rings].
-/
@[simps]
def ringLmapEquivSelf [Module S M] [SMulCommClass R S M] : (R →ₗ[R] M) ≃ₗ[S] M :=
  { applyₗ' S (1 : R) with
    toFun := fun f ↦ f 1
    invFun := smulRight (1 : R →ₗ[R] R)
    left_inv := fun f ↦ by
      ext
      simp only [coe_smulRight, Module.End.one_apply, smul_eq_mul, ← map_smul f, mul_one]
    right_inv := fun x ↦ by simp }

Equivalence between $R$-linear maps $R \to M$ and points of $M$

Informal description

The $S$-linear equivalence between $R$-linear maps from $R$ to $M$ and elements of $M$. This establishes that the forgetful functor from $R$-modules to types is representable by $R$. More precisely, the equivalence is given by: - The forward map evaluates an $R$-linear map $f: R \to M$ at $1 \in R$, yielding $f(1) \in M$. - The inverse map takes an element $x \in M$ and constructs the $R$-linear map $r \mapsto r \cdot x$. This equivalence holds when $S$ acts on $M$ in a way that commutes with the $R$-action. When $R$ is commutative, we can take $S = R$ for the usual action. In general, taking $S = \mathbb{N}$ shows the equivalence is additive.

addMonoidHomLequivNat definition

 {A B : Type*} (R : Type*) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B

Full source

/--
The `R`-linear equivalence between additive morphisms `A →+ B` and `ℕ`-linear morphisms `A →ₗ[ℕ] B`.
-/
@[simps]
def addMonoidHomLequivNat {A B : Type*} (R : Type*) [Semiring R] [AddCommMonoid A]
    [AddCommMonoid B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℕ] B where
  toFun := AddMonoidHom.toNatLinearMap
  invFun := LinearMap.toAddMonoidHom
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between additive monoid homomorphisms and $\mathbb{N}$-linear maps

Informal description

Given a semiring $R$ and additive commutative monoids $A$ and $B$ where $B$ is an $R$-module, there exists an $R$-linear equivalence between the additive monoid homomorphisms $A \to+ B$ and the $\mathbb{N}$-linear maps $A \to_{\mathbb{N}} B$. This equivalence is constructed via: - The forward map converts an additive monoid homomorphism to its $\mathbb{N}$-linear counterpart - The inverse map converts a $\mathbb{N}$-linear map back to an additive monoid homomorphism - The equivalence preserves addition and scalar multiplication by elements of $R$

addMonoidHomLequivInt definition

 {A B : Type*} (R : Type*) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B

Full source

/--
The `R`-linear equivalence between additive morphisms `A →+ B` and `ℤ`-linear morphisms `A →ₗ[ℤ] B`.
-/
@[simps]
def addMonoidHomLequivInt {A B : Type*} (R : Type*) [Semiring R] [AddCommGroup A] [AddCommGroup B]
    [Module R B] : (A →+ B) ≃ₗ[R] A →ₗ[ℤ] B where
  toFun := AddMonoidHom.toIntLinearMap
  invFun := LinearMap.toAddMonoidHom
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence between additive homomorphisms and $\mathbb{Z}$-linear maps

Informal description

Given a semiring $R$ and additive commutative groups $A$ and $B$ where $B$ is an $R$-module, there exists an $R$-linear equivalence between the additive group homomorphisms $A \to+ B$ and the $\mathbb{Z}$-linear maps $A \to_{\mathbb{Z}} B$. The equivalence is constructed via: - The forward map converts an additive homomorphism to a $\mathbb{Z}$-linear map - The inverse map converts a $\mathbb{Z}$-linear map back to an additive homomorphism - These operations preserve addition and scalar multiplication, and are mutual inverses

addMonoidEndRingEquivInt definition

(A : Type*) [AddCommGroup A] : AddMonoid.End A ≃+* Module.End ℤ A

Full source

/-- Ring equivalence between additive group endomorphisms of an `AddCommGroup` `A` and
`ℤ`-module endomorphisms of `A.` -/
@[simps] def addMonoidEndRingEquivInt (A : Type*) [AddCommGroup A] :
    AddMonoid.EndAddMonoid.End A ≃+* Module.End ℤ A :=
  { addMonoidHomLequivInt (B := A) ℤ with
    map_mul' := fun _ _ ↦ rfl }

Ring equivalence between additive endomorphisms and $\mathbb{Z}$-module endomorphisms

Informal description

Given an additive commutative group $A$, there exists a ring equivalence between the ring of additive endomorphisms of $A$ (with pointwise addition and composition as multiplication) and the ring of $\mathbb{Z}$-module endomorphisms of $A$ (viewed as a $\mathbb{Z}$-module). The equivalence is constructed by: 1. Mapping each additive endomorphism to its corresponding $\mathbb{Z}$-linear map 2. Preserving both the additive and multiplicative structures 3. Being bijective with an inverse that maps $\mathbb{Z}$-linear maps back to additive endomorphisms

LinearEquiv.instZero instance

: Zero (M ≃ₛₗ[σ₁₂] M₂)

Full source

/-- Between two zero modules, the zero map is an equivalence. -/
instance : Zero (M ≃ₛₗ[σ₁₂] M₂) :=
  ⟨{ (0 : M →ₛₗ[σ₁₂] M₂) with
      toFun := 0
      invFun := 0
      right_inv := Subsingleton.elim _
      left_inv := Subsingleton.elim _ }⟩

Zero Map as Semilinear Equivalence Between Zero Modules

Informal description

For any two modules $M$ and $M₂$ over semirings with a semilinear equivalence relation $\sigma₁₂$, the zero map between them is a semilinear equivalence.

LinearEquiv.zero_symm theorem

: (0 : M ≃ₛₗ[σ₁₂] M₂).symm = 0

Full source

@[simp]
theorem zero_symm : (0 : M ≃ₛₗ[σ₁₂] M₂).symm = 0 :=
  rfl

Inverse of Zero Semilinear Equivalence is Zero

Informal description

The inverse of the zero semilinear equivalence between modules $M$ and $M₂$ (with respect to a semilinear relation $\sigma₁₂$) is itself the zero equivalence. That is, $(0 : M ≃ₛₗ[σ₁₂] M₂)^{-1} = 0$.

LinearEquiv.coe_zero theorem

: ⇑(0 : M ≃ₛₗ[σ₁₂] M₂) = 0

Full source

@[simp]
theorem coe_zero : ⇑(0 : M ≃ₛₗ[σ₁₂] M₂) = 0 :=
  rfl

Zero Semilinear Equivalence is the Zero Map

Informal description

The zero semilinear equivalence between modules $M$ and $M₂$ (with respect to a semiring homomorphism $\sigma_{12}$) is equal to the zero map, i.e., $0(x) = 0$ for all $x \in M$.

LinearEquiv.zero_apply theorem

(x : M) : (0 : M ≃ₛₗ[σ₁₂] M₂) x = 0

Full source

theorem zero_apply (x : M) : (0 : M ≃ₛₗ[σ₁₂] M₂) x = 0 :=
  rfl

Zero Semilinear Equivalence Maps to Zero

Informal description

For any element $x$ in a module $M$, the zero semilinear equivalence map $0 \colon M \simeq_{σ₁₂} M₂$ satisfies $0(x) = 0$.

LinearEquiv.instUnique instance

: Unique (M ≃ₛₗ[σ₁₂] M₂)

Full source

/-- Between two zero modules, the zero map is the only equivalence. -/
instance : Unique (M ≃ₛₗ[σ₁₂] M₂) where
  uniq _ := toLinearMap_injective (Subsingleton.elim _ _)
  default := 0

Uniqueness of the Zero Semilinear Equivalence Between Zero Modules

Informal description

For any two modules $M$ and $M₂$ over semirings with a semilinear equivalence relation $\sigma₁₂$, there is exactly one semilinear equivalence between them, namely the zero map.

LinearEquiv.uniqueOfSubsingleton instance

[Subsingleton R] [Subsingleton R₂] : Unique (M ≃ₛₗ[σ₁₂] M₂)

Full source

instance uniqueOfSubsingleton [Subsingleton R] [Subsingleton R₂] : Unique (M ≃ₛₗ[σ₁₂] M₂) := by
  haveI := Module.subsingleton R M
  haveI := Module.subsingleton R₂ M₂
  infer_instance

Uniqueness of Semilinear Equivalence Between Modules over Subsingleton Semirings

Informal description

For any semirings $R$ and $R₂$ that are subsingletons (i.e., have at most one element), and any modules $M$ and $M₂$ over $R$ and $R₂$ respectively with a semilinear equivalence relation $\sigma_{12}$, there is exactly one semilinear equivalence between $M$ and $M₂$.

LinearEquiv.curry definition

: (V × V₂ → M) ≃ₗ[R] V → V₂ → M

Full source

/-- Linear equivalence between a curried and uncurried function.
  Differs from `TensorProduct.curry`. -/
protected def curry : (V × V₂ → M) ≃ₗ[R] V → V₂ → M :=
  { Equiv.curry _ _ _ with
    map_add' := fun _ _ ↦ rfl
    map_smul' := fun _ _ ↦ rfl }

Linear currying equivalence

Informal description

The linear equivalence between the space of linear maps from the product module $V \times V_2$ to $M$ and the space of curried linear maps $V \to V_2 \to M$ over a semiring $R$. This equivalence preserves addition and scalar multiplication, and differs from the tensor product version of currying.

LinearEquiv.coe_curry theorem

: ⇑(LinearEquiv.curry R M V V₂) = curry

Full source

@[simp]
theorem coe_curry : ⇑(LinearEquiv.curry R M V V₂) = curry :=
  rfl

Currying as a Linear Equivalence

Informal description

The underlying function of the linear equivalence `LinearEquiv.curry R M V V₂` is equal to the standard currying operation, which maps a function $f \colon V \times V_2 \to M$ to its curried form $\text{curry}(f) \colon V \to V_2 \to M$.

LinearEquiv.coe_curry_symm theorem

: ⇑(LinearEquiv.curry R M V V₂).symm = uncurry

Full source

@[simp]
theorem coe_curry_symm : ⇑(LinearEquiv.curry R M V V₂).symm = uncurry :=
  rfl

Inverse of Linear Currying Equivalence is Uncurry

Informal description

The underlying function of the inverse of the linear currying equivalence is equal to the uncurry function. That is, if $\text{LinearEquiv.curry}\,R\,M\,V\,V_2$ is the linear equivalence between linear maps from $V \times V_2$ to $M$ and curried linear maps $V \to V_2 \to M$, then its inverse is given by the uncurry operation.

LinearEquiv.ofLinear definition

(h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂

Full source

/-- If a linear map has an inverse, it is a linear equivalence. -/
def ofLinear (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) : M ≃ₛₗ[σ₁₂] M₂ :=
  { f with
    invFun := g
    left_inv := LinearMap.ext_iff.1 h₂
    right_inv := LinearMap.ext_iff.1 h₁ }

Linear equivalence from inverse linear maps

Informal description

Given two linear maps $f \colon M \to M₂$ and $g \colon M₂ \to M$ over a semiring $R$ with a ring homomorphism $\sigma_{12} \colon R \to R$, if $f \circ g$ is the identity map on $M₂$ and $g \circ f$ is the identity map on $M$, then $f$ is a linear equivalence between $M$ and $M₂$ with inverse $g$.

LinearEquiv.ofLinear_apply theorem

{h₁ h₂} (x : M) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) x = f x

Full source

@[simp]
theorem ofLinear_apply {h₁ h₂} (x : M) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) x = f x :=
  rfl

Evaluation of Linear Equivalence Constructed from Inverse Linear Maps

Informal description

Let $M$ and $M_2$ be modules over a semiring $R$ with a ring homomorphism $\sigma_{12} \colon R \to R$, and let $f \colon M \to M_2$ and $g \colon M_2 \to M$ be linear maps such that $f \circ g$ and $g \circ f$ are identity maps. For any $x \in M$, the linear equivalence $\text{ofLinear}\,f\,g\,h_1\,h_2$ evaluated at $x$ equals $f(x)$.

LinearEquiv.ofLinear_symm_apply theorem

{h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x

Full source

@[simp]
theorem ofLinear_symm_apply {h₁ h₂} (x : M₂) : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm x = g x :=
  rfl

Inverse Evaluation of Linear Equivalence Constructed from Inverse Linear Maps

Informal description

Let $M$ and $M_2$ be modules over a semiring $R$ with a ring homomorphism $\sigma_{12} \colon R \to R$, and let $f \colon M \to M_2$ and $g \colon M_2 \to M$ be linear maps such that $f \circ g$ and $g \circ f$ are identity maps. For any $x \in M_2$, the inverse of the linear equivalence $\text{ofLinear}\,f\,g\,h_1\,h_2$ evaluated at $x$ equals $g(x)$.

LinearEquiv.ofLinear_toLinearMap theorem

{h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f

Full source

@[simp]
theorem ofLinear_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂) = f := rfl

Linear Equivalence Construction Preserves Forward Map

Informal description

Given modules $M$ and $M₂$ over a semiring $R$ with a ring homomorphism $\sigma_{12} \colon R \to R$, and linear maps $f \colon M \to M₂$ and $g \colon M₂ \to M$ such that $f \circ g$ and $g \circ f$ are identity maps, the linear equivalence $\text{ofLinear}\,f\,g\,h_1\,h_2$ is equal to $f$ as a linear map.

LinearEquiv.ofLinear_symm_toLinearMap theorem

{h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g

Full source

@[simp]
theorem ofLinear_symm_toLinearMap {h₁ h₂} : (ofLinear f g h₁ h₂ : M ≃ₛₗ[σ₁₂] M₂).symm = g := rfl

Inverse of Linear Equivalence Construction Equals Backward Map

Informal description

Given modules $M$ and $M₂$ over a semiring $R$ with a ring homomorphism $\sigma_{12} \colon R \to R$, and linear maps $f \colon M \to M₂$ and $g \colon M₂ \to M$ such that $f \circ g$ and $g \circ f$ are identity maps, the inverse of the linear equivalence $\text{ofLinear}\,f\,g\,h_1\,h_2$ is equal to $g$ as a linear map.

LinearEquiv.neg definition

: M ≃ₗ[R] M

Full source

/-- `x ↦ -x` as a `LinearEquiv` -/
def neg : M ≃ₗ[R] M :=
  { Equiv.neg M, (-LinearMap.id : M →ₗ[R] M) with }

Negation as a linear equivalence

Informal description

The linear equivalence that maps each element $x$ in a module $M$ over a semiring $R$ to its additive inverse $-x$.

LinearEquiv.coe_neg theorem

: ⇑(neg R : M ≃ₗ[R] M) = -id

Full source

@[simp]
theorem coe_neg : ⇑(neg R : M ≃ₗ[R] M) = -id :=
  rfl

Negation Linear Equivalence as Negation Function

Informal description

The underlying function of the linear equivalence `neg R : M ≃ₗ[R] M` (which maps each element $x \in M$ to its additive inverse $-x$) is equal to the negation function $-id$ (where $id$ is the identity function on $M$).

LinearEquiv.neg_apply theorem

(x : M) : neg R x = -x

Full source

theorem neg_apply (x : M) : neg R x = -x := by simp

Negation Linear Equivalence Maps to Additive Inverse

Informal description

For any module $M$ over a semiring $R$ and any element $x \in M$, the linear equivalence `neg R` maps $x$ to its additive inverse $-x$.

LinearEquiv.symm_neg theorem

: (neg R : M ≃ₗ[R] M).symm = neg R

Full source

@[simp]
theorem symm_neg : (neg R : M ≃ₗ[R] M).symm = neg R :=
  rfl

Self-inverse property of negation as a linear equivalence: $\text{neg}_R^{-1} = \text{neg}_R$

Informal description

The inverse of the linear equivalence that maps each element $x$ in a module $M$ over a semiring $R$ to its additive inverse $-x$ is itself the same linear equivalence. In other words, the linear equivalence $\text{neg}_R : M \simeq_{R} M$ satisfies $\text{neg}_R^{-1} = \text{neg}_R$.

LinearEquiv.arrowCongrAddEquiv definition

 (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃+ (M₂ →ₗ[R] M₂₂)

Full source

/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives an
additive isomorphism between the two function spaces.

See also `LinearEquiv.arrowCongr` for the linear version of this isomorphism. -/
@[simps] def arrowCongrAddEquiv (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
    (M₁ →ₗ[R] M₂₁) ≃+ (M₂ →ₗ[R] M₂₂) where
  toFun f := e₂.comp (f.comp e₁.symm.toLinearMap)
  invFun f := e₂.symm.comp (f.comp e₁.toLinearMap)
  left_inv f := by
    ext x
    simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]
  right_inv f := by
    ext x
    simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]
  map_add' f g := by
    ext x
    simp only [map_add, add_apply, Function.comp_apply, coe_comp, coe_coe]

Additive isomorphism between linear map spaces induced by linear isomorphisms

Informal description

Given two linear isomorphisms $e_1 : M_1 \simeq_{R} M_2$ and $e_2 : M_{21} \simeq_{R} M_{22}$ between modules over a semiring $R$, the function `LinearEquiv.arrowCongrAddEquiv` constructs an additive isomorphism between the spaces of linear maps $(M_1 \to_{R} M_{21})$ and $(M_2 \to_{R} M_{22})$. Specifically, it maps a linear map $f : M_1 \to_{R} M_{21}$ to the composition $e_2 \circ f \circ e_1^{-1} : M_2 \to_{R} M_{22}$, and its inverse maps $g : M_2 \to_{R} M_{22}$ to $e_2^{-1} \circ g \circ e_1 : M_1 \to_{R} M_{21}$.

LinearEquiv.domMulActCongrRight definition

 [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[Sᵈᵐᵃ] (M₁ →ₗ[R] M₂₂)

Full source

/-- A linear isomorphism between the domains an codomains of two spaces of linear maps gives a
linear isomorphism with respect to an action on the domains. -/
@[simps] def domMulActCongrRight [Semiring S] [Module S M₁] [SMulCommClass R S M₁]
    (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[Sᵈᵐᵃ] (M₁ →ₗ[R] M₂₂) where
  __ := arrowCongrAddEquiv (.refl ..) e₂
  map_smul' := DomMulAct.mk.forall_congr_right.mp fun _ _ ↦ by ext; simp

Linear isomorphism of linear map spaces induced by a linear isomorphism on codomains with domain multiplication action

Informal description

Given a semiring $S$, an $S$-module $M_1$, and a linear isomorphism $e_2 : M_{21} \simeq_R M_{22}$ between $R$-modules such that the scalar multiplications by $R$ and $S$ on $M_1$ commute, the function `LinearEquiv.domMulActCongrRight` constructs a linear isomorphism $(M_1 \to_R M_{21}) \simeq_{S^{\text{dma}}} (M_1 \to_R M_{22})$. Here, $S^{\text{dma}}$ denotes the domain multiplication action type of $S$, which is a type synonym for the opposite semiring $S^{\text{op}}$. The isomorphism maps a linear map $f : M_1 \to_R M_{21}$ to the composition $e_2 \circ f : M_1 \to_R M_{22}$.

LinearEquiv.conjRingEquiv definition

(e : M₁ ≃ₗ[R] M₂) : Module.End R M₁ ≃+* Module.End R M₂

Full source

/-- If `M` and `M₂` are linearly isomorphic then the endomorphism rings of `M` and `M₂`
are isomorphic.

See `LinearEquiv.conj` for the linear version of this isomorphism. -/
@[simps!] def conjRingEquiv (e : M₁ ≃ₗ[R] M₂) : Module.EndModule.End R M₁ ≃+* Module.End R M₂ where
  __ := arrowCongrAddEquiv e e
  map_mul' _ _ := by ext; simp [arrowCongrAddEquiv]

Ring isomorphism between endomorphism rings induced by a linear isomorphism

Informal description

Given a linear isomorphism $e : M_1 \simeq_R M_2$ between $R$-modules, the function `LinearEquiv.conjRingEquiv` constructs a ring isomorphism between the endomorphism rings $\text{End}_R(M_1)$ and $\text{End}_R(M_2)$. Specifically, it maps an endomorphism $f \in \text{End}_R(M_1)$ to the conjugate endomorphism $e \circ f \circ e^{-1} \in \text{End}_R(M_2)$.

LinearEquiv.smulOfUnit definition

(a : Rˣ) : M ≃ₗ[R] M

Full source

/-- Multiplying by a unit `a` of the ring `R` is a linear equivalence. -/
def smulOfUnit (a : Rˣ) : M ≃ₗ[R] M :=
  DistribMulAction.toLinearEquiv R M a

Linear equivalence induced by scalar multiplication with a unit

Informal description

For any unit $ a $ of the ring $ R $, the function `LinearEquiv.smulOfUnit` constructs a linear equivalence $ M \simeq_R M $ by scalar multiplication by $ a $. This equivalence preserves both the additive and scalar multiplicative structures of the $ R $-module $ M $.

LinearEquiv.arrowCongr definition

 {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁]
  [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂)
  (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

Full source

/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
linear isomorphism between the two function spaces.

See `LinearEquiv.arrowCongrAddEquiv` for the additive version of this isomorphism that works
over a not necessarily commutative semiring. -/
def arrowCongr {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
    [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁]
    [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂ where
  __ := arrowCongrAddEquiv e₁ e₂
  map_smul' c f := by ext; simp [arrowCongrAddEquiv]

Linear isomorphism between linear map spaces induced by domain and codomain isomorphisms

Informal description

Given a commutative semiring $R$ and modules $M_1, M_2, M_{21}, M_{22}$ over $R$, any pair of linear isomorphisms $e_1: M_1 \simeq_R M_2$ and $e_2: M_{21} \simeq_R M_{22}$ induces a linear isomorphism between the spaces of linear maps $(M_1 \to_R M_{21})$ and $(M_2 \to_R M_{22})$. This isomorphism maps a linear map $f: M_1 \to_R M_{21}$ to the composition $e_2 \circ f \circ e_1^{-1}: M_2 \to_R M_{22}$.

LinearEquiv.arrowCongr_apply theorem

 {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁]
  [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂)
  (f : M₁ →ₗ[R] M₂₁) (x : M₂) : arrowCongr e₁ e₂ f x = e₂ (f (e₁.symm x))

Full source

@[simp]
theorem arrowCongr_apply {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁]
    [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂]
    [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁)
    (x : M₂) : arrowCongr e₁ e₂ f x = e₂ (f (e₁.symm x)) :=
  rfl

Evaluation of the Induced Linear Map Isomorphism via Composition with Domain and Codomain Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $M_1, M_2, M_{21}, M_{22}$ be $R$-modules. Given linear isomorphisms $e_1: M_1 \simeq_R M_2$ and $e_2: M_{21} \simeq_R M_{22}$, the induced linear isomorphism $\text{arrowCongr}(e_1, e_2)$ between the spaces of linear maps $(M_1 \to_R M_{21})$ and $(M_2 \to_R M_{22})$ satisfies the following: for any linear map $f: M_1 \to_R M_{21}$ and any $x \in M_2$, we have \[ \text{arrowCongr}(e_1, e_2)(f)(x) = e_2(f(e_1^{-1}(x))). \]

LinearEquiv.arrowCongr_symm_apply theorem

 {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁]
  [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂)
  (f : M₂ →ₗ[R] M₂₂) (x : M₁) : (arrowCongr e₁ e₂).symm f x = e₂.symm (f (e₁ x))

Full source

@[simp]
theorem arrowCongr_symm_apply {R M₁ M₂ M₂₁ M₂₂ : Sort _} [CommSemiring R] [AddCommMonoid M₁]
    [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂]
    [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂)
    (x : M₁) : (arrowCongr e₁ e₂).symm f x = e₂.symm (f (e₁ x)) :=
  rfl

Inverse of Linear Map Space Isomorphism Applied to a Linear Map

Informal description

Let $R$ be a commutative semiring, and let $M_1, M_2, M_{21}, M_{22}$ be $R$-modules. Given linear isomorphisms $e_1: M_1 \simeq_R M_2$ and $e_2: M_{21} \simeq_R M_{22}$, the inverse of the induced linear isomorphism $\text{arrowCongr}(e_1, e_2)$ between the spaces of linear maps $(M_1 \to_R M_{21})$ and $(M_2 \to_R M_{22})$ satisfies the following property: for any linear map $f: M_2 \to_R M_{22}$ and any $x \in M_1$, we have \[ (\text{arrowCongr}(e_1, e_2))^{-1}(f)(x) = e_2^{-1}(f(e_1(x))). \]

LinearEquiv.arrowCongr_comp theorem

 {N N₂ N₃ : Sort _} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N] [Module R N₂] [Module R N₃]
  (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
  arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f)

Full source

theorem arrowCongr_comp {N N₂ N₃ : Sort _} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃]
    [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃)
    (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
    arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) := by
  ext
  simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

Compatibility of Linear Map Composition with Induced Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $M, M_2, M_3, N, N_2, N_3$ be $R$-modules. Given linear isomorphisms $e_1: M \simeq_R N$, $e_2: M_2 \simeq_R N_2$, and $e_3: M_3 \simeq_R N_3$, and linear maps $f: M \to_R M_2$ and $g: M_2 \to_R M_3$, the following equality holds: \[ \text{arrowCongr}(e_1, e_3)(g \circ f) = \text{arrowCongr}(e_2, e_3)(g) \circ \text{arrowCongr}(e_1, e_2)(f). \] Here, $\text{arrowCongr}(e_i, e_j)$ denotes the linear isomorphism between spaces of linear maps induced by $e_i$ and $e_j$.

LinearEquiv.arrowCongr_trans theorem

 {M₁ M₂ M₃ N₁ N₂ N₃ : Sort _} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃]
  [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃]
  (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
  (arrowCongr e₁ e₂).trans (arrowCongr e₃ e₄) = arrowCongr (e₁.trans e₃) (e₂.trans e₄)

Full source

theorem arrowCongr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort _} [AddCommMonoid M₁] [Module R M₁]
    [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁]
    [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃]
    (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
    (arrowCongr e₁ e₂).trans (arrowCongr e₃ e₄) = arrowCongr (e₁.trans e₃) (e₂.trans e₄) :=
  rfl

Composition of Induced Linear Isomorphisms on Linear Map Spaces

Informal description

Let $R$ be a commutative semiring, and let $M_1, M_2, M_3$ and $N_1, N_2, N_3$ be $R$-modules. Given linear isomorphisms $e_1: M_1 \simeq_R M_2$, $e_2: N_1 \simeq_R N_2$, $e_3: M_2 \simeq_R M_3$, and $e_4: N_2 \simeq_R N_3$, the composition of the induced linear isomorphisms $\text{arrowCongr}(e_1, e_2)$ and $\text{arrowCongr}(e_3, e_4)$ between the respective linear map spaces is equal to the linear isomorphism $\text{arrowCongr}(e_1 \circ e_3, e_2 \circ e_4)$.

LinearEquiv.congrRight definition

(f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃

Full source

/-- If `M₂` and `M₃` are linearly isomorphic then the two spaces of linear maps from `M` into `M₂`
and `M` into `M₃` are linearly isomorphic. -/
def congrRight (f : M₂ ≃ₗ[R] M₃) : (M →ₗ[R] M₂) ≃ₗ[R] M →ₗ[R] M₃ :=
  arrowCongr (LinearEquiv.refl R M) f

Linear isomorphism between linear map spaces induced by codomain isomorphism

Informal description

Given a commutative semiring $R$ and modules $M$, $M_2$, $M_3$ over $R$, any linear isomorphism $f : M_2 \simeq_R M_3$ induces a linear isomorphism between the spaces of linear maps $(M \to_R M_2)$ and $(M \to_R M_3)$. This isomorphism maps a linear map $g : M \to_R M_2$ to the composition $f \circ g : M \to_R M_3$.

LinearEquiv.conj definition

(e : M ≃ₗ[R] M₂) : Module.End R M ≃ₗ[R] Module.End R M₂

Full source

/-- If `M` and `M₂` are linearly isomorphic then the two spaces of linear maps from `M` and `M₂` to
themselves are linearly isomorphic.

See `LinearEquiv.conjRingEquiv` for the isomorphism between endomorphism rings,
which works over a not necessarily commutative semiring. -/
-- TODO: upgrade to AlgEquiv (but this file currently cannot import AlgEquiv)
def conj (e : M ≃ₗ[R] M₂) : Module.EndModule.End R M ≃ₗ[R] Module.End R M₂ :=
  arrowCongr e e

Conjugation of endomorphisms by a linear isomorphism

Informal description

Given a commutative semiring $R$ and modules $M$, $M_2$ over $R$, any linear isomorphism $e : M \simeq_R M_2$ induces a linear isomorphism between the endomorphism rings $\text{End}_R(M)$ and $\text{End}_R(M_2)$. This isomorphism maps an endomorphism $f \in \text{End}_R(M)$ to the composition $e \circ f \circ e^{-1} \in \text{End}_R(M_2)$.

LinearEquiv.conj_apply theorem

 (e : M ≃ₗ[R] M₂) (f : Module.End R M) : e.conj f = ((↑e : M →ₗ[R] M₂).comp f).comp (e.symm : M₂ →ₗ[R] M)

Full source

theorem conj_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M) :
    e.conj f = ((↑e : M →ₗ[R] M₂).comp f).comp (e.symm : M₂ →ₗ[R] M) :=
  rfl

Conjugation Formula for Linear Endomorphisms via Linear Isomorphism

Informal description

Given a commutative semiring $R$ and modules $M$, $M_2$ over $R$, for any linear isomorphism $e : M \simeq_R M_2$ and any endomorphism $f \in \text{End}_R(M)$, the conjugation of $f$ by $e$ is equal to the composition $e \circ f \circ e^{-1}$ as a linear map from $M_2$ to $M_2$.

LinearEquiv.conj_apply_apply theorem

(e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) : e.conj f x = e (f (e.symm x))

Full source

theorem conj_apply_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) :
    e.conj f x = e (f (e.symm x)) :=
  rfl

Evaluation of Conjugated Endomorphism via Linear Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$ and $M_2$ be modules over $R$. Given a linear isomorphism $e : M \simeq_R M_2$, an endomorphism $f \in \text{End}_R(M)$, and an element $x \in M_2$, the conjugation of $f$ by $e$ evaluated at $x$ satisfies: \[ e_{\text{conj}}(f)(x) = e(f(e^{-1}(x))) \]

LinearEquiv.symm_conj_apply theorem

 (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) : e.symm.conj f = ((↑e.symm : M₂ →ₗ[R] M).comp f).comp (e : M →ₗ[R] M₂)

Full source

theorem symm_conj_apply (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) :
    e.symm.conj f = ((↑e.symm : M₂ →ₗ[R] M).comp f).comp (e : M →ₗ[R] M₂) :=
  rfl

Conjugation Formula for Linear Endomorphisms via Inverse Linear Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$ and $M_2$ be modules over $R$. For any linear isomorphism $e : M \simeq_R M_2$ and any endomorphism $f \in \text{End}_R(M_2)$, the conjugation of $f$ by the inverse isomorphism $e^{-1}$ is equal to the composition $e^{-1} \circ f \circ e$ as a linear map from $M$ to $M$.

LinearEquiv.conj_comp theorem

(e : M ≃ₗ[R] M₂) (f g : Module.End R M) : e.conj (g.comp f) = (e.conj g).comp (e.conj f)

Full source

theorem conj_comp (e : M ≃ₗ[R] M₂) (f g : Module.End R M) :
    e.conj (g.comp f) = (e.conj g).comp (e.conj f) :=
  arrowCongr_comp e e e f g

Compatibility of Endomorphism Composition with Conjugation by Linear Isomorphism

Informal description

Let $R$ be a commutative semiring and let $M$ and $M_2$ be $R$-modules. Given a linear isomorphism $e : M \simeq_R M_2$ and endomorphisms $f, g \in \text{End}_R(M)$, the following equality holds: \[ e_{\text{conj}}(g \circ f) = e_{\text{conj}}(g) \circ e_{\text{conj}}(f), \] where $e_{\text{conj}}$ denotes the conjugation by $e$, mapping an endomorphism $h \in \text{End}_R(M)$ to $e \circ h \circ e^{-1} \in \text{End}_R(M_2)$.

LinearEquiv.conj_trans theorem

(e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : e₁.conj.trans e₂.conj = (e₁.trans e₂).conj

Full source

theorem conj_trans (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :
    e₁.conj.trans e₂.conj = (e₁.trans e₂).conj :=
  rfl

Transitivity of Conjugation by Linear Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $M$, $M_2$, and $M_3$ be modules over $R$. Given linear isomorphisms $e_1: M \simeq_R M_2$ and $e_2: M_2 \simeq_R M_3$, the composition of the induced conjugation maps $e_1.\text{conj} \circ e_2.\text{conj}$ on the endomorphism rings is equal to the conjugation map induced by the composition $e_1 \circ e_2$. That is, the following diagram commutes: \[ \text{End}_R(M) \xrightarrow{e_1.\text{conj}} \text{End}_R(M_2) \xrightarrow{e_2.\text{conj}} \text{End}_R(M_3) = \text{End}_R(M) \xrightarrow{(e_1 \circ e_2).\text{conj}} \text{End}_R(M_3) \]

LinearEquiv.conj_id theorem

(e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id

Full source

@[simp]
theorem conj_id (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id := by
  ext
  simp [conj_apply]

Conjugation of Identity Endomorphism by Linear Isomorphism Yields Identity

Informal description

Let $R$ be a commutative semiring, and let $M$ and $M_2$ be modules over $R$. For any $R$-linear isomorphism $e : M \simeq_R M_2$, the conjugation of the identity endomorphism $\text{id}_M \in \text{End}_R(M)$ by $e$ equals the identity endomorphism $\text{id}_{M_2} \in \text{End}_R(M_2)$. That is, $e \circ \text{id}_M \circ e^{-1} = \text{id}_{M_2}$.

LinearEquiv.conj_refl theorem

(f : Module.End R M) : (refl R M).conj f = f

Full source

@[simp]
theorem conj_refl (f : Module.End R M) : (refl R M).conj f = f := rfl

Conjugation by Identity Equivalence Preserves Endomorphism

Informal description

For any endomorphism $f$ of an $R$-module $M$, the conjugation of $f$ by the identity linear equivalence $\text{refl}_R M$ equals $f$ itself, i.e., $(\text{refl}_R M).\text{conj}(f) = f$.

LinearEquiv.congrLeft definition

 {R} (S) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R S M]
  (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] (M₃ →ₗ[R] M)

Full source

/-- An `R`-linear isomorphism between two `R`-modules `M₂` and `M₃` induces an `S`-linear
isomorphism between `M₂ →ₗ[R] M` and `M₃ →ₗ[R] M`, if `M` is both an `R`-module and an
`S`-module and their actions commute. -/
def congrLeft {R} (S) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M]
    [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] (M₃ →ₗ[R] M) where
  __ := e.arrowCongrAddEquiv (.refl ..)
  map_smul' _ _ := rfl

Induced linear isomorphism between linear map spaces via domain isomorphism

Informal description

Given a semiring $R$ and a semiring $S$, modules $M_2$, $M_3$, and $M$ over $R$, and a module structure of $M$ over $S$ where the actions of $R$ and $S$ on $M$ commute, any $R$-linear isomorphism $e : M_2 \simeq_R M_3$ induces an $S$-linear isomorphism between the spaces of $R$-linear maps $(M_2 \to_R M)$ and $(M_3 \to_R M)$. Specifically, the isomorphism maps a linear map $f : M_2 \to_R M$ to the composition $f \circ e^{-1} : M_3 \to_R M$, and its inverse maps $g : M_3 \to_R M$ to $g \circ e : M_2 \to_R M$.

LinearEquiv.smulOfNeZero definition

(a : K) (ha : a ≠ 0) : M ≃ₗ[K] M

Full source

/-- Multiplying by a nonzero element `a` of the field `K` is a linear equivalence. -/
@[simps!]
def smulOfNeZero (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M :=
  smulOfUnit <| Units.mk0 a ha

Linear equivalence induced by scalar multiplication with a nonzero element

Informal description

For any nonzero element $ a $ of the field $ K $, the function `LinearEquiv.smulOfNeZero` constructs a linear equivalence $ M \simeq_K M $ by scalar multiplication by $ a $. This equivalence preserves both the additive and scalar multiplicative structures of the $ K $-module $ M $.

Equiv.toLinearEquiv definition

(e : M ≃ M₂) (h : IsLinearMap R (e : M → M₂)) : M ≃ₗ[R] M₂

Full source

/-- An equivalence whose underlying function is linear is a linear equivalence. -/
def toLinearEquiv (e : M ≃ M₂) (h : IsLinearMap R (e : M → M₂)) : M ≃ₗ[R] M₂ :=
  { e, h.mk' e with }

Linear equivalence induced by a bijective linear map

Informal description

Given a bijection $e : M \simeq M_2$ between modules $M$ and $M_2$ over a semiring $R$, if the underlying function of $e$ is $R$-linear, then $e$ can be promoted to a linear equivalence $M \simeq_R M_2$.

LinearMap.funLeft definition

(f : m → n) : (n → M) →ₗ[R] m → M

Full source

/-- Given an `R`-module `M` and a function `m → n` between arbitrary types,
construct a linear map `(n → M) →ₗ[R] (m → M)` -/
def funLeft (f : m → n) : (n → M) →ₗ[R] m → M where
  toFun := (· ∘ f)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear map induced by precomposition with a function

Informal description

Given a semiring $R$, an $R$-module $M$, and a function $f : m \to n$ between arbitrary types, the linear map $\text{funLeft}_R^M f : (n \to M) \to (m \to M)$ is defined by composition with $f$, i.e., $(\text{funLeft}_R^M f)(g) = g \circ f$ for any $g : n \to M$. This map is linear in the sense that it preserves addition and scalar multiplication.

LinearMap.funLeft_apply theorem

(f : m → n) (g : n → M) (i : m) : funLeft R M f g i = g (f i)

Full source

@[simp]
theorem funLeft_apply (f : m → n) (g : n → M) (i : m) : funLeft R M f g i = g (f i) :=
  rfl

Evaluation of Linear Map Induced by Precomposition

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any function $f : m \to n$ and any function $g : n \to M$, the linear map $\text{funLeft}_R^M f$ satisfies $(\text{funLeft}_R^M f)(g)(i) = g(f(i))$ for all $i \in m$.

LinearMap.funLeft_id theorem

(g : n → M) : funLeft R M _root_.id g = g

Full source

@[simp]
theorem funLeft_id (g : n → M) : funLeft R M _root_.id g = g :=
  rfl

Identity Function Preserved under $\text{funLeft}_R^M$

Informal description

For any function $g : n \to M$ where $M$ is an $R$-module, the linear map $\text{funLeft}_R^M \text{id}$ acts as the identity, i.e., $\text{funLeft}_R^M \text{id}(g) = g$.

LinearMap.funLeft_comp theorem

(f₁ : n → p) (f₂ : m → n) : funLeft R M (f₁ ∘ f₂) = (funLeft R M f₂).comp (funLeft R M f₁)

Full source

theorem funLeft_comp (f₁ : n → p) (f₂ : m → n) :
    funLeft R M (f₁ ∘ f₂) = (funLeft R M f₂).comp (funLeft R M f₁) :=
  rfl

Composition of Linear Maps Induced by Function Composition

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any functions $f_1 : n \to p$ and $f_2 : m \to n$, the linear map $\text{funLeft}_R^M (f_1 \circ f_2)$ is equal to the composition of the linear maps $\text{funLeft}_R^M f_2$ and $\text{funLeft}_R^M f_1$, i.e., \[ \text{funLeft}_R^M (f_1 \circ f_2) = (\text{funLeft}_R^M f_2) \circ (\text{funLeft}_R^M f_1). \]

LinearMap.funLeft_surjective_of_injective theorem

(f : m → n) (hf : Injective f) : Surjective (funLeft R M f)

Full source

theorem funLeft_surjective_of_injective (f : m → n) (hf : Injective f) :
    Surjective (funLeft R M f) :=
  hf.surjective_comp_right

Surjectivity of Precomposition-Induced Linear Map via Injective Function

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any injective function $f : m \to n$ between arbitrary types, the linear map $\text{funLeft}_R^M f : (n \to M) \to (m \to M)$ defined by precomposition with $f$ is surjective. That is, for any linear map $g : m \to M$, there exists a linear map $h : n \to M$ such that $h \circ f = g$.

LinearMap.funLeft_injective_of_surjective theorem

(f : m → n) (hf : Surjective f) : Injective (funLeft R M f)

Full source

theorem funLeft_injective_of_surjective (f : m → n) (hf : Surjective f) :
    Injective (funLeft R M f) :=
  hf.injective_comp_right

Injectivity of Precomposition-Induced Linear Map via Surjective Function

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any surjective function $f : m \to n$ between arbitrary types, the induced linear map $\text{funLeft}_R^M f : (n \to M) \to (m \to M)$ defined by precomposition with $f$ is injective.

LinearEquiv.funCongrLeft definition

(e : m ≃ n) : (n → M) ≃ₗ[R] m → M

Full source

/-- Given an `R`-module `M` and an equivalence `m ≃ n` between arbitrary types,
construct a linear equivalence `(n → M) ≃ₗ[R] (m → M)` -/
def funCongrLeft (e : m ≃ n) : (n → M) ≃ₗ[R] m → M :=
  LinearEquiv.ofLinear (funLeft R M e) (funLeft R M e.symm)
    (LinearMap.ext fun x ↦
      funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id])
    (LinearMap.ext fun x ↦
      funext fun i ↦ by rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id])

Linear equivalence induced by type equivalence via precomposition

Informal description

Given a semiring $R$, an $R$-module $M$, and an equivalence $e : m \simeq n$ between arbitrary types, the linear equivalence $\text{funCongrLeft}_R^M e : (n \to M) \simeq_{R} (m \to M)$ is constructed by precomposition with $e$ and its inverse. Specifically, it maps a function $f : n \to M$ to $f \circ e : m \to M$, and its inverse maps $g : m \to M$ to $g \circ e^{-1} : n \to M$.

LinearEquiv.funCongrLeft_apply theorem

(e : m ≃ n) (x : n → M) : funCongrLeft R M e x = funLeft R M e x

Full source

@[simp]
theorem funCongrLeft_apply (e : m ≃ n) (x : n → M) : funCongrLeft R M e x = funLeft R M e x :=
  rfl

Application of Linear Equivalence Induced by Type Equivalence via Precomposition

Informal description

Given a semiring $R$, an $R$-module $M$, and a type equivalence $e : m \simeq n$, the linear equivalence $\text{funCongrLeft}_R^M e$ applied to a function $x : n \to M$ is equal to the linear map $\text{funLeft}_R^M e$ applied to $x$. That is, $(\text{funCongrLeft}_R^M e)(x) = x \circ e$.

LinearEquiv.funCongrLeft_id theorem

: funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)

Full source

@[simp]
theorem funCongrLeft_id : funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M) :=
  rfl

Identity Equivalence Yields Identity Linear Equivalence under $\text{funCongrLeft}$

Informal description

For any semiring $R$ and $R$-module $M$, the linear equivalence $\text{funCongrLeft}_R^M$ applied to the identity equivalence $\text{refl}_n$ on a type $n$ yields the identity linear equivalence on the function space $n \to M$. That is, \[ \text{funCongrLeft}_R^M (\text{refl}_n) = \text{id}_{R, n \to M}, \] where $\text{id}_{R, n \to M}$ denotes the identity linear equivalence on $n \to M$ over $R$.

LinearEquiv.funCongrLeft_comp theorem

 (e₁ : m ≃ n) (e₂ : n ≃ p) :
  funCongrLeft R M (Equiv.trans e₁ e₂) = LinearEquiv.trans (funCongrLeft R M e₂) (funCongrLeft R M e₁)

Full source

@[simp]
theorem funCongrLeft_comp (e₁ : m ≃ n) (e₂ : n ≃ p) :
    funCongrLeft R M (Equiv.trans e₁ e₂) =
      LinearEquiv.trans (funCongrLeft R M e₂) (funCongrLeft R M e₁) :=
  rfl

Composition of Linear Equivalences Induced by Type Equivalences via Precomposition

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. Given two equivalences $e₁ : m \simeq n$ and $e₂ : n \simeq p$, the linear equivalence $\text{funCongrLeft}_R^M (e₂ \circ e₁)$ is equal to the composition of the linear equivalences $\text{funCongrLeft}_R^M e₂$ and $\text{funCongrLeft}_R^M e₁$. That is, the following diagram commutes: \[ (n \to M) \simeq_{R} (m \to M) \quad \text{via} \quad \text{funCongrLeft}_R^M e₁ \] \[ (p \to M) \simeq_{R} (n \to M) \quad \text{via} \quad \text{funCongrLeft}_R^M e₂ \] \[ (p \to M) \simeq_{R} (m \to M) \quad \text{via} \quad \text{funCongrLeft}_R^M (e₂ \circ e₁) \]

LinearEquiv.funCongrLeft_symm theorem

(e : m ≃ n) : (funCongrLeft R M e).symm = funCongrLeft R M e.symm

Full source

@[simp]
theorem funCongrLeft_symm (e : m ≃ n) : (funCongrLeft R M e).symm = funCongrLeft R M e.symm :=
  rfl

Inverse of Linear Precomposition Equivalence via Type Equivalence

Informal description

For any semiring $R$, $R$-module $M$, and equivalence $e : m \simeq n$ between types, the inverse of the linear equivalence $\text{funCongrLeft}_R^M e : (n \to M) \simeq_{R} (m \to M)$ is equal to the linear equivalence $\text{funCongrLeft}_R^M e^{-1} : (m \to M) \simeq_{R} (n \to M)$ induced by the inverse equivalence $e^{-1} : n \simeq m$.

LinearEquiv.sumPiEquivProdPi definition

 (R : Type*) [Semiring R] (S T : Type*) (A : S ⊕ T → Type*) [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
  (Π (st : S ⊕ T), A st) ≃ₗ[R] (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t))

Full source

/-- The product over `S ⊕ T` of a family of modules is isomorphic to the product of
(the product over `S`) and (the product over `T`).

This is `Equiv.sumPiEquivProdPi` as a `LinearEquiv`.
-/
@[simps -fullyApplied +simpRhs]
def sumPiEquivProdPi (R : Type*) [Semiring R] (S T : Type*) (A : S ⊕ T → Type*)
    [∀ st, AddCommMonoid (A st)] [∀ st, Module R (A st)] :
    (Π (st : S ⊕ T), A st) ≃ₗ[R] (Π (s : S), A (.inl s)) × (Π (t : T), A (.inr t)) where
  __ := Equiv.sumPiEquivProdPi _
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear equivalence between dependent functions on a sum type and product of dependent functions

Informal description

Given a semiring $R$, types $S$ and $T$, and a family of $R$-modules $(A_{st})_{st \in S \oplus T}$, the space of dependent functions $\prod_{st \in S \oplus T} A_{st}$ is linearly isomorphic to the product space $\left(\prod_{s \in S} A_{\text{inl}(s)}\right) \times \left(\prod_{t \in T} A_{\text{inr}(t)}\right)$. Here, $\text{inl}$ and $\text{inr}$ are the left and right inclusion maps into the sum type $S \oplus T$. This is the linear equivalence version of the equivalence `Equiv.sumPiEquivProdPi`.

LinearEquiv.piUnique definition

 {α : Type*} [Unique α] (R : Type*) [Semiring R] (f : α → Type*) [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] :
  (Π t : α, f t) ≃ₗ[R] f default

Full source

/-- The product `Π t : α, f t` of a family of modules is linearly isomorphic to the module
`f ⬝` when `α` only contains `⬝`.

This is `Equiv.piUnique` as a `LinearEquiv`.
-/
@[simps -fullyApplied]
def piUnique {α : Type*} [Unique α] (R : Type*) [Semiring R] (f : α → Type*)
    [∀ x, AddCommMonoid (f x)] [∀ x, Module R (f x)] : (Π t : α, f t) ≃ₗ[R] f default where
  __ := Equiv.piUnique _
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear equivalence between product of modules over a unique type and the module at the default element

Informal description

Given a type $\alpha$ with a unique element, a semiring $R$, and a family of $R$-modules $(f_t)_{t \in \alpha}$, the product module $\prod_{t \in \alpha} f_t$ is linearly isomorphic to the module $f_{\text{default}}$ (where $\text{default}$ is the unique element of $\alpha$). This isomorphism maps a dependent function $g \in \prod_{t \in \alpha} f_t$ to its value at the default element $g(\text{default})$, and conversely, any element $x \in f_{\text{default}}$ can be extended to a constant function in $\prod_{t \in \alpha} f_t$ with value $x$. The isomorphism preserves addition and scalar multiplication.