mathlib3 documentation

algebra.module.equiv

(Semi)linear equivalences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

Implementation notes #

To ensure that composition works smoothly for semilinear equivalences, we use the typeclasses ring_hom_comp_triple, ring_hom_inv_pair and ring_hom_surjective from algebra/ring/comp_typeclasses.

The group structure on automorphisms, linear_equiv.automorphism_group, is provided elsewhere.

TODO #

Tags #

linear equiv, linear equivalences, linear isomorphism, linear isomorphic

@[nolint]
structure linear_equiv {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] (σ : R →+* S) {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : Type u_18) (M₂ : Type u_19) [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_18 u_19)

A linear equivalence is an invertible linear map.

Instances for linear_equiv
@[nolint]
def linear_equiv.to_add_equiv {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M : Type u_18} {M₂ : Type u_19} [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] (self : M ≃ₛₗ[σ] M₂) :
M ≃+ M₂
@[nolint]
def linear_equiv.to_linear_map {R : Type u_16} {S : Type u_17} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M : Type u_18} {M₂ : Type u_19} [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] (self : M ≃ₛₗ[σ] M₂) :
M →ₛₗ[σ] M₂
@[class]
structure semilinear_equiv_class (F : Type u_16) {R : out_param (Type u_17)} {S : out_param (Type u_18)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_19)) (M₂ : out_param (Type u_20)) [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] :
Type (max u_16 u_19 u_20)

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

See also linear_equiv_class 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 of this typeclass
Instances of other typeclasses for semilinear_equiv_class
  • semilinear_equiv_class.has_sizeof_inst
@[nolint, instance]
def semilinear_equiv_class.to_add_equiv_class (F : Type u_16) {R : out_param (Type u_17)} {S : out_param (Type u_18)} [semiring R] [semiring S] (σ : out_param (R →+* S)) {σ' : out_param (S →+* R)} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] (M : out_param (Type u_19)) (M₂ : out_param (Type u_20)) [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] [self : semilinear_equiv_class F σ M M₂] :
@[reducible]
def linear_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (M : out_param (Type u_3)) (M₂ : out_param (Type u_4)) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] :
Type (max u_1 u_3 u_4)

linear_equiv_class F R M M₂ asserts F is a type of bundled R-linear equivs M → M₂. This is an abbreviation for semilinear_equiv_class F (ring_hom.id R) M M₂.

@[protected, nolint, instance]
def semilinear_equiv_class.semilinear_map_class {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} (F : Type u_16) [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] [s : semilinear_equiv_class F σ M M₂] :
Equations
@[protected, instance]
def linear_equiv.linear_map.has_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
has_coe (M ≃ₛₗ[σ] M₂) (M →ₛₗ[σ] M₂)
Equations
@[protected, instance]
def linear_equiv.has_coe_to_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
has_coe_to_fun (M ≃ₛₗ[σ] M₂) (λ (_x : M ≃ₛₗ[σ] M₂), M M₂)
Equations
@[simp]
theorem linear_equiv.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {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), to_fun (r x) = σ r to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} :
{to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv} = to_fun
@[nolint]
def linear_equiv.to_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
(M ≃ₛₗ[σ] M₂) M M₂
Equations
theorem linear_equiv.to_equiv_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
@[simp]
theorem linear_equiv.to_equiv_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} :
e₁.to_equiv = e₂.to_equiv e₁ = e₂
theorem linear_equiv.to_linear_map_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
@[simp, norm_cast]
theorem linear_equiv.to_linear_map_inj {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {e₁ e₂ : M ≃ₛₗ[σ] M₂} :
e₁ = e₂ e₁ = e₂
@[protected, instance]
def linear_equiv.semilinear_equiv_class {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
semilinear_equiv_class (M ≃ₛₗ[σ] M₂) σ M M₂
Equations
theorem linear_equiv.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] :
theorem linear_equiv.to_linear_map_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp, norm_cast]
theorem linear_equiv.coe_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_linear_map {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.to_fun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[ext]
theorem linear_equiv.ext {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} (h : (x : M), e x = e' x) :
e = e'
theorem linear_equiv.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} :
e = e' (x : M), e x = e' x
@[protected]
theorem linear_equiv.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} {e : M ≃ₛₗ[σ] M₂} {x x' : M} :
x = x' e x = e x'
@[protected]
theorem linear_equiv.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} {e e' : M ≃ₛₗ[σ] M₂} (h : e = e') (x : M) :
e x = e' x
@[refl]
def linear_equiv.refl (R : Type u_1) (M : Type u_7) [semiring R] [add_comm_monoid M] [module R M] :

The identity map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.refl_apply {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
@[symm]
def linear_equiv.symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
M₂ ≃ₛₗ[σ'] M

Linear equivalences are symmetric.

Equations
def linear_equiv.simps.symm_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] {σ : R →+* S} {σ' : S →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {M : Type u_3} {M₂ : Type u_4} [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂] (e : M ≃ₛₗ[σ] M₂) :
M₂ M

See Note [custom simps projection]

Equations
@[simp]
theorem linear_equiv.inv_fun_eq_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.coe_to_equiv_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[nolint, trans]
def linear_equiv.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid 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₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} [ring_hom_inv_pair σ₁₃ σ₃₁] {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} [ring_hom_inv_pair σ₃₁ σ₁₃] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
M₁ ≃ₛₗ[σ₁₃] M₃

Linear equivalences are transitive.

Equations
@[simp]
theorem linear_equiv.coe_to_add_equiv {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
theorem linear_equiv.to_add_monoid_hom_commutes {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :

The two paths coercion can take to an add_monoid_hom are equivalent

@[simp]
theorem linear_equiv.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid 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₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} [ring_hom_inv_pair σ₁₃ σ₃₁] {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} [ring_hom_inv_pair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₁) :
(e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)
theorem linear_equiv.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid 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₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} [ring_hom_inv_pair σ₁₃ σ₃₁] {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} [ring_hom_inv_pair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃) = e₂₃.comp e₁₂
@[simp]
theorem linear_equiv.apply_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : M₂) :
e ((e.symm) c) = c
@[simp]
theorem linear_equiv.symm_apply_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (b : M) :
(e.symm) (e b) = b
@[simp]
theorem linear_equiv.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid 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₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} [ring_hom_inv_pair σ₁₃ σ₃₁] {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} [ring_hom_inv_pair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} :
(e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm
theorem linear_equiv.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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid 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₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₃ : ring_hom_inv_pair σ₂₃ σ₃₂} [ring_hom_inv_pair σ₁₃ σ₃₁] {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {re₃₂ : ring_hom_inv_pair σ₃₂ σ₂₃} [ring_hom_inv_pair σ₃₁ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃) :
((e₁₂.trans e₂₃).symm) c = (e₁₂.symm) ((e₂₃.symm) c)
@[simp]
theorem linear_equiv.trans_refl {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[simp]
theorem linear_equiv.refl_trans {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
theorem linear_equiv.symm_apply_eq {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
(e.symm) x = y x = e y
theorem linear_equiv.eq_symm_apply {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂} {y : M} :
y = (e.symm) x e y = x
theorem linear_equiv.eq_comp_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : M₂ α) (g : M₁ α) :
f = g (e₁₂.symm) f e₁₂ = g
theorem linear_equiv.comp_symm_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : M₂ α) (g : M₁ α) :
g (e₁₂.symm) = f g = f e₁₂
theorem linear_equiv.eq_symm_comp {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : α M₁) (g : α M₂) :
f = (e₁₂.symm) g e₁₂ f = g
theorem linear_equiv.symm_comp_eq {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_1} (f : α M₁) (g : α M₂) :
(e₁₂.symm) g = f g = e₁₂ f
theorem linear_equiv.eq_comp_to_linear_map_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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ring_hom_comp_triple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
f = g.comp e₁₂.symm.to_linear_map f.comp e₁₂.to_linear_map = g
theorem linear_equiv.comp_to_linear_map_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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {σ₂₁ : R₂ →+* R₁} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ring_hom_comp_triple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃) :
g.comp e₁₂.symm.to_linear_map = f g = f.comp e₁₂.to_linear_map
theorem linear_equiv.eq_to_linear_map_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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ring_hom_comp_triple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
f = e₁₂.symm.to_linear_map.comp g e₁₂.to_linear_map.comp f = g
theorem linear_equiv.to_linear_map_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₃] [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₃] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {module_M₃ : module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} [ring_hom_comp_triple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ →ₛₗ[σ₃₂] M₂) :
e₁₂.symm.to_linear_map.comp g = f g = e₁₂.to_linear_map.comp f
@[simp]
theorem linear_equiv.refl_symm {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem linear_equiv.self_trans_symm {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
@[simp]
theorem linear_equiv.symm_trans_self {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [semiring R₁] [semiring R₂] [add_comm_monoid M₁] [add_comm_monoid M₂] {module_M₁ : module R₁ M₁} {module_M₂ : module R₂ M₂} {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : ring_hom_inv_pair σ₁₂ σ₂₁} {re₂₁ : ring_hom_inv_pair σ₂₁ σ₁₂} (f : M₁ ≃ₛₗ[σ₁₂] M₂) :
@[simp, norm_cast]
@[simp, norm_cast]
theorem linear_equiv.comp_coe {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M] [module R M₂] [module R M₃] (f : M ≃ₗ[R] M₂) (f' : M₂ ≃ₗ[R] M₃) :
f'.comp f = (f.trans f')
@[simp]
theorem linear_equiv.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (h₁ : (x y : M), e (x + y) = e x + e y) (h₂ : (r : R) (x : M), e (r x) = σ r e x) (f : M₂ M) (h₃ : function.left_inverse f e) (h₄ : function.right_inverse f e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄} = e
@[protected]
theorem linear_equiv.map_add {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a b : M) :
e (a + b) = e a + e b
@[protected]
theorem linear_equiv.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
e 0 = 0
@[protected, simp]
theorem linear_equiv.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : R) (x : M) :
e (c x) = σ c e x
theorem linear_equiv.map_smul {R₁ : Type u_2} {N₁ : Type u_11} {N₂ : Type u_12} [semiring R₁] [add_comm_monoid N₁] [add_comm_monoid 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
@[simp]
theorem linear_equiv.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x = 0 x = 0
theorem linear_equiv.map_ne_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M} :
e x 0 x 0
@[simp]
theorem linear_equiv.symm_symm {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
e.symm.symm = e
theorem linear_equiv.symm_bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {σ : R →+* S} {σ' : S →+* R} [module R M] [module S M₂] [ring_hom_inv_pair σ' σ] [ring_hom_inv_pair σ σ'] :
@[simp]
theorem linear_equiv.mk_coe' {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ M) (h₁ : (x y : M₂), f (x + y) = f x + f y) (h₂ : (r : S) (x : M₂), f (r x) = σ' r f x) (h₃ : function.left_inverse e f) (h₄ : function.right_inverse e f) :
{to_fun := f, map_add' := h₁, map_smul' := h₂, inv_fun := e, left_inv := h₃, right_inv := h₄} = e.symm
@[simp]
theorem linear_equiv.symm_mk {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (f : M₂ M) (h₁ : (x y : M), e (x + y) = e x + e y) (h₂ : (r : R) (x : M), e (r x) = σ r e x) (h₃ : function.left_inverse f e) (h₄ : function.right_inverse f e) :
{to_fun := e, map_add' := h₁, map_smul' := h₂, inv_fun := f, left_inv := h₃, right_inv := h₄}.symm = {to_fun := f, map_add' := _, map_smul' := _, inv_fun := e, left_inv := _, right_inv := _}
@[simp]
theorem linear_equiv.coe_symm_mk {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M] [add_comm_monoid 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), to_fun (r x) = (ring_hom.id R) r to_fun x} {left_inv : function.left_inverse inv_fun to_fun} {right_inv : function.right_inverse inv_fun to_fun} :
({to_fun := to_fun, map_add' := map_add, map_smul' := map_smul, inv_fun := inv_fun, left_inv := left_inv, right_inv := right_inv}.symm) = inv_fun
@[protected]
theorem linear_equiv.bijective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.injective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.surjective {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) :
@[protected]
theorem linear_equiv.image_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : set M) :
e '' s = (e.symm) ⁻¹' s
@[protected]
theorem linear_equiv.image_symm_eq_preimage {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] {module_M : module R M} {module_S_M₂ : module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : ring_hom_inv_pair σ σ'} {re₂ : ring_hom_inv_pair σ' σ} (e : M ≃ₛₗ[σ] M₂) (s : set M₂) :
(e.symm) '' s = e ⁻¹' s
@[simp]
theorem ring_equiv.to_semilinear_equiv_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) (ᾰ : R) :
def ring_equiv.to_semilinear_equiv {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) :

Interpret a ring_equiv f as an f-semilinear equiv.

Equations
@[simp]
theorem ring_equiv.to_semilinear_equiv_symm_apply {R : Type u_1} {S : Type u_6} [semiring R] [semiring S] (f : R ≃+* S) (ᾰ : S) :
def linear_equiv.of_involutive {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] {σ σ' : R →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {module_M : module R M} (f : M →ₛₗ[σ] M) (hf : function.involutive f) :

An involutive linear map is a linear equivalence.

Equations
@[simp]
theorem linear_equiv.coe_of_involutive {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] {σ σ' : R →+* R} [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] {module_M : module R M} (f : M →ₛₗ[σ] M) (hf : function.involutive f) :
def linear_equiv.restrict_scalars (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul 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 linear_map.restrict_scalars.

Equations
@[simp]
theorem linear_equiv.restrict_scalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f : M ≃ₗ[S] M₂) (ᾰ : M) :
@[simp]
theorem linear_equiv.restrict_scalars_symm_apply (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f : M ≃ₗ[S] M₂) (ᾰ : M₂) :
theorem linear_equiv.restrict_scalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] :
@[simp]
theorem linear_equiv.restrict_scalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [semiring R] [semiring S] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [module S M] [module S M₂] [linear_map.compatible_smul M M₂ R S] (f g : M ≃ₗ[S] M₂) :
@[protected, instance]
def linear_equiv.automorphism_group {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :
Equations

Restriction from R-linear automorphisms of M to R-linear endomorphisms of M, promoted to a monoid hom.

Equations
@[protected, instance]

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

This generalizes function.End.apply_mul_action.

Equations
@[protected, simp]
theorem linear_equiv.smul_def {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] (f : M ≃ₗ[R] M) (a : M) :
f a = f a
@[protected, instance]

linear_equiv.apply_distrib_mul_action is faithful.

@[protected, instance]
@[protected, instance]
@[simp]
theorem linear_equiv.of_subsingleton_symm_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [subsingleton M] [subsingleton M₂] (_x : M₂) :
def linear_equiv.of_subsingleton {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [subsingleton M] [subsingleton M₂] :
M ≃ₗ[R] M₂

Any two modules that are subsingletons are isomorphic.

Equations
@[simp]
theorem linear_equiv.of_subsingleton_apply {R : Type u_1} (M : Type u_7) (M₂ : Type u_9) [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] [subsingleton M] [subsingleton M₂] (_x : M) :
@[simp]
theorem module.comp_hom.to_linear_equiv_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) (ᾰ : R) :
def module.comp_hom.to_linear_equiv {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) :

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

Equations
@[simp]
theorem module.comp_hom.to_linear_equiv_symm_apply {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (g : R ≃+* S) (ᾰ : S) :
@[simp]
def distrib_mul_action.to_linear_equiv (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [add_comm_monoid M] [module R M] [group S] [distrib_mul_action S M] [smul_comm_class S R M] (s : S) :

Each element of the group defines a linear equivalence.

This is a stronger version of distrib_mul_action.to_add_equiv.

Equations
@[simp]
def distrib_mul_action.to_module_aut (R : Type u_1) {S : Type u_6} (M : Type u_7) [semiring R] [add_comm_monoid M] [module R M] [group S] [distrib_mul_action S M] [smul_comm_class S R M] :
S →* M ≃ₗ[R] M

Each element of the group defines a module automorphism.

This is a stronger version of distrib_mul_action.to_add_aut.

Equations
def add_equiv.to_linear_equiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M] [add_comm_monoid 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
@[simp]
theorem add_equiv.coe_to_linear_equiv {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃+ M₂) (h : (c : R) (x : M), e (c x) = c e x) :
@[simp]
theorem add_equiv.coe_to_linear_equiv_symm {R : Type u_1} {M : Type u_7} {M₂ : Type u_9} [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R M₂] (e : M ≃+ M₂) (h : (c : R) (x : M), e (c x) = c e x) :
def add_equiv.to_nat_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M] [add_comm_monoid M₂] (e : M ≃+ M₂) :

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

Equations
@[simp]
theorem add_equiv.coe_to_nat_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_monoid M] [add_comm_monoid M₂] (e : M ≃+ M₂) :
@[simp]
theorem add_equiv.to_nat_linear_equiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :
def add_equiv.to_int_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M] [add_comm_group M₂] (e : M ≃+ M₂) :

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

Equations
@[simp]
theorem add_equiv.coe_to_int_linear_equiv {M : Type u_7} {M₂ : Type u_9} [add_comm_group M] [add_comm_group M₂] (e : M ≃+ M₂) :
@[simp]
@[simp]
theorem add_equiv.to_int_linear_equiv_trans {M : Type u_7} {M₂ : Type u_9} {M₃ : Type u_10} [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] (e : M ≃+ M₂) (e₂ : M₂ ≃+ M₃) :