Documentation

Mathlib.Algebra.Module.Equiv.Basic

Further results on (semi)linear equivalences. #

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

Instances For

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

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

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)

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

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

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

Group (M ≃ₗ[R] M)

Equations

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

1 = refl R M

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

@[simp]

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

⇑1 = id

@[simp]

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

⇑f⁻¹ = ⇑f.symm

@[simp]

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

↑1 = LinearMap.id

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

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]

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

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

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

Instances For

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

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

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

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.

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

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

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

Instances For

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

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

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

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

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

Equations

Instances For

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

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

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

Each element of the group defines a linear equivalence.

This is a stronger version of DistribMulAction.toAddEquiv.

Equations

Instances For

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

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

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

Instances For

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

theorem LinearEquiv.smul_refl {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] [SMul S R] [IsScalarTower S R M] (α : Sˣ) :

α • refl R M = DistribMulAction.toLinearEquiv R M α

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

Instances For

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

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

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

Instances For

@[simp]

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

⇑e.toNatLinearEquiv = ⇑e

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

@[simp]

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

↑e.toNatLinearEquiv = e

@[simp]

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

(↑e).toNatLinearEquiv = e

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

@[simp]

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

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

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

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

M ≃ₗ[ℤ ] M₂

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

Equations

Instances For

@[simp]

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

⇑e.toIntLinearEquiv = ⇑e

@[simp]

theorem AddEquiv.coe_symm_toIntLinearEquiv {M : Type u_5} {M₂ : Type u_7} [AddCommGroup M] [AddCommGroup M₂] {modM : Module ℤ M} {modM₂ : Module ℤ M₂} (e : M ≃+ M₂) :

⇑e.toIntLinearEquiv.symm = ⇑e.symm

@[simp]

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

↑e.toIntLinearEquiv = e

@[simp]

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

(↑e).toIntLinearEquiv = e

@[simp]

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

e.symm.toIntLinearEquiv = e.toIntLinearEquiv.symm

@[simp]

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

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

@[simp]

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

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

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

Instances For

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

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

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

Instances For

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

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

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

Instances For

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

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

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

Instances For

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

Instances For

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

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

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

Instances For

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

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

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

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

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

x ↦ -x as a LinearEquiv

Equations

Instances For

@[simp]

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

⇑(neg R) = -id

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

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

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

Instances For

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

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

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

Instances For

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

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

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 and codomains of two spaces of linear maps gives a linear isomorphism with respect to an action on the domains.

Equations

Instances For

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

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

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

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

Equations

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.

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

Instances For

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

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

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

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

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

Instances For

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

@[simp]

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

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

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

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

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

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

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

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

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

Instances For

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

Instances For

@[simp]

theorem LinearEquiv.congrLeft_symm_apply (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₃) (a✝ : M₃ →ₗ[R] M) :

(congrLeft M S e).symm a✝ = (e.arrowCongrAddEquiv (refl R M)).invFun a✝

@[simp]

theorem LinearEquiv.congrLeft_apply (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₃) (a✝ : M₂ →ₗ[R] M) :

(congrLeft M S e) a✝ = (e.arrowCongrAddEquiv (refl R M)).toFun a✝

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

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

Equations

Instances For

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

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

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

Instances For

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

Instances For

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

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

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₁

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)

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)

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

Instances For

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

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

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

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

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

Instances For

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

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

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

Instances For

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

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