(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_17} {S : Type u_18} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_19) (M₂ : Type u_20) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends LinearMap : Type (max u_19 u_20)

A linear equivalence is an invertible linear map.

• toFun : M → M₂
• 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.

@[reducible]

abbrev LinearEquiv.toAddEquiv {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_19} {M₂ : Type u_20} [AddCommMonoid M] [AddCommMonoid M₂] [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' := ⋯ }

theorem LinearEquiv.right_inv {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_19} {M₂ : Type u_20} [AddCommMonoid M] [AddCommMonoid M₂] [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_17} {S : Type u_18} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_19} {M₂ : Type u_20} [AddCommMonoid M] [AddCommMonoid M₂] [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.

def «term_≃ₛₗ[_]_» : Lean.TrailingParserDescr

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.

def «term_≃ₗ[_]_» : Lean.TrailingParserDescr

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.

class SemilinearEquivClass (F : Type u_17) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) {σ' : outParam (S →+* R)} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : outParam (Type u_20)) (M₂ : outParam (Type u_21)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [EquivLike F M M₂] extends AddEquivClass : Prop

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.

theorem SemilinearEquivClass.map_smulₛₗ {F : Type u_17} {R : outParam (Type u_18)} {S : outParam (Type u_19)} [Semiring R] [Semiring S] {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : outParam (Type u_20)} {M₂ : outParam (Type u_21)} [AddCommMonoid M] [AddCommMonoid M₂] [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_17) (R : outParam (Type u_18)) (M : outParam (Type u_19)) (M₂ : outParam (Type u_20)) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [EquivLike F M M₂] : Prop

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

• LinearEquivClass F R M M₂ = SemilinearEquivClass F (RingHom.id R) M M₂

@[instance 100]

instance SemilinearEquivClass.instSemilinearMapClass {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} (F : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂

Equations

• ⋯ = ⋯

def SemilinearEquivClass.semilinearEquiv {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [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 := ⋯ }

instance SemilinearEquivClass.instCoeToSemilinearEquiv {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂] : CoeHead 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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)

Equations

• LinearEquiv.instCoeLinearMap = { coe := LinearEquiv.toLinearMap }

def LinearEquiv.toEquiv {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : (M ≃ₛₗ[σ] M₂) → M ≃ M₂

The equivalence of types underlying a linear equivalence.

Equations

• f.toEquiv = f.toAddEquiv.toEquiv

theorem LinearEquiv.toEquiv_injective {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective LinearEquiv.toEquiv

@[simp]

theorem LinearEquiv.toEquiv_inj {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} : e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

theorem LinearEquiv.toLinearMap_injective {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective LinearEquiv.toLinearMap

@[simp]

theorem LinearEquiv.toLinearMap_inj {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {e₁ : M ≃ₛₗ[σ] M₂} {e₂ : M ≃ₛₗ[σ] M₂} : ↑e₁ = ↑e₂ ↔ e₁ = e₂

instance LinearEquiv.instEquivLike {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : 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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : 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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂

Equations

• ⋯ = ⋯

@[simp]

theorem LinearEquiv.coe_mk {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {to_fun : M → M₂} {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : Function.Injective CoeFun.coe

@[simp]

theorem LinearEquiv.coe_coe {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑↑e = ⇑e

@[simp]

theorem LinearEquiv.coe_toEquiv {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑e.toEquiv = ⇑e

@[simp]

theorem LinearEquiv.coe_toLinearMap {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : ⇑↑e = ⇑e

theorem LinearEquiv.toFun_eq_coe {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (↑e).toFun = ⇑e

theorem LinearEquiv.ext {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e : M ≃ₛₗ[σ] M₂} {x : M} {x' : M} : x = x' → e x = e x'

theorem LinearEquiv.congr_fun {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {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_8) [Semiring R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] M

The identity map is a linear equivalence.

Equations

• LinearEquiv.refl R M = let __src := LinearMap.id; let __src_1 := Equiv.refl M; { toLinearMap := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.refl_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (LinearEquiv.refl R M) x = x

def LinearEquiv.symm {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : M₂ ≃ₛₗ[σ'] M

Linear equivalences are symmetric.

Equations

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

def LinearEquiv.Simps.apply {R : Type u_18} {S : Type u_19} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_20} {M₂ : Type u_21} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) : M → M₂

See Note [custom simps projection]

Equations

• LinearEquiv.Simps.apply e = ⇑e

def LinearEquiv.Simps.symm_apply {R : Type u_18} {S : Type u_19} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] {M : Type u_20} {M₂ : Type u_21} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (e : M ≃ₛₗ[σ] M₂) : M₂ → M

See Note [custom simps projection]

Equations

• LinearEquiv.Simps.symm_apply e = ⇑e.symm

@[simp]

theorem LinearEquiv.invFun_eq_symm {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.invFun = ⇑e.symm

@[simp]

theorem LinearEquiv.coe_toEquiv_symm {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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 := ⋯ }

def LinearEquiv.transNotation : Lean.TrailingParserDescr

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

Equations

• LinearEquiv.transNotation = Lean.ParserDescr.trailingNode `LinearEquiv.transNotation 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪≫ₗ ") (Lean.ParserDescr.cat `term 81))

def LinearEquiv.transNotation.delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

@[simp]

theorem LinearEquiv.coe_toAddEquiv {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.toAddEquiv = ↑e

theorem LinearEquiv.toAddMonoidHom_commutes {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (↑e).toAddMonoidHom = e.toAddEquiv.toAddMonoidHom

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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : M₂) : e (e.symm c) = c

@[simp]

theorem LinearEquiv.symm_apply_apply {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.trans (LinearEquiv.refl S M₂) = e

@[simp]

theorem LinearEquiv.refl_trans {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : (LinearEquiv.refl R M).trans e = e

theorem LinearEquiv.symm_apply_eq {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_9} {M₂ : Type u_10} [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 σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_18} (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_9} {M₂ : Type u_10} [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 σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_18} (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_9} {M₂ : Type u_10} [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 σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_18} (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_9} {M₂ : Type u_10} [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 σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_18} (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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_9} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {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_8} [Semiring R] [AddCommMonoid M] [Module R M] : (LinearEquiv.refl R M).symm = LinearEquiv.refl R M

@[simp]

theorem LinearEquiv.self_trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_9} {M₂ : Type u_10} [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₂) : 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_9} {M₂ : Type u_10} [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₂) : f.symm.trans f = LinearEquiv.refl R₂ M₂

@[simp]

theorem LinearEquiv.refl_toLinearMap {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : ↑(LinearEquiv.refl R M) = LinearMap.id

@[simp]

theorem LinearEquiv.comp_coe {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e 0 = 0

theorem LinearEquiv.map_smulₛₗ {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : R) (x : M) : e (c • x) = σ c • e x

theorem LinearEquiv.map_smul {R₁ : Type u_2} {N₁ : Type u_12} {N₂ : Type u_13} [Semiring R₁] [AddCommMonoid N₁] [AddCommMonoid N₂] {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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} : e x = 0 ↔ x = 0

theorem LinearEquiv.map_ne_zero_iff {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} : e x ≠ 0 ↔ x ≠ 0

@[simp]

theorem LinearEquiv.symm_symm {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : e.symm.symm = e

theorem LinearEquiv.symm_bijective {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {σ : R →+* S} {σ' : S →+* R} [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] : Function.Bijective LinearEquiv.symm

@[simp]

theorem LinearEquiv.mk_coe' {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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

def LinearEquiv.symm_mk.aux {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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) : M₂ ≃ₛₗ[σ'] M

Auxilliary definition to avoid looping in dsimp with LinearEquiv.symm_mk.

Equations

• LinearEquiv.symm_mk.aux e f h₁ h₂ h₃ h₄ = { toFun := ⇑e, map_add' := h₁, map_smul' := h₂, invFun := f, left_inv := h₃, right_inv := h₄ }.symm

@[simp]

theorem LinearEquiv.symm_mk {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (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 := LinearEquiv.symm_mk.aux e f h₁ h₂ h₃ h₄; { 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_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {to_fun : M → M₂} {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) = (RingHom.id R) 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_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Bijective ⇑e

theorem LinearEquiv.injective {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Injective ⇑e

theorem LinearEquiv.surjective {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) : Function.Surjective ⇑e

theorem LinearEquiv.image_eq_preimage {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M) : ⇑e '' s = ⇑e.symm ⁻¹' s

theorem LinearEquiv.image_symm_eq_preimage {R : Type u_1} {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : Set M₂) : ⇑e.symm '' s = ⇑e ⁻¹' s

@[simp]

theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_7} [Semiring R] [Semiring S] (f : R ≃+* S) : ∀ (a : S), f.toSemilinearEquiv.symm a = f.invFun a

@[simp]

theorem RingEquiv.toSemilinearEquiv_apply {R : Type u_1} {S : Type u_7} [Semiring R] [Semiring S] (f : R ≃+* S) (a : R) : f.toSemilinearEquiv a = f a

def RingEquiv.toSemilinearEquiv {R : Type u_1} {S : Type u_7} [Semiring R] [Semiring S] (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 := ⋯ }

def LinearEquiv.ofInvolutive {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] {σ : R →+* R} {σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : {x : Module R M} → (f : M →ₛₗ[σ] M) → Function.Involutive ⇑f → M ≃ₛₗ[σ] M

An involutive linear map is a linear equivalence.

Equations

• LinearEquiv.ofInvolutive f hf = let __src := Function.Involutive.toPerm (⇑f) hf; { toLinearMap := f, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.coe_ofInvolutive {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] {σ : R →+* R} {σ' : R →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] : ∀ {x : Module R M} (f : M →ₛₗ[σ] M) (hf : Function.Involutive ⇑f), ⇑(LinearEquiv.ofInvolutive f hf) = ⇑f

@[simp]

theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M₂) : (LinearEquiv.restrictScalars R f).symm a = f.symm a

@[simp]

theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M ≃ₗ[S] M₂) (a : M) : (LinearEquiv.restrictScalars R f) a = f a

def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [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 = let __src := ↑R ↑f; { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

theorem LinearEquiv.restrictScalars_injective (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] : Function.Injective (LinearEquiv.restrictScalars R)

@[simp]

theorem LinearEquiv.restrictScalars_inj (R : Type u_1) {S : Type u_7} {M : Type u_8} {M₂ : Type u_10} [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₂) (g : M ≃ₗ[S] M₂) : LinearEquiv.restrictScalars R f = LinearEquiv.restrictScalars R g ↔ f = g

theorem Module.End_isUnit_iff {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : IsUnit f ↔ Function.Bijective ⇑f

instance LinearEquiv.automorphismGroup {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : Group (M ≃ₗ[R] M)

Equations

• LinearEquiv.automorphismGroup = Group.mk ⋯

@[simp]

theorem LinearEquiv.coe_one {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : ⇑1 = id

@[simp]

theorem LinearEquiv.coe_toLinearMap_one {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : ↑1 = LinearMap.id

@[simp]

theorem LinearEquiv.coe_toLinearMap_mul {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [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_8} [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_8} [Semiring R] [AddCommMonoid M] [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_8} [Semiring R] [AddCommMonoid M] [Module R M] (e : M ≃ₗ[R] M) : LinearEquiv.automorphismGroup.toLinearMapMonoidHom e = ↑e

def LinearEquiv.automorphismGroup.toLinearMapMonoidHom {R : Type u_1} {M : Type u_8} [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' := ⋯ }

instance LinearEquiv.applyDistribMulAction {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : DistribMulAction (M ≃ₗ[R] M) M

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

This generalizes Function.End.applyMulAction.

Equations

• LinearEquiv.applyDistribMulAction = DistribMulAction.mk ⋯ ⋯

@[simp]

theorem LinearEquiv.smul_def {R : Type u_1} {M : Type u_8} [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_8} [Semiring R] [AddCommMonoid M] [Module R M] : FaithfulSMul (M ≃ₗ[R] M) M

LinearEquiv.applyDistribMulAction is faithful.

Equations

• ⋯ = ⋯

instance LinearEquiv.apply_smulCommClass {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : SMulCommClass R (M ≃ₗ[R] M) M

Equations

• ⋯ = ⋯

instance LinearEquiv.apply_smulCommClass' {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] : SMulCommClass (M ≃ₗ[R] M) R M

Equations

• ⋯ = ⋯

@[simp]

theorem LinearEquiv.ofSubsingleton_symm_apply {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] : ∀ (x : M₂), (LinearEquiv.ofSubsingleton M M₂).symm x = 0

@[simp]

theorem LinearEquiv.ofSubsingleton_apply {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Subsingleton M] [Subsingleton M₂] : ∀ (x : M), (LinearEquiv.ofSubsingleton M M₂) x = 0

def LinearEquiv.ofSubsingleton {R : Type u_1} (M : Type u_8) (M₂ : Type u_10) [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₂ = let __src := 0; { toFun := fun (x : M) => 0, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : M₂) => 0, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.ofSubsingleton_self {R : Type u_1} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : LinearEquiv.ofSubsingleton M M = LinearEquiv.refl R M

@[simp]

theorem Module.compHom.toLinearEquiv_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R ≃+* S) (a : R) : (Module.compHom.toLinearEquiv g) a = g a

@[simp]

theorem Module.compHom.toLinearEquiv_symm_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R ≃+* S) (a : S) : (Module.compHom.toLinearEquiv g).symm a = g.symm a

def Module.compHom.toLinearEquiv {R : Type u_17} {S : Type u_18} [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 := ⋯ }

@[simp]

theorem DistribMulAction.toLinearEquiv_apply (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : ∀ (a : M), (DistribMulAction.toLinearEquiv R M s) a = s • a

@[simp]

theorem DistribMulAction.toLinearEquiv_symm_apply (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : ∀ (a : M), (DistribMulAction.toLinearEquiv R M s).symm a = s⁻¹ • a

def DistribMulAction.toLinearEquiv (R : Type u_1) {S : Type u_7} (M : Type u_8) [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.

@[simp]

theorem DistribMulAction.toModuleAut_apply (R : Type u_1) {S : Type u_7} (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] [Group S] [DistribMulAction S M] [SMulCommClass S R M] (s : S) : (DistribMulAction.toModuleAut R M) s = DistribMulAction.toLinearEquiv R M s

def DistribMulAction.toModuleAut (R : Type u_1) {S : Type u_7} (M : Type u_8) [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' := ⋯ }

def AddEquiv.toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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 := ⋯ }

@[simp]

theorem AddEquiv.coe_toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [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 ⋯

@[simp]

theorem AddEquiv.coe_toNatLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : ⇑e.toNatLinearEquiv = ⇑e

@[simp]

theorem AddEquiv.toNatLinearEquiv_toAddEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : ↑e.toNatLinearEquiv = e

@[simp]

theorem LinearEquiv.toAddEquiv_toNatLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃ₗ[ℕ] M₂) : (↑e).toNatLinearEquiv = e

@[simp]

theorem AddEquiv.toNatLinearEquiv_symm {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (e : M ≃+ M₂) : e.toNatLinearEquiv.symm = e.symm.toNatLinearEquiv

@[simp]

theorem AddEquiv.toNatLinearEquiv_refl {M : Type u_8} [AddCommMonoid M] : (AddEquiv.refl M).toNatLinearEquiv = LinearEquiv.refl ℕ M

@[simp]

theorem AddEquiv.toNatLinearEquiv_trans {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) : e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv = (e.trans e₂).toNatLinearEquiv

def AddEquiv.toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [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 ⋯

@[simp]

theorem AddEquiv.coe_toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : ⇑e.toIntLinearEquiv = ⇑e

@[simp]

theorem AddEquiv.toIntLinearEquiv_toAddEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : ↑e.toIntLinearEquiv = e

@[simp]

theorem LinearEquiv.toAddEquiv_toIntLinearEquiv {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃ₗ[ℤ] M₂) : (↑e).toIntLinearEquiv = e

@[simp]

theorem AddEquiv.toIntLinearEquiv_symm {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (e : M ≃+ M₂) : e.toIntLinearEquiv.symm = e.symm.toIntLinearEquiv

@[simp]

theorem AddEquiv.toIntLinearEquiv_refl {M : Type u_8} [AddCommGroup M] : (AddEquiv.refl M).toIntLinearEquiv = LinearEquiv.refl ℤ M

@[simp]

theorem AddEquiv.toIntLinearEquiv_trans {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) : e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv = (e.trans e₂).toIntLinearEquiv

@[simp]

theorem LinearMap.ringLmapEquivSelf_symm_apply (R : Type u_1) (S : Type u_7) (M : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (x : M) : (LinearMap.ringLmapEquivSelf R S M).symm x = LinearMap.smulRight 1 x

@[simp]

theorem LinearMap.ringLmapEquivSelf_apply (R : Type u_1) (S : Type u_7) (M : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : R →ₗ[R] M) : (LinearMap.ringLmapEquivSelf R S M) f = f 1

def LinearMap.ringLmapEquivSelf (R : Type u_1) (S : Type u_7) (M : Type u_8) [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

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

@[simp]

theorem addMonoidHomLequivNat_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [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_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R B] (f : A →ₗ[ℕ] B) : (addMonoidHomLequivNat R).symm f = f.toAddMonoidHom

def addMonoidHomLequivNat {A : Type u_17} {B : Type u_18} (R : Type u_19) [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 := ⋯ }

@[simp]

theorem addMonoidHomLequivInt_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →+ B) : (addMonoidHomLequivInt R) f = f.toIntLinearMap

@[simp]

theorem addMonoidHomLequivInt_symm_apply {A : Type u_17} {B : Type u_18} (R : Type u_19) [Semiring R] [AddCommGroup A] [AddCommGroup B] [Module R B] (f : A →ₗ[ℤ] B) : (addMonoidHomLequivInt R).symm f = f.toAddMonoidHom

def addMonoidHomLequivInt {A : Type u_17} {B : Type u_18} (R : Type u_19) [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 := ⋯ }

@[simp]

theorem addMonoidEndRingEquivInt_symm_apply (A : Type u_17) [AddCommGroup A] : ∀ (a : A →ₗ[ℤ] A), (addMonoidEndRingEquivInt A).symm a = (addMonoidHomLequivInt ℤ).invFun a

@[simp]

theorem addMonoidEndRingEquivInt_apply (A : Type u_17) [AddCommGroup A] : ∀ (a : A →+ A), (addMonoidEndRingEquivInt A) a = (↑(addMonoidHomLequivInt ℤ)).toFun a

def addMonoidEndRingEquivInt (A : Type u_17) [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 = let __src := addMonoidHomLequivInt ℤ; { toFun := (↑__src).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

instance LinearEquiv.instZero {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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 := ⋯ } }

@[simp]

theorem LinearEquiv.zero_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] [Subsingleton M] [Subsingleton M₂] : LinearEquiv.symm 0 = 0

@[simp]

theorem LinearEquiv.coe_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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_3} {M : Type u_8} {M₂ : Type u_10} [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_3} {M : Type u_8} {M₂ : Type u_10} [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 := ⋯ }

instance LinearEquiv.uniqueOfSubsingleton {R : Type u_1} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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

def LinearEquiv.curry (R : Type u_1) [Semiring R] (V : Type u_17) (V₂ : Type u_18) : (V × V₂ → R) ≃ₗ[R] V → V₂ → R

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

Equations

• LinearEquiv.curry R V V₂ = let __src := Equiv.curry V V₂ R; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.coe_curry (R : Type u_1) [Semiring R] (V : Type u_18) (V₂ : Type u_17) : ⇑(LinearEquiv.curry R V V₂) = Function.curry

@[simp]

theorem LinearEquiv.coe_curry_symm (R : Type u_1) [Semiring R] (V : Type u_18) (V₂ : Type u_17) : ⇑(LinearEquiv.curry R V V₂).symm = Function.uncurry

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

x ↦ -x as a LinearEquiv

Equations

• LinearEquiv.neg R = let __src := Equiv.neg M; let __src_1 := -LinearMap.id; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LinearEquiv.coe_neg {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] : ⇑(LinearEquiv.neg R) = -id

theorem LinearEquiv.neg_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] (x : M) : (LinearEquiv.neg R) x = -x

@[simp]

theorem LinearEquiv.symm_neg {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommGroup M] [Module R M] : (LinearEquiv.neg R).symm = LinearEquiv.neg R

def LinearEquiv.smulOfUnit {R : Type u_1} {M : Type u_8} [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

def LinearEquiv.arrowCongr {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[R] M₂ →ₗ[R] M₂₂

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

Equations

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

@[simp]

theorem LinearEquiv.arrowCongr_apply {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) : ((e₁.arrowCongr e₂) f) x = e₂ (f (e₁.symm x))

@[simp]

theorem LinearEquiv.arrowCongr_symm_apply {R : Type u_17} {M₁ : Type u_18} {M₂ : Type u_19} {M₂₁ : Type u_20} {M₂₂ : Type u_21} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) : ((e₁.arrowCongr e₂).symm f) x = e₂.symm (f (e₁ x))

theorem LinearEquiv.arrowCongr_comp {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] {N : Type u_17} {N₂ : Type u_18} {N₃ : Type u_19} [AddCommMonoid N] [AddCommMonoid N₂] [AddCommMonoid N₃] [Module R N] [Module R N₂] [Module R N₃] (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : (e₁.arrowCongr e₃) (g ∘ₗ f) = (e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f

theorem LinearEquiv.arrowCongr_trans {R : Type u_1} [CommSemiring R] {M₁ : Type u_17} {M₂ : Type u_18} {M₃ : Type u_19} {N₁ : Type u_20} {N₂ : Type u_21} {N₃ : Type u_22} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) : e₁.arrowCongr e₂ ≪≫ₗ e₃.arrowCongr e₄ = (e₁ ≪≫ₗ e₃).arrowCongr (e₂ ≪≫ₗ e₄)

def LinearEquiv.congrRight {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [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

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

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

Equations

• e.conj = e.arrowCongr e

theorem LinearEquiv.conj_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) : e.conj f = (↑e ∘ₗ f) ∘ₗ ↑e.symm

theorem LinearEquiv.conj_apply_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (x : M₂) : (e.conj f) x = e (f (e.symm x))

theorem LinearEquiv.symm_conj_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M₂) : e.symm.conj f = (↑e.symm ∘ₗ f) ∘ₗ ↑e

theorem LinearEquiv.conj_comp {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) (f : Module.End R M) (g : Module.End R M) : e.conj (g ∘ₗ f) = e.conj g ∘ₗ e.conj f

theorem LinearEquiv.conj_trans {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : e₁.conj ≪≫ₗ e₂.conj = (e₁ ≪≫ₗ e₂).conj

@[simp]

theorem LinearEquiv.conj_id {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id

def LinearEquiv.congrLeft (M : Type u_8) {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {R : Type u_17} (S : Type u_18) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M] [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] M₃ →ₗ[R] M

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

Equations

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

@[simp]

theorem LinearEquiv.smulOfNeZero_symm_apply (K : Type u_6) (M : Type u_8) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : ∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha).symm a_1 = (Units.mk0 a ha)⁻¹ • a_1

@[simp]

theorem LinearEquiv.smulOfNeZero_apply (K : Type u_6) (M : Type u_8) [Field K] [AddCommGroup M] [Module K M] (a : K) (ha : a ≠ 0) : ∀ (a_1 : M), (LinearEquiv.smulOfNeZero K M a ha) a_1 = Units.mk0 a ha • a_1

def LinearEquiv.smulOfNeZero (K : Type u_6) (M : Type u_8) [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)

def Equiv.toLinearEquiv {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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 = let __src := IsLinearMap.mk' (⇑e) h; { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

def LinearMap.funLeft (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (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' := ⋯ }

@[simp]

theorem LinearMap.funLeft_apply (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : m → n) (g : n → M) (i : m) : (LinearMap.funLeft R M f) g i = g (f i)

@[simp]

theorem LinearMap.funLeft_id (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_18} (g : n → M) : (LinearMap.funLeft R M id) g = g

theorem LinearMap.funLeft_comp (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} {p : Type u_19} (f₁ : n → p) (f₂ : m → n) : LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁

theorem LinearMap.funLeft_surjective_of_injective (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : m → n) (hf : Function.Injective f) : Function.Surjective ⇑(LinearMap.funLeft R M f)

theorem LinearMap.funLeft_injective_of_surjective (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (f : m → n) (hf : Function.Surjective f) : Function.Injective ⇑(LinearMap.funLeft R M f)

def LinearEquiv.funCongrLeft (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (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) ⋯ ⋯

@[simp]

theorem LinearEquiv.funCongrLeft_apply (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (e : m ≃ n) (x : n → M) : (LinearEquiv.funCongrLeft R M e) x = (LinearMap.funLeft R M ⇑e) x

@[simp]

theorem LinearEquiv.funCongrLeft_id (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {n : Type u_18} : LinearEquiv.funCongrLeft R M (Equiv.refl n) = LinearEquiv.refl R (n → M)

@[simp]

theorem LinearEquiv.funCongrLeft_comp (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} {p : Type u_19} (e₁ : m ≃ n) (e₂ : n ≃ p) : LinearEquiv.funCongrLeft R M (e₁.trans e₂) = LinearEquiv.funCongrLeft R M e₂ ≪≫ₗ LinearEquiv.funCongrLeft R M e₁

@[simp]

theorem LinearEquiv.funCongrLeft_symm (R : Type u_1) (M : Type u_8) [Semiring R] [AddCommMonoid M] [Module R M] {m : Type u_17} {n : Type u_18} (e : m ≃ n) : (LinearEquiv.funCongrLeft R M e).symm = LinearEquiv.funCongrLeft R M e.symm