(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
linear_equiv σ M M₂,M ≃ₛₗ[σ] M₂: an invertible semilinear map. Here,σis aring_homfromRtoR₂and ane : M ≃ₛₗ[σ] M₂satisfiese (c • x) = (σ c) • (e x). The plain linear version, withσbeingring_hom.id R, is denoted byM ≃ₗ[R] M₂, and the star-linear version (withσbeingstar_ring_end) is denoted byM ≃ₗ⋆[R] M₂.
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 #
- Parts of this file have not yet been generalized to semilinear maps
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)
- to_fun : M → M₂
- map_add' : ∀ (x y : M), self.to_fun (x + y) = self.to_fun x + self.to_fun y
- map_smul' : ∀ (r : R) (x : M), self.to_fun (r • x) = ⇑σ r • self.to_fun x
- inv_fun : M₂ → M
- left_inv : function.left_inverse self.inv_fun self.to_fun
- right_inv : function.right_inverse self.inv_fun self.to_fun
A linear equivalence is an invertible linear map.
Instances for linear_equiv
- linear_equiv.has_sizeof_inst
- linear_equiv.linear_map.has_coe
- linear_equiv.has_coe_to_fun
- linear_equiv.semilinear_equiv_class
- linear_equiv.automorphism_group
- linear_equiv.apply_distrib_mul_action
- linear_equiv.apply_has_faithful_smul
- linear_equiv.apply_smul_comm_class
- linear_equiv.apply_smul_comm_class'
- linear_equiv.has_zero
- linear_equiv.unique
- linear_equiv.unique_of_subsingleton
- linear_equiv.can_lift_continuous_linear_equiv
- lie_equiv.has_coe_to_linear_equiv
- lie_module_equiv.has_coe_to_linear_equiv
- quadratic_form.isometry.linear_equiv.has_coe
@[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₂) :
@[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)
- coe : F → M → M₂
- inv : F → M₂ → M
- left_inv : ∀ (e : F), function.left_inverse (semilinear_equiv_class.inv e) (semilinear_equiv_class.coe e)
- right_inv : ∀ (e : F), function.right_inverse (semilinear_equiv_class.inv e) (semilinear_equiv_class.coe e)
- coe_injective' : ∀ (e g : F), semilinear_equiv_class.coe e = semilinear_equiv_class.coe g → semilinear_equiv_class.inv e = semilinear_equiv_class.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
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₂] :
add_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₂] :
semilinear_map_class F σ M M₂
Equations
- semilinear_equiv_class.semilinear_map_class F = {coe := semilinear_equiv_class.coe s, coe_injective' := _, map_add := _, map_smulₛₗ := _}
@[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 σ' σ] :
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 σ' σ] :
Equations
- linear_equiv.has_coe_to_fun = {coe := linear_equiv.to_fun _inst_7}
@[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} :
@[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 σ' σ] :
Equations
- linear_equiv.to_equiv = λ (f : M ≃ₛₗ[σ] M₂), f.to_add_equiv.to_equiv
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₂} :
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₂} :
@[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
- linear_equiv.semilinear_equiv_class = {coe := linear_equiv.to_fun _inst_7, inv := linear_equiv.inv_fun _inst_7, left_inv := _, right_inv := _, coe_injective' := _, map_add := _, map_smulₛₗ := _}
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₂) :
e.to_linear_map = ↑e
@[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₂) :
⇑(e.to_linear_map) = ⇑e
@[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₂} :
@[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} :
@[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) :
@[refl]
The identity map is a linear equivalence.
Equations
- linear_equiv.refl R M = {to_fun := linear_map.id.to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.refl M).inv_fun, left_inv := _, right_inv := _}
@[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) :
⇑(linear_equiv.refl R M) x = x
@[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₂) :
Linear equivalences are symmetric.
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₃) :
Linear equivalences are transitive.
@[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₂) :
⇑(e.to_add_equiv) = ⇑e
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₁) :
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₃} :
@[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₂) :
@[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) :
@[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₃} :
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₃) :
@[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₂) :
e.trans (linear_equiv.refl S M₂) = e
@[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₂) :
(linear_equiv.refl R M).trans e = e
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} :
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} :
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₁ → α) :
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₁ → α) :
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₂) :
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₂) :
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] :
(linear_equiv.refl R M).symm = linear_equiv.refl 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₂) :
f.trans f.symm = linear_equiv.refl R₁ 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₂) :
f.symm.trans f = linear_equiv.refl 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] :
↑(linear_equiv.refl R M) = linear_map.id
@[simp, norm_cast]
@[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) :
@[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) :
@[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₂) :
@[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) :
@[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} :
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} :
@[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₂) :
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) :
@[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) :
@[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} :
@[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) :
@[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₂) :
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.
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.
@[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) :
⇑(linear_equiv.of_involutive f hf) = ⇑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₂) :
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.
@[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) :
⇑(linear_equiv.restrict_scalars R f) ᾰ = ⇑f ᾰ
@[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₂) :
linear_equiv.restrict_scalars R f = linear_equiv.restrict_scalars R g ↔ f = g
@[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
- linear_equiv.automorphism_group = {mul := λ (f g : M ≃ₗ[R] M), g.trans f, mul_assoc := _, one := linear_equiv.refl R M _inst_9, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (linear_equiv.refl R M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7, npow_zero' := _, npow_succ' := _, inv := λ (f : M ≃ₗ[R] M), f.symm, div := div_inv_monoid.div._default (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_10 (linear_equiv.refl R M) linear_equiv.automorphism_group._proof_11 linear_equiv.automorphism_group._proof_12 (div_inv_monoid.npow._default (linear_equiv.refl R M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7) linear_equiv.automorphism_group._proof_13 linear_equiv.automorphism_group._proof_14 (λ (f : M ≃ₗ[R] M), f.symm), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_16 (linear_equiv.refl R M) linear_equiv.automorphism_group._proof_17 linear_equiv.automorphism_group._proof_18 (div_inv_monoid.npow._default (linear_equiv.refl R M) (λ (f g : M ≃ₗ[R] M), g.trans f) linear_equiv.automorphism_group._proof_6 linear_equiv.automorphism_group._proof_7) linear_equiv.automorphism_group._proof_19 linear_equiv.automorphism_group._proof_20 (λ (f : M ≃ₗ[R] M), f.symm), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
linear_equiv.automorphism_group.to_linear_map_monoid_hom_apply
{R : Type u_1}
{M : Type u_7}
[semiring R]
[add_comm_monoid M]
[module R M]
(ᾰ : M ≃ₗ[R] M) :
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] :
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] :
distrib_mul_action (M ≃ₗ[R] M) M
The tautological action by M ≃ₗ[R] M on M.
This generalizes function.End.apply_mul_action.
Equations
- linear_equiv.apply_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := λ (_x : M ≃ₗ[R] M) (_y : M), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[protected, instance]
def
linear_equiv.apply_has_faithful_smul
{R : Type u_1}
{M : Type u_7}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_faithful_smul (M ≃ₗ[R] M) 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] :
smul_comm_class R (M ≃ₗ[R] M) 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] :
smul_comm_class (M ≃ₗ[R] M) R M
@[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₂) :
⇑((linear_equiv.of_subsingleton M M₂).symm) _x = 0
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₂] :
Any two modules that are subsingletons are isomorphic.
@[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) :
⇑(linear_equiv.of_subsingleton M M₂) _x = 0
@[simp]
theorem
linear_equiv.of_subsingleton_self
{R : Type u_1}
(M : Type u_7)
[semiring R]
[add_comm_monoid M]
[module R M]
[subsingleton M] :
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 .
@[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) :
⇑((distrib_mul_action.to_linear_equiv R M s).symm) ᾰ = (distrib_mul_action.to_add_equiv M s).inv_fun ᾰ
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
- distrib_mul_action.to_linear_equiv R M s = {to_fun := (distrib_mul_action.to_add_equiv M s).to_fun, map_add' := _, map_smul' := _, inv_fun := (distrib_mul_action.to_add_equiv M s).inv_fun, left_inv := _, right_inv := _}
@[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) :
⇑(distrib_mul_action.to_linear_equiv R M s) ᾰ = (distrib_mul_action.to_add_equiv M s).to_fun ᾰ
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] :
Each element of the group defines a module automorphism.
This is a stronger version of distrib_mul_action.to_add_aut.
Equations
- distrib_mul_action.to_module_aut R M = {to_fun := distrib_mul_action.to_linear_equiv R M _inst_6, map_one' := _, map_mul' := _}
@[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) :
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) :
An additive equivalence whose underlying function preserves smul is a linear equivalence.
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₂) :
⇑(e.to_nat_linear_equiv) = ⇑e
@[simp]
theorem
add_equiv.to_nat_linear_equiv_to_add_equiv
{M : Type u_7}
{M₂ : Type u_9}
[add_comm_monoid M]
[add_comm_monoid M₂]
(e : M ≃+ M₂) :
@[simp]
theorem
linear_equiv.to_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₂) :
@[simp]
theorem
add_equiv.to_nat_linear_equiv_symm
{M : Type u_7}
{M₂ : Type u_9}
[add_comm_monoid M]
[add_comm_monoid M₂]
(e : M ≃+ M₂) :
@[simp]
@[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₃) :
e.to_nat_linear_equiv.trans e₂.to_nat_linear_equiv = (e.trans e₂).to_nat_linear_equiv
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₂) :
⇑(e.to_int_linear_equiv) = ⇑e
@[simp]
theorem
add_equiv.to_int_linear_equiv_to_add_equiv
{M : Type u_7}
{M₂ : Type u_9}
[add_comm_group M]
[add_comm_group M₂]
(e : M ≃+ M₂) :
@[simp]
theorem
linear_equiv.to_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₂) :
@[simp]
theorem
add_equiv.to_int_linear_equiv_symm
{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₃) :
e.to_int_linear_equiv.trans e₂.to_int_linear_equiv = (e.trans e₂).to_int_linear_equiv