Further results on (semi)linear equivalences. #

source

def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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-semimodules and S-semimodules and R-semimodule structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear equivalence from M to M₂ is also an R-linear equivalence.

See also LinearMap.restrictScalars.

Equations

LinearEquiv.restrictScalars R f = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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₂) (a : M₂) :

(LinearEquiv.restrictScalars R f).symm a = f.symm a

source

@[simp]

theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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₂) (a : M) :

(LinearEquiv.restrictScalars R f) a = f a

source

theorem LinearEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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 (LinearEquiv.restrictScalars R)

source

@[simp]

theorem LinearEquiv.restrictScalars_inj (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [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 g : M ≃ₗ[S] M₂) :

LinearEquiv.restrictScalars R f = LinearEquiv.restrictScalars R g ↔ f = g

source

theorem Module.End_isUnit_iff {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) :

IsUnit f ↔ Function.Bijective ⇑f

source

instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

Group (M ≃ₗ[R] M)

Equations

LinearEquiv.automorphismGroup = Group.mk ⋯

source

@[simp]

theorem LinearEquiv.coe_one {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

⇑1 = id

source

@[simp]

theorem LinearEquiv.coe_toLinearMap_one {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

↑1 = LinearMap.id

source

@[simp]

theorem LinearEquiv.coe_toLinearMap_mul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {e₁ e₂ : M ≃ₗ[R] M} :

↑(e₁ * e₂) = ↑e₁ * ↑e₂

source

theorem LinearEquiv.coe_pow {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ℕ) :

⇑(e ^ n) = (⇑e)^[n]

source

theorem LinearEquiv.pow_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) (n : ℕ) (m : M) :

(e ^ n) m = (⇑e)^[n] m

source

def LinearEquiv.automorphismGroup.toLinearMapMonoidHom {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

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

Restriction from R-linear automorphisms of M to R-linear endomorphisms of M, promoted to a monoid hom.

Equations

LinearEquiv.automorphismGroup.toLinearMapMonoidHom = { toFun := fun (e : M ≃ₗ[R] M) => ↑e, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) :

LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = ↑e

source

instance LinearEquiv.applyDistribMulAction {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

DistribMulAction (M ≃ₗ[R] M) M

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

This generalizes Function.End.applyMulAction.

Equations

LinearEquiv.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯

source

@[simp]

theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) (a : M) :

f • a = f a

source

theorem LinearEquiv.apply_faithfulSMul {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :

FaithfulSMul (M ≃ₗ[R] M) M

LinearEquiv.applyDistribMulAction is faithful.

source

theorem LinearEquiv.apply_smulCommClass {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :

SMulCommClass S (M ≃ₗ[R] M) M

source

theorem LinearEquiv.apply_smulCommClass' {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] :

SMulCommClass (M ≃ₗ[R] M) S M

source

def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] :

M ≃ₗ[R] M₂

Any two modules that are subsingletons are isomorphic.

Equations

LinearEquiv.ofSubsingleton M M₂ = { toFun := fun (x : M) => 0, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : M₂) => 0, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] (x✝ : M₂) :

(LinearEquiv.ofSubsingleton M M₂).symm x✝ = 0

source

@[simp]

theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] (x✝ : M) :

(LinearEquiv.ofSubsingleton M M₂) x✝ = 0

source

@[simp]

theorem LinearEquiv.ofSubsingleton_self {R : Type u_1} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] :

LinearEquiv.ofSubsingleton M M = LinearEquiv.refl R M

source

def Module.compHom.toLinearEquiv {R : Type u_9} {S : Type u_10} [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.toLinearEquiv g = { toFun := ⇑g, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑g.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Module.compHom.toLinearEquiv_apply {R : Type u_9} {S : Type u_10} [Semiring R] [Semiring S] (g : R ≃+* S) (a : R) :

(Module.compHom.toLinearEquiv g) a = g a

source

@[simp]

theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_9} {S : Type u_10} [Semiring R] [Semiring S] (g : R ≃+* S) (a : S) :

(Module.compHom.toLinearEquiv g).symm a = g.symm a

source

def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :

M ≃ₗ[R] M

Each element of the group defines a linear equivalence.

This is a stronger version of DistribMulAction.toAddEquiv.

Equations

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

Instances For

source

@[simp]

theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (a✝ : M) :

(DistribMulAction.toLinearEquiv R M s).symm a✝ = s⁻¹ • a✝

source

@[simp]

theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) (a✝ : M) :

(DistribMulAction.toLinearEquiv R M s) a✝ = s • a✝

source

def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] :

S →* M ≃ₗ[R] M

Each element of the group defines a module automorphism.

This is a stronger version of DistribMulAction.toAddAut.

Equations

DistribMulAction.toModuleAut R M = { toFun := DistribMulAction.toLinearEquiv R M, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem DistribMulAction.toModuleAut_apply (R : Type u_1) {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) :

(DistribMulAction.toModuleAut R M) s = DistribMulAction.toLinearEquiv R M s

source

def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c • x) = c • e x) :

M ≃ₗ[R] M₂

An additive equivalence whose underlying function preserves smul is a linear equivalence.

Equations

e.toLinearEquiv h = { toFun := e.toFun, map_add' := ⋯, map_smul' := h, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.coe_toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c • x) = c • e x) :

⇑(e.toLinearEquiv h) = ⇑e

source

@[simp]

theorem AddEquiv.coe_toLinearEquiv_symm {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃+ M₂) (h : ∀ (c : R) (x : M), e (c • x) = c • e x) :

⇑(e.toLinearEquiv h).symm = ⇑e.symm

source

def AddEquiv.toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

M ≃ₗ[ℕ ] M₂

An additive equivalence between commutative additive monoids is a linear equivalence between ℕ-modules

Equations

e.toNatLinearEquiv = e.toLinearEquiv ⋯

Instances For

source

@[simp]

theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

⇑e.toNatLinearEquiv = ⇑e

source

@[simp]

theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

↑e.toNatLinearEquiv = e

source

@[simp]

theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃ₗ[ℕ ] M₂) :

(↑e).toNatLinearEquiv = e

source

@[simp]

theorem AddEquiv.toNatLinearEquiv_symm {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv

source

@[simp]

theorem AddEquiv.toNatLinearEquiv_refl {M : Type u_5} [AddCommMonoid M] :

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

source

@[simp]

theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :

e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv

source

def AddEquiv.toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

M ≃ₗ[ℤ ] M₂

An additive equivalence between commutative additive groups is a linear equivalence between ℤ-modules

Equations

e.toIntLinearEquiv = e.toLinearEquiv ⋯

Instances For

source

@[simp]

theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

⇑e.toIntLinearEquiv = ⇑e

source

@[simp]

theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

↑e.toIntLinearEquiv = e

source

@[simp]

theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃ₗ[ℤ ] M₂) :

(↑e).toIntLinearEquiv = e

source

@[simp]

theorem AddEquiv.toIntLinearEquiv_symm {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv

source

@[simp]

theorem AddEquiv.toIntLinearEquiv_refl {M : Type u_5} [AddCommGroup M] :

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

source

@[simp]

theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :

e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv

source

def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] :

(R →ₗ[R] M) ≃ₗ[S] M

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

This is an S-linear equivalence, under the assumption that S acts on M commuting with R. When R is commutative, we can take this to be the usual action with S = R. Otherwise, S = ℕ shows that the equivalence is additive. See note [bundled maps over different rings].

Equations

LinearMap.ringLmapEquivSelf R S M = { toFun := fun (f : R →ₗ[R] M) => f 1, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.smulRight 1, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (x : M) :

(LinearMap.ringLmapEquivSelf R S M).symm x = LinearMap.smulRight 1 x

source

@[simp]

theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_4) (M : Type u_5) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : R →ₗ[R] M) :

(LinearMap.ringLmapEquivSelf R S M) f = f 1

source

def addMonoidHomLequivNat {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] :

(A →+ B) ≃ₗ[R] A →ₗ[ℕ ] B

The R-linear equivalence between additive morphisms A →+ B and ℕ-linear morphisms A →ₗ[ℕ] B.

Equations

addMonoidHomLequivNat R = { toFun := AddMonoidHom.toNatLinearMap, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.toAddMonoidHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem addMonoidHomLequivNat_symm_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →ₗ[ℕ ] B) :

(addMonoidHomLequivNat R).symm f = f.toAddMonoidHom

source

@[simp]

theorem addMonoidHomLequivNat_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →+ B) :

(addMonoidHomLequivNat R) f = f.toNatLinearMap

source

def addMonoidHomLequivInt {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] :

(A →+ B) ≃ₗ[R] A →ₗ[ℤ ] B

The R-linear equivalence between additive morphisms A →+ B and ℤ-linear morphisms A →ₗ[ℤ] B.

Equations

addMonoidHomLequivInt R = { toFun := AddMonoidHom.toIntLinearMap, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.toAddMonoidHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem addMonoidHomLequivInt_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →+ B) :

(addMonoidHomLequivInt R) f = f.toIntLinearMap

source

@[simp]

theorem addMonoidHomLequivInt_symm_apply {A : Type u_9} {B : Type u_10} (R : Type u_11) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →ₗ[ℤ ] B) :

(addMonoidHomLequivInt R).symm f = f.toAddMonoidHom

source

def addMonoidEndRingEquivInt (A : Type u_9) [AddCommGroup A] :

AddMonoid.End A ≃+* Module.End ℤ A

Ring equivalence between additive group endomorphisms of an AddCommGroup A and ℤ-module endomorphisms of A.

Equations

addMonoidEndRingEquivInt A = { toFun := (↑(addMonoidHomLequivInt ℤ)).toFun, invFun := (addMonoidHomLequivInt ℤ).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem addMonoidEndRingEquivInt_apply (A : Type u_9) [AddCommGroup A] (a✝ : A →+ A) :

(addMonoidEndRingEquivInt A) a✝ = (↑(addMonoidHomLequivInt ℤ)).toFun a✝

source

@[simp]

theorem addMonoidEndRingEquivInt_symm_apply (A : Type u_9) [AddCommGroup A] (a✝ : A →ₗ[ℤ ] A) :

(addMonoidEndRingEquivInt A).symm a✝ = (addMonoidHomLequivInt ℤ).invFun a✝

source

instance LinearEquiv.instZero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :

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

Between two zero modules, the zero map is an equivalence.

Equations

LinearEquiv.instZero = { zero := let __src := 0; { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯ } }

source

@[simp]

theorem LinearEquiv.zero_symm {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :

LinearEquiv.symm 0 = 0

source

@[simp]

theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :

⇑0 = 0

source

theorem LinearEquiv.zero_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] (x : M) :

0 x = 0

source

instance LinearEquiv.instUnique {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] :

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

Between two zero modules, the zero map is the only equivalence.

Equations

LinearEquiv.instUnique = { default := 0, uniq := ⋯ }

source

instance LinearEquiv.uniqueOfSubsingleton {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton R] [Subsingleton R₂] :

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

Equations

LinearEquiv.uniqueOfSubsingleton = inferInstance

source

def LinearEquiv.curry (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) :

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

Linear equivalence between a curried and uncurried function. Differs from TensorProduct.curry.

Equations

LinearEquiv.curry R M V V₂ = { toFun := (Equiv.curry V V₂ M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.curry V V₂ M).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.coe_curry (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) :

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

source

@[simp]

theorem LinearEquiv.coe_curry_symm (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (V : Type u_9) (V₂ : Type u_10) :

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

source

def LinearEquiv.ofLinear {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f.comp g = LinearMap.id) (h₂ : g.comp f = LinearMap.id) :

M ≃ₛₗ[σ₁₂] M₂

If a linear map has an inverse, it is a linear equivalence.

Equations

LinearEquiv.ofLinear f g h₁ h₂ = { toLinearMap := f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.ofLinear_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} (x : M) :

(LinearEquiv.ofLinear f g h₁ h₂) x = f x

source

@[simp]

theorem LinearEquiv.ofLinear_symm_apply {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} (x : M₂) :

(LinearEquiv.ofLinear f g h₁ h₂).symm x = g x

source

@[simp]

theorem LinearEquiv.ofLinear_toLinearMap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} :

↑(LinearEquiv.ofLinear f g h₁ h₂) = f

source

@[simp]

theorem LinearEquiv.ofLinear_symm_toLinearMap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₁] M) {h₁ : f.comp g = LinearMap.id} {h₂ : g.comp f = LinearMap.id} :

↑(LinearEquiv.ofLinear f g h₁ h₂).symm = g

source

def LinearEquiv.neg (R : Type u_1) {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] :

M ≃ₗ[R] M

x ↦ -x as a LinearEquiv

Equations

LinearEquiv.neg R = { toFun := (Equiv.neg M).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.neg M).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] :

⇑(LinearEquiv.neg R) = -id

source

theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] (x : M) :

(LinearEquiv.neg R) x = -x

source

@[simp]

theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] :

(LinearEquiv.neg R).symm = LinearEquiv.neg R

source

def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : Rˣ) :

M ≃ₗ[R] M

Multiplying by a unit a of the ring R is a linear equivalence.

Equations

LinearEquiv.smulOfUnit a = DistribMulAction.toLinearEquiv R M a

Instances For

source

def LinearEquiv.arrowCongr {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :

(M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

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

Equations

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

Instances For

source

@[simp]

theorem LinearEquiv.arrowCongr_apply {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) :

((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))

source

@[simp]

theorem LinearEquiv.arrowCongr_symm_apply {R : Type u_9} {M₁ : Type u_10} {M₂ : Type u_11} {M₂₁ : Type u_12} {M₂₂ : Type u_13} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) :

((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))

source

theorem LinearEquiv.arrowCongr_comp {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {N : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :

(e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f

source

theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [CommSemiring R] {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} {N₃ : Type u_14} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :

e₁.arrowCongr e₂ ≪≫ₗ e₃.arrowCongr e₄ = (e₁ ≪≫ₗ e₃).arrowCongr (e₂ ≪≫ₗ e₄)

source

def LinearEquiv.congrRight {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M₂ ≃ₗ[R] M₃) :

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

If M₂ and M₃ are linearly isomorphic then the two spaces of linear maps from M into M₂ and M into M₃ are linearly isomorphic.

Equations

f.congrRight = (LinearEquiv.refl R M).arrowCongr f

Instances For

source

def LinearEquiv.conj {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) :

Module.End R M ≃ₗ[R] Module.End R M₂

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

Equations

e.conj = e.arrowCongr e

Instances For

source

theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) :

e.conj f = (↑e ∘ₗ f) ∘ₗ ↑e.symm

source

theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) :

(e.conj f) x = e (f (e.symm x))

source

theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) :

e.symm.conj f = (↑e.symm ∘ₗ f) ∘ₗ ↑e

source

theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f g : Module.End R M) :

e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f

source

theorem LinearEquiv.conj_trans {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) :

e₁.conj ≪≫ₗ e₂.conj = (e₁ ≪≫ₗ e₂).conj

source

@[simp]

theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) :

e.conj LinearMap.id = LinearMap.id

source

def LinearEquiv.congrLeft (M : Type u_5) {M₂ : Type u_7} {M₃ : Type u_8} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {R : Type u_9} (S : Type u_10) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) :

(M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M

An R-linear isomorphism between two R-modules M₂ and M₃ induces an S-linear isomorphism between M₂ →ₗ[R] M and M₃ →ₗ[R] M, if M is both an R-module and an S-module and their actions commute.

Equations

LinearEquiv.congrLeft M S e = { toFun := fun (f : M₂ →ₗ[R] M) => f ∘ₗ ↑e.symm, map_add' := ⋯, map_smul' := ⋯, invFun := fun (f : M₃ →ₗ[R] M) => f ∘ₗ ↑e, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def LinearEquiv.smulOfNeZero (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) :

M ≃ₗ[K] M

Multiplying by a nonzero element a of the field K is a linear equivalence.

Equations

LinearEquiv.smulOfNeZero K M a ha = LinearEquiv.smulOfUnit (Units.mk0 a ha)

Instances For

source

@[simp]

theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) (a✝ : M) :

(LinearEquiv.smulOfNeZero K M a ha).symm a✝ = (Units.mk0 a ha)⁻¹ • a✝

source

@[simp]

theorem LinearEquiv.smulOfNeZero_apply (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) (a✝ : M) :

(LinearEquiv.smulOfNeZero K M a ha) a✝ = Units.mk0 a ha • a✝

source

def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (e : M ≃ M₂) (h : IsLinearMap R ⇑e) :

M ≃ₗ[R] M₂

An equivalence whose underlying function is linear is a linear equivalence.

Equations

e.toLinearEquiv h = { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def LinearMap.funLeft (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) :

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

Given an R-module M and a function m → n between arbitrary types, construct a linear map (n → M) →ₗ[R] (m → M)

Equations

LinearMap.funLeft R M f = { toFun := fun (x : n → M) => x ∘ f, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (g : n → M) (i : m) :

(LinearMap.funLeft R M f) g i = g (f i)

source

@[simp]

theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_10} (g : n → M) :

(LinearMap.funLeft R M id) g = g

source

theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} {p : Type u_11} (f₁ : n → p) (f₂ : m → n) :

LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁

source

theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (hf : Function.Injective f) :

Function.Surjective ⇑(LinearMap.funLeft R M f)

source

theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (f : m → n) (hf : Function.Surjective f) :

Function.Injective ⇑(LinearMap.funLeft R M f)

source

def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) :

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

Given an R-module M and an equivalence m ≃ n between arbitrary types, construct a linear equivalence (n → M) ≃ₗ[R] (m → M)

Equations

LinearEquiv.funCongrLeft R M e = LinearEquiv.ofLinear (LinearMap.funLeft R M ⇑e) (LinearMap.funLeft R M ⇑e.symm) ⋯ ⋯

Instances For

source

@[simp]

theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) (x : n → M) :

(LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x

source

@[simp]

theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_10} :

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

source

@[simp]

theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} {p : Type u_11} (e₁ : m ≃ n) (e₂ : n ≃ p) :

LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁

source

@[simp]

theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_9} {n : Type u_10} (e : m ≃ n) :

(LinearEquiv.funCongrLeft R M e).symm = LinearEquiv.funCongrLeft R M e.symm

Documentation

Mathlib.Algebra.Module.Equiv.Basic

Further results on (semi)linear equivalences. #