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₂) :

(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) :

(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 (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₂) :

restrictScalars R f = 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 : End R M) :

IsUnit f ↔ Function.Bijective ⇑f

source

@[deprecated Module.End.isUnit_iff (since := "2025-04-28")]

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

IsUnit f ↔ Function.Bijective ⇑f

Alias of Module.End.isUnit_iff.

source

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

Group (M ≃ₗ[R] M)

Equations

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

source

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

1 = refl R M

source

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

f * g = g ≪≫ₗ f

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

@[simp]

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

(f * g) x = f (g x)

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) :

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 = { smul := fun (x1 : M ≃ₗ[R] M) (x2 : M) => x1 x2, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

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

instance 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

instance 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

instance 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_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) :

(ofSubsingleton M M₂) x✝ = 0

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₂) :

(ofSubsingleton M M₂).symm 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] :

ofSubsingleton M M = 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) :

(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) :

(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_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) :

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

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) :

(toLinearEquiv R M s).symm 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) :

(toModuleAut R M) s = 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] :

(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] :

(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) :

(ringLmapEquivSelf R S M).symm x = 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) :

(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_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

@[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

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₂] :

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 ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ 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 ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M) :

(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 ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} (x : M₂) :

(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 ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} :

↑(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 ∘ₛₗ g = LinearMap.id} {h₂ : g ∘ₛₗ f = LinearMap.id} :

↑(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] :

⇑(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) :

(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] :

(neg R).symm = neg R

source

def LinearEquiv.arrowCongrAddEquiv {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring 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₂₁) ≃+ (M₂ →ₗ[R] M₂₂)

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

See also LinearEquiv.arrowCongr for the linear version of this isomorphism.

Equations

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

Instances For

source

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_symm_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring 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₂₂) :

(e₁.arrowCongrAddEquiv e₂).symm f = ↑e₂.symm ∘ₗ f ∘ₗ ↑e₁

source

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring 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₂₁) :

(e₁.arrowCongrAddEquiv e₂) f = ↑e₂ ∘ₗ f ∘ₗ ↑e₁.symm

source

def LinearEquiv.domMulActCongrRight {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂₁] [Module R M₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) :

(M₁ →ₗ[R] M₂₁) ≃ₗ[Sᵈᵐᵃ ] M₁ →ₗ[R] M₂₂

A linear isomorphism between the domains an codomains of two spaces of linear maps gives a linear isomorphism with respect to an action on the domains.

Equations

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

Instances For

source

@[simp]

theorem LinearEquiv.domMulActCongrRight_apply {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂₁] [Module R M₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) (a✝ : M₁ →ₗ[R] M₂₁) :

e₂.domMulActCongrRight a✝ = ((refl R M₁).arrowCongrAddEquiv e₂).toFun a✝

source

@[simp]

theorem LinearEquiv.domMulActCongrRight_symm_apply {R : Type u_1} {S : Type u_4} {M₁ : Type u_6} {M₂₁ : Type u_9} {M₂₂ : Type u_10} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂₁] [Module R M₂₂] [Semiring S] [Module S M₁] [SMulCommClass R S M₁] (e₂ : M₂₁ ≃ₗ[R] M₂₂) (a✝ : M₁ →ₗ[R] M₂₂) :

e₂.domMulActCongrRight.symm a✝ = ((refl R M₁).arrowCongrAddEquiv e₂).invFun a✝

source

def LinearEquiv.conjRingEquiv {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) :

Module.End R M₁ ≃+* Module.End R M₂

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

See LinearEquiv.conj for the linear version of this isomorphism.

Equations

e.conjRingEquiv = { toEquiv := (e.arrowCongrAddEquiv e).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.conjRingEquiv_apply_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : M₁ →ₗ[R] M₁) (a✝ : M₂) :

(e.conjRingEquiv f) a✝ = e (f (e.symm a✝))

source

@[simp]

theorem LinearEquiv.conjRingEquiv_symm_apply_apply {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : M₂ →ₗ[R] M₂) (a✝ : M₁) :

(e.conjRingEquiv.symm f) a✝ = e.symm (f (e a✝))

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.

See LinearEquiv.arrowCongrAddEquiv for the additive version of this isomorphism that works over a not necessarily commutative semiring.

Equations

e₁.arrowCongr e₂ = { toFun := (e₁.arrowCongrAddEquiv e₂).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (e₁.arrowCongrAddEquiv e₂).invFun, left_inv := ⋯, right_inv := ⋯ }

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.

See LinearEquiv.conjRingEquiv for the isomorphism between endomorphism rings, which works over a not necessarily commutative semiring.

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

@[simp]

theorem LinearEquiv.conj_refl {R : Type u_1} {M : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) :

(refl R M).conj f = f

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

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

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_apply (K : Type u_3) (M : Type u_5) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) (a✝ : M) :

(smulOfNeZero K M a ha) a✝ = a • a✝

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) :

(smulOfNeZero K M a ha).symm 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) :

(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) :

(funLeft R M _root_.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) :

funLeft R M (f₁ ∘ f₂) = funLeft R M f₂ ∘ₗ 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 ⇑(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 ⇑(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) :

(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} :

funCongrLeft R M (Equiv.refl n) = 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) :

funCongrLeft R M (e₁.trans e₂) = funCongrLeft R M e₂ ≪≫ₗ 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) :

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

source

def LinearEquiv.sumPiEquivProdPi (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] :

((st : S ⊕ T) → A st) ≃ₗ[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))

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

This is Equiv.sumPiEquivProdPi as a LinearEquiv.

Equations

LinearEquiv.sumPiEquivProdPi R S T A = { toFun := (Equiv.sumPiEquivProdPi A).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Equiv.sumPiEquivProdPi A).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LinearEquiv.sumPiEquivProdPi_symm_apply (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] :

⇑(sumPiEquivProdPi R S T A).symm = ⇑(Equiv.sumPiEquivProdPi A).symm

source

@[simp]

theorem LinearEquiv.sumPiEquivProdPi_apply (R : Type u_9) [Semiring R] (S : Type u_10) (T : Type u_11) (A : S ⊕ T → Type u_12) [(st : S ⊕ T) → AddCommMonoid (A st)] [(st : S ⊕ T) → Module R (A st)] :

⇑(sumPiEquivProdPi R S T A) = ⇑(Equiv.sumPiEquivProdPi A)

source

def LinearEquiv.piUnique {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] :

((t : α) → f t) ≃ₗ[R] f default

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

This is Equiv.piUnique as a LinearEquiv.

Equations

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

Instances For

source

@[simp]

theorem LinearEquiv.piUnique_symm_apply {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] :

⇑(piUnique R f).symm = (Equiv.piUnique f).invFun

source

@[simp]

theorem LinearEquiv.piUnique_apply {α : Type u_9} [Unique α] (R : Type u_10) [Semiring R] (f : α → Type u_11) [(x : α) → AddCommMonoid (f x)] [(x : α) → Module R (f x)] :

⇑(piUnique R f) = (Equiv.piUnique f).toFun

Documentation

Mathlib.Algebra.Module.Equiv.Basic

Further results on (semi)linear equivalences. #