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

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

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.coe_symm_toNatLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) :

⇑e.toNatLinearEquiv.symm = ⇑e.symm

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.symm.toNatLinearEquiv = e.toNatLinearEquiv.symm

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.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv ≪≫ₗ 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.coe_symm_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) :

⇑e.toIntLinearEquiv.symm = ⇑e.symm

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.symm.toIntLinearEquiv = e.toIntLinearEquiv.symm

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.trans e₂).toIntLinearEquiv = e.toIntLinearEquiv ≪≫ₗ 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_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

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

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

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

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_symm_apply (A : Type u_9) [AddCommGroup A] (a✝ : A →ₗ[ℤ ] A) :

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

source

@[simp]

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

(addMonoidEndRingEquivInt A) a✝ = (↑(addMonoidHomLequivInt ℤ)).toFun 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_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {M₁' : Type u_15} {M₂' : Type u_16} [Semiring R₁] [Semiring R₂] [Semiring R₁'] [Semiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') :

(M₁ →ₛₗ[σ₁₁'] M₁') ≃+ (M₂ →ₛₗ[σ₂₂'] 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

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

Instances For

source

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_apply {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {M₁' : Type u_15} {M₂' : Type u_16} [Semiring R₁] [Semiring R₂] [Semiring R₁'] [Semiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₁ →ₛₗ[σ₁₁'] M₁') :

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

source

@[simp]

theorem LinearEquiv.arrowCongrAddEquiv_symm_apply {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₂ : Type u_14} {M₁' : Type u_15} {M₂' : Type u_16} [Semiring R₁] [Semiring R₂] [Semiring R₁'] [Semiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂') :

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

source

def LinearEquiv.conjRingEquiv {R₁ : Type u_9} {R₂ : Type u_10} {M₁ : Type u_13} {M₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] 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_9} {R₂ : Type u_10} {M₁ : Type u_13} {M₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] 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_9} {R₂ : Type u_10} {M₁ : Type u_13} {M₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₂ →ₗ[R₂] M₂) (a✝ : M₁) :

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

source

def LinearEquiv.domMulActCongrRight {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15} {M₂' : Type u_16} [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₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [Semiring S] [Module S M₁] [SMulCommClass R₁ S M₁] [RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') :

(M₁ →ₛₗ[σ₁₁'] M₁') ≃ₗ[Sᵈᵐᵃ ] M₁ →ₛₗ[σ₁₂'] 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_symm_apply {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15} {M₂' : Type u_16} [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₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [Semiring S] [Module S M₁] [SMulCommClass R₁ S M₁] [RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (a✝ : M₁ →ₛₗ[σ₁₂'] M₂') :

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

source

@[simp]

theorem LinearEquiv.domMulActCongrRight_apply {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15} {M₂' : Type u_16} [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₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [Semiring S] [Module S M₁] [SMulCommClass R₁ S M₁] [RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (a✝ : M₁ →ₛₗ[σ₁₁'] M₁') :

e₂.domMulActCongrRight a✝ = ((refl R₁ M₁).arrowCongrAddEquiv e₂).toFun 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

The modules for arrowCongr and its lemmas below are related via the semilinearities

M₁  ←⎯⎯⎯σ₁₂⎯⎯⎯→ M₂  ←⎯⎯⎯σ₂₃⎯⎯⎯→ M₃
⏐               ⏐               ⏐
σ₁₁'            σ₂₂'            σ₃₃'
↓               ↓               ↓
M₁' ←⎯⎯σ₁'₂'⎯⎯→ M₂' ←⎯⎯σ₂'₃'⎯⎯→ M₃
⏐               ⏐
σ₁'₁''          σ₂'₂''
↓               ↓
M₁''←⎯σ₁''₂''⎯→ M₂''

where the horizontal direction corresponds to the ≃ₛₗs, and is needed for arrowCongr_trans, while the vertical direction corresponds to the →ₛₗs, and is needed arrowCongr_comp.

Rᵢ is not necessarily commutative, but Rᵢ' and Rᵢ'' are.

source

def LinearEquiv.arrowCongr {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} [Semiring R₁] [Semiring R₂] [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') :

(M₁ →ₛₗ[σ₁₁'] M₁') ≃ₛₗ[σ₁'₂'] M₂ →ₛₗ[σ₂₂'] 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} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} [Semiring R₁] [Semiring R₂] [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₁ →ₛₗ[σ₁₁'] M₁') (x : M₂) :

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

source

@[simp]

theorem LinearEquiv.arrowCongr_symm_apply {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} [Semiring R₁] [Semiring R₂] [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : M₂ →ₛₗ[σ₂₂'] M₂') (x : M₁) :

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

source

theorem LinearEquiv.arrowCongr_comp {R₁ : Type u_9} {R₂ : Type u_10} {R₁' : Type u_12} {R₂' : Type u_13} {R₁'' : Type u_15} {R₂'' : Type u_16} {M₁ : Type u_17} {M₂ : Type u_18} {M₁' : Type u_20} {M₂' : Type u_21} {M₁'' : Type u_23} {M₂'' : Type u_24} [Semiring R₁] [Semiring R₂] [CommSemiring R₁'] [CommSemiring R₂'] [CommSemiring R₁''] [CommSemiring R₂''] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [AddCommMonoid M₁''] [AddCommMonoid M₂''] [Module R₁ M₁] [Module R₂ M₂] [Module R₁' M₁'] [Module R₂' M₂'] [Module R₁'' M₁''] [Module R₂'' M₂''] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁''₂'' : R₁'' →+* R₂''} {σ₂''₁'' : R₂'' →+* R₁''} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₁'₁'' : R₁' →+* R₁''} {σ₂'₂'' : R₂' →+* R₂''} {σ₁₁'' : R₁ →+* R₁''} {σ₂₂'' : R₂ →+* R₂''} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} {σ₂'₁'' : R₂' →+* R₁''} {σ₁'₂'' : R₁' →+* R₂''} {σ₂₁'' : R₂ →+* R₁''} {σ₁₂'' : R₁ →+* R₂''} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomInvPair σ₁''₂'' σ₂''₁''] [RingHomInvPair σ₂''₁'' σ₁''₂''] [RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''] [RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] [RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''] [RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''] [RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''] [RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''] [RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''] [RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''] [RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''] [RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂'') (f : M₁ →ₛₗ[σ₁₁'] M₁') (g : M₁' →ₛₗ[σ₁'₁''] M₁'') :

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

source

theorem LinearEquiv.arrowCongr_trans {R₁ : Type u_9} {R₂ : Type u_10} {R₃ : Type u_11} {R₁' : Type u_12} {R₂' : Type u_13} {R₃' : Type u_14} {M₁ : Type u_17} {M₂ : Type u_18} {M₃ : Type u_19} {M₁' : Type u_20} {M₂' : Type u_21} {M₃' : Type u_22} [Semiring R₁] [Semiring R₂] [Semiring R₃] [CommSemiring R₁'] [CommSemiring R₂'] [CommSemiring R₃'] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [AddCommMonoid M₃'] [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃] [Module R₁' M₁'] [Module R₂' M₂'] [Module R₃' M₃'] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₂'₃' : R₂' →+* R₃'} {σ₃'₂' : R₃' →+* R₂'} {σ₁'₃' : R₁' →+* R₃'} {σ₃'₁' : R₃' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₂₂' : R₂ →+* R₂'} {σ₃₃' : R₃ →+* R₃'} {σ₂₁' : R₂ →+* R₁'} {σ₁₂' : R₁ →+* R₂'} {σ₃₂' : R₃ →+* R₂'} {σ₂₃' : R₂ →+* R₃'} {σ₃₁' : R₃ →+* R₁'} {σ₁₃' : R₁ →+* R₃'} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₂'₃' σ₃'₂'] [RingHomInvPair σ₃'₂' σ₂'₃'] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomInvPair σ₁'₃' σ₃'₁'] [RingHomInvPair σ₃'₁' σ₁'₃'] [RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'] [RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'] [RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'] [RingHomCompTriple σ₁₁' σ₁'₃' σ₁₃'] [RingHomCompTriple σ₃₁ σ₁₃' σ₃₃'] [RingHomCompTriple σ₃₃' σ₃'₁' σ₃₁'] [RingHomCompTriple σ₁₃ σ₃₁' σ₁₁'] [RingHomCompTriple σ₂₂' σ₂'₃' σ₂₃'] [RingHomCompTriple σ₃₂ σ₂₃' σ₃₃'] [RingHomCompTriple σ₃₃' σ₃'₂' σ₃₂'] [RingHomCompTriple σ₂₃ σ₃₂' σ₂₂'] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'] [RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'] (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₁' : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (e₂' : M₂' ≃ₛₗ[σ₂'₃'] M₃') :

(e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂') = (e₁.trans e₂).arrowCongr (e₁'.trans e₂')

source

def LinearEquiv.conj {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') :

Module.End R₁' M₁' ≃ₛₗ[σ₁'₂'] 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_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') :

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

source

theorem LinearEquiv.conj_apply_apply {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] 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_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₂' M₂') :

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

source

theorem LinearEquiv.conj_comp {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] 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_12} {R₂' : Type u_13} {R₃' : Type u_14} {M₁' : Type u_20} {M₂' : Type u_21} {M₃' : Type u_22} [CommSemiring R₁'] [CommSemiring R₂'] [CommSemiring R₃'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [AddCommMonoid M₃'] [Module R₁' M₁'] [Module R₂' M₂'] [Module R₃' M₃'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₂'₃' : R₂' →+* R₃'} {σ₃'₂' : R₃' →+* R₂'} {σ₁'₃' : R₁' →+* R₃'} {σ₃'₁' : R₃' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] [RingHomInvPair σ₂'₃' σ₃'₂'] [RingHomInvPair σ₃'₂' σ₂'₃'] [RingHomInvPair σ₁'₃' σ₃'₁'] [RingHomInvPair σ₃'₁' σ₁'₃'] [RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'] [RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'] (e₁ : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₂ : M₂' ≃ₛₗ[σ₂'₃'] M₃') :

e₁.conj.trans e₂.conj = (e₁.trans e₂).conj

source

@[simp]

theorem LinearEquiv.conj_conj_symm {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₂' M₂') :

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

source

@[simp]

theorem LinearEquiv.conj_symm_conj {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] M₂') (f : Module.End R₁' M₁') :

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

source

@[simp]

theorem LinearEquiv.conj_id {R₁' : Type u_12} {R₂' : Type u_13} {M₁' : Type u_20} {M₂' : Type u_21} [CommSemiring R₁'] [CommSemiring R₂'] [AddCommMonoid M₁'] [AddCommMonoid M₂'] [Module R₁' M₁'] [Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} [RingHomInvPair σ₁'₂' σ₂'₁'] [RingHomInvPair σ₂'₁' σ₁'₂'] (e : M₁' ≃ₛₗ[σ₁'₂'] 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.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.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_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

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

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

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

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

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

Documentation

Mathlib.Algebra.Module.Equiv.Basic

Further results on (semi)linear equivalences. #