(Semi)linear maps #
In this file we define
-
linear_map σ M M₂,M →ₛₗ[σ] M₂: a semilinear map between twomodules. Here,σis aring_homfromRtoR₂and anf : M →ₛₗ[σ] M₂satisfiesf (c • x) = (σ c) • (f x). We recover plain linear maps by choosingσto bering_hom.id R. This is denoted byM →ₗ[R] M₂. We also add the notationM →ₗ⋆[R] M₂for star-linear maps. -
is_linear_map R f: predicate saying thatf : M → M₂is a linear map. (Note that this was not generalized to semilinear maps.)
We then provide linear_map with the following instances:
linear_map.add_comm_monoidandlinear_map.add_comm_group: the elementwise addition structures corresponding to addition in the codomainlinear_map.distrib_mul_actionandlinear_map.module: the elementwise scalar action structures corresponding to applying the action in the codomain.module.End.semiringandmodule.End.ring: the (semi)ring of endomorphisms formed by taking the additive structure above with composition as multiplication.
Implementation notes #
To ensure that composition works smoothly for semilinear maps, we use the typeclasses
ring_hom_comp_triple, ring_hom_inv_pair and ring_hom_surjective from
algebra/ring/comp_typeclasses.
Notation #
- Throughout the file, we denote regular linear maps by
fₗ,gₗ, etc, and semilinear maps byf,g, etc.
TODO #
- Parts of this file have not yet been generalized to semilinear maps (i.e.
compatible_smul)
Tags #
linear map
structure
is_linear_map
(R : Type u)
{M : Type v}
{M₂ : Type w}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M → M₂) :
Prop
A map f between modules over a semiring is linear if it satisfies the two properties
f (x + y) = f x + f y and f (c • x) = c • f x. The predicate is_linear_map R f asserts this
property. A bundled version is available with linear_map, and should be favored over
is_linear_map most of the time.
structure
linear_map
{R : Type u_17}
{S : Type u_18}
[semiring R]
[semiring S]
(σ : R →+* S)
(M : Type u_19)
(M₂ : Type u_20)
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module S M₂] :
Type (max u_19 u_20)
- 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
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. Elements of linear_map σ M M₂ (available under the notation
M →ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which
σ = ring_hom.id R), the notation M →ₗ[R] M₂ is available. An unbundled version of plain linear
maps is available with the predicate is_linear_map, but it should be avoided most of the time.
def
linear_map.to_add_hom
{R : Type u_17}
{S : Type u_18}
[semiring R]
[semiring S]
{σ : R →+* S}
{M : Type u_19}
{M₂ : Type u_20}
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module S M₂]
(self : M →ₛₗ[σ] M₂) :
add_hom M M₂
The add_hom underlying a linear_map.
@[protected, instance]
def
linear_map.add_monoid_hom_class
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S} :
add_monoid_hom_class (M →ₛₗ[σ] M₃) M M₃
Equations
- linear_map.add_monoid_hom_class = {coe := linear_map.to_fun _inst_12, coe_injective' := _, map_add := _, map_zero := _}
def
linear_map.to_distrib_mul_action_hom
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂) :
The distrib_mul_action_hom underlying a linear_map.
@[protected, instance]
def
linear_map.has_coe_to_fun
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S} :
has_coe_to_fun (M →ₛₗ[σ] M₃) (λ (_x : M →ₛₗ[σ] M₃), M → M₃)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
- linear_map.has_coe_to_fun = {coe := linear_map.to_fun _inst_12}
@[simp]
theorem
linear_map.to_fun_eq_coe
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
{f : M →ₛₗ[σ] M₃} :
@[ext]
theorem
linear_map.ext
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
{f g : M →ₛₗ[σ] M₃}
(h : ∀ (x : M), ⇑f x = ⇑g x) :
f = g
@[protected]
def
linear_map.copy
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃)
(f' : M → M₃)
(h : f' = ⇑f) :
Copy of a linear_map with a new to_fun equal to the old one. Useful to fix definitional
equalities.
@[simp]
theorem
linear_map.coe_mk
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M → M₃)
(h₁ : ∀ (x y : M), f (x + y) = f x + f y)
(h₂ : ∀ (r : R) (x : M), f (r • x) = ⇑σ r • f x) :
Identity map as a linear_map
theorem
linear_map.id_apply
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
⇑linear_map.id x = x
@[simp, norm_cast]
theorem
linear_map.id_coe
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
linear_map.is_linear
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(fₗ : M →ₗ[R] M₂) :
is_linear_map R ⇑fₗ
theorem
linear_map.coe_injective
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S} :
@[protected]
theorem
linear_map.congr_arg
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
{f : M →ₛₗ[σ] M₃}
{x x' : M} :
@[protected]
theorem
linear_map.congr_fun
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
{f g : M →ₛₗ[σ] M₃}
(h : f = g)
(x : M) :
If two linear maps are equal, they are equal at each point.
@[simp]
theorem
linear_map.mk_coe
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃)
(h₁ : ∀ (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y)
(h₂ : ∀ (r : R) (x : M), ⇑f (r • x) = ⇑σ r • ⇑f x) :
theorem
linear_map.map_smul
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(fₗ : M →ₗ[R] M₂)
(c : R)
(x : M) :
theorem
linear_map.map_smul_inv
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃)
{σ' : S →+* R}
[ring_hom_inv_pair σ σ']
(c : S)
(x : M) :
@[protected]
theorem
linear_map.map_zero
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃) :
@[simp]
theorem
linear_map.map_eq_zero_iff
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃)
(h : function.injective ⇑f)
{x : M} :
@[class]
structure
linear_map.compatible_smul
(M : Type u_9)
(M₂ : Type u_11)
[add_comm_monoid M]
[add_comm_monoid M₂]
(R : Type u_17)
(S : Type u_18)
[semiring S]
[has_scalar R M]
[module S M]
[has_scalar R M₂]
[module S M₂] :
Type
A typeclass for has_scalar structures which can be moved through a linear_map.
This typeclass is generated automatically from a is_scalar_tower instance, but exists so that
we can also add an instance for add_comm_group.int_module, allowing z • to be moved even if
R does not support negation.
@[protected, instance]
def
linear_map.is_scalar_tower.compatible_smul
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid M₂]
{R : Type u_1}
{S : Type u_2}
[semiring S]
[has_scalar R S]
[has_scalar R M]
[module S M]
[is_scalar_tower R S M]
[has_scalar R M₂]
[module S M₂]
[is_scalar_tower R S M₂] :
linear_map.compatible_smul M M₂ R S
Equations
@[simp]
theorem
linear_map.map_smul_of_tower
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid M₂]
{R : Type u_1}
{S : Type u_2}
[semiring S]
[has_scalar R M]
[module S M]
[has_scalar R M₂]
[module S M₂]
[linear_map.compatible_smul M M₂ R S]
(fₗ : M →ₗ[S] M₂)
(c : R)
(x : M) :
def
linear_map.to_add_monoid_hom
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃) :
M →+ M₃
convert a linear map to an additive map
@[simp]
theorem
linear_map.to_add_monoid_hom_coe
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃) :
⇑(f.to_add_monoid_hom) = ⇑f
def
linear_map.restrict_scalars
(R : Type u_1)
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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-modules and S-modules and R-module structures
are defined by an action of R on S (formally, we have two scalar towers), then any S-linear
map from M to M₂ is R-linear.
See also linear_map.map_smul_of_tower.
@[simp]
theorem
linear_map.coe_restrict_scalars
(R : Type u_1)
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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₂) :
⇑(linear_map.restrict_scalars R fₗ) = ⇑fₗ
theorem
linear_map.restrict_scalars_apply
(R : Type u_1)
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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₂)
(x : M) :
⇑(linear_map.restrict_scalars R fₗ) x = ⇑fₗ x
theorem
linear_map.restrict_scalars_injective
(R : Type u_1)
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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_map.restrict_scalars_inj
(R : Type u_1)
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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_map.restrict_scalars R fₗ = linear_map.restrict_scalars R gₗ ↔ fₗ = gₗ
@[simp]
theorem
linear_map.map_sum
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S}
(f : M →ₛₗ[σ] M₃)
{ι : Type u_2}
{t : finset ι}
{g : ι → M} :
theorem
linear_map.to_add_monoid_hom_injective
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₃ : Type u_12}
[semiring R]
[semiring S]
[add_comm_monoid M]
[add_comm_monoid M₃]
[module R M]
[module S M₃]
{σ : R →+* S} :
@[simp]
theorem
ring_hom.to_semilinear_map_apply
{R : Type u_1}
{S : Type u_6}
[semiring R]
[semiring S]
(f : R →+* S)
(ᾰ : R) :
⇑(f.to_semilinear_map) ᾰ = ⇑f ᾰ
def
linear_map.comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M₁ : Type u_10}
{M₂ : Type u_11}
{M₃ : Type u_12}
[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₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M₂ →ₛₗ[σ₂₃] M₃)
(g : M₁ →ₛₗ[σ₁₂] M₂) :
Composition of two linear maps is a linear map
theorem
linear_map.comp_apply
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M₁ : Type u_10}
{M₂ : Type u_11}
{M₃ : Type u_12}
[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₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M₂ →ₛₗ[σ₂₃] M₃)
(g : M₁ →ₛₗ[σ₁₂] M₂)
(x : M₁) :
@[simp, norm_cast]
theorem
linear_map.coe_comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M₁ : Type u_10}
{M₂ : Type u_11}
{M₃ : Type u_12}
[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₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M₂ →ₛₗ[σ₂₃] M₃)
(g : M₁ →ₛₗ[σ₁₂] M₂) :
@[simp]
theorem
linear_map.comp_id
{R₂ : Type u_3}
{R₃ : Type u_4}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₂]
[semiring R₃]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
{module_M₂ : module R₂ M₂}
{module_M₃ : module R₃ M₃}
{σ₂₃ : R₂ →+* R₃}
(f : M₂ →ₛₗ[σ₂₃] M₃) :
f.comp linear_map.id = f
@[simp]
theorem
linear_map.id_comp
{R₂ : Type u_3}
{R₃ : Type u_4}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₂]
[semiring R₃]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
{module_M₂ : module R₂ M₂}
{module_M₃ : module R₃ M₃}
{σ₂₃ : R₂ →+* R₃}
(f : M₂ →ₛₗ[σ₂₃] M₃) :
linear_map.id.comp f = f
def
linear_map.inverse
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[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 σ σ']
(f : M →ₛₗ[σ] M₂)
(g : M₂ → M)
(h₁ : function.left_inverse g ⇑f)
(h₂ : function.right_inverse g ⇑f) :
If a function g is a left and right inverse of a linear map f, then g is linear itself.
@[protected, instance]
def
linear_map.compatible_smul.int_module
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[add_comm_group M₂]
{S : Type u_1}
[semiring S]
[module S M]
[module S M₂] :
linear_map.compatible_smul M M₂ ℤ S
Equations
@[protected, instance]
def
linear_map.compatible_smul.units
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[add_comm_group M₂]
{R : Type u_1}
{S : Type u_2}
[monoid R]
[mul_action R M]
[mul_action R M₂]
[semiring S]
[module S M]
[module S M₂]
[linear_map.compatible_smul M M₂ R S] :
linear_map.compatible_smul M M₂ Rˣ S
Equations
@[simp]
theorem
module.comp_hom.to_linear_map_apply
{R : Type u_1}
{S : Type u_2}
[semiring R]
[semiring S]
(g : R →+* S)
(ᾰ : R) :
⇑(module.comp_hom.to_linear_map g) ᾰ = ⇑g ᾰ
def
module.comp_hom.to_linear_map
{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 .
def
distrib_mul_action_hom.to_linear_map
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(fₗ : M →+[R] M₂) :
A distrib_mul_action_hom between two modules is a linear map.
@[protected, instance]
def
distrib_mul_action_hom.linear_map.has_coe
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂] :
Equations
@[simp]
theorem
distrib_mul_action_hom.to_linear_map_eq_coe
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →+[R] M₂) :
f.to_linear_map = ↑f
@[simp, norm_cast]
theorem
distrib_mul_action_hom.coe_to_linear_map
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M →+[R] M₂) :
theorem
distrib_mul_action_hom.to_linear_map_injective
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f g : M →+[R] M₂}
(h : ↑f = ↑g) :
f = g
def
is_linear_map.mk'
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
(f : M → M₂)
(H : is_linear_map R f) :
Convert an is_linear_map predicate to a linear_map
@[simp]
theorem
is_linear_map.mk'_apply
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f : M → M₂}
(H : is_linear_map R f)
(x : M) :
⇑(is_linear_map.mk' f H) x = f x
theorem
is_linear_map.is_linear_map_smul
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(c : R) :
is_linear_map R (λ (z : M), c • z)
theorem
is_linear_map.is_linear_map_smul'
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
(a : M) :
is_linear_map R (λ (c : R), c • a)
theorem
is_linear_map.map_zero
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R M₂]
{f : M → M₂}
(lin : is_linear_map R f) :
f 0 = 0
theorem
is_linear_map.is_linear_map_neg
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_group M]
[module R M] :
is_linear_map R (λ (z : M), -z)
theorem
is_linear_map.map_neg
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
{f : M → M₂}
(lin : is_linear_map R f)
(x : M) :
theorem
is_linear_map.map_sub
{R : Type u_1}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
{f : M → M₂}
(lin : is_linear_map R f)
(x y : M) :
Linear endomorphisms of a module, with associated ring structure
module.End.semiring and algebra structure module.End.algebra.
def
add_monoid_hom.to_nat_linear_map
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid M₂]
(f : M →+ M₂) :
Reinterpret an additive homomorphism as a ℕ-linear map.
theorem
add_monoid_hom.to_nat_linear_map_injective
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_monoid M]
[add_comm_monoid M₂] :
def
add_monoid_hom.to_int_linear_map
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[add_comm_group M₂]
(f : M →+ M₂) :
Reinterpret an additive homomorphism as a ℤ-linear map.
theorem
add_monoid_hom.to_int_linear_map_injective
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[add_comm_group M₂] :
@[simp]
theorem
add_monoid_hom.coe_to_int_linear_map
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[add_comm_group M₂]
(f : M →+ M₂) :
⇑(f.to_int_linear_map) = ⇑f
def
add_monoid_hom.to_rat_linear_map
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[module ℚ M]
[add_comm_group M₂]
[module ℚ M₂]
(f : M →+ M₂) :
Reinterpret an additive homomorphism as a ℚ-linear map.
theorem
add_monoid_hom.to_rat_linear_map_injective
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[module ℚ M]
[add_comm_group M₂]
[module ℚ M₂] :
@[simp]
theorem
add_monoid_hom.coe_to_rat_linear_map
{M : Type u_9}
{M₂ : Type u_11}
[add_comm_group M]
[module ℚ M]
[add_comm_group M₂]
[module ℚ M₂]
(f : M →+ M₂) :
⇑(f.to_rat_linear_map) = ⇑f
@[protected, instance]
def
linear_map.has_scalar
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂] :
has_scalar S (M →ₛₗ[σ₁₂] M₂)
@[simp]
theorem
linear_map.smul_apply
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂]
(a : S)
(f : M →ₛₗ[σ₁₂] M₂)
(x : M) :
theorem
linear_map.coe_smul
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂]
(a : S)
(f : M →ₛₗ[σ₁₂] M₂) :
@[protected, instance]
def
linear_map.smul_comm_class
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{T : Type u_8}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂]
[monoid T]
[distrib_mul_action T M₂]
[smul_comm_class R₂ T M₂]
[smul_comm_class S T M₂] :
smul_comm_class S T (M →ₛₗ[σ₁₂] M₂)
@[protected, instance]
def
linear_map.is_scalar_tower
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{T : Type u_8}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂]
[monoid T]
[distrib_mul_action T M₂]
[smul_comm_class R₂ T M₂]
[has_scalar S T]
[is_scalar_tower S T M₂] :
is_scalar_tower S T (M →ₛₗ[σ₁₂] M₂)
@[protected, instance]
def
linear_map.is_central_scalar
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂]
[distrib_mul_action Sᵐᵒᵖ M₂]
[smul_comm_class R₂ Sᵐᵒᵖ M₂]
[is_central_scalar S M₂] :
is_central_scalar S (M →ₛₗ[σ₁₂] M₂)
Arithmetic on the codomain #
@[protected, instance]
def
linear_map.has_zero
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} :
The constant 0 map is linear.
@[simp]
theorem
linear_map.zero_apply
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂}
(x : M) :
@[simp]
theorem
linear_map.comp_zero
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(g : M₂ →ₛₗ[σ₂₃] M₃) :
@[simp]
theorem
linear_map.zero_comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂) :
@[protected, instance]
def
linear_map.inhabited
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} :
Equations
- linear_map.inhabited = {default := 0}
@[simp]
theorem
linear_map.default_def
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} :
@[protected, instance]
def
linear_map.has_add
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} :
The sum of two linear maps is linear.
theorem
linear_map.add_comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g h : M₂ →ₛₗ[σ₂₃] M₃) :
theorem
linear_map.comp_add
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f g : M →ₛₗ[σ₁₂] M₂)
(h : M₂ →ₛₗ[σ₂₃] M₃) :
@[protected, instance]
def
linear_map.add_comm_monoid
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R₁ M]
[module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} :
add_comm_monoid (M →ₛₗ[σ₁₂] M₂)
The type of linear maps is an additive monoid.
Equations
- linear_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn linear_map.add_comm_monoid._proof_2 linear_map.add_comm_monoid._proof_3 linear_map.add_comm_monoid._proof_4 linear_map.add_comm_monoid._proof_5
@[protected, instance]
def
linear_map.has_neg
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{N₂ : Type u_14}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_group N₂]
[module R₁ M]
[module R₂ N₂]
{σ₁₂ : R₁ →+* R₂} :
The negation of a linear map is linear.
@[simp]
theorem
linear_map.neg_comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{N₃ : Type u_15}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_group N₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ N₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g : M₂ →ₛₗ[σ₂₃] N₃) :
@[simp]
theorem
linear_map.comp_neg
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{N₂ : Type u_14}
{N₃ : Type u_15}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_group N₂]
[add_comm_group N₃]
[module R₁ M]
[module R₂ N₂]
[module R₃ N₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] N₂)
(g : N₂ →ₛₗ[σ₂₃] N₃) :
@[protected, instance]
def
linear_map.has_sub
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{N₂ : Type u_14}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_group N₂]
[module R₁ M]
[module R₂ N₂]
{σ₁₂ : R₁ →+* R₂} :
The negation of a linear map is linear.
theorem
linear_map.sub_comp
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{M₂ : Type u_11}
{N₃ : Type u_15}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_group N₃]
[module R₁ M]
[module R₂ M₂]
[module R₃ N₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f : M →ₛₗ[σ₁₂] M₂)
(g h : M₂ →ₛₗ[σ₂₃] N₃) :
theorem
linear_map.comp_sub
{R₁ : Type u_2}
{R₂ : Type u_3}
{R₃ : Type u_4}
{M : Type u_9}
{N₂ : Type u_14}
{N₃ : Type u_15}
[semiring R₁]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_group N₂]
[add_comm_group N₃]
[module R₁ M]
[module R₂ N₂]
[module R₃ N₃]
{σ₁₂ : R₁ →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R₁ →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
(f g : M →ₛₗ[σ₁₂] N₂)
(h : N₂ →ₛₗ[σ₂₃] N₃) :
@[protected, instance]
def
linear_map.add_comm_group
{R₁ : Type u_2}
{R₂ : Type u_3}
{M : Type u_9}
{N₂ : Type u_14}
[semiring R₁]
[semiring R₂]
[add_comm_monoid M]
[add_comm_group N₂]
[module R₁ M]
[module R₂ N₂]
{σ₁₂ : R₁ →+* R₂} :
add_comm_group (M →ₛₗ[σ₁₂] N₂)
The type of linear maps is an additive group.
Equations
- linear_map.add_comm_group = function.injective.add_comm_group coe_fn linear_map.add_comm_group._proof_3 linear_map.add_comm_group._proof_4 linear_map.add_comm_group._proof_5 linear_map.add_comm_group._proof_6 linear_map.add_comm_group._proof_7 linear_map.add_comm_group._proof_8 linear_map.add_comm_group._proof_9
@[protected, instance]
def
linear_map.distrib_mul_action
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[monoid S]
[distrib_mul_action S M₂]
[smul_comm_class R₂ S M₂] :
distrib_mul_action S (M →ₛₗ[σ₁₂] M₂)
Equations
- linear_map.distrib_mul_action = {to_mul_action := {to_has_scalar := linear_map.has_scalar _inst_13, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
theorem
linear_map.smul_comp
{R : Type u_1}
{R₂ : Type u_3}
{R₃ : Type u_4}
{S₃ : Type u_7}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R]
[semiring R₂]
[semiring R₃]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{σ₁₂ : R →+* R₂}
{σ₂₃ : R₂ →+* R₃}
{σ₁₃ : R →+* R₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[monoid S₃]
[distrib_mul_action S₃ M₃]
[smul_comm_class R₃ S₃ M₃]
(a : S₃)
(g : M₂ →ₛₗ[σ₂₃] M₃)
(f : M →ₛₗ[σ₁₂] M₂) :
theorem
linear_map.comp_smul
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
{M₃ : Type u_12}
[semiring R]
[add_comm_monoid M]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M]
[monoid S]
[distrib_mul_action S M₂]
[module R M₂]
[module R M₃]
[smul_comm_class R S M₂]
[distrib_mul_action S M₃]
[smul_comm_class R S M₃]
[linear_map.compatible_smul M₃ M₂ S R]
(g : M₃ →ₗ[R] M₂)
(a : S)
(f : M →ₗ[R] M₃) :
@[protected, instance]
def
linear_map.module
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[semiring S]
[module S M₂]
[smul_comm_class R₂ S M₂] :
Equations
- linear_map.module = {to_distrib_mul_action := linear_map.distrib_mul_action _inst_13, add_smul := _, zero_smul := _}
@[protected, instance]
def
linear_map.no_zero_smul_divisors
{R : Type u_1}
{R₂ : Type u_3}
{S : Type u_6}
{M : Type u_9}
{M₂ : Type u_11}
[semiring R]
[semiring R₂]
[add_comm_monoid M]
[add_comm_monoid M₂]
[module R M]
[module R₂ M₂]
{σ₁₂ : R →+* R₂}
[semiring S]
[module S M₂]
[smul_comm_class R₂ S M₂]
[no_zero_smul_divisors S M₂] :
no_zero_smul_divisors S (M →ₛₗ[σ₁₂] M₂)
Monoid structure of endomorphisms #
Lemmas about pow such as linear_map.pow_apply appear in later files.
@[protected, instance]
def
linear_map.module.End.has_one
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_one (module.End R M)
Equations
- linear_map.module.End.has_one = {one := linear_map.id _inst_4}
@[protected, instance]
def
linear_map.module.End.has_mul
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_mul (module.End R M)
Equations
- linear_map.module.End.has_mul = {mul := linear_map.comp linear_map.module.End.has_mul._proof_1}
theorem
linear_map.one_eq_id
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
linear_map.mul_eq_comp
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f g : module.End R M) :
f * g = linear_map.comp f g
@[simp]
theorem
linear_map.one_apply
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(x : M) :
@[simp]
theorem
linear_map.mul_apply
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f g : module.End R M)
(x : M) :
theorem
linear_map.coe_one
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
linear_map.coe_mul
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f g : module.End R M) :
@[protected, instance]
def
module.End.monoid
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
monoid (module.End R M)
Equations
- module.End.monoid = {mul := has_mul.mul linear_map.module.End.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (module.End R M)), npow_zero' := _, npow_succ' := _}
@[protected, instance]
def
module.End.semiring
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
semiring (module.End R M)
Equations
- module.End.semiring = {add := has_add.add linear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul linear_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul linear_map.module.End.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul linear_map.module.End.has_mul}, npow_zero' := _, npow_succ' := _}
@[protected, instance]
def
module.End.ring
{R : Type u_1}
{N₁ : Type u_13}
[semiring R]
[add_comm_group N₁]
[module R N₁] :
ring (module.End R N₁)
Equations
- module.End.ring = {add := semiring.add module.End.semiring, add_assoc := _, zero := semiring.zero module.End.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul module.End.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg linear_map.add_comm_group, sub := add_comm_group.sub linear_map.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul linear_map.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul module.End.semiring, mul_assoc := _, one := semiring.one module.End.semiring, one_mul := _, mul_one := _, npow := semiring.npow module.End.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
def
module.End.is_scalar_tower
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class R S M] :
is_scalar_tower S (module.End R M) (module.End R M)
@[protected, instance]
def
module.End.smul_comm_class
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class R S M]
[has_scalar S R]
[is_scalar_tower S R M] :
smul_comm_class S (module.End R M) (module.End R M)
@[protected, instance]
def
module.End.smul_comm_class'
{R : Type u_1}
{S : Type u_6}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class R S M]
[has_scalar S R]
[is_scalar_tower S R M] :
smul_comm_class (module.End R M) S (module.End R M)
Action by a module endomorphism. #
@[protected, instance]
def
linear_map.apply_module
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
module (module.End R M) M
The tautological action by module.End R M (aka M →ₗ[R] M) on M.
This generalizes function.End.apply_mul_action.
Equations
- linear_map.apply_module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (_x : module.End R M) (_y : M), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[protected, simp]
theorem
linear_map.smul_def
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M]
(f : module.End R M)
(a : M) :
@[protected, instance]
def
linear_map.apply_has_faithful_scalar
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
has_faithful_scalar (module.End R M) M
linear_map.apply_module is faithful.
@[protected, instance]
def
linear_map.apply_smul_comm_class
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
smul_comm_class R (module.End R M) M
@[protected, instance]
def
linear_map.apply_smul_comm_class'
{R : Type u_1}
{M : Type u_9}
[semiring R]
[add_comm_monoid M]
[module R M] :
smul_comm_class (module.End R M) R M
@[protected, instance]
def
linear_map.apply_is_scalar_tower
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
is_scalar_tower R (module.End R M) M
Actions as module endomorphisms #
@[simp]
theorem
distrib_mul_action.to_linear_map_apply
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class S R M]
(s : S)
(ᾰ : M) :
⇑(distrib_mul_action.to_linear_map R M s) ᾰ = s • ᾰ
def
distrib_mul_action.to_linear_map
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class S R M]
(s : S) :
Each element of the monoid defines a linear map.
This is a stronger version of distrib_mul_action.to_add_monoid_hom.
Equations
- distrib_mul_action.to_linear_map R M s = {to_fun := has_scalar.smul s, map_add' := _, map_smul' := _}
def
distrib_mul_action.to_module_End
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class S R M] :
S →* module.End R M
Each element of the monoid defines a module endomorphism.
This is a stronger version of distrib_mul_action.to_add_monoid_End.
Equations
- distrib_mul_action.to_module_End R M = {to_fun := distrib_mul_action.to_linear_map R M _inst_6, map_one' := _, map_mul' := _}
@[simp]
theorem
distrib_mul_action.to_module_End_apply
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[monoid S]
[distrib_mul_action S M]
[smul_comm_class S R M]
(s : S) :
def
module.to_module_End
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring S]
[module S M]
[smul_comm_class S R M] :
S →+* module.End R M
Each element of the monoid defines a module endomorphism.
This is a stronger version of distrib_mul_action.to_module_End.
Equations
- module.to_module_End R M = {to_fun := distrib_mul_action.to_linear_map R M _inst_6, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
module.to_module_End_apply
(R : Type u_1)
{S : Type u_6}
(M : Type u_9)
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring S]
[module S M]
[smul_comm_class S R M]
(s : S) :
⇑(module.to_module_End R M) s = distrib_mul_action.to_linear_map R M s