(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

source

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

Type (max u_18 u_19)

toFun : M → M₂
map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑σ r • AddHom.toFun s.toAddHom x
invFun : M₂ → M
The backwards directed function underlying a linear equivalence.
left_inv : Function.LeftInverse s.invFun s.toFun
LinearEquiv.invFun is a left inverse to the linear equivalence's underlying function.
right_inv : Function.RightInverse s.invFun s.toFun
LinearEquiv.invFun is a right inverse to the linear equivalence's underlying function.

A linear equivalence is an invertible linear map.

Instances For

source

@[reducible]

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

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

def «term_≃ₗ⋆[_]_» :

Lean.TrailingParserDescr

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

source

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

Type (max (max u_16 u_19) u_20)

coe : F → M → M₂
inv : F → M₂ → M
left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
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.

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.

Instances

source

@[inline, reducible]

abbrev LinearEquivClass (F : Type u_16) (R : outParam (Type u_17)) (M : outParam (Type u_18)) (M₂ : outParam (Type u_19)) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] :

Type (max (max u_16 u_18) u_19)

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₂

Instances For

source

instance SemilinearEquivClass.instSemilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_16) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [s : SemilinearEquivClass F σ M M₂] :

SemilinearMapClass F σ M M₂

Equations

SemilinearEquivClass.instSemilinearMapClass F = SemilinearMapClass.mk (_ : ∀ (f : F) (r : R) (x : M), ↑f (r • x) = ↑σ r • ↑f x)

source

instance LinearEquiv.instCoeLinearEquivLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.instCoeLinearEquivLinearMap = { coe := LinearEquiv.toLinearMap }

source

def LinearEquiv.toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

LinearEquiv.toEquiv f = (LinearEquiv.toAddEquiv f).toEquiv

Instances For

source

theorem LinearEquiv.toEquiv_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :

Function.Injective LinearEquiv.toEquiv

source

@[simp]

theorem LinearEquiv.toEquiv_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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₂} :

LinearEquiv.toEquiv e₁ = LinearEquiv.toEquiv e₂ ↔ e₁ = e₂

source

theorem LinearEquiv.toLinearMap_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :

Function.Injective LinearEquiv.toLinearMap

source

@[simp]

theorem LinearEquiv.toLinearMap_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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₂

source

instance LinearEquiv.instSemilinearEquivClassLinearEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

LinearEquiv.instSemilinearEquivClassLinearEquiv = SemilinearEquivClass.mk (_ : ∀ (x : M ≃ₛₗ[σ] M₂) (r : R) (x_1 : M), AddHom.toFun x.toAddHom (r • x_1) = ↑σ r • AddHom.toFun x.toAddHom x_1)

source

@[simp]

theorem LinearEquiv.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 : ∀ (r : R) (x : M), AddHom.toFun { toFun := to_fun, map_add' := map_add } (r • x) = ↑σ r • AddHom.toFun { toFun := to_fun, map_add' := map_add } x} {left_inv : Function.LeftInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} {right_inv : Function.RightInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} :

↑{ toLinearMap := { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv } = to_fun

source

theorem LinearEquiv.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] :

Function.Injective CoeFun.coe

source

@[simp]

theorem LinearEquiv.coe_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

@[simp]

theorem LinearEquiv.coe_toEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.toEquiv e) = ↑e

source

@[simp]

theorem LinearEquiv.coe_toLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.ext {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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'

source

theorem LinearEquiv.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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'

source

theorem LinearEquiv.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

def LinearEquiv.refl (R : Type u_1) (M : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] :

M ≃ₗ[R] M

The identity map is a linear equivalence.

Equations

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

Instances For

source

@[simp]

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

↑(LinearEquiv.refl R M) x = x

source

def LinearEquiv.symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.

Instances For

source

def LinearEquiv.Simps.apply {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₂] (e : M ≃ₛₗ[σ] M₂) :

M → M₂

See Note [custom simps projection]

Equations

LinearEquiv.Simps.apply e = ↑e

Instances For

source

def LinearEquiv.Simps.symm_apply {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₂] (e : M ≃ₛₗ[σ] M₂) :

M₂ → M

See Note [custom simps projection]

Equations

LinearEquiv.Simps.symm_apply e = ↑(LinearEquiv.symm e)

Instances For

source

@[simp]

theorem LinearEquiv.invFun_eq_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 = ↑(LinearEquiv.symm e)

source

@[simp]

theorem LinearEquiv.coe_toEquiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.toEquiv e).symm = ↑(LinearEquiv.symm e)

source

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₃] [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

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

Instances For

source

def LinearEquiv.«term_≪≫ₗ_» :

Lean.TrailingParserDescr

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

Equations

LinearEquiv.«term_≪≫ₗ_» = Lean.ParserDescr.trailingNode `LinearEquiv.term_≪≫ₗ_ 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪≫ₗ ") (Lean.ParserDescr.cat `term 81))

Instances For

source

@[simp]

theorem LinearEquiv.coe_toAddEquiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.toAddEquiv e = ↑e

source

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

LinearMap.toAddMonoidHom ↑e = AddEquiv.toAddMonoidHom (LinearEquiv.toAddEquiv e)

The two paths coercion can take to an AddMonoidHom are equivalent

source

@[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₃] [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₁) :

↑(LinearEquiv.trans e₁₂ e₂₃) c = ↑e₂₃ (↑e₁₂ c)

source

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₃] [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₃} :

↑(LinearEquiv.trans e₁₂ e₂₃) = LinearMap.comp ↑e₂₃ ↑e₁₂

source

@[simp]

theorem LinearEquiv.apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 (↑(LinearEquiv.symm e) c) = c

source

@[simp]

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

↑(LinearEquiv.symm e) (↑e b) = b

source

@[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₃] [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₃} :

LinearEquiv.symm (LinearEquiv.trans e₁₂ e₂₃) = LinearEquiv.trans (LinearEquiv.symm e₂₃) (LinearEquiv.symm e₁₂)

source

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₃] [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₃) :

↑(LinearEquiv.symm (LinearEquiv.trans e₁₂ e₂₃)) c = ↑(LinearEquiv.symm e₁₂) (↑(LinearEquiv.symm e₂₃) c)

source

@[simp]

theorem LinearEquiv.trans_refl {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.trans e (LinearEquiv.refl S M₂) = e

source

@[simp]

theorem LinearEquiv.refl_trans {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.trans (LinearEquiv.refl R M) e = e

source

theorem LinearEquiv.symm_apply_eq {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 : (fun x => M) x} :

↑(LinearEquiv.symm e) x = y ↔ x = ↑e y

source

theorem LinearEquiv.eq_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 : (fun x => M) x} :

y = ↑(LinearEquiv.symm e) x ↔ ↑e y = x

source

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₂] [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_17} (f : M₂ → α) (g : M₁ → α) :

f = g ∘ ↑(LinearEquiv.symm e₁₂) ↔ f ∘ ↑e₁₂ = g

source

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₂] [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_17} (f : M₂ → α) (g : M₁ → α) :

g ∘ ↑(LinearEquiv.symm e₁₂) = f ↔ g = f ∘ ↑e₁₂

source

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₂] [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_17} (f : α → M₁) (g : α → M₂) :

f = ↑(LinearEquiv.symm e₁₂) ∘ g ↔ ↑e₁₂ ∘ f = g

source

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₂] [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_17} (f : α → M₁) (g : α → M₂) :

↑(LinearEquiv.symm e₁₂) ∘ g = f ↔ g = ↑e₁₂ ∘ f

source

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₃] [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 = LinearMap.comp g ↑(LinearEquiv.symm e₁₂) ↔ LinearMap.comp f ↑e₁₂ = g

source

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₃] [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₃) :

LinearMap.comp g ↑(LinearEquiv.symm e₁₂) = f ↔ g = LinearMap.comp f ↑e₁₂

source

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₃] [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 = LinearMap.comp (↑(LinearEquiv.symm e₁₂)) g ↔ LinearMap.comp (↑e₁₂) f = g

source

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₃] [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₂) :

LinearMap.comp (↑(LinearEquiv.symm e₁₂)) g = f ↔ g = LinearMap.comp (↑e₁₂) f

source

@[simp]

theorem LinearEquiv.refl_symm {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] :

LinearEquiv.symm (LinearEquiv.refl R M) = LinearEquiv.refl R M

source

@[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₂] [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₂) :

LinearEquiv.trans f (LinearEquiv.symm f) = LinearEquiv.refl R₁ M₁

source

@[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₂] [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₂) :

LinearEquiv.trans (LinearEquiv.symm f) f = LinearEquiv.refl R₂ M₂

source

@[simp]

theorem LinearEquiv.refl_toLinearMap {R : Type u_1} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] :

↑(LinearEquiv.refl R M) = LinearMap.id

source

@[simp]

theorem LinearEquiv.comp_coe {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R M₂] [Module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :

LinearMap.comp ↑f' ↑f = ↑(LinearEquiv.trans f f')

source

@[simp]

theorem LinearEquiv.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.map_add {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.map_smul {R₁ : Type u_2} {N₁ : Type u_11} {N₂ : Type u_12} [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

source

theorem LinearEquiv.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.map_ne_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

@[simp]

theorem LinearEquiv.symm_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.symm (LinearEquiv.symm e) = e

source

theorem LinearEquiv.symm_bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] {σ : R →+* S} {σ' : S →+* R} [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] :

Function.Bijective LinearEquiv.symm

source

@[simp]

theorem LinearEquiv.mk_coe' {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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₂ : ∀ (r : S) (x : M₂), AddHom.toFun { toFun := f, map_add' := h₁ } (r • x) = ↑σ' r • AddHom.toFun { toFun := f, map_add' := h₁ } x) (h₃ : Function.LeftInverse ↑e { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) (h₄ : Function.RightInverse ↑e { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) :

{ toLinearMap := { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }, invFun := ↑e, left_inv := h₃, right_inv := h₄ } = LinearEquiv.symm e

source

@[simp]

theorem LinearEquiv.symm_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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₂ : ∀ (r : R) (x : M), AddHom.toFun { toFun := ↑e, map_add' := h₁ } (r • x) = ↑σ r • AddHom.toFun { toFun := ↑e, map_add' := h₁ } x) (h₃ : Function.LeftInverse f { toAddHom := { toFun := ↑e, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) (h₄ : Function.RightInverse f { toAddHom := { toFun := ↑e, map_add' := h₁ }, map_smul' := h₂ }.toAddHom.toFun) :

LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := ↑e, map_add' := h₁ }, map_smul' := h₂ }, invFun := f, left_inv := h₃, right_inv := h₄ } = let src := LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := ↑e, map_add' := h₁ }, map_smul' := h₂ }, invFun := f, left_inv := h₃, right_inv := h₄ }; { toLinearMap := { toAddHom := { toFun := f, map_add' := (_ : ∀ (x y : M₂), AddHom.toFun src.toAddHom (x + y) = AddHom.toFun src.toAddHom x + AddHom.toFun src.toAddHom y) }, map_smul' := (_ : ∀ (r : S) (x : M₂), AddHom.toFun src.toAddHom (r • x) = ↑σ' r • AddHom.toFun src.toAddHom x) }, invFun := ↑e, left_inv := (_ : Function.LeftInverse src.invFun src.toFun), right_inv := (_ : Function.RightInverse src.invFun src.toFun) }

source

@[simp]

theorem LinearEquiv.coe_symm_mk {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [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 : ∀ (r : R) (x : M), AddHom.toFun { toFun := to_fun, map_add' := map_add } (r • x) = ↑(RingHom.id R) r • AddHom.toFun { toFun := to_fun, map_add' := map_add } x} {left_inv : Function.LeftInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} {right_inv : Function.RightInverse inv_fun { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }.toAddHom.toFun} :

↑(LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := to_fun, map_add' := map_add }, map_smul' := map_smul }, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }) = inv_fun

source

theorem LinearEquiv.bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.surjective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

theorem LinearEquiv.image_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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 = ↑(LinearEquiv.symm e) ⁻¹' s

source

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

↑(LinearEquiv.symm e) '' s = ↑e ⁻¹' s

source

@[simp]

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

↑(RingEquiv.toSemilinearEquiv f) a = ↑f a

source

@[simp]

theorem RingEquiv.toSemilinearEquiv_symm_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) :

∀ (a : S), ↑(LinearEquiv.symm (RingEquiv.toSemilinearEquiv f)) a = Equiv.invFun f.toEquiv a

source

def RingEquiv.toSemilinearEquiv {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R ≃+* S) :

R ≃ₛₗ[↑f] S

Interpret a RingEquiv f as an f-semilinear equiv.

Equations

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

Instances For

source

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

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

Instances For

source

@[simp]

theorem LinearEquiv.coe_ofInvolutive {R : Type u_1} {M : Type u_7} [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

source

@[simp]

theorem LinearEquiv.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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

source

@[simp]

theorem LinearEquiv.restrictScalars_symm_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.symm (LinearEquiv.restrictScalars R f)) a = ↑(LinearEquiv.symm f) a

source

def LinearEquiv.restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [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.