(Semi)linear maps

In this file we define

• LinearMap σ M M₂, M →ₛₗ[σ] M₂ : a semilinear map between two Modules. Here, σ is a RingHom from R to R₂ and an f : M →ₛₗ[σ] M₂ satisfies f (c • x) = (σ c) • (f x). We recover plain linear maps by choosing σ to be RingHom.id R. This is denoted by M →ₗ[R] M₂. We also add the notation M →ₗ⋆[R] M₂ for star-linear maps.

• IsLinearMap R f : predicate saying that f : M → M₂ is a linear map. (Note that this was not generalized to semilinear maps.)

We then provide LinearMap with the following instances:

• LinearMap.addCommMonoid and LinearMap.addCommGroup: the elementwise addition structures corresponding to addition in the codomain
• LinearMap.distribMulAction and LinearMap.module: the elementwise scalar action structures corresponding to applying the action in the codomain.
• Module.End.semiring and Module.End.ring: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.

Implementation notes

To ensure that composition works smoothly for semilinear maps, we use the typeclasses RingHomCompTriple, RingHomInvPair and RingHomSurjective from Mathlib.Algebra.Ring.CompTypeclasses.

Notation

• Throughout the file, we denote regular linear maps by fₗ, gₗ, etc, and semilinear maps by f, g, etc.

TODO

• Parts of this file have not yet been generalized to semilinear maps (i.e. CompatibleSMul)

Tags

linear map

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

• map_add : ∀ (x y : M), f (x + y) = f x + f y

  A linear map preserves addition.

• map_smul : ∀ (c : R) (x : M), f (c • x) = c • f x

  A linear map preserves scalar multiplication.

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 LinearMap {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_19) (M₂ : Type u_20) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHom : Type (max u_19 u_20)

• toFun : M → M₂
• map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑σ r • AddHom.toFun s.toAddHom x

  A linear map preserves scalar multiplication. We prefer the spelling _root_.map_smul instead.

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.

def «term_→ₛₗ[_]_» : Lean.TrailingParserDescr

M →ₛₗ[σ] N is the type of σ-semilinear maps from M to N.

Equations

• One or more equations did not get rendered due to their size.

def «term_→ₗ[_]_» : Lean.TrailingParserDescr

M →ₗ[R] N is the type of R-linear maps from M to N.

Equations

• One or more equations did not get rendered due to their size.

def «term_→ₗ⋆[_]_» : Lean.TrailingParserDescr

M →ₗ⋆[R] N is the type of R-conjugate-linear maps from M to N.

Equations

• One or more equations did not get rendered due to their size.

class SemilinearMapClass (F : Type u_17) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_20)) (M₂ : outParam (Type u_21)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHomClass : Type (max (max u_17 u_20) u_21)

• coe : F → M → M₂
• coe_injective' : Function.Injective FunLike.coe
• map_add : ∀ (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
• map_smulₛₗ : ∀ (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x

  A semilinear map preserves scalar multiplication up to some ring homomorphism σ. See also _root_.map_smul for the case where σ is the identity.

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.

@[inline, reducible]

abbrev LinearMapClass (F : Type u_17) (R : outParam (Type u_18)) (M : outParam (Type u_19)) (M₂ : outParam (Type u_20)) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : Type (max (max u_17 u_19) u_20)

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

Equations

• LinearMapClass F R M M₂ = SemilinearMapClass F (RingHom.id R) M M₂

instance SemilinearMapClass.addMonoidHomClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [SemilinearMapClass F σ M M₃] : AddMonoidHomClass F M M₃

Equations

• SemilinearMapClass.addMonoidHomClass F = let src := SemilinearMapClass.toAddHomClass; AddMonoidHomClass.mk (_ : ∀ (f : F), ↑f 0 = 0)

instance SemilinearMapClass.distribMulActionHomClass {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} (F : Type u_17) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [LinearMapClass F R M M₂] : DistribMulActionHomClass F R M M₂

Equations

• One or more equations did not get rendered due to their size.

theorem SemilinearMapClass.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • ↑f x = ↑f (↑σ' c • x)

instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃

Equations

• LinearMap.semilinearMapClass = SemilinearMapClass.mk (_ : ∀ (self : M →ₛₗ[σ] M₃) (r : R) (x : M), AddHom.toFun self.toAddHom (r • x) = ↑σ r • AddHom.toFun self.toAddHom x)

instance LinearMap.instFunLike {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M fun x => M₃

Equations

• LinearMap.instFunLike = let src := AddHomClass.toFunLike; { coe := FunLike.coe, coe_injective' := (_ : Function.Injective FunLike.coe) }

def LinearMap.toDistribMulActionHom {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) : M →+[R] M₂

The DistribMulActionHom underlying a LinearMap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : ↑f.toAddHom = ↑f

theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} : f.toFun = ↑f

theorem LinearMap.ext {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), ↑f x = ↑g x) : f = g

def LinearMap.copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f) : M →ₛₗ[σ] M₃

Copy of a LinearMap with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f) : ↑(LinearMap.copy f f' h) = f'

theorem LinearMap.copy_eq {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ↑f) : LinearMap.copy f f' h = f

@[simp]

theorem LinearMap.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x) : ↑{ toAddHom := f, map_smul' := h } = ↑f

@[simp]

theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r • x) = ↑σ r • AddHom.toFun f x) : ↑{ toAddHom := f, map_smul' := h } = f

def LinearMap.id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] M

Identity map as a LinearMap

Equations

• One or more equations did not get rendered due to their size.

theorem LinearMap.id_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑LinearMap.id x = x

@[simp]

theorem LinearMap.id_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : ↑LinearMap.id = id

@[simp]

theorem LinearMap.id'_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] (x : M) : ↑LinearMap.id' x = x

def LinearMap.id' {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M

A generalisation of LinearMap.id that constructs the identity function as a σ-semilinear map for any ring homomorphism σ which we know is the identity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.id'_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] : ↑LinearMap.id' = id

theorem LinearMap.isLinear {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) : IsLinearMap R ↑fₗ

theorem LinearMap.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : Function.Injective FunLike.coe

theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x : M} {x' : M} : x = x' → ↑f x = ↑f x'

theorem LinearMap.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : f = g) (x : M) : ↑f x = ↑g x

If two linear maps are equal, they are equal at each point.

theorem LinearMap.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} : f = g ↔ ∀ (x : M), ↑f x = ↑g x

@[simp]

theorem LinearMap.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), AddHom.toFun (↑f) (r • x) = ↑σ r • AddHom.toFun (↑f) x) : { toAddHom := ↑f, map_smul' := h } = f

theorem LinearMap.map_add {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x : M) (y : M) : ↑f (x + y) = ↑f x + ↑f y

theorem LinearMap.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : ↑f 0 = 0

theorem LinearMap.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (c : R) (x : M) : ↑f (c • x) = ↑σ c • ↑f x

theorem LinearMap.map_smul {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M) : ↑fₗ (c • x) = c • ↑fₗ x

theorem LinearMap.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • ↑f x = ↑f (↑σ' c • x)

@[simp]

theorem LinearMap.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : Function.Injective ↑f) {x : M} : ↑f x = 0 ↔ x = 0

@[simp]

theorem image_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [SemilinearMapClass F σ M M₃] (c : R) (s : Set M) : ↑h '' (c • s) = ↑σ c • ↑h '' s

theorem preimage_smul_setₛₗ {R : Type u_1} {S : Type u_6} (M : Type u_9) (M₃ : Type u_12) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] (σ : R →+* S) {F : Type u_17} (h : F) [SemilinearMapClass F σ M M₃] {c : R} (hc : IsUnit c) (s : Set M₃) : ↑h ⁻¹' (↑σ c • s) = c • ↑h ⁻¹' s

theorem image_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type u_17} (h : F) [LinearMapClass F R M M₂] (c : R) (s : Set M) : ↑h '' (c • s) = c • ↑h '' s

theorem preimage_smul_set (R : Type u_1) (M : Type u_9) (M₂ : Type u_11) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type u_17} (h : F) [LinearMapClass F R M M₂] {c : R} (hc : IsUnit c) (s : Set M₂) : ↑h ⁻¹' (c • s) = c • ↑h ⁻¹' s

class LinearMap.CompatibleSMul (M : Type u_9) (M₂ : Type u_11) [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_17) (S : Type u_18) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] : Prop

• map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), ↑fₗ (c • x) = c • ↑fₗ x

  Scalar multiplication by R of M can be moved through linear maps.

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.intModule, allowing z • to be moved even if R does not support negation.

instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R S] [SMul R M] [Module S M] [IsScalarTower R S M] [SMul R M₂] [Module S M₂] [IsScalarTower R S M₂] : LinearMap.CompatibleSMul M M₂ R S

Equations

• @LinearMap.IsScalarTower.compatibleSMul = @LinearMap.IsScalarTower.compatibleSMul.proof_1

@[simp]

theorem LinearMap.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : ↑fₗ (c • x) = c • ↑fₗ x

def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : M →+ M₃

convert a linear map to an additive map

Equations

• LinearMap.toAddMonoidHom f = { toZeroHom := { toFun := ↑f, map_zero' := (_ : ↑f 0 = 0) }, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) }

@[simp]

theorem LinearMap.toAddMonoidHom_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) : ↑(LinearMap.toAddMonoidHom f) = ↑f

def LinearMap.restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂

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.

Equations

• ↑R fₗ = { toAddHom := { toFun := ↑fₗ, map_add' := (_ : ∀ (x y : M), ↑fₗ (x + y) = ↑fₗ x + ↑fₗ y) }, map_smul' := (_ : ∀ (c : R) (x : M), ↑fₗ (c • x) = c • ↑fₗ x) }

instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)

Equations

• LinearMap.coeIsScalarTower R = { coe := ↑R }

@[simp]

theorem LinearMap.coe_restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) : ↑(↑R f) = ↑f

theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) : ↑(↑R fₗ) x = ↑fₗ x

theorem LinearMap.restrictScalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : Function.Injective ↑R

@[simp]

theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (gₗ : M →ₗ[S] M₂) : ↑R fₗ = ↑R gₗ ↔ fₗ = gₗ

theorem LinearMap.toAddMonoidHom_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} : Function.Injective LinearMap.toAddMonoidHom

theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : R →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : ↑f 1 = ↑g 1) : f = g

If two σ-linear maps from R are equal on 1, then they are equal.

theorem LinearMap.ext_ring_iff {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} {f : R →ₛₗ[σ] M} {g : R →ₛₗ[σ] M} : f = g ↔ ↑f 1 = ↑g 1

theorem LinearMap.ext_ring_op {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : Rᵐᵒᵖ →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : ↑f 1 = ↑g 1) : f = g

@[simp]

theorem RingHom.toSemilinearMap_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R →+* S) : ∀ (a : R), ↑(RingHom.toSemilinearMap f) a = OneHom.toFun (↑↑f) a

def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R →+* S) : R →ₛₗ[f] S

Interpret a RingHom f as an f-semilinear map.

Equations

• One or more equations did not get rendered due to their size.

def LinearMap.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₃] M₃

Composition of two linear maps is a linear map

Equations

• One or more equations did not get rendered due to their size.

def LinearMap.«term_∘ₗ_» : Lean.TrailingParserDescr

∘ₗ 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.

Equations

• LinearMap.«term_∘ₗ_» = Lean.ParserDescr.trailingNode `LinearMap.term_∘ₗ_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ₗ ") (Lean.ParserDescr.cat `term 80))

theorem LinearMap.comp_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁) : ↑(LinearMap.comp f g) x = ↑f (↑g x)

@[simp]

theorem LinearMap.coe_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) : ↑(LinearMap.comp f g) = ↑f ∘ ↑g

@[simp]

theorem LinearMap.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.comp f LinearMap.id = f

@[simp]

theorem LinearMap.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.comp LinearMap.id f = f

theorem LinearMap.comp_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_17} {M₄ : Type u_18} [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₄) : LinearMap.comp (LinearMap.comp h g) f = LinearMap.comp h (LinearMap.comp g f)

theorem Function.Surjective.injective_linearMapComp_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂} (hg : Function.Surjective ↑g) : Function.Injective fun f => LinearMap.comp f g

The linear map version of Function.Surjective.injective_comp_right

@[simp]

theorem LinearMap.cancel_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : Function.Surjective ↑g) : LinearMap.comp f g = LinearMap.comp f' g ↔ f = f'

theorem Function.Injective.injective_linearMapComp_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} (hf : Function.Injective ↑f) : Function.Injective fun g => LinearMap.comp f g

The linear map version of Function.Injective.comp_left

@[simp]

theorem LinearMap.cancel_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective ↑f) : LinearMap.comp f g = LinearMap.comp f g' ↔ g = g'

def LinearMap.inverse {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) : M₂ →ₛₗ[σ'] M

If a function g is a left and right inverse of a linear map f, then g is linear itself.

Equations

• One or more equations did not get rendered due to their size.

theorem LinearMap.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) : ↑f (-x) = -↑f x

theorem LinearMap.map_sub {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) (y : M) : ↑f (x - y) = ↑f x - ↑f y

instance LinearMap.CompatibleSMul.intModule {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {S : Type u_17} [Semiring S] [Module S M] [Module S M₂] : LinearMap.CompatibleSMul M M₂ ℤ S

Equations

• @LinearMap.CompatibleSMul.intModule = @LinearMap.CompatibleSMul.intModule.proof_1

instance LinearMap.CompatibleSMul.units {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_17} {S : Type u_18} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : LinearMap.CompatibleSMul M M₂ Rˣ S

Equations

• @LinearMap.CompatibleSMul.units = @LinearMap.CompatibleSMul.units.proof_1

@[simp]

theorem Module.compHom.toLinearMap_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R →+* S) (a : R) : ↑(Module.compHom.toLinearMap g) a = ↑g a

def Module.compHom.toLinearMap {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R →+* S) : R →ₗ[R] S

g : R →+* S is R-linear when the module structure on S is Module.compHom S g .

Equations

• Module.compHom.toLinearMap g = { toAddHom := { toFun := ↑g, map_add' := (_ : ∀ (a b : R), ↑g (a + b) = ↑g a + ↑g b) }, map_smul' := (_ : ∀ (a b : R), ↑g (a * b) = ↑g a * ↑g b) }

def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →+[R] M₂) : M →ₗ[R] M₂

A DistribMulActionHom between two modules is a linear map.

Equations

• One or more equations did not get rendered due to their size.

instance DistribMulActionHom.instCoeTCDistribMulActionHomToMonoidToMonoidWithZeroToAddMonoidToDistribMulActionToAddMonoidToDistribMulActionLinearMapIdToNonAssocSemiring {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : CoeTC (M →+[R] M₂) (M →ₗ[R] M₂)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →+[R] M₂) : ↑↑f = ↑f

theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M →+[R] M₂} {g : M →+[R] M₂} (h : ↑f = ↑g) : f = g

def IsLinearMap.mk' {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) (H : IsLinearMap R f) : M →ₗ[R] M₂

Convert an IsLinearMap predicate to a LinearMap

Equations

• IsLinearMap.mk' f H = { toAddHom := { toFun := f, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }, map_smul' := (_ : ∀ (c : R) (x : M), f (c • x) = c • f x) }

@[simp]

theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (H : IsLinearMap R f) (x : M) : ↑(IsLinearMap.mk' f H) x = f x

theorem IsLinearMap.isLinearMap_smul {R : Type u_17} {M : Type u_18} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : IsLinearMap R fun z => c • z

theorem IsLinearMap.isLinearMap_smul' {R : Type u_17} {M : Type u_18} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : IsLinearMap R fun c => c • a

theorem IsLinearMap.map_zero {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) : f 0 = 0

theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] : IsLinearMap R fun z => -z

theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) : f (-x) = -f x

theorem IsLinearMap.map_sub {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M) (y : M) : f (x - y) = f x - f y

@[inline, reducible]

abbrev Module.End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v

Linear endomorphisms of a module, with associated ring structure Module.End.semiring and algebra structure Module.End.algebra.

Equations

• Module.End R M = (M →ₗ[R] M)

def AddMonoidHom.toNatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂

Reinterpret an additive homomorphism as an ℕ-linear map.

Equations

• AddMonoidHom.toNatLinearMap f = { toAddHom := { toFun := ↑f, map_add' := (_ : ∀ (a b : M), ↑f (a + b) = ↑f a + ↑f b) }, map_smul' := (_ : ∀ (n : ℕ) (a : M), ↑f (n • a) = n • ↑f a) }

theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] : Function.Injective AddMonoidHom.toNatLinearMap

def AddMonoidHom.toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂

Reinterpret an additive homomorphism as a ℤ-linear map.

Equations

• AddMonoidHom.toIntLinearMap f = { toAddHom := { toFun := ↑f, map_add' := (_ : ∀ (a b : M), ↑f (a + b) = ↑f a + ↑f b) }, map_smul' := (_ : ∀ (n : ℤ) (g : M), ↑f (n • g) = n • ↑f g) }

theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] : Function.Injective AddMonoidHom.toIntLinearMap

@[simp]

theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : ↑(AddMonoidHom.toIntLinearMap f) = ↑f

def AddMonoidHom.toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) : M →ₗ[ℚ] M₂

Reinterpret an additive homomorphism as a ℚ-linear map.

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] : Function.Injective AddMonoidHom.toRatLinearMap

@[simp]

theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) : ↑(AddMonoidHom.toRatLinearMap f) = ↑f

instance LinearMap.instSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] : SMul S (M →ₛₗ[σ₁₂] M₂)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : ↑(a • f) x = a • ↑f x

theorem LinearMap.coe_smul {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ↑(a • f) = a • ↑f

instance LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMulCommClass S T M₂] : SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)

Equations

• @LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap = @LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap.proof_1

instance LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)

Equations

• @LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap = @LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap.proof_1

instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] : IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)

Equations

• @LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid = @LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid.proof_1

Arithmetic on the codomain

instance LinearMap.instZeroLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Zero (M →ₛₗ[σ₁₂] M₂)

The constant 0 map is linear.

Equations

• LinearMap.instZeroLinearMap = { zero := { toAddHom := { toFun := 0, map_add' := (_ : M → M → 0 = 0 + 0) }, map_smul' := (_ : ∀ (a : R₁), M → 0 = ↑σ₁₂ a • 0) } }

@[simp]

theorem LinearMap.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (x : M) : ↑0 x = 0

@[simp]

theorem LinearMap.comp_zero {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.comp g 0 = 0

@[simp]

theorem LinearMap.zero_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) : LinearMap.comp 0 f = 0

instance LinearMap.instInhabitedLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Inhabited (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.instInhabitedLinearMap = { default := 0 }

@[simp]

theorem LinearMap.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : default = 0

instance LinearMap.instAddLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : Add (M →ₛₗ[σ₁₂] M₂)

The sum of two linear maps is linear.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (x : M) : ↑(f + g) x = ↑f x + ↑g x

theorem LinearMap.add_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.comp (h + g) f = LinearMap.comp h f + LinearMap.comp g f

theorem LinearMap.comp_add {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : LinearMap.comp h (f + g) = LinearMap.comp h f + LinearMap.comp h g

instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} : AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

The type of linear maps is an additive monoid.

Equations

• One or more equations did not get rendered due to their size.

instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : Neg (M →ₛₗ[σ₁₂] N₂)

The negation of a linear map is linear.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) : ↑(-f) x = -↑f x

@[simp]

theorem LinearMap.neg_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : LinearMap.comp (-g) f = -LinearMap.comp g f

@[simp]

theorem LinearMap.comp_neg {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : LinearMap.comp g (-f) = -LinearMap.comp g f

instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : Sub (M →ₛₗ[σ₁₂] N₂)

The subtraction of two linear maps is linear.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (x : M) : ↑(f - g) x = ↑f x - ↑g x

theorem LinearMap.sub_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) : LinearMap.comp (g - h) f = LinearMap.comp g f - LinearMap.comp h f

theorem LinearMap.comp_sub {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : LinearMap.comp h (g - f) = LinearMap.comp h g - LinearMap.comp h f

instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} : AddCommGroup (M →ₛₗ[σ₁₂] N₂)

The type of linear maps is an additive group.

Equations

• One or more equations did not get rendered due to their size.

instance LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] : DistribMulAction S (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid = DistribMulAction.mk (_ : ∀ (x : S), x • 0 = 0) (_ : ∀ (x : S) (x_1 x_2 : M →ₛₗ[σ₁₂] M₂), x • (x_1 + x_2) = x • x_1 + x • x_2)

theorem LinearMap.smul_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {S₃ : Type u_7} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : LinearMap.comp (a • g) f = a • LinearMap.comp g f

theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Monoid S] [DistribMulAction S M₂] [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : LinearMap.comp g (a • f) = a • LinearMap.comp g f

instance LinearMap.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] : Module S (M →ₛₗ[σ₁₂] M₂)

Equations

• LinearMap.module = Module.mk (_ : ∀ (x x_1 : S) (x_2 : M →ₛₗ[σ₁₂] M₂), (x + x_1) • x_2 = x • x_2 + x_1 • x_2) (_ : ∀ (x : M →ₛₗ[σ₁₂] M₂), 0 • x = 0)

instance LinearMap.instNoZeroSMulDivisorsLinearMapToZeroToMonoidWithZeroInstZeroLinearMapInstSMulLinearMapToMonoidToDistribMulAction {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)

Equations

• One or more equations did not get rendered due to their size.

Monoid structure of endomorphisms

instance LinearMap.instOneEnd {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : One (Module.End R M)

Equations

• LinearMap.instOneEnd = { one := LinearMap.id }

instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Mul (Module.End R M)

Equations

• LinearMap.instMulEnd = { mul := LinearMap.comp }

theorem LinearMap.one_eq_id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : 1 = LinearMap.id

theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) : f * g = LinearMap.comp f g

@[simp]

theorem LinearMap.one_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑1 x = x

@[simp]

theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) (x : M) : ↑(f * g) x = ↑f (↑g x)

theorem LinearMap.coe_one {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : ↑1 = id

theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (g : Module.End R M) : ↑(f * g) = ↑f ∘ ↑g

instance Module.End.monoid {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Monoid (Module.End R M)

Equations

• Module.End.monoid = Monoid.mk (_ : ∀ (f : M →ₗ[R] M), LinearMap.comp LinearMap.id f = f) (_ : ∀ (f : M →ₗ[R] M), LinearMap.comp f LinearMap.id = f) npowRec

instance Module.End.semiring {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Semiring (Module.End R M)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.End.natCast_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : ↑↑n m = n • m

See also Module.End.natCast_def.

instance Module.End.ring {R : Type u_1} {N₁ : Type u_13} [Semiring R] [AddCommGroup N₁] [Module R N₁] : Ring (Module.End R N₁)

Equations

• Module.End.ring = let src := Module.End.semiring; let src_1 := LinearMap.addCommGroup; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : N₁ →ₗ[R] N₁), -a + a = 0)

@[simp]

theorem Module.End.intCast_apply {R : Type u_1} {N₁ : Type u_13} [Semiring R] [AddCommGroup N₁] [Module R N₁] (z : ℤ) (m : N₁) : ↑↑z m = z • m

See also Module.End.intCast_def.

instance Module.End.isScalarTower {R : Type u_1} {S : Type u_6} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] : IsScalarTower S (Module.End R M) (Module.End R M)

Equations

• @Module.End.isScalarTower = @Module.End.isScalarTower.proof_1

instance Module.End.smulCommClass {R : Type u_1} {S : Type u_6} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) (Module.End R M)

Equations

• @Module.End.smulCommClass = @Module.End.smulCommClass.proof_1

instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_6} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S (Module.End R M)

Equations

• @Module.End.smulCommClass' = @Module.End.smulCommClass'.proof_1

theorem Module.End_isUnit_apply_inv_apply_of_isUnit {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} (h : IsUnit f) (x : M) : ↑f (↑(IsUnit.unit h).inv x) = x

theorem Module.End_isUnit_inv_apply_apply_of_isUnit {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} (h : IsUnit f) (x : M) : ↑(IsUnit.unit h).inv (↑f x) = x

theorem LinearMap.coe_pow {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ℕ) : ↑(f ^ n) = (↑f)^[n]

theorem LinearMap.pow_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ℕ) (m : M) : ↑(f ^ n) m = (↑f)^[n] m

theorem LinearMap.pow_map_zero_of_le {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {m : M} {k : ℕ} {l : ℕ} (hk : k ≤ l) (hm : ↑(f ^ k) m = 0) : ↑(f ^ l) m = 0

theorem LinearMap.commute_pow_left_of_commute {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂} {g : Module.End R M} {g₂ : Module.End R₂ M₂} (h : LinearMap.comp g₂ f = LinearMap.comp f g) (k : ℕ) : LinearMap.comp (g₂ ^ k) f = LinearMap.comp f (g ^ k)

@[simp]

theorem LinearMap.id_pow {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : LinearMap.id ^ n = LinearMap.id

theorem LinearMap.iterate_succ {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (n : ℕ) : f' ^ (n + 1) = LinearMap.comp (f' ^ n) f'

theorem LinearMap.iterate_surjective {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Surjective ↑f') (n : ℕ) : Function.Surjective ↑(f' ^ n)

theorem LinearMap.iterate_injective {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Injective ↑f') (n : ℕ) : Function.Injective ↑(f' ^ n)

theorem LinearMap.iterate_bijective {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} (h : Function.Bijective ↑f') (n : ℕ) : Function.Bijective ↑(f' ^ n)

theorem LinearMap.injective_of_iterate_injective {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {n : ℕ} (hn : n ≠ 0) (h : Function.Injective ↑(f' ^ n)) : Function.Injective ↑f'

theorem LinearMap.surjective_of_iterate_surjective {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {n : ℕ} (hn : n ≠ 0) (h : Function.Surjective ↑(f' ^ n)) : Function.Surjective ↑f'

Action by a module endomorphism.

instance LinearMap.applyModule {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : Module (Module.End R M) M

The tautological action by Module.End R M (aka M →ₗ[R] M) on M.

This generalizes Function.End.applyMulAction.

Equations

• LinearMap.applyModule = Module.mk (_ : ∀ (f g : M →ₗ[R] M) (x : M), ↑(f + g) x = ↑f x + ↑g x) (_ : ∀ (x : M), ↑0 x = 0)

@[simp]

theorem LinearMap.smul_def {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) (a : M) : f • a = ↑f a

instance LinearMap.apply_faithfulSMul {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : FaithfulSMul (Module.End R M) M

LinearMap.applyModule is faithful.

Equations

• @LinearMap.apply_faithfulSMul = @LinearMap.apply_faithfulSMul.proof_1

instance LinearMap.apply_smulCommClass {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : SMulCommClass R (Module.End R M) M

Equations

• @LinearMap.apply_smulCommClass = @LinearMap.apply_smulCommClass.proof_1

instance LinearMap.apply_smulCommClass' {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] : SMulCommClass (Module.End R M) R M

Equations

• @LinearMap.apply_smulCommClass' = @LinearMap.apply_smulCommClass'.proof_1

instance LinearMap.apply_isScalarTower {R : Type u_17} {M : Type u_18} [CommSemiring R] [AddCommMonoid M] [Module R M] : IsScalarTower R (Module.End R M) M

Equations

• @LinearMap.apply_isScalarTower = @LinearMap.apply_isScalarTower.proof_1

Actions as module endomorphisms

@[simp]

theorem DistribMulAction.toLinearMap_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : ∀ (a : M), ↑(DistribMulAction.toLinearMap R M s) a = s • a

def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : M →ₗ[R] M

Each element of the monoid defines a linear map.

This is a stronger version of DistribMulAction.toAddMonoidHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : ↑(DistribMulAction.toModuleEnd R M) s = DistribMulAction.toLinearMap R M s

def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] : S →* Module.End R M

Each element of the monoid defines a module endomorphism.

This is a stronger version of DistribMulAction.toAddMonoidEnd.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S M] [SMulCommClass S R M] (s : S) : ↑(Module.toModuleEnd R M) s = DistribMulAction.toLinearMap R M s

def Module.toModuleEnd (R : Type u_1) {S : Type u_6} (M : Type u_9) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Module S M] [SMulCommClass S R M] : S →+* Module.End R M

Each element of the semiring defines a module endomorphism.

This is a stronger version of DistribMulAction.toModuleEnd.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.moduleEndSelf_symm_apply (R : Type u_1) [Semiring R] (f : Module.End R R) : ↑(RingEquiv.symm (Module.moduleEndSelf R)) f = MulOpposite.op (↑f 1)

@[simp]

theorem Module.moduleEndSelf_apply (R : Type u_1) [Semiring R] (s : Rᵐᵒᵖ) : ↑(Module.moduleEndSelf R) s = DistribMulAction.toLinearMap R R s

def Module.moduleEndSelf (R : Type u_1) [Semiring R] : Rᵐᵒᵖ ≃+* Module.End R R

The canonical (semi)ring isomorphism from Rᵐᵒᵖ to Module.End R R induced by the right multiplication.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.moduleEndSelfOp_symm_apply (R : Type u_1) [Semiring R] (f : Module.End Rᵐᵒᵖ R) : ↑(RingEquiv.symm (Module.moduleEndSelfOp R)) f = ↑f 1

@[simp]

theorem Module.moduleEndSelfOp_apply (R : Type u_1) [Semiring R] (s : R) : ↑(Module.moduleEndSelfOp R) s = DistribMulAction.toLinearMap Rᵐᵒᵖ R s

def Module.moduleEndSelfOp (R : Type u_1) [Semiring R] : R ≃+* Module.End Rᵐᵒᵖ R

The canonical (semi)ring isomorphism from R to Module.End Rᵐᵒᵖ R induced by the left multiplication.

Equations

• One or more equations did not get rendered due to their size.

theorem Module.End.natCast_def (R : Type u_1) {N₁ : Type u_13} [Semiring R] (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : ↑n = ↑(Module.toModuleEnd R N₁) n

theorem Module.End.intCast_def (R : Type u_1) {N₁ : Type u_13} [Semiring R] (z : ℤ) [AddCommGroup N₁] [Module R N₁] : ↑z = ↑(Module.toModuleEnd R N₁) z