mathlib documentation

data.equiv.module

(Semi)linear equivalences #

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.

@[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₂
@[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.add_monoid_hom_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 σ' σ] :
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
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) :
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₂) :
@[nolint]
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)
@[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.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
@[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_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₂] (f : M ≃ₗ[R] M₂) :
@[simp]
theorem linear_equiv.symm_trans_self {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₂] (f : M ≃ₗ[R] M₂) :
@[simp, norm_cast]
theorem linear_equiv.refl_to_linear_map {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :
@[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
@[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_sum {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} {ι : Type u_15} [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 : finset ι} (u : ι → M) :
e (∑ (i : ι) in s, u i) = ∑ (i : ι) in s, e (u i)
@[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 linear_equiv.image_smul_setₛₗ {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) (s : set M) :
e '' (c s) = σ c e '' s
@[simp]
theorem linear_equiv.preimage_smul_setₛₗ {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 : S) (s : set M₂) :
e ⁻¹' (c s) = σ' c e ⁻¹' s
@[simp]
theorem linear_equiv.image_smul_set {R₁ : Type u_2} {M₁ : Type u_8} {N₁ : Type u_11} [semiring R₁] [add_comm_monoid M₁] [add_comm_monoid N₁] {module_M₁ : module R₁ M₁} {module_N₁ : module R₁ N₁} (e : M₁ ≃ₗ[R₁] N₁) (c : R₁) (s : set M₁) :
e '' (c s) = c e '' s
@[simp]
theorem linear_equiv.preimage_smul_set {R₁ : Type u_2} {M₁ : Type u_8} {N₁ : Type u_11} [semiring R₁] [add_comm_monoid M₁] [add_comm_monoid N₁] {module_M₁ : module R₁ M₁} {module_N₁ : module R₁ N₁} (e : M₁ ≃ₗ[R₁] N₁) (c : R₁) (s : set N₁) :
e ⁻¹' (c s) = c 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
def linear_equiv.automorphism_group.to_linear_map_monoid_hom {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid 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
@[protected, instance]
def linear_equiv.apply_distrib_mul_action {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :

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]
def linear_equiv.apply_has_faithful_scalar {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :

linear_equiv.apply_distrib_mul_action is faithful.

@[protected, instance]
def linear_equiv.apply_smul_comm_class {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R M] :
@[protected, instance]
def linear_equiv.apply_smul_comm_class' {R : Type u_1} {M : Type u_7} [semiring R] [add_comm_monoid M] [module R 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]
theorem distrib_mul_action.to_linear_equiv_symm_apply (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) (ᾰ : M) :
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]
theorem distrib_mul_action.to_linear_equiv_apply (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) (ᾰ : M) :
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
@[simp]
theorem distrib_mul_action.to_module_aut_apply (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) :