# (Semi)linear equivalences #

In this file we define

• LinearEquiv σ M M₂, M ≃ₛₗ[σ] M₂: an invertible semilinear map. Here, σ is a RingHom from R to R₂ and an e : M ≃ₛₗ[σ] M₂ satisfies e (c • x) = (σ c) • (e x). The plain linear version, with σ being RingHom.id R, is denoted by M ≃ₗ[R] M₂, and the star-linear version (with σ being starRingEnd) is denoted by M ≃ₗ⋆[R] M₂.

## Implementation notes #

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

The group structure on automorphisms, LinearEquiv.automorphismGroup, is provided elsewhere.

## TODO #

• Parts of this file have not yet been generalized to semilinear maps

## Tags #

linear equiv, linear equivalences, linear isomorphism, linear isomorphic

structure LinearEquiv {R : Type u_16} {S : Type u_17} [] [] (σ : R →+* S) {σ' : S →+* R} [] [] (M : Type u_18) (M₂ : Type u_19) [] [] [Module R M] [Module S M₂] extends :
Type (max u_18 u_19)

A linear equivalence is an invertible linear map.

• toFun : MM₂
• map_add' : ∀ (x y : M), (self).toFun (x + y) = (self).toFun x + (self).toFun y
• map_smul' : ∀ (m : R) (x : M), (self).toFun (m x) = σ m (self).toFun x
• invFun : M₂M

The backwards directed function underlying a linear equivalence.

• left_inv : Function.LeftInverse self.invFun (self).toFun

LinearEquiv.invFun is a left inverse to the linear equivalence's underlying function.

• right_inv : Function.RightInverse self.invFun (self).toFun

LinearEquiv.invFun is a right inverse to the linear equivalence's underlying function.

Instances For
@[reducible]
abbrev LinearEquiv.toAddEquiv {R : Type u_16} {S : Type u_17} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_18} {M₂ : Type u_19} [] [] [Module R M] [Module S M₂] (self : M ≃ₛₗ[σ] M₂) :
M ≃+ M₂

The additive equivalence of types underlying a linear equivalence.

Equations
• self.toAddEquiv = { toFun := (self).toFun, invFun := self.invFun, left_inv := , right_inv := , map_add' := }
Instances For
theorem LinearEquiv.right_inv {R : Type u_16} {S : Type u_17} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_18} {M₂ : Type u_19} [] [] [Module R M] [Module S M₂] (self : M ≃ₛₗ[σ] M₂) :
Function.RightInverse self.invFun (self).toFun

LinearEquiv.invFun is a right inverse to the linear equivalence's underlying function.

theorem LinearEquiv.left_inv {R : Type u_16} {S : Type u_17} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_18} {M₂ : Type u_19} [] [] [Module R M] [Module S M₂] (self : M ≃ₛₗ[σ] M₂) :
Function.LeftInverse self.invFun (self).toFun

LinearEquiv.invFun is a left inverse to the linear equivalence's underlying function.

The notation M ≃ₛₗ[σ] M₂ denotes the type of linear equivalences between M and M₂ over a ring homomorphism σ.

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

The notation M ≃ₗ [R] M₂ denotes the type of linear equivalences between M and M₂ over a plain linear map M →ₗ M₂.

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

The notation M ≃ₗ⋆[R] M₂ denotes the type of star-linear equivalences between M and M₂ over the ⋆ endomorphism of the underlying starred ring R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class SemilinearEquivClass (F : Type u_16) {R : outParam (Type u_17)} {S : outParam (Type u_18)} [] [] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [] [] (M : outParam (Type u_19)) (M₂ : outParam (Type u_20)) [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] extends :

SemilinearEquivClass F σ M M₂ asserts F is a type of bundled σ-semilinear equivs M → M₂.

See also LinearEquivClass F R M M₂ for the case where σ is the identity map on R.

A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

• map_add : ∀ (f : F) (a b : M), f (a + b) = f a + f b
• map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x

Applying a semilinear equivalence f over σ to r • x equals σ r • f x.

Instances
theorem SemilinearEquivClass.map_smulₛₗ {F : Type u_16} {R : outParam (Type u_17)} {S : outParam (Type u_18)} [] [] {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [] [] {M : outParam (Type u_19)} {M₂ : outParam (Type u_20)} [] [] [Module R M] [Module S M₂] [EquivLike F M M₂] [self : SemilinearEquivClass F σ M M₂] (f : F) (r : R) (x : M) :
f (r x) = σ r f x

Applying a semilinear equivalence f over σ to r • x equals σ r • f x.

@[reducible, inline]
abbrev LinearEquivClass (F : Type u_16) (R : outParam (Type u_17)) (M : outParam (Type u_18)) (M₂ : outParam (Type u_19)) [] [] [] [Module R M] [Module R M₂] [EquivLike F M M₂] :

LinearEquivClass F R M M₂ asserts F is a type of bundled R-linear equivs M → M₂. This is an abbreviation for SemilinearEquivClass F (RingHom.id R) M M₂.

Equations
Instances For
@[instance 100]
instance SemilinearEquivClass.instSemilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_16) [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] [EquivLike F M M₂] [s : SemilinearEquivClass F σ M M₂] :
SemilinearMapClass F σ M M₂
Equations
• =
def SemilinearEquivClass.semilinearEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} {F : Type u_16} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] (f : F) :
M ≃ₛₗ[σ] M₂

Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence.

Equations
• f = let __src := f; let __src_1 := f; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
instance SemilinearEquivClass.instCoeToSemilinearEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} {F : Type u_16} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] :

Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence.

Equations
• SemilinearEquivClass.instCoeToSemilinearEquiv = { coe := fun (f : F) => f }
instance LinearEquiv.instCoeLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
Equations
• LinearEquiv.instCoeLinearMap = { coe := LinearEquiv.toLinearMap }
def LinearEquiv.toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
(M ≃ₛₗ[σ] M₂)M M₂

The equivalence of types underlying a linear equivalence.

Equations
Instances For
theorem LinearEquiv.toEquiv_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
Function.Injective LinearEquiv.toEquiv
@[simp]
theorem LinearEquiv.toEquiv_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} :
e₁.toEquiv = e₂.toEquiv e₁ = e₂
theorem LinearEquiv.toLinearMap_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
Function.Injective LinearEquiv.toLinearMap
@[simp]
theorem LinearEquiv.toLinearMap_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} :
e₁ = e₂ e₁ = e₂
instance LinearEquiv.instEquivLike {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
EquivLike (M ≃ₛₗ[σ] M₂) M M₂
Equations
• LinearEquiv.instEquivLike = { coe := fun (e : M ≃ₛₗ[σ] M₂) => (e).toFun, inv := LinearEquiv.invFun, left_inv := , right_inv := , coe_injective' := }
instance LinearEquiv.instFunLike {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
FunLike (M ≃ₛₗ[σ] M₂) M M₂

Helper instance for when inference gets stuck on following the normal chain EquivLike → FunLike.

TODO: this instance doesn't appear to be necessary: remove it (after benchmarking?)

Equations
• LinearEquiv.instFunLike = { coe := DFunLike.coe, coe_injective' := }
instance LinearEquiv.instSemilinearEquivClass {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂
Equations
• =
@[simp]
theorem LinearEquiv.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] {to_fun : MM₂} {inv_fun : M₂M} {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y} {map_smul : ∀ (m : R) (x : M), { toFun := to_fun, map_add' := map_add }.toFun (m x) = σ m { toFun := to_fun, map_add' := map_add }.toFun x} {left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} {right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} :
{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv } = to_fun
theorem LinearEquiv.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [] [] :
@[simp]
theorem LinearEquiv.coe_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e = e
@[simp]
theorem LinearEquiv.coe_toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e.toEquiv = e
@[simp]
theorem LinearEquiv.coe_toLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e = e
theorem LinearEquiv.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
(e).toFun = e
theorem LinearEquiv.ext {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } {e : M ≃ₛₗ[σ] M₂} {e' : M ≃ₛₗ[σ] M₂} (h : ∀ (x : M), e x = e' x) :
e = e'
theorem LinearEquiv.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } {e : M ≃ₛₗ[σ] M₂} {e' : M ≃ₛₗ[σ] M₂} :
e = e' ∀ (x : M), e x = e' x
theorem LinearEquiv.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } {e : M ≃ₛₗ[σ] M₂} {x : M} {x' : M} :
x = x'e x = e x'
theorem LinearEquiv.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } {e : M ≃ₛₗ[σ] M₂} {e' : M ≃ₛₗ[σ] M₂} (h : e = e') (x : M) :
e x = e' x
def LinearEquiv.refl (R : Type u_1) (M : Type u_7) [] [] [Module R M] :

The identity map is a linear equivalence.

Equations
• = let __src := LinearMap.id; let __src_1 := ; { toLinearMap := __src, invFun := __src_1.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.refl_apply {R : Type u_1} {M : Type u_7} [] [] [Module R M] (x : M) :
() x = x
def LinearEquiv.symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
M₂ ≃ₛₗ[σ'] M

Linear equivalences are symmetric.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def LinearEquiv.Simps.apply {R : Type u_17} {S : Type u_18} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_19} {M₂ : Type u_20} [] [] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) :
MM₂

See Note [custom simps projection]

Equations
Instances For
def LinearEquiv.Simps.symm_apply {R : Type u_17} {S : Type u_18} [] [] {σ : R →+* S} {σ' : S →+* R} [] [] {M : Type u_19} {M₂ : Type u_20} [] [] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) :
M₂M

See Note [custom simps projection]

Equations
• = e.symm
Instances For
@[simp]
theorem LinearEquiv.invFun_eq_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e.invFun = e.symm
@[simp]
theorem LinearEquiv.coe_toEquiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e.toEquiv.symm = e.symm
def LinearEquiv.trans {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
M₁ ≃ₛₗ[σ₁₃] M₃

Linear equivalences are transitive.

Equations
• e₁₂.trans e₂₃ = let __src := (e₂₃).comp e₁₂; let __src_1 := e₁₂.toEquiv.trans e₂₃.toEquiv; { toLinearMap := __src, invFun := __src_1.invFun, left_inv := , right_inv := }
Instances For

Pretty printer defined by notation3 command.

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

The notation e₁ ≪≫ₗ e₂ denotes the composition of the linear equivalences e₁ and e₂.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LinearEquiv.coe_toAddEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
theorem LinearEquiv.toAddMonoidHom_commutes {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :

The two paths coercion can take to an AddMonoidHom are equivalent

@[simp]
theorem LinearEquiv.trans_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁) :
(e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)
theorem LinearEquiv.coe_trans {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃) = (e₂₃).comp e₁₂
@[simp]
theorem LinearEquiv.apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (c : M₂) :
e (e.symm c) = c
@[simp]
theorem LinearEquiv.symm_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (b : M) :
e.symm (e b) = b
@[simp]
theorem LinearEquiv.trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm
theorem LinearEquiv.symm_trans_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃) :
(e₁₂.trans e₂₃).symm c = e₁₂.symm (e₂₃.symm c)
@[simp]
theorem LinearEquiv.trans_refl {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e.trans () = e
@[simp]
theorem LinearEquiv.refl_trans {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
().trans e = e
theorem LinearEquiv.symm_apply_eq {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
e.symm x = y x = e y
theorem LinearEquiv.eq_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
y = e.symm x e y = x
theorem LinearEquiv.eq_comp_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_17} (f : M₂α) (g : M₁α) :
f = g e₁₂.symm f e₁₂ = g
theorem LinearEquiv.comp_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_17} (f : M₂α) (g : M₁α) :
g e₁₂.symm = f g = f e₁₂
theorem LinearEquiv.eq_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_17} (f : αM₁) (g : αM₂) :
f = e₁₂.symm g e₁₂ f = g
theorem LinearEquiv.symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_17} (f : αM₁) (g : αM₂) :
e₁₂.symm g = f g = e₁₂ f
theorem LinearEquiv.eq_comp_toLinearMap_symm {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
f = g.comp e₁₂.symm f.comp e₁₂ = g
theorem LinearEquiv.comp_toLinearMap_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
g.comp e₁₂.symm = f g = f.comp e₁₂
theorem LinearEquiv.eq_toLinearMap_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
f = (e₁₂.symm).comp g (e₁₂).comp f = g
theorem LinearEquiv.toLinearMap_symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R₁] [Semiring R₂] [Semiring R₃] [] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
(e₁₂.symm).comp g = f g = (e₁₂).comp f
@[simp]
theorem LinearEquiv.refl_symm {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
().symm =
@[simp]
theorem LinearEquiv.self_trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
f.trans f.symm = LinearEquiv.refl R₁ M₁
@[simp]
theorem LinearEquiv.symm_trans_self {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [Semiring R₁] [Semiring R₂] [] [] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
f.symm.trans f = LinearEquiv.refl R₂ M₂
@[simp]
theorem LinearEquiv.refl_toLinearMap {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
() = LinearMap.id
@[simp]
theorem LinearEquiv.comp_coe {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [] [] [] [] [Module R M] [Module R M₂] [Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
f' ∘ₗ f = (f ≪≫ₗ f')
@[simp]
theorem LinearEquiv.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (f : M₂M) (h₁ : Function.LeftInverse f (e).toFun) (h₂ : Function.RightInverse f (e).toFun) :
{ toLinearMap := e, invFun := f, left_inv := h₁, right_inv := h₂ } = e
theorem LinearEquiv.map_add {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (a : M) (b : M) :
e (a + b) = e a + e b
theorem LinearEquiv.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e 0 = 0
theorem LinearEquiv.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (c : R) (x : M) :
e (c x) = σ c e x
theorem LinearEquiv.map_smul {R₁ : Type u_2} {N₁ : Type u_11} {N₂ : Type u_12} [Semiring R₁] [] [] {module_N₁ : Module R₁ N₁} {module_N₂ : Module R₁ N₂} (e : N₁ ≃ₗ[R₁] N₂) (c : R₁) (x : N₁) :
e (c x) = c e x
theorem LinearEquiv.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x = 0 x = 0
theorem LinearEquiv.map_ne_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x 0 x 0
@[simp]
theorem LinearEquiv.symm_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
e.symm.symm = e
theorem LinearEquiv.symm_bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {σ : R →+* S} {σ' : S →+* R} [Module R M] [Module S M₂] [] [] :
Function.Bijective LinearEquiv.symm
@[simp]
theorem LinearEquiv.mk_coe' {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (f : M₂M) (h₁ : ∀ (x y : M₂), f (x + y) = f x + f y) (h₂ : ∀ (m : S) (x : M₂), { toFun := f, map_add' := h₁ }.toFun (m x) = σ' m { toFun := f, map_add' := h₁ }.toFun x) (h₃ : Function.LeftInverse e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun) (h₄ : Function.RightInverse e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun) :
{ toFun := f, map_add' := h₁, map_smul' := h₂, invFun := e, left_inv := h₃, right_inv := h₄ } = e.symm
@[simp]
theorem LinearEquiv.symm_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (f : M₂M) (h₁ : ∀ (x y : M), e (x + y) = e x + e y) (h₂ : ∀ (m : R) (x : M), { toFun := e, map_add' := h₁ }.toFun (m x) = σ m { toFun := e, map_add' := h₁ }.toFun x) (h₃ : Function.LeftInverse f { toFun := e, map_add' := h₁, map_smul' := h₂ }.toFun) (h₄ : Function.RightInverse f { toFun := e, map_add' := h₁, map_smul' := h₂ }.toFun) :
{ toFun := e, map_add' := h₁, map_smul' := h₂, invFun := f, left_inv := h₃, right_inv := h₄ }.symm = let __src := { toFun := e, map_add' := h₁, map_smul' := h₂, invFun := f, left_inv := h₃, right_inv := h₄ }.symm; { toFun := f, map_add' := , map_smul' := , invFun := e, left_inv := , right_inv := }
@[simp]
theorem LinearEquiv.coe_symm_mk {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [] [] [] [Module R M] [Module R M₂] {to_fun : MM₂} {inv_fun : M₂M} {map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y} {map_smul : ∀ (m : R) (x : M), { toFun := to_fun, map_add' := map_add }.toFun (m x) = () m { toFun := to_fun, map_add' := map_add }.toFun x} {left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} {right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun} :
{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }.symm = inv_fun
theorem LinearEquiv.bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
theorem LinearEquiv.injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
theorem LinearEquiv.surjective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) :
theorem LinearEquiv.image_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (s : Set M) :
e '' s = e.symm ⁻¹' s
theorem LinearEquiv.image_symm_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : } {re₂ : } (e : M ≃ₛₗ[σ] M₂) (s : Set M₂) :
e.symm '' s = e ⁻¹' s
@[simp]
theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_6} [] [] (f : R ≃+* S) :
∀ (a : S), f.toSemilinearEquiv.symm a = f.invFun a
@[simp]
theorem RingEquiv.toSemilinearEquiv_apply {R : Type u_1} {S : Type u_6} [] [] (f : R ≃+* S) (a : R) :
f.toSemilinearEquiv a = f a
def RingEquiv.toSemilinearEquiv {R : Type u_1} {S : Type u_6} [] [] (f : R ≃+* S) :
R ≃ₛₗ[f] S

Interpret a RingEquiv f as an f-semilinear equiv.

Equations
• f.toSemilinearEquiv = { toFun := f, map_add' := , map_smul' := , invFun := f.invFun, left_inv := , right_inv := }
Instances For
def LinearEquiv.ofInvolutive {R : Type u_1} {M : Type u_7} [] [] {σ : R →+* R} {σ' : R →+* R} [] [] :
{x : Module R M} → (f : M →ₛₗ[σ] M) → M ≃ₛₗ[σ] M

An involutive linear map is a linear equivalence.

Equations
• = let __src := ; { toLinearMap := f, invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.coe_ofInvolutive {R : Type u_1} {M : Type u_7} [] [] {σ : R →+* R} {σ' : R →+* R} [] [] :
∀ {x : Module R M} (f : M →ₛₗ[σ] M) (hf : ), () = f
@[simp]
theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (f : M ≃ₗ[S] M₂) (a : M₂) :
.symm a = f.symm a
@[simp]
theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (f : M ≃ₗ[S] M₂) (a : M) :
a = f a
def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (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
• = let __src := R f; { toFun := f, map_add' := , map_smul' := , invFun := f.symm, left_inv := , right_inv := }
Instances For
theorem LinearEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] :
@[simp]
theorem LinearEquiv.restrictScalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [] [] [] [] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [] (f : M ≃ₗ[S] M₂) (g : M ≃ₗ[S] M₂) :
theorem Module.End_isUnit_iff {R : Type u_1} {M : Type u_7} [] [] [Module R M] (f : ) :
instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
Equations
• LinearEquiv.automorphismGroup =
@[simp]
theorem LinearEquiv.coe_one {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
1 = id
@[simp]
theorem LinearEquiv.coe_toLinearMap_one {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
1 = LinearMap.id
@[simp]
theorem LinearEquiv.coe_toLinearMap_mul {R : Type u_1} {M : Type u_7} [] [] [Module R M] {e₁ : M ≃ₗ[R] M} {e₂ : M ≃ₗ[R] M} :
(e₁ * e₂) = e₁ * e₂
theorem LinearEquiv.coe_pow {R : Type u_1} {M : Type u_7} [] [] [Module R M] (e : M ≃ₗ[R] M) (n : ) :
(e ^ n) = (e)^[n]
theorem LinearEquiv.pow_apply {R : Type u_1} {M : Type u_7} [] [] [Module R M] (e : M ≃ₗ[R] M) (n : ) (m : M) :
(e ^ n) m = (e)^[n] m
@[simp]
theorem LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply {R : Type u_1} {M : Type u_7} [] [] [Module R M] (e : M ≃ₗ[R] M) :
LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = e

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
instance LinearEquiv.applyDistribMulAction {R : Type u_1} {M : Type u_7} [] [] [Module R M] :

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

This generalizes Function.End.applyMulAction.

Equations
• LinearEquiv.applyDistribMulAction =
@[simp]
theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_7} [] [] [Module R M] (f : M ≃ₗ[R] M) (a : M) :
f a = f a
instance LinearEquiv.apply_faithfulSMul {R : Type u_1} {M : Type u_7} [] [] [Module R M] :

LinearEquiv.applyDistribMulAction is faithful.

Equations
• =
instance LinearEquiv.apply_smulCommClass {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
Equations
• =
instance LinearEquiv.apply_smulCommClass' {R : Type u_1} {M : Type u_7} [] [] [Module R M] :
Equations
• =
@[simp]
theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [] [] [] [Module R M] [Module R M₂] [] [] :
∀ (x : M₂), ().symm x = 0
@[simp]
theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [] [] [] [Module R M] [Module R M₂] [] [] :
∀ (x : M), () x = 0
def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [] [] [] [Module R M] [Module R M₂] [] [] :
M ≃ₗ[R] M₂

Any two modules that are subsingletons are isomorphic.

Equations
• = let __src := 0; { toFun := fun (x : M) => 0, map_add' := , map_smul' := , invFun := fun (x : M₂) => 0, left_inv := , right_inv := }
Instances For
@[simp]
theorem LinearEquiv.ofSubsingleton_self {R : Type u_1} (M : Type u_7) [] [] [Module R M] [] :
@[simp]
theorem Module.compHom.toLinearEquiv_apply {R : Type u_16} {S : Type u_17} [] [] (g : R ≃+* S) (a : R) :
= g a
@[simp]
theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_16} {S : Type u_17} [] [] (g : R ≃+* S) (a : S) :
.symm a = g.symm a
def Module.compHom.toLinearEquiv {R : Type u_16} {S : Type u_17} [] [] (g : R ≃+* S) :

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

Equations
• = { toFun := g, map_add' := , map_smul' := , invFun := g.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [] [] [Module R M] [] [] [] (s : S) :
∀ (a : M), () a = s a
@[simp]
theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [] [] [Module R M] [] [] [] (s : S) :
∀ (a : M), ().symm a = s⁻¹ a
def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_6} (M : Type u_7) [] [] [Module R M] [] [] [] (s : S) :

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
@[simp]
theorem DistribMulAction.toModuleAut_apply (R : Type u_1) {S : Type u_6} (M : Type u_7) [] [] [Module R M] [] [] [] (s : S) :
def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_6} (M : Type u_7) [] [] [Module R M] [] [] [] :
S →* M ≃ₗ[R] M

Each element of the group defines a module automorphism.

This is a stronger version of DistribMulAction.toAddAut.

Equations
• = { toFun := , map_one' := , map_mul' := }
Instances For
def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [] [] [] [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
@[simp]
theorem AddEquiv.coe_toLinearEquiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [] [] [] [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_7} {M₂ : Type u_9} [] [] [] [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_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :

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

Equations
• e.toNatLinearEquiv = e.toLinearEquiv
Instances For
@[simp]
theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toNatLinearEquiv = e
@[simp]
theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toNatLinearEquiv = e
@[simp]
theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃ₗ[] M₂) :
(e).toNatLinearEquiv = e
@[simp]
theorem AddEquiv.toNatLinearEquiv_symm {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv
@[simp]
theorem AddEquiv.toNatLinearEquiv_refl {M : Type u_7} [] :
().toNatLinearEquiv =
@[simp]
theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [] [] [] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv
def AddEquiv.toIntLinearEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :

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

Equations
• e.toIntLinearEquiv = e.toLinearEquiv
Instances For
@[simp]
theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toIntLinearEquiv = e
@[simp]
theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toIntLinearEquiv = e
@[simp]
theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃ₗ[] M₂) :
(e).toIntLinearEquiv = e
@[simp]
theorem AddEquiv.toIntLinearEquiv_symm {M : Type u_7} {M₂ : Type u_9} [] [] (e : M ≃+ M₂) :
e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv
@[simp]
theorem AddEquiv.toIntLinearEquiv_refl {M : Type u_7} [] :
().toIntLinearEquiv =
@[simp]
theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [] [] [] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv
@[simp]
theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_6) (M : Type u_7) [] [] [] [Module R M] [Module S M] [] (f : R →ₗ[R] M) :
() f = f 1
@[simp]
theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_6) (M : Type u_7) [] [] [] [Module R M] [Module S M] [] (x : M) :
().symm x =
def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_6) (M : Type u_7) [] [] [] [Module R M] [Module 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
• One or more equations did not get rendered due to their size.
Instances For