Mathlib.Algebra.Module.LinearMap.Defs

IsLinearMap structure

 (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
  (f : M → M₂)

Full source

/-- A map `f` between modules over a semiring is linear if it satisfies the two properties
`f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this
property. A bundled version is available with `LinearMap`, and should be favored over
`IsLinearMap` most of the time. -/
structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M]
  [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) : Prop where
  /-- A linear map preserves addition. -/
  map_add : ∀ x y, f (x + y) = f x + f y
  /-- A linear map preserves scalar multiplication. -/
  map_smul : ∀ (c : R) (x), f (c • x) = c • f x

Linear map predicate

Informal description

Given a semiring $R$ and modules $M$ and $M₂$ over $R$, a function $f \colon M \to M₂$ is called a linear map if it satisfies the following two properties: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Homogeneity: $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in M$ This predicate `IsLinearMap R f` captures these properties for an unbundled function $f$.

LinearMap structure

{R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*)
    (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
    AddHom M M₂, MulActionHom σ M M₂

Full source

/-- A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. -/
structure LinearMap {R S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type*)
    (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
    AddHom M M₂, MulActionHom σ M M₂

Semilinear map

Informal description

A semilinear map between an $R$-module $M$ and an $S$-module $M₂$ with respect to a ring homomorphism $\sigma \colon R \to S$ is a map $f \colon M \to M₂$ that satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Semilinearity: $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in R$ and $x \in M$ When $\sigma$ is the identity ring homomorphism, this reduces to the definition of a linear map between $R$-modules.

term_→ₛₗ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →ₛₗ[σ] N` is the type of `σ`-semilinear maps from `M` to `N`. -/
notation:25 M " →ₛₗ[" σ:25 "] " M₂:0 => LinearMap σ M M₂

Semilinear map notation

Informal description

The notation $ M \to_{s\ell}[\sigma] N $ denotes the type of $\sigma$-semilinear maps from $ M $ to $ N $, where $\sigma$ is a ring homomorphism. These maps satisfy the property $ f(c \cdot x) = \sigma(c) \cdot f(x) $ for all $ c $ in the base ring and $ x $ in $ M $.

term_→ₗ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `M →ₗ[R] N` is the type of `R`-linear maps from `M` to `N`. -/
notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂

Notation for $ R $-linear maps

Informal description

The notation $ M \to_{\ell}[R] N $ denotes the type of $ R $-linear maps from $ M $ to $ N $, where $ R $ is a ring and $ M $ and $ N $ are modules over $ R $. A linear map $ f \colon M \to_{\ell}[R] N $ satisfies $ f(a \cdot x + y) = a \cdot f(x) + f(y) $ for all $ a \in R $ and $ x, y \in M $.

SemilinearMapClass structure

(F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
    (σ : outParam (R →+* S)) (M M₂ : outParam Type*) [AddCommMonoid M] [AddCommMonoid M₂]
    [Module R M] [Module S M₂] [FunLike F M M₂] : Prop
    extends AddHomClass F M M₂, MulActionSemiHomClass F σ M M₂

Full source

/-- `SemilinearMapClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`.

See also `LinearMapClass F R M M₂` for the case where `σ` is the identity map on `R`.

A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. -/
class SemilinearMapClass (F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
    (σ : outParam (R →+* S)) (M M₂ : outParam Type*) [AddCommMonoid M] [AddCommMonoid M₂]
    [Module R M] [Module S M₂] [FunLike F M M₂] : Prop
    extends AddHomClass F M M₂, MulActionSemiHomClass F σ M M₂

Class of σ-Semilinear Maps

Informal description

The class `SemilinearMapClass F σ M M₂` asserts that `F` is a type of bundled `σ`-semilinear maps from `M` to `M₂`, where `σ : R →+* S` is a ring homomorphism. A map `f : M → M₂` is `σ`-semilinear if it satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Semilinearity: $f(r \bullet x) = (\sigma r) \bullet f(x)$ for all $r \in R$ and $x \in M$ Here, `M` is an `R`-module and `M₂` is an `S`-module. When `σ` is the identity map, this reduces to the case of ordinary linear maps.

LinearMapClass abbrev

 (F : Type*) (R : outParam Type*) (M M₂ : Type*) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]
  [Module R M₂] [FunLike F M M₂]

Full source

/-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`.

This is an abbreviation for `SemilinearMapClass F (RingHom.id R) M M₂`.
-/
abbrev LinearMapClass (F : Type*) (R : outParam Type*) (M M₂ : Type*)
    [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂]
    [FunLike F M M₂] :=
  SemilinearMapClass F (RingHom.id R) M M₂

Class of $R$-Linear Maps

Informal description

The class `LinearMapClass F R M M₂` asserts that `F` is a type of bundled $R$-linear maps from $M$ to $M₂$, where $M$ and $M₂$ are modules over a semiring $R$. A map $f \in F$ satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Linearity: $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in M$ Here, $M$ and $M₂$ are additive commutative monoids equipped with compatible scalar multiplication operations from $R$.

LinearMapClass.map_smul theorem

 {R M M₂ : outParam Type*} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type*}
  [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) : f (r • x) = r • f x

Full source

protected lemma LinearMapClass.map_smul {R M M₂ : outParam Type*} [Semiring R] [AddCommMonoid M]
    [AddCommMonoid M₂] [Module R M] [Module R M₂]
    {F : Type*} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) :
    f (r • x) = r • f x := by rw [map_smul]

Linearity Property of $R$-Linear Maps: $f(r \cdot x) = r \cdot f(x)$

Informal description

Let $R$ be a semiring, and let $M$ and $M₂$ be $R$-modules. For any $R$-linear map $f \colon M \to M₂$ (i.e., $f \in F$ where $F$ is a type of linear maps), scalar $r \in R$, and element $x \in M$, the map $f$ satisfies the linearity property: \[ f(r \cdot x) = r \cdot f(x). \]

SemilinearMapClass.instAddMonoidHomClass instance

[FunLike F M M₃] [SemilinearMapClass F σ M M₃] : AddMonoidHomClass F M M₃

Full source

instance (priority := 100) instAddMonoidHomClass [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
    AddMonoidHomClass F M M₃ :=
  { SemilinearMapClass.toAddHomClass with
    map_zero := fun f ↦
      show f 0 = 0 by
        rw [← zero_smul R (0 : M), map_smulₛₗ]
        simp }

$\sigma$-Semilinear Maps as Additive Monoid Homomorphisms

Informal description

For any type $F$ of $\sigma$-semilinear maps between modules $M$ and $M_3$ (where $\sigma: R \to S$ is a ring homomorphism), the elements of $F$ naturally form an additive monoid homomorphism class. This means every $\sigma$-semilinear map preserves addition and zero, satisfying $f(x + y) = f(x) + f(y)$ and $f(0) = 0$ for all $x, y \in M$.

SemilinearMapClass.distribMulActionSemiHomClass instance

[FunLike F M M₃] [SemilinearMapClass F σ M M₃] : DistribMulActionSemiHomClass F σ M M₃

Full source

instance (priority := 100) distribMulActionSemiHomClass
    [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
    DistribMulActionSemiHomClass F σ M M₃ :=
  { SemilinearMapClass.toAddHomClass with
    map_smulₛₗ := fun f c x ↦ by rw [map_smulₛₗ] }

$\sigma$-Semilinear Maps as Equivariant Distributive Action Homomorphisms

Informal description

For any type $F$ of $\sigma$-semilinear maps between modules $M$ and $M_3$ (where $\sigma: R \to S$ is a ring homomorphism), the elements of $F$ naturally form a class of equivariant additive monoid homomorphisms with distributive actions. This means every $\sigma$-semilinear map preserves addition and scalar multiplication, satisfying $f(x + y) = f(x) + f(y)$ and $f(r \cdot x) = (\sigma r) \cdot f(x)$ for all $x, y \in M$ and $r \in R$.

SemilinearMapClass.map_smul_inv theorem

{σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x)

Full source

theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
    c • f x = f (σ' c • x) := by simp [map_smulₛₗ _]

Inverse Scalar Multiplication Property for Semilinear Maps

Informal description

Let $F$ be a type of $\sigma$-semilinear maps from an $R$-module $M$ to an $S$-module $M_3$, where $\sigma: R \to S$ is a ring homomorphism. Given a ring homomorphism $\sigma': S \to R$ such that $\sigma$ and $\sigma'$ form a ring homomorphism inverse pair, then for any scalar $c \in S$ and any element $x \in M$, we have $c \bullet f(x) = f(\sigma'(c) \bullet x)$.

SemilinearMapClass.semilinearMap definition

: M →ₛₗ[σ] M₃

Full source

/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
@[coe]
def semilinearMap : M →ₛₗ[σ] M₃ where
  toFun := f
  map_add' := map_add f
  map_smul' := map_smulₛₗ f

Conversion to σ-semilinear map

Informal description

Given a type `F` of σ-semilinear maps between modules `M` and `M₃`, where `σ : R →+* S` is a ring homomorphism, the function `semilinearMap` converts an element `f : F` into an explicit σ-semilinear map `M →ₛₗ[σ] M₃`. This map satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Semilinearity: $f(r \cdot x) = (\sigma r) \cdot f(x)$ for all $r \in R$ and $x \in M$

SemilinearMapClass.instCoeToSemilinearMap instance

: CoeHead F (M →ₛₗ[σ] M₃)

Full source

/-- Reinterpret an element of a type of semilinear maps as a semilinear map. -/
instance instCoeToSemilinearMap : CoeHead F (M →ₛₗ[σ] M₃) where
  coe f := semilinearMap f

Canonical Interpretation of Semilinear Map Elements as Bundled Maps

Informal description

For any type `F` of σ-semilinear maps between modules `M` and `M₃` with respect to a ring homomorphism `σ : R →+* S`, there is a canonical way to interpret an element of `F` as a bundled σ-semilinear map `M →ₛₗ[σ] M₃`.

LinearMapClass.linearMap abbrev

: M₁ →ₗ[R] M₂

Full source

/-- Reinterpret an element of a type of linear maps as a linear map. -/
abbrev linearMap : M₁ →ₗ[R] M₂ := SemilinearMapClass.semilinearMap f

Conversion to $R$-Linear Map

Informal description

Given a type `F` of $R$-linear maps between modules `M₁` and `M₂` over a semiring `R`, the function `linearMap` converts an element `f : F` into an explicit $R$-linear map `M₁ →ₗ[R] M₂`. This map satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M₁$ 2. Linearity: $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in M₁$

LinearMapClass.instCoeToLinearMap instance

: CoeHead F (M₁ →ₗ[R] M₂)

Full source

/-- Reinterpret an element of a type of linear maps as a linear map. -/
instance instCoeToLinearMap : CoeHead F (M₁ →ₗ[R] M₂) where
  coe f := SemilinearMapClass.semilinearMap f

CoeToLinearMap: CoeHead for Linear Maps

Informal description

For any type $F$ of $R$-linear maps between modules $M₁$ and $M₂$, there is a canonical way to interpret an element of $F$ as a linear map $M₁ →ₗ[R] M₂$.

LinearMap.instFunLike instance

: FunLike (M →ₛₗ[σ] M₃) M M₃

Full source

instance instFunLike : FunLike (M →ₛₗ[σ] M₃) M M₃ where
  coe f := f.toFun
  coe_injective' f g h := by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective'
    exact h

Semilinear Maps as Functions

Informal description

For any semilinear map $f : M \to_{σ} M₃$ between modules, $f$ can be treated as a function from $M$ to $M₃$.

LinearMap.semilinearMapClass instance

: SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃

Full source

instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ where
  map_add f := f.map_add'
  map_smulₛₗ := LinearMap.map_smul'

Class of Semilinear Maps

Informal description

The collection of $\sigma$-semilinear maps $M \to_{\sigma} M_3$ forms a class of semilinear maps with respect to the ring homomorphism $\sigma \colon R \to S$, where $M$ is an $R$-module and $M_3$ is an $S$-module. This means that every such map $f$ satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Semilinearity: $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all $r \in R$ and $x \in M$

LinearMap.coe_coe theorem

{F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} : ⇑(f : M →ₛₗ[σ] M₃) = f

Full source

@[simp, norm_cast]
lemma coe_coe {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} :
    ⇑(f : M →ₛₗ[σ] M₃) = f :=
  rfl

Coercion of Semilinear Maps to Functions is Identity

Informal description

For any type `F` of σ-semilinear maps between modules `M` and `M₃` (where `σ : R →+* S` is a ring homomorphism), and for any `f : F`, the underlying function of the explicit σ-semilinear map `f : M →ₛₗ[σ] M₃` is equal to `f` itself.

LinearMap.toDistribMulActionHom definition

(f : M →ₛₗ[σ] M₃) : DistribMulActionHom σ.toMonoidHom M M₃

Full source

/-- The `DistribMulActionHom` underlying a `LinearMap`. -/
def toDistribMulActionHom (f : M →ₛₗ[σ] M₃) : DistribMulActionHom σ.toMonoidHom M M₃ :=
  { f with map_zero' := show f 0 = 0 from map_zero f }

Underlying equivariant additive monoid homomorphism of a semilinear map

Informal description

Given a semilinear map $ f \colon M \to M₃ $ with respect to a ring homomorphism $ \sigma \colon R \to S $, the underlying `DistribMulActionHom` is obtained by viewing $ f $ as an equivariant additive monoid homomorphism with respect to the monoid homomorphism $ \sigma $. Specifically, it preserves the additive structure (i.e., $ f(0) = 0 $ and $ f(x + y) = f(x) + f(y) $) and is $ \sigma $-equivariant (i.e., $ f(r \cdot x) = \sigma(r) \cdot f(x) $ for all $ r \in R $ and $ x \in M $).

LinearMap.coe_toAddHom theorem

(f : M →ₛₗ[σ] M₃) : ⇑f.toAddHom = f

Full source

@[simp]
theorem coe_toAddHom (f : M →ₛₗ[σ] M₃) : ⇑f.toAddHom = f := rfl

Semilinear Map Coincides with its Additive Homomorphism Component

Informal description

For any semilinear map $f \colon M \to_{σ} M₃$, the underlying additive homomorphism of $f$ is equal to $f$ itself when viewed as a function from $M$ to $M₃$.

LinearMap.toFun_eq_coe theorem

{f : M →ₛₗ[σ] M₃} : f.toFun = (f : M → M₃)

Full source

theorem toFun_eq_coe {f : M →ₛₗ[σ] M₃} : f.toFun = (f : M → M₃) := rfl

Semilinear Map Function Coincidence: $f.\text{toFun} = f$

Informal description

For any semilinear map $f \colon M \to_{\sigma} M₃$, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function from $M$ to $M₃$.

LinearMap.ext theorem

{f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Semilinear Maps

Informal description

For any two semilinear maps $f, g \colon M \to_{σ} M₃$ between modules, if $f(x) = g(x)$ for all $x \in M$, then $f = g$.

LinearMap.copy definition

(f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃

Full source

/-- Copy of a `LinearMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃ where
  toFun := f'
  map_add' := h.symm ▸ f.map_add'
  map_smul' := h.symm ▸ f.map_smul'

Copy of a semilinear map with specified function

Informal description

Given a semilinear map $f \colon M \to_{\sigma} M₃$ and a function $f' \colon M \to M₃$ that is definitionally equal to $f$, the function `LinearMap.copy` constructs a new semilinear map with $f'$ as its underlying function, while preserving the additivity and semilinearity properties of $f$. More precisely, if $f' = f$ as functions, then `LinearMap.copy f f' h` is a semilinear map that: 1. Acts as $f'$ on elements of $M$ 2. Satisfies $f'(x + y) = f'(x) + f'(y)$ for all $x, y \in M$ 3. Satisfies $f'(c \cdot x) = \sigma(c) \cdot f'(x)$ for all $c \in R$ and $x \in M$

LinearMap.coe_copy theorem

(f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Semilinear Map Equals Specified Function

Informal description

For any semilinear map $f \colon M \to_{\sigma} M₃$, function $f' \colon M \to M₃$, and proof $h$ that $f' = f$, the underlying function of the copied semilinear map $f.copy\, f'\, h$ is equal to $f'$.

LinearMap.copy_eq theorem

(f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : f.copy f' h = f

Full source

theorem copy_eq (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Semilinear Map with Identical Function Preserves Original Map

Informal description

Given a semilinear map $f \colon M \to_{\sigma} M₃$ and a function $f' \colon M \to M₃$ such that $f' = f$ as functions, the copy of $f$ with underlying function $f'$ is equal to $f$ itself.

LinearMap.coe_mk theorem

{σ : R →+* S} (f : AddHom M M₃) (h) : ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f

Full source

@[simp]
theorem coe_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f :=
  rfl

Underlying Function of Constructed Semilinear Map Equals Original Additive Homomorphism

Informal description

Given a ring homomorphism $\sigma \colon R \to S$, an additive homomorphism $f \colon M \to M₃$ between additive commutative monoids, and a proof $h$ that $f$ is $\sigma$-semilinear, the underlying function of the constructed semilinear map $\text{LinearMap.mk}\, f\, h \colon M \to_{σ} M₃$ is equal to $f$.

LinearMap.coe_addHom_mk theorem

{σ : R →+* S} (f : AddHom M M₃) (h) : ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f

Full source

@[simp]
theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f :=
  rfl

Underlying Additive Homomorphism of Constructed Semilinear Map Equals Original

Informal description

Let $R$ and $S$ be semirings with a ring homomorphism $\sigma \colon R \to S$, and let $M$ and $M₃$ be additive commutative monoids equipped with $R$-module and $S$-module structures respectively. Given an additive homomorphism $f \colon M \to M₃$ and a proof $h$ that $f$ is $\sigma$-semilinear, the underlying additive homomorphism of the constructed semilinear map $\text{LinearMap.mk}\, f\, h \colon M \to_{σ} M₃$ is equal to $f$.

LinearMap.coe_semilinearMap theorem

{F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) : ((f : M →ₛₗ[σ] M₃) : M → M₃) = f

Full source

theorem coe_semilinearMap {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
    ((f : M →ₛₗ[σ] M₃) : M → M₃) = f :=
  rfl

Coercion of σ-semilinear maps to functions is the identity

Informal description

For any type `F` of σ-semilinear maps between modules `M` and `M₃` (where `σ : R →+* S` is a ring homomorphism), and any `f : F`, the underlying function of `f` when viewed as a σ-semilinear map `M →ₛₗ[σ] M₃` is equal to `f` itself. In other words, the coercion from `F` to function type `M → M₃` via the σ-semilinear map structure is the identity.

LinearMap.toLinearMap_injective theorem

 {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
  f = g

Full source

theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃]
    {f g : F} (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) :
    f = g := by
  apply DFunLike.ext
  intro m
  exact DFunLike.congr_fun h m

Injectivity of Semilinear Map Conversion

Informal description

Let $F$ be a type of $\sigma$-semilinear maps between $R$-module $M$ and $S$-module $M₃$, where $\sigma : R \to S$ is a ring homomorphism. For any two maps $f, g \in F$, if their underlying semilinear maps are equal (i.e., $f = g$ as functions $M \to M₃$), then $f = g$ as elements of $F$.

LinearMap.id definition

: M →ₗ[R] M

Full source

/-- Identity map as a `LinearMap` -/
def id : M →ₗ[R] M :=
  { DistribMulActionHom.id R with toFun := _root_.id }

Identity linear map

Informal description

The identity map on an $R$-module $M$, viewed as a linear map from $M$ to itself. This map sends each element $x \in M$ to itself and satisfies both the additivity condition $\text{id}(x + y) = \text{id}(x) + \text{id}(y)$ and the linearity condition $\text{id}(r \cdot x) = r \cdot \text{id}(x)$ for all $x, y \in M$ and $r \in R$.

LinearMap.id_apply theorem

(x : M) : @id R M _ _ _ x = x

Full source

theorem id_apply (x : M) : @id R M _ _ _ x = x :=
  rfl

Identity Linear Map Evaluation: $\text{id}(x) = x$

Informal description

For any element $x$ in an $R$-module $M$, the identity linear map evaluated at $x$ is equal to $x$ itself, i.e., $\text{id}(x) = x$.

LinearMap.id_coe theorem

: ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id

Full source

@[simp, norm_cast]
theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id :=
  rfl

Identity Linear Map as Function

Informal description

The underlying function of the identity linear map $\text{id} \colon M \to M$ on an $R$-module $M$ is equal to the identity function on $M$.

LinearMap.id' definition

{σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M

Full source

/-- A generalisation of `LinearMap.id` that constructs the identity function
as a `σ`-semilinear map for any ring homomorphism `σ` which we know is the identity. -/
@[simps]
def id' {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M where
  toFun x := x
  map_add' _ _ := rfl
  map_smul' r x := by
    have := (RingHomId.eq_id : σ = _)
    subst this
    rfl

Identity semilinear map with respect to identity ring homomorphism

Informal description

The identity semilinear map $M \to M$ with respect to a ring homomorphism $\sigma \colon R \to R$ that is known to be the identity map. This means the map sends each $x \in M$ to itself and satisfies the semilinearity condition $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all $r \in R$ and $x \in M$, where $\sigma$ is the identity ring homomorphism.

LinearMap.id'_coe theorem

{σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id

Full source

@[simp, norm_cast]
theorem id'_coe {σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id :=
  rfl

Identity Semilinear Map as Identity Function

Informal description

For any ring homomorphism $\sigma \colon R \to R$ that is known to be the identity map, the underlying function of the identity semilinear map $\mathrm{id}' \colon M \to_{\sigma} M$ is equal to the identity function on $M$.

LinearMap.isLinear theorem

: IsLinearMap R fₗ

Full source

theorem isLinear : IsLinearMap R fₗ :=
  ⟨fₗ.map_add', fₗ.map_smul'⟩

Characterization of Linear Maps

Informal description

Let $R$ be a semiring, and let $M$ and $M₂$ be $R$-modules. A function $f \colon M \to M₂$ is a linear map if it satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. Homogeneity: $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in M$

LinearMap.coe_injective theorem

: Injective (DFunLike.coe : (M →ₛₗ[σ] M₃) → _)

Full source

theorem coe_injective : Injective (DFunLike.coe : (M →ₛₗ[σ] M₃) → _) :=
  DFunLike.coe_injective

Injectivity of the Semilinear Map to Function Coercion

Informal description

The canonical map from the type of semilinear maps $M \to_{\sigma} M_3$ to the type of functions $M \to M_3$ is injective. That is, if two semilinear maps $f, g \colon M \to_{\sigma} M_3$ satisfy $f(x) = g(x)$ for all $x \in M$, then $f = g$.

LinearMap.congr_arg theorem

{x x' : M} : x = x' → f x = f x'

Full source

protected theorem congr_arg {x x' : M} : x = x' → f x = f x' :=
  DFunLike.congr_arg f

Semilinear Maps Preserve Equality: $x = x' \implies f(x) = f(x')$

Informal description

For any semilinear map $f \colon M \to_{σ} M₃$ and elements $x, x' \in M$, if $x = x'$, then $f(x) = f(x')$.

LinearMap.congr_fun theorem

(h : f = g) (x : M) : f x = g x

Full source

/-- If two linear maps are equal, they are equal at each point. -/
protected theorem congr_fun (h : f = g) (x : M) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Semilinear Maps

Informal description

For any two semilinear maps $f, g \colon M \to M₃$ between modules, if $f = g$, then $f(x) = g(x)$ for all $x \in M$.

LinearMap.mk_coe theorem

(f : M →ₛₗ[σ] M₃) (h) : (LinearMap.mk f h : M →ₛₗ[σ] M₃) = f

Full source

@[simp]
theorem mk_coe (f : M →ₛₗ[σ] M₃) (h) : (LinearMap.mk f h : M →ₛₗ[σ] M₃) = f :=
  rfl

Construction of Semilinear Map Preserves Original Function

Informal description

For any semilinear map $f \colon M \to_{\sigma} M_3$ and any proof $h$ of its semilinearity, the constructed linear map $\text{LinearMap.mk}(f, h)$ is equal to $f$ itself.

LinearMap.map_add theorem

(x y : M) : f (x + y) = f x + f y

Full source

protected theorem map_add (x y : M) : f (x + y) = f x + f y :=
  map_add f x y

Additivity of Semilinear Maps

Informal description

For any semilinear map $f \colon M \to M_3$ between modules and any elements $x, y \in M$, the map $f$ satisfies the additive property: $f(x + y) = f(x) + f(y)$.

LinearMap.map_zero theorem

: f 0 = 0

Full source

protected theorem map_zero : f 0 = 0 :=
  map_zero f

Semilinear Maps Preserve Zero: $f(0) = 0$

Informal description

For any semilinear map $f \colon M \to M_3$ between modules, the image of the zero element is zero, i.e., $f(0) = 0$.

LinearMap.map_smulₛₗ theorem

(c : R) (x : M) : f (c • x) = σ c • f x

Full source

@[simp]
protected theorem map_smulₛₗ (c : R) (x : M) : f (c • x) = σ c • f x :=
  map_smulₛₗ f c x

Semilinearity Property: $f(c \cdot x) = \sigma(c) \cdot f(x)$

Informal description

For any semilinear map $f \colon M \to M_2$ with respect to a ring homomorphism $\sigma \colon R \to S$, and for any scalar $c \in R$ and vector $x \in M$, the map satisfies the semilinear property: $f(c \cdot x) = \sigma(c) \cdot f(x)$.

LinearMap.map_smul theorem

(c : R) (x : M) : fₗ (c • x) = c • fₗ x

Full source

protected theorem map_smul (c : R) (x : M) : fₗ (c • x) = c • fₗ x :=
  map_smul fₗ c x

Linearity Property: $f_\ell(c \cdot x) = c \cdot f_\ell(x)$

Informal description

For any linear map $f_\ell \colon M \to M$ over a semiring $R$ and any scalar $c \in R$ and element $x \in M$, the map satisfies the linearity property: \[ f_\ell(c \cdot x) = c \cdot f_\ell(x). \]

LinearMap.map_smul_inv theorem

{σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x)

Full source

protected theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
    c • f x = f (σ' c • x) := by simp

Inverse Semilinearity Property: $c \cdot f(x) = f(\sigma'(c) \cdot x)$

Informal description

Let $R$ and $S$ be semirings, $\sigma \colon R \to S$ and $\sigma' \colon S \to R$ be ring homomorphisms forming a ring homomorphism inverse pair (i.e., $\sigma \circ \sigma' = \text{id}_S$ and $\sigma' \circ \sigma = \text{id}_R$). For any semilinear map $f \colon M \to M_2$ with respect to $\sigma$, any scalar $c \in S$, and any element $x \in M$, we have: \[ c \cdot f(x) = f(\sigma'(c) \cdot x). \]

LinearMap.map_eq_zero_iff theorem

(h : Function.Injective f) {x : M} : f x = 0 ↔ x = 0

Full source

@[simp]
theorem map_eq_zero_iff (h : Function.Injective f) {x : M} : f x = 0 ↔ x = 0 :=
  _root_.map_eq_zero_iff f h

Injective Semilinear Maps Preserve Nonzero Elements

Informal description

For an injective semilinear map $f \colon M \to M_2$ between modules, and any element $x \in M$, we have $f(x) = 0$ if and only if $x = 0$.

LinearMap.CompatibleSMul structure

(R S : Type*) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂]

Full source

/-- A typeclass for `SMul` structures which can be moved through a `LinearMap`.
This typeclass is generated automatically from an `IsScalarTower` instance, but exists so that
we can also add an instance for `AddCommGroup.toIntModule`, allowing `z •` to be moved even if
`S` does not support negation.
-/
class CompatibleSMul (R S : Type*) [Semiring S] [SMul R M] [Module S M] [SMul R M₂]
  [Module S M₂] : Prop where
  /-- Scalar multiplication by `R` of `M` can be moved through linear maps. -/
  map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x

Compatible Scalar Multiplication through Linear Maps

Informal description

A typeclass for scalar multiplication structures that can be transferred through a linear map. This means that for a linear map `f : M → M₂` and a scalar multiplication operation `•` defined on both `M` and `M₂`, the scalar multiplication commutes with the application of `f`, i.e., `f (r • x) = r • f x` for any scalar `r` and element `x` in `M`.

LinearMap.IsScalarTower.compatibleSMul instance

[SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] : CompatibleSMul M M₂ R S

Full source

instance (priority := 100) IsScalarTower.compatibleSMul [SMul R S]
    [IsScalarTower R S M] [IsScalarTower R S M₂] :
    CompatibleSMul M M₂ R S :=
  ⟨fun fₗ c x ↦ by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩

Scalar Tower Compatibility for Linear Maps

Informal description

Given a scalar multiplication action of $R$ on $S$ and scalar tower structures `IsScalarTower R S M` and `IsScalarTower R S M₂`, the scalar multiplication operations on $M$ and $M₂$ are compatible through $S$-linear maps. This means that for any $S$-linear map $f \colon M \to M₂$, scalar $c \in R$, and element $x \in M$, we have $f(c \cdot x) = c \cdot f(x)$.

LinearMap.IsScalarTower.compatibleSMul' instance

[SMul R S] [IsScalarTower R S M] : CompatibleSMul S M R S

Full source

instance IsScalarTower.compatibleSMul' [SMul R S] [IsScalarTower R S M] :
    CompatibleSMul S M R S where
  map_smul := (IsScalarTower.smulHomClass R S M (S →ₗ[S] M)).map_smulₛₗ

Compatibility of Scalar Multiplication in a Scalar Tower

Informal description

For any semiring $S$ and any $S$-module $M$, if there is a scalar multiplication action of $R$ on $S$ and the actions form a scalar tower (i.e., for all $r \in R$, $s \in S$, and $m \in M$, we have $r \cdot (s \cdot m) = (r \cdot s) \cdot m$), then the scalar multiplication operations of $R$ and $S$ on $M$ are compatible.

LinearMap.map_smul_of_tower theorem

[CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : fₗ (c • x) = c • fₗ x

Full source

@[simp]
theorem map_smul_of_tower [CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
    fₗ (c • x) = c • fₗ x :=
  CompatibleSMul.map_smul fₗ c x

Linear maps preserve compatible scalar multiplication

Informal description

Let $R$ and $S$ be semirings, and let $M$ and $M₂$ be modules over $S$ with compatible scalar multiplication by $R$. For any $S$-linear map $f \colon M \to M₂$, scalar $c \in R$, and element $x \in M$, we have $f(c \cdot x) = c \cdot f(x)$.

LinearMapClass.map_smul_of_tower theorem

 {F : Type*} [CompatibleSMul M M₂ R S] [FunLike F M M₂] [LinearMapClass F S M M₂] (fₗ : F) (c : R) (x : M) :
  fₗ (c • x) = c • fₗ x

Full source

theorem _root_.LinearMapClass.map_smul_of_tower {F : Type*} [CompatibleSMul M M₂ R S]
    [FunLike F M M₂] [LinearMapClass F S M M₂] (fₗ : F) (c : R) (x : M) :
    fₗ (c • x) = c • fₗ x :=
  LinearMap.CompatibleSMul.map_smul (fₗ : M →ₗ[S] M₂) c x

Scalar Multiplication Commutes with Linear Maps under Compatible Actions

Informal description

Let $M$ and $M₂$ be modules over a semiring $S$, and let $R$ be a type with a scalar multiplication operation compatible with $S$ (i.e., `[CompatibleSMul M M₂ R S]`). For any $S$-linear map $f \colon M \to M₂$ in the class `LinearMapClass F S M M₂`, and for any scalar $c \in R$ and element $x \in M$, we have: \[ f(c \cdot x) = c \cdot f(x). \]

LinearMap.isScalarTower_of_injective theorem

 [SMul R S] [CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective f) :
  IsScalarTower R S M

Full source

theorem isScalarTower_of_injective [SMul R S] [CompatibleSMul M M₂ R S] [IsScalarTower R S M₂]
    (f : M →ₗ[S] M₂) (hf : Function.Injective f) : IsScalarTower R S M where
  smul_assoc r s _ := hf <| by rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]

Injective Linear Maps Preserve Scalar Tower Structure

Informal description

Let $R$ and $S$ be semirings with a scalar multiplication action of $R$ on $S$, and let $M$ and $M₂$ be $S$-modules with compatible scalar multiplication by $R$. Suppose $M₂$ forms a scalar tower over $R$ and $S$ (i.e., $(r \cdot s) \cdot m₂ = r \cdot (s \cdot m₂)$ for all $r \in R$, $s \in S$, $m₂ \in M₂$). If $f \colon M \to M₂$ is an injective $S$-linear map, then $M$ also forms a scalar tower over $R$ and $S$.

map_zsmul_unit theorem

 {F M N : Type*} [AddGroup M] [AddGroup N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (c : ℤˣ) (m : M) :
  f (c • m) = c • f m

Full source

@[simp] lemma _root_.map_zsmul_unit {F M N : Type*}
    [AddGroup M] [AddGroup N] [FunLike F M N] [AddMonoidHomClass F M N]
    (f : F) (c : ℤℤˣ) (m : M) :
    f (c • m) = c • f m := by
  simp [Units.smul_def]

Preservation of Integer Unit Scalar Multiplication by Additive Monoid Homomorphisms

Informal description

Let $M$ and $N$ be additive groups, and let $F$ be a type of additive monoid homomorphisms from $M$ to $N$. For any homomorphism $f \in F$, any unit $c$ in the group of units of the integers $\mathbb{Z}^\times$, and any element $m \in M$, we have: \[ f(c \cdot m) = c \cdot f(m). \]

LinearMap.isLinearMap_of_compatibleSMul theorem

[Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) : IsLinearMap R f

Full source

theorem isLinearMap_of_compatibleSMul [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S]
    (f : M →ₗ[S] M₂) : IsLinearMap R f where
  map_add := map_add f
  map_smul := map_smul_of_tower f

$S$-linear maps with compatible scalar multiplication are $R$-linear

Informal description

Let $R$ and $S$ be semirings, and let $M$ and $M₂$ be modules over $S$ with compatible scalar multiplication by $R$. For any $S$-linear map $f \colon M \to M₂$, the function $f$ is also $R$-linear.

LinearMap.toAddMonoidHom definition

: M →+ M₃

Full source

/-- convert a linear map to an additive map -/
def toAddMonoidHom : M →+ M₃ where
  toFun := f
  map_zero' := f.map_zero
  map_add' := f.map_add

Conversion of semilinear map to additive monoid homomorphism

Informal description

The function converts a semilinear map $f \colon M \to M_3$ between modules to an additive monoid homomorphism, preserving the zero element and addition. Specifically: 1. $f(0) = 0$ (preservation of zero) 2. $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ (preservation of addition)

LinearMap.toAddMonoidHom_coe theorem

: ⇑f.toAddMonoidHom = f

Full source

@[simp]
theorem toAddMonoidHom_coe : ⇑f.toAddMonoidHom = f :=
  rfl

Equality of Semilinear Map and its Additive Monoid Homomorphism Form

Informal description

For any semilinear map $f \colon M \to M_3$, the underlying function of the additive monoid homomorphism obtained from $f$ is equal to $f$ itself, i.e., $f_{\text{toAddMonoidHom}} = f$.

LinearMap.restrictScalars definition

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

Full source

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

See also `LinearMap.map_smul_of_tower`. -/
@[coe] def restrictScalars (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂ where
  toFun := fₗ
  map_add' := fₗ.map_add
  map_smul' := fₗ.map_smul_of_tower

Restriction of scalars for linear maps

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 scalar towers), any $S$-linear map $fₗ: M \to M₂$ can be viewed as an $R$-linear map. This map preserves addition and satisfies $fₗ(r \cdot x) = r \cdot fₗ(x)$ for all $r \in R$ and $x \in M$.

LinearMap.coeIsScalarTower instance

: CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)

Full source

instance coeIsScalarTower : CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂) :=
  ⟨restrictScalars R⟩

Coercion of Linear Maps in Scalar Towers

Informal description

Given modules $M$ and $M₂$ over semirings $R$ and $S$, where the $R$-module structure is compatible with the $S$-module structure (forming scalar towers), any $S$-linear map $f \colon M \to M₂$ can be coerced to an $R$-linear map. This coercion preserves the underlying function, meaning that the $R$-linear map acts identically to the original $S$-linear map on all elements of $M$.

LinearMap.coe_restrictScalars theorem

(f : M →ₗ[S] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f

Full source

@[simp, norm_cast]
theorem coe_restrictScalars (f : M →ₗ[S] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f :=
  rfl

Restriction of Scalars Preserves Underlying Function

Informal description

For any $S$-linear map $f \colon M \to M₂$, the underlying function of the $R$-linear map obtained by restricting scalars is equal to $f$ itself. That is, $f$ viewed as an $R$-linear map is the same function as $f$ viewed as an $S$-linear map.

LinearMap.restrictScalars_apply theorem

(fₗ : M →ₗ[S] M₂) (x) : restrictScalars R fₗ x = fₗ x

Full source

theorem restrictScalars_apply (fₗ : M →ₗ[S] M₂) (x) : restrictScalars R fₗ x = fₗ x :=
  rfl

Restriction of Scalars Preserves Application: $(f_\ell \restriction_R)(x) = f_\ell(x)$

Informal description

For any $S$-linear map $f_\ell \colon M \to M₂$ and any element $x \in M$, the application of the restricted scalar map $f_\ell$ (viewed as an $R$-linear map) to $x$ is equal to the application of the original $S$-linear map $f_\ell$ to $x$, i.e., $(f_\ell \restriction_R)(x) = f_\ell(x)$.

LinearMap.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 (LinearMap.congr_fun h :)

Injectivity of Scalar Restriction for Linear Maps

Informal description

The restriction of scalars operation on linear maps is injective. That is, for any two $S$-linear maps $f, g \colon M \to M₂$, if their restrictions to $R$-linear maps are equal, then $f = g$.

LinearMap.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

Equivalence of Linear Map Equality Before and After Scalar Restriction

Informal description

For any two $S$-linear maps $f_\ell, g_\ell \colon M \to M₂$, the equality of their restrictions as $R$-linear maps is equivalent to the equality of the original $S$-linear maps, i.e., $f_\ell \restriction_R = g_\ell \restriction_R$ if and only if $f_\ell = g_\ell$.

LinearMap.toAddMonoidHom_injective theorem

: Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃)

Full source

theorem toAddMonoidHom_injective :
    Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun fₗ gₗ h ↦
  ext <| (DFunLike.congr_fun h : ∀ x, fₗ.toAddMonoidHom x = gₗ.toAddMonoidHom x)

Injectivity of the Semilinear-to-Additive Homomorphism Conversion

Informal description

The map that converts a semilinear map $f \colon M \to_{\sigma} M_3$ to an additive monoid homomorphism is injective. That is, if two semilinear maps induce the same additive monoid homomorphism, then they must be equal.

LinearMap.ext_ring theorem

{f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g

Full source

/-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/
@[ext high]
theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g :=
  ext fun x ↦ by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]

Equality of Semilinear Maps Determined by Action on 1

Informal description

Let $R$ and $S$ be semirings with a ring homomorphism $\sigma \colon R \to S$, and let $M₃$ be an $S$-module. For any two $\sigma$-semilinear maps $f, g \colon R \to M₃$, if $f(1) = g(1)$, then $f = g$.

RingHom.toSemilinearMap definition

(f : R →+* S) : R →ₛₗ[f] S

Full source

/-- Interpret a `RingHom` `f` as an `f`-semilinear map. -/
@[simps]
def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S :=
  { f with
    map_smul' := f.map_mul }

Ring homomorphism as a semilinear map

Informal description

Given a ring homomorphism $f \colon R \to S$, the function $f$ can be interpreted as an $f$-semilinear map from $R$ to $S$, where $R$ and $S$ are viewed as modules over themselves. This semilinear map satisfies $f(c \cdot x) = f(c) \cdot f(x)$ for all $c, x \in R$.

RingHom.coe_toSemilinearMap theorem

(f : R →+* S) : ⇑f.toSemilinearMap = f

Full source

@[simp] theorem _root_.RingHom.coe_toSemilinearMap (f : R →+* S) : ⇑f.toSemilinearMap = f := rfl

Ring Homomorphism as Semilinear Map Preserves Function

Informal description

For any ring homomorphism $f \colon R \to S$, the underlying function of the semilinear map induced by $f$ (viewing $R$ and $S$ as modules over themselves) is equal to $f$ itself. That is, $f_{\text{toSemilinearMap}}(x) = f(x)$ for all $x \in R$.

LinearMap.comp definition

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₃] M₃

Full source

/-- Composition of two linear maps is a linear map -/
def comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
    M₁ →ₛₗ[σ₁₃] M₃ where
  toFun := f ∘ g
  map_add' := by simp only [map_add, forall_const, Function.comp_apply]
  -- Note that https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` to `map_smulₛₗ _`
  map_smul' r x := by simp only [Function.comp_apply, map_smulₛₗ _, RingHomCompTriple.comp_apply]

Composition of semilinear maps

Informal description

Given ring homomorphisms $\sigma_{12} \colon R \to S$, $\sigma_{23} \colon S \to T$, and $\sigma_{13} \colon R \to T$ forming a `RingHomCompTriple`, and given semilinear maps $f \colon M_2 \to_{\sigma_{23}} M_3$ and $g \colon M_1 \to_{\sigma_{12}} M_2$, their composition $f \circ g \colon M_1 \to_{\sigma_{13}} M_3$ is a semilinear map defined by $(f \circ g)(x) = f(g(x))$ for all $x \in M_1$. This composition preserves addition and satisfies the semilinearity condition $(f \circ g)(r \cdot x) = \sigma_{13}(r) \cdot (f \circ g)(x)$ for all $r \in R$ and $x \in M_1$.

LinearMap.compNotation definition

: Lean.TrailingParserDescr✝

Full source

/-- `∘ₗ` is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the `RingHomCompTriple` instance. -/
notation3:80 (name := compNotation) f:81 " ∘ₗ " g:80 =>
  LinearMap.comp (σ₁₂ := RingHom.id _) (σ₂₃ := RingHom.id _) (σ₁₃ := RingHom.id _) f g

Composition notation for linear maps

Informal description

The notation `f ∘ₗ g` denotes the composition of two linear maps `f` and `g` (not semilinear), resulting in a linear map. This notation is particularly useful when Lean has difficulty inferring the `RingHomCompTriple` instance automatically.

LinearMap.compNotation.delab_app.LinearMap.comp definition

: Delab✝

Full source

/-- `∘ₗ` is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the `RingHomCompTriple` instance. -/
notation3:80 (name := compNotation) f:81 " ∘ₗ " g:80 =>
  LinearMap.comp (σ₁₂ := RingHom.id _) (σ₂₃ := RingHom.id _) (σ₁₃ := RingHom.id _) f g

Composition notation for linear maps

Informal description

The notation `f ∘ₗ g` denotes the composition of two linear maps `f` and `g` (not semilinear), resulting in a linear map. This notation is particularly useful when Lean has difficulty inferring the `RingHomCompTriple` instance automatically.

LinearMap.term_∘ₛₗ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixr:90 " ∘ₛₗ " => comp

Composition notation for semilinear maps

Informal description

The notation `f ∘ₛₗ g` represents the composition of two semilinear maps $f$ and $g$, where the composition is right-associative with precedence level 90. This means that in an expression like `f ∘ₛₗ g ∘ₛₗ h`, it will be parsed as `f ∘ₛₗ (g ∘ₛₗ h)` due to the right-associative nature of the notation.

LinearMap.comp_apply theorem

(x : M₁) : f.comp g x = f (g x)

Full source

theorem comp_apply (x : M₁) : f.comp g x = f (g x) :=
  rfl

Composition of Semilinear Maps Preserves Evaluation

Informal description

For any semilinear maps $f \colon M_2 \to_{\sigma_{23}} M_3$ and $g \colon M_1 \to_{\sigma_{12}} M_2$, and any element $x \in M_1$, the composition $f \circ g$ evaluated at $x$ equals $f$ applied to $g(x)$, i.e., $(f \circ g)(x) = f(g(x))$.

LinearMap.coe_comp theorem

: (f.comp g : M₁ → M₃) = f ∘ g

Full source

@[simp, norm_cast]
theorem coe_comp : (f.comp g : M₁ → M₃) = f ∘ g :=
  rfl

Composition of Semilinear Maps as Function Composition

Informal description

For semilinear maps $f \colon M_2 \to_{\sigma_{23}} M_3$ and $g \colon M_1 \to_{\sigma_{12}} M_2$, the underlying function of their composition $f \circ g \colon M_1 \to_{\sigma_{13}} M_3$ is equal to the function composition $f \circ g$ of their underlying functions.

LinearMap.comp_id theorem

: f.comp id = f

Full source

@[simp]
theorem comp_id : f.comp id = f :=
  rfl

Right Identity Property of Linear Map Composition

Informal description

For any linear map $f \colon M \to M₂$ between $R$-modules, the composition of $f$ with the identity map on $M$ equals $f$ itself, i.e., $f \circ \text{id} = f$.

LinearMap.id_comp theorem

: id.comp f = f

Full source

@[simp]
theorem id_comp : id.comp f = f :=
  rfl

Identity Map is Left Identity for Composition of Semilinear Maps

Informal description

For any semilinear map $f \colon M_1 \to_{\sigma_{12}} M_2$ between modules, the composition of the identity map $\text{id} \colon M_2 \to M_2$ with $f$ equals $f$ itself, i.e., $\text{id} \circ f = f$.

LinearMap.comp_assoc theorem

 {R₄ M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄}
  [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
  ((h.comp g : M₂ →ₛₗ[σ₂₄] M₄).comp f : M₁ →ₛₗ[σ₁₄] M₄) = h.comp (g.comp f : M₁ →ₛₗ[σ₁₃] M₃)

Full source

theorem comp_assoc
    {R₄ M₄ : Type*} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄]
    {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄}
    [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
    (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
    ((h.comp g : M₂ →ₛₗ[σ₂₄] M₄).comp f : M₁ →ₛₗ[σ₁₄] M₄) = h.comp (g.comp f : M₁ →ₛₗ[σ₁₃] M₃) :=
  rfl

Associativity of Composition of Semilinear Maps

Informal description

Let $R_1, R_2, R_3, R_4$ be semirings and $M_1, M_2, M_3, M_4$ be additive commutative monoids with module structures over $R_1, R_2, R_3, R_4$ respectively. Given ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$, $\sigma_{23} \colon R_2 \to R_3}$, $\sigma_{34} \colon R_3 \to R_4}$, $\sigma_{24} \colon R_2 \to R_4}$, and $\sigma_{14} \colon R_1 \to R_4}$ forming compatible composition triples, and given semilinear maps $f \colon M_1 \to_{\sigma_{12}} M_2$, $g \colon M_2 \to_{\sigma_{23}} M_3}$, and $h \colon M_3 \to_{\sigma_{34}} M_4}$, the composition of semilinear maps is associative: $$(h \circ g) \circ f = h \circ (g \circ f)$$ as maps from $M_1$ to $M_4$ with respect to $\sigma_{14}$.

Function.Surjective.injective_linearMapComp_right theorem

(hg : Surjective g) : Injective fun f : M₂ →ₛₗ[σ₂₃] M₃ ↦ f.comp g

Full source

/-- The linear map version of `Function.Surjective.injective_comp_right` -/
lemma _root_.Function.Surjective.injective_linearMapComp_right (hg : Surjective g) :
    Injective fun f : M₂ →ₛₗ[σ₂₃] M₃ ↦ f.comp g :=
  fun _ _ h ↦ ext <| hg.forall.2 (LinearMap.ext_iff.1 h)

Injectivity of Post-Composition with a Surjective Semilinear Map

Informal description

Let $g \colon M_1 \to_{\sigma_{12}} M_2$ be a surjective semilinear map between modules. Then the composition map $f \mapsto f \circ g$ is injective, i.e., for any two semilinear maps $f, f' \colon M_2 \to_{\sigma_{23}} M_3$, if $f \circ g = f' \circ g$, then $f = f'$.

LinearMap.cancel_right theorem

(hg : Surjective g) : f.comp g = f'.comp g ↔ f = f'

Full source

@[simp]
theorem cancel_right (hg : Surjective g) : f.comp g = f'.comp g ↔ f = f' :=
  hg.injective_linearMapComp_right.eq_iff

Cancellation of Semilinear Maps by Surjective Composition on the Right

Informal description

Let $g \colon M_1 \to_{\sigma_{12}} M_2$ be a surjective semilinear map between modules. Then for any two semilinear maps $f, f' \colon M_2 \to_{\sigma_{23}} M_3$, the compositions $f \circ g$ and $f' \circ g$ are equal if and only if $f = f'$.

Function.Injective.injective_linearMapComp_left theorem

(hf : Injective f) : Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g

Full source

/-- The linear map version of `Function.Injective.comp_left` -/
lemma _root_.Function.Injective.injective_linearMapComp_left (hf : Injective f) :
    Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g :=
  fun g₁ g₂ (h : f.comp g₁ = f.comp g₂) ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply]

Injectivity of Left Composition with Injective Semilinear Map

Informal description

Let $R_1, R_2, R_3$ be semirings with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$. Let $M_1$ be an $R_1$-module, $M_2$ an $R_2$-module, and $M_3$ an $R_3$-module. Given an injective semilinear map $f \colon M_2 \to_{\sigma_{23}} M_3$, the composition map $g \mapsto f \circ g$ from $\text{Hom}_{\sigma_{12}}(M_1, M_2)$ to $\text{Hom}_{\sigma_{13}}(M_1, M_3)$ is injective.

LinearMap.surjective_comp_left_of_exists_rightInverse theorem

 {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂]
  (hf : ∃ f' : M₃ →ₛₗ[σ₃₂] M₂, f.comp f' = .id) : Surjective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g

Full source

theorem surjective_comp_left_of_exists_rightInverse {σ₃₂ : R₃ →+* R₂}
    [RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂]
    (hf : ∃ f' : M₃ →ₛₗ[σ₃₂] M₂, f.comp f' = .id) :
    Surjective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g := by
  intro h
  obtain ⟨f', hf'⟩ := hf
  refine ⟨f'.comp h, ?_⟩
  simp_rw [← comp_assoc, hf', id_comp]

Surjectivity of Left Composition with Semilinear Map Having Right Inverse

Informal description

Let $R_1, R_2, R_3$ be semirings with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$, $\sigma_{23} \colon R_2 \to R_3$, and $\sigma_{13} \colon R_1 \to R_3$ forming a `RingHomCompTriple`. Let $M_1$ be an $R_1$-module, $M_2$ an $R_2$-module, and $M_3$ an $R_3$-module. Given a semilinear map $f \colon M_2 \to_{\sigma_{23}} M_3$ such that there exists a semilinear map $f' \colon M_3 \to_{\sigma_{32}} M_2$ with $f \circ f' = \text{id}_{M_3}$, then the composition map $g \mapsto f \circ g$ from $\text{Hom}_{\sigma_{12}}(M_1, M_2)$ to $\text{Hom}_{\sigma_{13}}(M_1, M_3)$ is surjective.

LinearMap.cancel_left theorem

(hf : Injective f) : f.comp g = f.comp g' ↔ g = g'

Full source

@[simp]
theorem cancel_left (hf : Injective f) : f.comp g = f.comp g' ↔ g = g' :=
  hf.injective_linearMapComp_left.eq_iff

Cancellation Property for Composition with Injective Semilinear Map

Informal description

Let $R_1, R_2, R_3$ be semirings with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$. Let $M_1$ be an $R_1$-module, $M_2$ an $R_2$-module, and $M_3$ an $R_3$-module. Given an injective semilinear map $f \colon M_2 \to_{\sigma_{23}} M_3$ and semilinear maps $g, g' \colon M_1 \to_{\sigma_{12}} M_2$, we have $f \circ g = f \circ g'$ if and only if $g = g'$.

LinearMap.inverse definition

(f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : M₂ →ₛₗ[σ'] M

Full source

/-- If a function `g` is a left and right inverse of a linear map `f`, then `g` is linear itself. -/
def inverse (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : LeftInverse g f) (h₂ : RightInverse g f) :
    M₂ →ₛₗ[σ'] M := by
  dsimp [LeftInverse, Function.RightInverse] at h₁ h₂
  exact
    { toFun := g
      map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂]
      map_smul' := fun a b ↦ by
        rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
        simp [h₂] }

Inverse of a semilinear map as a semilinear map

Informal description

Given a semilinear map $f \colon M \to_{\sigma} M₂$ and a function $g \colon M₂ \to M$ that is both a left and right inverse of $f$, then $g$ can be equipped with the structure of a semilinear map $M₂ \to_{\sigma'} M$, where $\sigma'$ is the appropriate ring homomorphism. Specifically: 1. $g$ preserves addition: $g(x + y) = g(x) + g(y)$ for all $x, y \in M₂$ 2. $g$ is semilinear: $g(a \cdot b) = \sigma'(a) \cdot g(b)$ for all $a$ in the appropriate ring and $b \in M₂$

LinearMap.injective_of_comp_eq_id theorem

: Injective f

Full source

theorem injective_of_comp_eq_id : Injective f :=
  .of_comp (f := g) <| by simp_rw [← coe_comp, h, id_coe, bijective_id.1]

Injectivity from Composition with Identity

Informal description

If the composition of two linear maps $f \circ g$ equals the identity map, then $f$ is injective.

LinearMap.surjective_of_comp_eq_id theorem

: Surjective g

Full source

theorem surjective_of_comp_eq_id : Surjective g :=
  .of_comp (g := f) <| by simp_rw [← coe_comp, h, id_coe, bijective_id.2]

Surjectivity of a Linear Map with Right Inverse

Informal description

Let $f \colon M \to M'$ and $g \colon M' \to M$ be linear maps between modules such that $f \circ g = \text{id}_{M'}$. Then $g$ is surjective.

LinearMap.map_neg theorem

(x : M) : f (-x) = -f x

Full source

protected theorem map_neg (x : M) : f (-x) = -f x :=
  map_neg f x

Linear Maps Preserve Additive Inverses: $f(-x) = -f(x)$

Informal description

Let $f \colon M \to M'$ be a linear map between modules over a ring. For any element $x \in M$, the image of the additive inverse $-x$ under $f$ is equal to the additive inverse of the image of $x$, i.e., $f(-x) = -f(x)$.

LinearMap.map_sub theorem

(x y : M) : f (x - y) = f x - f y

Full source

protected theorem map_sub (x y : M) : f (x - y) = f x - f y :=
  map_sub f x y

Linear maps preserve subtraction

Informal description

Let $f \colon M \to M_2$ be a linear map between modules over a ring. For any elements $x, y \in M$, the map $f$ satisfies $f(x - y) = f(x) - f(y)$.

LinearMap.CompatibleSMul.intModule instance

{S : Type*} [Semiring S] [Module S M] [Module S M₂] : CompatibleSMul M M₂ ℤ S

Full source

instance CompatibleSMul.intModule {S : Type*} [Semiring S] [Module S M] [Module S M₂] :
    CompatibleSMul M M₂ ℤ S :=
  ⟨fun fₗ c x ↦ by
    induction c with
    | hz => simp
    | hp n ih => simp [add_smul, ih]
    | hn n ih => simp [sub_smul, ih]⟩

Compatibility of Integer Scalar Multiplication with Linear Maps

Informal description

For any semiring $S$ and $S$-modules $M$ and $M₂$, the scalar multiplication by integers on $M$ and $M₂$ is compatible with $S$-linear maps between them. That is, for any $S$-linear map $f \colon M \to M₂$, integer $n \in \mathbb{Z}$, and element $x \in M$, we have $f(n \cdot x) = n \cdot f(x)$.

LinearMap.CompatibleSMul.units instance

 {R S : Type*} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂]
  [CompatibleSMul M M₂ R S] : CompatibleSMul M M₂ Rˣ S

Full source

instance CompatibleSMul.units {R S : Type*} [Monoid R] [MulAction R M] [MulAction R M₂]
    [Semiring S] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] : CompatibleSMul M M₂ Rˣ S :=
  ⟨fun fₗ c x ↦ (CompatibleSMul.map_smul fₗ (c : R) x :)⟩

Compatibility of Scalar Multiplication by Units with Linear Maps

Informal description

For any monoid $R$, semiring $S$, and $S$-modules $M$ and $M₂$ with compatible scalar multiplication actions by $R$, the group of units $R^\times$ also has a compatible scalar multiplication action on $M$ and $M₂$ through $S$-linear maps.

Module.compHom.toLinearMap definition

 {R S : Type*} [Semiring R] [Semiring S] (g : R →+* S) :
  letI := compHom S g;
  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.toLinearMap {R S : Type*} [Semiring R] [Semiring S] (g : R →+* S) :
    letI := compHom S g; R →ₗ[R] S :=
  letI := compHom S g
  { toFun := (g : R → S)
    map_add' := g.map_add
    map_smul' := g.map_mul }

Ring homomorphism as linear map via composition-induced module structure

Informal description

Given a ring homomorphism $g \colon R \to S$ between semirings, the function $g$ can be viewed as an $R$-linear map from $R$ to $S$, where $S$ is equipped with the $R$-module structure induced by $g$ via `Module.compHom`. This means $g$ preserves addition and satisfies the linearity condition $g(r \cdot x) = r \cdot g(x)$ for all $r, x \in R$.

DistribMulActionHom.toSemilinearMap definition

(fₗ : M →ₑ+[σ.toMonoidHom] M₂) : M →ₛₗ[σ] M₂

Full source

/-- A `DistribMulActionHom` between two modules is a linear map. -/
@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
def toSemilinearMap (fₗ : M →ₑ+[σ.toMonoidHom] M₂) : M →ₛₗ[σ] M₂ :=
  { fₗ with }

Equivariant additive monoid homomorphism as semilinear map

Informal description

Given an equivariant additive monoid homomorphism $f_\ell \colon M \to M₂$ with respect to a ring homomorphism $\sigma \colon R \to S$, the function $f_\ell$ can be viewed as a semilinear map between the $R$-module $M$ and the $S$-module $M₂$. This means $f_\ell$ preserves addition and satisfies the semilinearity condition $f_\ell(r \cdot x) = \sigma(r) \cdot f_\ell(x)$ for all $r \in R$ and $x \in M$.

DistribMulActionHom.instSemilinearMapClass instance

: SemilinearMapClass (M →ₑ+[σ.toMonoidHom] M₂) σ M M₂

Full source

instance : SemilinearMapClass (M →ₑ+[σ.toMonoidHom] M₂) σ M M₂ where

Equivariant Additive Monoid Homomorphisms as Semilinear Maps

Informal description

The type of equivariant additive monoid homomorphisms $M \to_{e+}[\sigma] M₂$ forms a class of $\sigma$-semilinear maps, where $\sigma: R \to S$ is a ring homomorphism. Specifically, these maps are additive and satisfy the semilinearity condition $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all $r \in R$ and $x \in M$.

DistribMulActionHom.toLinearMap definition

(fₗ : M →+[R] M₃) : M →ₗ[R] M₃

Full source

/-- A `DistribMulActionHom` between two modules is a linear map. -/
@[deprecated "No deprecation message was provided." (since := "2024-11-08")]
def toLinearMap (fₗ : M →+[R] M₃) : M →ₗ[R] M₃ :=
  { fₗ with }

Conversion from `DistribMulActionHom` to linear map

Informal description

Given a `DistribMulActionHom` $f_\ell \colon M \to_{+[R]} M_3$ between modules over the same semiring $R$, this function converts it into a linear map $M \to_{\ell[R]} M_3$ by preserving the additive structure and scalar multiplication. Specifically, the resulting linear map satisfies: 1. Additivity: $f_\ell(x + y) = f_\ell(x) + f_\ell(y)$ for all $x, y \in M$ 2. Linearity: $f_\ell(r \cdot x) = r \cdot f_\ell(x)$ for all $r \in R$ and $x \in M$

DistribMulActionHom.instLinearMapClassId instance

: LinearMapClass (M →+[R] M₃) R M M₃

Full source

/-- A `DistribMulActionHom` between two modules is a linear map. -/
instance : LinearMapClass (M →+[R] M₃) R M M₃ where

Additive $R$-Linear Maps as Linear Maps

Informal description

For any semiring $R$ and $R$-modules $M$ and $M₃$, the type of additive $R$-linear maps $M \to M₃$ forms a class of linear maps. That is, every additive $R$-linear map preserves addition and scalar multiplication: 1. $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ 2. $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in M$

DistribMulActionHom.coe_toLinearMap theorem

(f : M →ₑ+[σ.toMonoidHom] M₂) : ((f : M →ₛₗ[σ] M₂) : M → M₂) = f

Full source

@[simp]
theorem coe_toLinearMap (f : M →ₑ+[σ.toMonoidHom] M₂) : ((f : M →ₛₗ[σ] M₂) : M → M₂) = f :=
  rfl

Underlying Function of Semilinear Map Coincides with Original Homomorphism

Informal description

For any $\sigma$-equivariant additive monoid homomorphism $f \colon M \to M₂$, the underlying function of the corresponding $\sigma$-semilinear map is equal to $f$ itself.

DistribMulActionHom.toLinearMap_injective theorem

{f g : M →ₑ+[σ.toMonoidHom] M₂} (h : (f : M →ₛₗ[σ] M₂) = (g : M →ₛₗ[σ] M₂)) : f = g

Full source

theorem toLinearMap_injective {f g : M →ₑ+[σ.toMonoidHom] M₂}
    (h : (f : M →ₛₗ[σ] M₂) = (g : M →ₛₗ[σ] M₂)) :
    f = g := by
  ext m
  exact LinearMap.congr_fun h m

Injectivity of Conversion from Equivariant Homomorphisms to Semilinear Maps

Informal description

For any two $\sigma$-equivariant additive monoid homomorphisms $f, g \colon M \to M₂$, if their corresponding $\sigma$-semilinear maps are equal, then $f$ and $g$ are equal.

IsLinearMap.mk' definition

(f : M → M₂) (lin : IsLinearMap R f) : M →ₗ[R] M₂

Full source

/-- Convert an `IsLinearMap` predicate to a `LinearMap` -/
def mk' (f : M → M₂) (lin : IsLinearMap R f) : M →ₗ[R] M₂ where
  toFun := f
  map_add' := lin.1
  map_smul' := lin.2

Construction of linear map from linearity conditions

Informal description

Given a function $f \colon M \to M₂$ between modules over a semiring $R$ that satisfies the linearity conditions (additivity and homogeneity), this definition constructs a bundled linear map from $f$ and its proof of linearity. The constructed linear map has: - Underlying function $f$ - Proof of additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ - Proof of scalar multiplication preservation: $f(r \cdot x) = r \cdot f(x)$ for all $r \in R$ and $x \in M$

IsLinearMap.mk'_apply theorem

{f : M → M₂} (lin : IsLinearMap R f) (x : M) : mk' f lin x = f x

Full source

@[simp]
theorem mk'_apply {f : M → M₂} (lin : IsLinearMap R f) (x : M) : mk' f lin x = f x :=
  rfl

Evaluation of Constructed Linear Map Equals Original Function

Informal description

Given a function $f \colon M \to M₂$ between modules over a semiring $R$ that satisfies the linearity conditions (i.e., $f$ is additive and homogeneous), the evaluation of the constructed linear map $\text{mk'}(f, \text{lin})$ at any point $x \in M$ equals $f(x)$. In other words, for all $x \in M$, we have $\text{mk'}(f, \text{lin})(x) = f(x)$.

IsLinearMap.isLinearMap_smul theorem

{R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : IsLinearMap R fun z : M ↦ c • z

Full source

theorem isLinearMap_smul {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :
    IsLinearMap R fun z : M ↦ c • z := by
  refine IsLinearMap.mk (smul_add c) ?_
  intro _ _
  simp only [smul_smul, mul_comm]

Scalar multiplication is a linear map

Informal description

Let $R$ be a commutative semiring and $M$ be an $R$-module. For any element $c \in R$, the scalar multiplication map $z \mapsto c \cdot z$ is a linear map from $M$ to itself.

IsLinearMap.isLinearMap_smul' theorem

{R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : IsLinearMap R fun c : R ↦ c • a

Full source

theorem isLinearMap_smul' {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) :
    IsLinearMap R fun c : R ↦ c • a :=
  IsLinearMap.mk (fun x y ↦ add_smul x y a) fun x y ↦ mul_smul x y a

Scalar Multiplication by Fixed Element is Linear

Informal description

For any semiring $R$ and any $R$-module $M$, the function $f_a \colon R \to M$ defined by $f_a(c) = c \bullet a$ for a fixed element $a \in M$ is a linear map.

IsLinearMap.map_zero theorem

{f : M → M₂} (lin : IsLinearMap R f) : f (0 : M) = (0 : M₂)

Full source

theorem map_zero {f : M → M₂} (lin : IsLinearMap R f) : f (0 : M) = (0 : M₂) :=
  (lin.mk' f).map_zero

Linear Maps Preserve Zero: $f(0) = 0$

Informal description

For any linear map $f \colon M \to M_2$ between modules over a semiring $R$, the image of the zero element in $M$ is the zero element in $M_2$, i.e., $f(0) = 0$.

IsLinearMap.isLinearMap_neg theorem

: IsLinearMap R fun z : M ↦ -z

Full source

theorem isLinearMap_neg : IsLinearMap R fun z : M ↦ -z :=
  IsLinearMap.mk neg_add fun x y ↦ (smul_neg x y).symm

Negation is a Linear Map

Informal description

For any module $M$ over a semiring $R$, the negation function $z \mapsto -z$ is a linear map from $M$ to itself.

IsLinearMap.map_neg theorem

{f : M → M₂} (lin : IsLinearMap R f) (x : M) : f (-x) = -f x

Full source

theorem map_neg {f : M → M₂} (lin : IsLinearMap R f) (x : M) : f (-x) = -f x :=
  (lin.mk' f).map_neg x

Linear Maps Preserve Negation: $f(-x) = -f(x)$

Informal description

Let $R$ be a semiring, and let $M$ and $M₂$ be modules over $R$. For any linear map $f \colon M \to M₂$ and any element $x \in M$, we have $f(-x) = -f(x)$.

IsLinearMap.map_sub theorem

{f : M → M₂} (lin : IsLinearMap R f) (x y : M) : f (x - y) = f x - f y

Full source

theorem map_sub {f : M → M₂} (lin : IsLinearMap R f) (x y : M) : f (x - y) = f x - f y :=
  (lin.mk' f).map_sub x y

Linear maps preserve subtraction: $f(x - y) = f(x) - f(y)$

Informal description

Let $R$ be a semiring and $M$, $M₂$ be modules over $R$. For any linear map $f \colon M \to M₂$ and any elements $x, y \in M$, we have $f(x - y) = f(x) - f(y)$.

AddMonoidHom.toNatLinearMap definition

[AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂

Full source

/-- Reinterpret an additive homomorphism as an `ℕ`-linear map. -/
def AddMonoidHom.toNatLinearMap [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) :
    M →ₗ[ℕ] M₂ where
  toFun := f
  map_add' := f.map_add
  map_smul' := map_nsmul f

Natural number linear map induced by an additive monoid homomorphism

Informal description

Given two additive commutative monoids $M$ and $M₂$, any additive monoid homomorphism $f \colon M \to M₂$ can be reinterpreted as a $\mathbb{N}$-linear map between $M$ and $M₂$, where the scalar multiplication by natural numbers is defined via repeated addition.

AddMonoidHom.toNatLinearMap_injective theorem

[AddCommMonoid M] [AddCommMonoid M₂] : Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _)

Full source

theorem AddMonoidHom.toNatLinearMap_injective [AddCommMonoid M] [AddCommMonoid M₂] :
    Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _) := by
  intro f g h
  ext x
  exact LinearMap.congr_fun h x

Injectivity of the Natural Number Linear Map Construction from Additive Monoid Homomorphisms

Informal description

For any two additive commutative monoids $M$ and $M₂$, the map from additive monoid homomorphisms $M \to M₂$ to $\mathbb{N}$-linear maps $M \to M₂$ is injective. That is, if two additive monoid homomorphisms induce the same $\mathbb{N}$-linear map, then they must be equal.

AddMonoidHom.toIntLinearMap definition

[AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂

Full source

/-- Reinterpret an additive homomorphism as a `ℤ`-linear map. -/
def AddMonoidHom.toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂ where
  toFun := f
  map_add' := f.map_add
  map_smul' := map_zsmul f

Additive group homomorphism as $\mathbb{Z}$-linear map

Informal description

Given two additive commutative groups $M$ and $M₂$, any additive group homomorphism $f \colon M \to M₂$ can be reinterpreted as a $\mathbb{Z}$-linear map between these groups when they are viewed as $\mathbb{Z}$-modules. This linear map satisfies: 1. $f(x + y) = f(x) + f(y)$ for all $x, y \in M$ (additivity) 2. $f(n \cdot x) = n \cdot f(x)$ for all $n \in \mathbb{Z}$ and $x \in M$ ($\mathbb{Z}$-linearity)

AddMonoidHom.toIntLinearMap_injective theorem

[AddCommGroup M] [AddCommGroup M₂] : Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _)

Full source

theorem AddMonoidHom.toIntLinearMap_injective [AddCommGroup M] [AddCommGroup M₂] :
    Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _) := by
  intro f g h
  ext x
  exact LinearMap.congr_fun h x

Injectivity of the Conversion from Additive Group Homomorphisms to $\mathbb{Z}$-Linear Maps

Informal description

For any additive commutative groups $M$ and $M₂$, the map that converts an additive group homomorphism $f \colon M \to M₂$ into a $\mathbb{Z}$-linear map is injective. That is, if two additive group homomorphisms $f, g \colon M \to M₂$ induce the same $\mathbb{Z}$-linear map, then $f = g$.

AddMonoidHom.coe_toIntLinearMap theorem

[AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : ⇑f.toIntLinearMap = f

Full source

@[simp]
theorem AddMonoidHom.coe_toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
    ⇑f.toIntLinearMap = f :=
  rfl

Coefficient Equality for $\mathbb{Z}$-linear Maps from Additive Group Homomorphisms

Informal description

For any additive group homomorphism $f \colon M \to M₂$ between additive commutative groups $M$ and $M₂$, the underlying function of the corresponding $\mathbb{Z}$-linear map $f.toIntLinearMap$ is equal to $f$ itself.

LinearMap.instSMul instance

: SMul S (M →ₛₗ[σ₁₂] M₂)

Full source

instance : SMul S (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun a f ↦
    { toFun := a • (f : M → M₂)
      map_add' := fun x y ↦ by simp only [Pi.smul_apply, f.map_add, smul_add]
      map_smul' := fun c x ↦ by simp [Pi.smul_apply, smul_comm] }⟩

Scalar Multiplication on Semilinear Maps

Informal description

For any semilinear map $f \colon M \to_{\sigma_{12}} M_2$ between modules, the space of such maps is equipped with a scalar multiplication operation by elements of $S$, where $(a \cdot f)(x) = a \cdot f(x)$ for any $a \in S$ and $x \in M$.

LinearMap.smul_apply theorem

(a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x

Full source

@[simp]
theorem smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x :=
  rfl

Evaluation of Scalar Multiple of Semilinear Map: $(a \cdot f)(x) = a \cdot f(x)$

Informal description

For any scalar $a \in S$ and any semilinear map $f \colon M \to_{\sigma_{12}} M_2$ between modules, the evaluation of the scalar multiple $a \cdot f$ at a point $x \in M$ is equal to the scalar multiple of the evaluation, i.e., $(a \cdot f)(x) = a \cdot f(x)$.

LinearMap.coe_smul theorem

(a : S) (f : M →ₛₗ[σ₁₂] M₂) : (a • f : M →ₛₗ[σ₁₂] M₂) = a • (f : M → M₂)

Full source

theorem coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : (a • f : M →ₛₗ[σ₁₂] M₂) = a • (f : M → M₂) :=
  rfl

Scalar Multiplication of Semilinear Maps is Pointwise

Informal description

For any scalar $a \in S$ and any semilinear map $f \colon M \to_{\sigma_{12}} M_2$, the underlying function of the scalar multiple $a \cdot f$ is equal to the pointwise scalar multiple of $a$ with the underlying function of $f$. That is, $(a \cdot f)(x) = a \cdot f(x)$ for all $x \in M$.

LinearMap.instSMulCommClass instance

[SMulCommClass S T M₂] : SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)

Full source

instance [SMulCommClass S T M₂] : SMulCommClass S T (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun _ _ _ ↦ ext fun _ ↦ smul_comm _ _ _⟩

Commutativity of Scalar Multiplication on Semilinear Maps

Informal description

For any two scalar multiplication operations $S$ and $T$ on a module $M₂$ that commute with each other, the corresponding scalar multiplication operations on the space of semilinear maps $M \to_{\sigma_{12}} M₂$ also commute. That is, for any $s \in S$, $t \in T$, and semilinear map $f \colon M \to_{\sigma_{12}} M₂$, we have $(s \cdot t) \cdot f = (t \cdot s) \cdot f$.

LinearMap.instIsScalarTower instance

[SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)

Full source

instance [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂) where
  smul_assoc _ _ _ := ext fun _ ↦ smul_assoc _ _ _

Scalar Tower Property for Semilinear Maps

Informal description

For any semilinear maps between modules $M$ and $M₂$ with respect to a ring homomorphism $\sigma_{12} \colon R \to S$, if the scalar multiplications by $S$ and $T$ on $M₂$ form a scalar tower (i.e., $(s \cdot t) \cdot m = s \cdot (t \cdot m)$ for all $s \in S$, $t \in T$, and $m \in M₂$), then the corresponding scalar multiplications on the space of semilinear maps $M \to_{\sigma_{12}} M₂$ also form a scalar tower.

LinearMap.instIsCentralScalar instance

 [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] : IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)

Full source

instance [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] :
    IsCentralScalar S (M →ₛₗ[σ₁₂] M₂) where
  op_smul_eq_smul _ _ := ext fun _ ↦ op_smul_eq_smul _ _

Centrality of Scalar Multiplication on Semilinear Maps

Informal description

For any semilinear map $f \colon M \to_{\sigma_{12}} M_2$ between modules, if the scalar multiplication by $S$ on $M_2$ is central (i.e., the left and right actions coincide), then the induced scalar multiplication on the space of semilinear maps is also central.

LinearMap.instZero instance

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

Full source

/-- The constant 0 map is linear. -/
instance : Zero (M →ₛₗ[σ₁₂] M₂) :=
  ⟨{  toFun := 0
      map_add' := by simp
      map_smul' := by simp }⟩

The Zero Map is Semilinear

Informal description

The zero map between two modules $M$ and $M₂$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma \colon R \to S$, is a semilinear map. That is, the map $0 \colon M \to M₂$ defined by $0(x) = 0$ for all $x \in M$ satisfies: 1. $0(x + y) = 0(x) + 0(y)$ for all $x, y \in M$ 2. $0(c \cdot x) = \sigma(c) \cdot 0(x)$ for all $c \in R$ and $x \in M$

LinearMap.zero_apply theorem

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

Full source

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

Zero Semilinear Map Evaluates to Zero: $0(x) = 0$

Informal description

For any element $x$ in an $R$-module $M$, the zero semilinear map $0 \colon M \to_{σ} M₂$ satisfies $0(x) = 0$.

LinearMap.comp_zero theorem

(g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0

Full source

@[simp]
theorem comp_zero (g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 :=
  ext fun c ↦ by rw [comp_apply, zero_apply, zero_apply, g.map_zero]

Composition with Zero Map Yields Zero Map: $g \circ 0 = 0$

Informal description

For any semilinear map $g \colon M_2 \to_{\sigma_{23}} M_3$ between modules $M_2$ and $M_3$ with respect to a ring homomorphism $\sigma_{23} \colon S \to T$, the composition of $g$ with the zero map $0 \colon M \to_{\sigma_{12}} M_2$ is equal to the zero map $0 \colon M \to_{\sigma_{13}} M_3$. That is, $g \circ 0 = 0$.

LinearMap.zero_comp theorem

(f : M →ₛₗ[σ₁₂] M₂) : ((0 : M₂ →ₛₗ[σ₂₃] M₃).comp f : M →ₛₗ[σ₁₃] M₃) = 0

Full source

@[simp]
theorem zero_comp (f : M →ₛₗ[σ₁₂] M₂) : ((0 : M₂ →ₛₗ[σ₂₃] M₃).comp f : M →ₛₗ[σ₁₃] M₃) = 0 :=
  rfl

Composition with Zero Map Yields Zero Map: $0 \circ f = 0$

Informal description

For any semilinear map $f \colon M \to_{\sigma_{12}} M_2$ between modules $M$ and $M_2$ with respect to a ring homomorphism $\sigma_{12} \colon R \to S$, the composition of the zero map $0 \colon M_2 \to_{\sigma_{23}} M_3$ with $f$ is equal to the zero map $0 \colon M \to_{\sigma_{13}} M_3$. That is, $0 \circ f = 0$.

LinearMap.instInhabited instance

: Inhabited (M →ₛₗ[σ₁₂] M₂)

Full source

instance : Inhabited (M →ₛₗ[σ₁₂] M₂) :=
  ⟨0⟩

Inhabited Type of Semilinear Maps

Informal description

For any semilinear maps between modules $M$ and $M₂$ with respect to a ring homomorphism $\sigma \colon R \to S$, the type $M \to_{ₛₗ}[\sigma] M₂$ is inhabited. In particular, the zero map serves as a default inhabitant.

LinearMap.default_def theorem

: (default : M →ₛₗ[σ₁₂] M₂) = 0

Full source

@[simp]
theorem default_def : (default : M →ₛₗ[σ₁₂] M₂) = 0 :=
  rfl

Default Semilinear Map is Zero Map

Informal description

The default semilinear map from $M$ to $M₂$ with respect to a ring homomorphism $\sigma \colon R \to S$ is the zero map, i.e., $\text{default} = 0$.

LinearMap.uniqueOfLeft instance

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

Full source

instance uniqueOfLeft [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂) :=
  { inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)) with
    uniq := fun f => ext fun x => by rw [Subsingleton.elim x 0, map_zero, map_zero] }

Uniqueness of Semilinear Maps from Subsingleton Domain

Informal description

For any modules $M$ over a semiring $R$ and $M₂$ over a semiring $S$ with respect to a ring homomorphism $\sigma \colon R \to S$, if $M$ is a subsingleton (i.e., has at most one element), then the type of semilinear maps $M \to_{ₛₗ}[\sigma] M₂$ has exactly one element, namely the zero map.

LinearMap.uniqueOfRight instance

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

Full source

instance uniqueOfRight [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂) :=
  coe_injective.unique

Uniqueness of Semilinear Maps to Subsingleton Codomain

Informal description

If the codomain module $M₂$ is a subsingleton (i.e., has at most one element), then the space of semilinear maps $M \to_{\sigma} M₂$ is unique (has exactly one element, the zero map).

LinearMap.ne_zero_of_injective theorem

[Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂} (hf : Injective f) : f ≠ 0

Full source

theorem ne_zero_of_injective [Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂} (hf : Injective f) : f ≠ 0 :=
  have ⟨x, ne⟩ := exists_ne (0 : M)
  fun h ↦ hf.ne ne <| by simp [h]

Injective Semilinear Maps from Nontrivial Modules Are Nonzero

Informal description

Let $M$ be a nontrivial module over a semiring $R$, and $M₂$ be a module over a semiring $S$ with respect to a ring homomorphism $\sigma \colon R \to S$. If $f \colon M \to M₂$ is an injective semilinear map, then $f$ is not the zero map.

LinearMap.ne_zero_of_surjective theorem

[Nontrivial M₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : Surjective f) : f ≠ 0

Full source

theorem ne_zero_of_surjective [Nontrivial M₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : Surjective f) : f ≠ 0 := by
  have ⟨y, ne⟩ := exists_ne (0 : M₂)
  obtain ⟨x, rfl⟩ := hf y
  exact fun h ↦ ne congr($h x)

Surjective Semilinear Maps to Nontrivial Modules are Nonzero

Informal description

Let $M$ and $M₂$ be modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma \colon R \to S$. If $M₂$ is nontrivial and $f \colon M \to M₂$ is a surjective semilinear map with respect to $\sigma$, then $f$ is not the zero map.

LinearMap.instAdd instance

: Add (M →ₛₗ[σ₁₂] M₂)

Full source

/-- The sum of two linear maps is linear. -/
instance : Add (M →ₛₗ[σ₁₂] M₂) :=
  ⟨fun f g ↦
    { toFun := f + g
      map_add' := by simp [add_comm, add_left_comm]
      map_smul' := by simp [smul_add] }⟩

Addition of Semilinear Maps

Informal description

The set of semilinear maps between two modules $M$ and $M₂$ over rings $R$ and $S$ (with respect to a ring homomorphism $\sigma \colon R \to S$) forms an additive structure, where the sum of two semilinear maps $f$ and $g$ is defined pointwise as $(f + g)(x) = f(x) + g(x)$ for all $x \in M$.

LinearMap.add_apply theorem

(f g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x

Full source

@[simp]
theorem add_apply (f g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x :=
  rfl

Pointwise Addition of Semilinear Maps

Informal description

For any semilinear maps $f, g \colon M \to_{σ} M₂$ and any element $x \in M$, the evaluation of their sum at $x$ equals the sum of their evaluations, i.e., $(f + g)(x) = f(x) + g(x)$.

LinearMap.add_comp theorem

 (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) : ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f

Full source

theorem add_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) :
    ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f :=
  rfl

Distributivity of Composition over Addition for Semilinear Maps

Informal description

Let $M$, $M_2$, and $M_3$ be modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$ forming a `RingHomCompTriple` with $\sigma_{13} \colon R \to T$. For any semilinear maps $f \colon M \to_{\sigma_{12}} M_2$ and $g, h \colon M_2 \to_{\sigma_{23}} M_3$, the composition of the sum $g + h$ with $f$ equals the sum of the compositions: $$(g + h) \circ f = (g \circ f) + (h \circ f).$$

LinearMap.comp_add theorem

 (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g

Full source

theorem comp_add (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
    (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g :=
  ext fun _ ↦ h.map_add _ _

Additivity of Composition for Semilinear Maps

Informal description

Let $M$, $M₂$, and $M₃$ be modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$ forming a `RingHomCompTriple` with $\sigma_{13} \colon R \to T$. For any semilinear maps $f, g \colon M \to_{\sigma_{12}} M₂$ and $h \colon M₂ \to_{\sigma_{23}} M₃$, the composition of $h$ with the sum $f + g$ equals the sum of the compositions: $$h \circ (f + g) = (h \circ f) + (h \circ g).$$

LinearMap.addCommMonoid instance

: AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

Full source

/-- The type of linear maps is an additive monoid. -/
instance addCommMonoid : AddCommMonoid (M →ₛₗ[σ₁₂] M₂) :=
  DFunLike.coe_injective.addCommMonoid _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl

Additive Commutative Monoid Structure on Semilinear Maps

Informal description

The set of semilinear maps $M \to_{\sigma} M₂$ between two modules $M$ and $M₂$ over semirings $R$ and $S$ (with respect to a ring homomorphism $\sigma \colon R \to S$) forms an additive commutative monoid, where addition is defined pointwise and the zero map serves as the additive identity.

LinearMap.instNeg instance

: Neg (M →ₛₗ[σ₁₂] N₂)

Full source

/-- The negation of a linear map is linear. -/
instance : Neg (M →ₛₗ[σ₁₂] N₂) :=
  ⟨fun f ↦
    { toFun := -f
      map_add' := by simp [add_comm]
      map_smul' := by simp }⟩

Negation of Semilinear Maps

Informal description

For any semilinear map $f \colon M \to_{\sigma} N₂$ between modules, the negation $-f$ is also a semilinear map.

LinearMap.neg_apply theorem

(f : M →ₛₗ[σ₁₂] N₂) (x : M) : (-f) x = -f x

Full source

@[simp]
theorem neg_apply (f : M →ₛₗ[σ₁₂] N₂) (x : M) : (-f) x = -f x :=
  rfl

Negation of Semilinear Map Evaluation: $(-f)(x) = -f(x)$

Informal description

For any semilinear map $f \colon M \to_{\sigma} N₂$ and any element $x \in M$, the evaluation of the negated map $-f$ at $x$ equals the negation of the evaluation of $f$ at $x$, i.e., $(-f)(x) = -f(x)$.

LinearMap.neg_comp theorem

(f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f

Full source

@[simp]
theorem neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f :=
  rfl

Negation and Composition of Semilinear Maps: $(-g) \circ f = -(g \circ f)$

Informal description

For any semilinear maps $f \colon M \to_{\sigma_{12}} M_2$ and $g \colon M_2 \to_{\sigma_{23}} N_3$, the composition of the negation of $g$ with $f$ equals the negation of the composition of $g$ with $f$, i.e., $(-g) \circ f = -(g \circ f)$.

LinearMap.comp_neg theorem

(f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (-f) = -g.comp f

Full source

@[simp]
theorem comp_neg (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (-f) = -g.comp f :=
  ext fun _ ↦ g.map_neg _

Composition with Negated Semilinear Map: $g \circ (-f) = -(g \circ f)$

Informal description

Let $M$, $N₂$, and $N₃$ be modules over semirings with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$. For any semilinear maps $f \colon M \to_{\sigma_{12}} N₂$ and $g \colon N₂ \to_{\sigma_{23}} N₃$, the composition of $g$ with the negation of $f$ equals the negation of the composition of $g$ with $f$, i.e., $g \circ (-f) = -(g \circ f)$.

LinearMap.instSub instance

: Sub (M →ₛₗ[σ₁₂] N₂)

Full source

/-- The subtraction of two linear maps is linear. -/
instance : Sub (M →ₛₗ[σ₁₂] N₂) :=
  ⟨fun f g ↦
    { toFun := f - g
      map_add' := fun x y ↦ by simp only [Pi.sub_apply, map_add, add_sub_add_comm]
      map_smul' := fun r x ↦ by simp [Pi.sub_apply, map_smul, smul_sub] }⟩

Subtraction of Semilinear Maps

Informal description

For any two semilinear maps $f, g \colon M \to_{\sigma} N₂$ between modules, the difference $f - g$ is also a semilinear map.

LinearMap.sub_apply theorem

(f g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x

Full source

@[simp]
theorem sub_apply (f g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x :=
  rfl

Evaluation of Difference of Semilinear Maps

Informal description

Let $M$ and $N₂$ be modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma \colon R \to S$. For any two semilinear maps $f, g \colon M \to_{\sigma} N₂$ and any element $x \in M$, the evaluation of the difference map at $x$ satisfies $(f - g)(x) = f(x) - g(x)$.

LinearMap.sub_comp theorem

(f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) : (g - h).comp f = g.comp f - h.comp f

Full source

theorem sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) :
    (g - h).comp f = g.comp f - h.comp f :=
  rfl

Composition Distributes Over Subtraction of Semilinear Maps

Informal description

Let $M$, $M₂$, and $N₃$ be modules over semirings with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$. For any semilinear map $f \colon M \to_{\sigma_{12}} M₂$ and semilinear maps $g, h \colon M₂ \to_{\sigma_{23}} N₃$, the composition of the difference $(g - h)$ with $f$ equals the difference of the compositions $(g \circ f) - (h \circ f)$. In other words: $$(g - h) \circ f = g \circ f - h \circ f$$

LinearMap.comp_sub theorem

(f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : h.comp (g - f) = h.comp g - h.comp f

Full source

theorem comp_sub (f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
    h.comp (g - f) = h.comp g - h.comp f :=
  ext fun _ ↦ h.map_sub _ _

Composition Distributes Over Subtraction of Semilinear Maps in Reverse Order

Informal description

Let $M$, $N₂$, and $N₃$ be modules over semirings with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$. For any semilinear maps $f, g \colon M \to_{\sigma_{12}} N₂$ and any semilinear map $h \colon N₂ \to_{\sigma_{23}} N₃$, the composition of $h$ with the difference $(g - f)$ equals the difference of the compositions $(h \circ g) - (h \circ f)$. In other words: $$h \circ (g - f) = h \circ g - h \circ f$$

LinearMap.addCommGroup instance

: AddCommGroup (M →ₛₗ[σ₁₂] N₂)

Full source

/-- The type of linear maps is an additive group. -/
instance addCommGroup : AddCommGroup (M →ₛₗ[σ₁₂] N₂) :=
  DFunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) fun _ _ ↦ rfl

Additive Commutative Group Structure on Semilinear Maps

Informal description

The set of semilinear maps $M \to_{\sigma} N₂$ between two modules $M$ and $N₂$ over semirings $R$ and $S$ (with respect to a ring homomorphism $\sigma \colon R \to S$) forms an additive commutative group, where addition is defined pointwise and the zero map serves as the additive identity.

LinearMap.evalAddMonoidHom definition

(a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂

Full source

/-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `AddMonoidHom`. -/
@[simps]
def evalAddMonoidHom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂ where
  toFun f := f a
  map_add' f g := LinearMap.add_apply f g a
  map_zero' := rfl

Evaluation at a point as an additive monoid homomorphism

Informal description

For a fixed element $a \in M$, the evaluation map that sends a semilinear map $f \colon M \to_{\sigma} M₂$ to its value $f(a) \in M₂$ is an additive monoid homomorphism from the space of semilinear maps to $M₂$. That is, it satisfies: 1. $(f + g)(a) = f(a) + g(a)$ for all semilinear maps $f, g$ 2. The zero map evaluates to $0 \in M₂$ at $a$ Here, $\sigma \colon R \to S$ is a ring homomorphism between semirings $R$ and $S$, and $M$ and $M₂$ are modules over $R$ and $S$ respectively.

LinearMap.toAddMonoidHom' definition

: (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

Full source

/-- `LinearMap.toAddMonoidHom` promoted to an `AddMonoidHom`. -/
@[simps]
def toAddMonoidHom' : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂ where
  toFun := toAddMonoidHom
  map_zero' := by ext; rfl
  map_add' := by intros; ext; rfl

Additive monoid homomorphism of semilinear maps to additive monoid homomorphisms

Informal description

The function that converts a semilinear map $f \colon M \to_{\sigma} M₂$ between modules to an additive monoid homomorphism is itself an additive monoid homomorphism from the space of semilinear maps to the space of additive monoid homomorphisms. Specifically: 1. The zero semilinear map is mapped to the zero additive monoid homomorphism. 2. The sum of two semilinear maps is mapped to the sum of their corresponding additive monoid homomorphisms. Here, $\sigma \colon R \to S$ is a ring homomorphism between semirings $R$ and $S$, and $M$ and $M₂$ are modules over $R$ and $S$ respectively.

LinearMap.identityMapOfZeroModuleIsZero theorem

[Subsingleton M] : id (R := R₁) (M := M) = 0

Full source

/-- If `M` is the zero module, then the identity map of `M` is the zero map. -/
@[simp]
theorem identityMapOfZeroModuleIsZero [Subsingleton M] : id (R := R₁) (M := M) = 0 :=
  Subsingleton.eq_zero id

Identity Map Equals Zero Map for Zero Module

Informal description

If $M$ is a zero module (i.e., a module with at most one element), then the identity linear map on $M$ is equal to the zero map.

LinearMap.instDistribMulAction instance

: DistribMulAction S (M →ₛₗ[σ₁₂] M₂)

Full source

instance : DistribMulAction S (M →ₛₗ[σ₁₂] M₂) where
  one_smul _ := ext fun _ ↦ one_smul _ _
  mul_smul _ _ _ := ext fun _ ↦ mul_smul _ _ _
  smul_add _ _ _ := ext fun _ ↦ smul_add _ _ _
  smul_zero _ := ext fun _ ↦ smul_zero _

Distributive Multiplicative Action on Semilinear Maps

Informal description

The set of semilinear maps $M \to_{\sigma} M₂$ between two modules $M$ and $M₂$ over semirings $R$ and $S$ (with respect to a ring homomorphism $\sigma \colon R \to S$) forms a distributive multiplicative action structure, where scalar multiplication by elements of $S$ is defined pointwise.

LinearMap.smul_comp theorem

(a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : (a • g).comp f = a • g.comp f

Full source

theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) :
    (a • g).comp f = a • g.comp f :=
  rfl

Compatibility of scalar multiplication with composition of semilinear maps: $(a \cdot g) \circ f = a \cdot (g \circ f)$

Informal description

Let $S_3$ be a semiring, and let $M$, $M_2$, and $M_3$ be modules over semirings with appropriate ring homomorphisms $\sigma_{12} \colon R \to S_2$, $\sigma_{23} \colon S_2 \to S_3$, and $\sigma_{13} \colon R \to S_3$ forming a `RingHomCompTriple`. For any scalar $a \in S_3$, any semilinear map $g \colon M_2 \to_{\sigma_{23}} M_3$, and any semilinear map $f \colon M \to_{\sigma_{12}} M_2$, the composition of the scalar multiple $a \cdot g$ with $f$ equals the scalar multiple $a$ applied to the composition $g \circ f$, i.e., $$(a \cdot g) \circ f = a \cdot (g \circ f).$$

LinearMap.comp_smul theorem

 [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃]
  [CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • g.comp f

Full source

theorem comp_smul [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃]
    [SMulCommClass R S M₃] [CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
    g.comp (a • f) = a • g.comp f :=
  ext fun _ ↦ g.map_smul_of_tower _ _

Compatibility of scalar multiplication with composition of linear maps: $g \circ (a \cdot f) = a \cdot (g \circ f)$

Informal description

Let $R$ and $S$ be semirings, and let $M$, $M_2$, and $M_3$ be modules over $R$ and $S$ with compatible scalar multiplications. For any $R$-linear map $g \colon M_3 \to M_2$, any scalar $a \in S$, and any $R$-linear map $f \colon M \to M_3$, the composition of $g$ with the scalar multiple $a \cdot f$ equals the scalar multiple $a$ applied to the composition $g \circ f$, i.e., $$g \circ (a \cdot f) = a \cdot (g \circ f).$$

LinearMap.module instance

: Module S (M →ₛₗ[σ₁₂] M₂)

Full source

instance module : Module S (M →ₛₗ[σ₁₂] M₂) where
  add_smul _ _ _ := ext fun _ ↦ add_smul _ _ _
  zero_smul _ := ext fun _ ↦ zero_smul _ _

Module Structure on Semilinear Maps

Informal description

The set of semilinear maps $M \to_{\sigma} M₂$ between two modules $M$ and $M₂$ over semirings $R$ and $S$ (with respect to a ring homomorphism $\sigma \colon R \to S$) forms a module over $S$, where addition and scalar multiplication are defined pointwise.

LinearMap.restrictScalars_zero theorem

: (0 : M →ₗ[S] N).restrictScalars R = 0

Full source

@[simp]
lemma restrictScalars_zero : (0 : M →ₗ[S] N).restrictScalars R = 0 :=
  rfl

Restriction of scalars preserves the zero map

Informal description

For the zero linear map $0 \colon M \to N$ between modules over a semiring $S$, the restriction of scalars to a semiring $R$ yields the zero map, i.e., $0.\text{restrictScalars}_R = 0$.

LinearMap.restrictScalars_add theorem

(f g : M →ₗ[S] N) : (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R

Full source

@[simp]
theorem restrictScalars_add (f g : M →ₗ[S] N) :
    (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R :=
  rfl

Additivity of Restriction of Scalars for Linear Maps

Informal description

For any two $S$-linear maps $f, g \colon M \to N$, the restriction of scalars of their sum equals the sum of their restrictions of scalars. That is, $(f + g).\text{restrictScalars}_R = f.\text{restrictScalars}_R + g.\text{restrictScalars}_R$.

LinearMap.restrictScalars_neg theorem

 {M N : Type*} [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [Module S M] [Module S N]
  [CompatibleSMul M N R S] (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R

Full source

@[simp]
theorem restrictScalars_neg {M N : Type*} [AddCommMonoid M] [AddCommGroup N]
    [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S]
    (f : M →ₗ[S] N) : (-f).restrictScalars R = -f.restrictScalars R :=
  rfl

Negation Commutes with Restriction of Scalars for Linear Maps

Informal description

Let $M$ be an additive commutative monoid and $N$ an additive commutative group, both equipped with compatible $R$-module and $S$-module structures. For any $S$-linear map $f \colon M \to N$, the restriction of scalars of the negation $-f$ equals the negation of the restriction of scalars of $f$, i.e., $$(-f)\restrictScalars R = -(f\restrictScalars R).$$

LinearMap.restrictScalars_smul theorem

(c : R₁) (f : M →ₗ[S] N) : (c • f).restrictScalars R = c • f.restrictScalars R

Full source

@[simp]
theorem restrictScalars_smul (c : R₁) (f : M →ₗ[S] N) :
    (c • f).restrictScalars R = c • f.restrictScalars R :=
  rfl

Compatibility of Scalar Multiplication with Restriction of Scalars for Linear Maps

Informal description

Let $R$, $S$ be semirings, and let $M$, $N$ be modules over both $R$ and $S$ with compatible scalar multiplications. For any scalar $c \in R_1$ and any $S$-linear map $f \colon M \to N$, the restriction of scalars of the scalar multiple $c \cdot f$ equals the scalar multiple of the restriction of scalars of $f$, i.e., $$(c \cdot f)\!\restriction_R = c \cdot (f\!\restriction_R).$$

LinearMap.restrictScalars_comp theorem

 [AddCommMonoid P] [Module S P] [Module R P] [CompatibleSMul N P R S] [CompatibleSMul M P R S] (f : N →ₗ[S] P)
  (g : M →ₗ[S] N) : (f ∘ₗ g).restrictScalars R = f.restrictScalars R ∘ₗ g.restrictScalars R

Full source

@[simp]
lemma restrictScalars_comp [AddCommMonoid P] [Module S P] [Module R P]
    [CompatibleSMul N P R S] [CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) :
    (f ∘ₗ g).restrictScalars R = f.restrictScalars R ∘ₗ g.restrictScalars R := by
  rfl

Compatibility of Restriction of Scalars with Composition of Linear Maps

Informal description

Let $R$ and $S$ be semirings, and let $M$, $N$, and $P$ be additive commutative monoids equipped with compatible $R$- and $S$-module structures. For any $S$-linear maps $f \colon N \to P$ and $g \colon M \to N$, the restriction of scalars of the composition $f \circ g$ equals the composition of the restrictions of scalars of $f$ and $g$, i.e., $$(f \circ g)\restriction_R = f\restriction_R \circ g\restriction_R.$$

LinearMap.restrictScalars_trans theorem

 {T : Type*} [Semiring T] [Module T M] [Module T N] [CompatibleSMul M N S T] [CompatibleSMul M N R T] (f : M →ₗ[T] N) :
  (f.restrictScalars S).restrictScalars R = f.restrictScalars R

Full source

@[simp]
lemma restrictScalars_trans {T : Type*} [Semiring T] [Module T M] [Module T N]
    [CompatibleSMul M N S T] [CompatibleSMul M N R T] (f : M →ₗ[T] N) :
    (f.restrictScalars S).restrictScalars R = f.restrictScalars R :=
  rfl

Transitivity of Scalar Restriction for Linear Maps

Informal description

Let $R$, $S$, and $T$ be semirings, and let $M$ and $N$ be modules over $T$ with compatible scalar multiplications from $R$ and $S$. For any $T$-linear map $f \colon M \to N$, the restriction of scalars from $S$ to $R$ of the restriction from $T$ to $S$ of $f$ is equal to the restriction of scalars from $T$ directly to $R$ of $f$. That is, $(f|_{S})|_{R} = f|_{R}$.

LinearMap.restrictScalarsₗ definition

: (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N

Full source

/-- `LinearMap.restrictScalars` as a `LinearMap`. -/
@[simps apply]
def restrictScalarsₗ : (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N where
  toFun := restrictScalars R
  map_add' := restrictScalars_add
  map_smul' := restrictScalars_smul

Linear map of scalar restriction for linear maps

Informal description

The linear map that restricts the scalars of an $S$-linear map $f \colon M \to N$ to $R$, where $M$ and $N$ are modules over both $R$ and $S$ with compatible scalar multiplications. The map sends an $S$-linear map $f$ to its restriction as an $R$-linear map, preserving addition and scalar multiplication.

Mathlib.Algebra.Module.LinearMap.Defs

Implementation notes

Notation

TODO

Tags