From 118e809b5f4ed450c6f9660b9778c548fb9be3f6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 30 Sep 2021 16:11:19 +0000 Subject: [PATCH] refactor(algebra/module/linear_map): Move elementwise structure from linear_algebra/basic (#9331) This helps reduce the size of linear_algebra/basic, and by virtue of being a smaller file makes it easier to spot typeclasses which can be relaxed. As an example, `linear_map.endomorphism_ring` now requires only `semiring R` not `ring R`. Having instances available as early as possible is generally good, as otherwise it is hard to even state things elsewhere. --- src/algebra/module/linear_map.lean | 270 ++++++++++++++++++++++++++++- src/linear_algebra/basic.lean | 238 ------------------------- 2 files changed, 268 insertions(+), 240 deletions(-) diff --git a/src/algebra/module/linear_map.lean b/src/algebra/module/linear_map.lean index 39a74aa300b22..d52ff8e5e1cef 100644 --- a/src/algebra/module/linear_map.lean +++ b/src/algebra/module/linear_map.lean @@ -6,6 +6,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne -/ import algebra.group.hom import algebra.module.basic +import algebra.module.pi import algebra.group_action_hom import algebra.ring.comp_typeclasses @@ -22,6 +23,15 @@ In this file we define * `is_linear_map R f` : predicate saying that `f : 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_monoid` and `linear_map.add_comm_group`: the elementwise addition structures + corresponding to addition in the codomain +* `linear_map.distrib_mul_action` and `linear_map.module`: the elementwise scalar action structures + corresponding to applying the action in the codomain. +* `module.End.semiring` and `module.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 @@ -47,8 +57,9 @@ open_locale big_operators universes u u' v w x y z variables {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} -variables {k : Type*} {S : Type*} {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} -variables {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {N₄ : Type*} {ι : Type*} +variables {k : Type*} {S : Type*} {T : Type*} +variables {M : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} +variables {N₁ : Type*} {N₂ : Type*} {N₃ : Type*} {ι : Type*} /-- 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 @@ -458,3 +469,258 @@ by { intros f g h, ext, exact linear_map.congr_fun h x } @[simp] lemma add_monoid_hom.coe_to_rat_linear_map [add_comm_group M] [module ℚ M] [add_comm_group M₂] [module ℚ M₂] (f : M →+ M₂) : ⇑f.to_rat_linear_map = f := rfl + +namespace linear_map + +/-! ### Arithmetic on the codomain -/ +section arithmetic + +variables [semiring R₁] [semiring R₂] [semiring R₃] +variables [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] +variables [add_comm_group N₁] [add_comm_group N₂] [add_comm_group N₃] +variables [module R₁ M] [module R₂ M₂] [module R₃ M₃] +variables [module R₁ N₁] [module R₂ N₂] [module R₃ N₃] +variables {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] + +/-- The constant 0 map is linear. -/ +instance : has_zero (M →ₛₗ[σ₁₂] M₂) := +⟨{ to_fun := 0, map_add' := by simp, map_smul' := by simp }⟩ + +@[simp] lemma zero_apply (x : M) : (0 : M →ₛₗ[σ₁₂] M₂) x = 0 := rfl + +@[simp] theorem comp_zero (g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 := +ext $ assume c, by rw [comp_apply, zero_apply, zero_apply, g.map_zero] + +@[simp] theorem zero_comp (f : M →ₛₗ[σ₁₂] M₂) : ((0 : M₂ →ₛₗ[σ₂₃] M₃).comp f : M →ₛₗ[σ₁₃] M₃) = 0 := +rfl + +instance : inhabited (M →ₛₗ[σ₁₂] M₂) := ⟨0⟩ + +@[simp] lemma default_def : default (M →ₛₗ[σ₁₂] M₂) = 0 := rfl + +/-- The sum of two linear maps is linear. -/ +instance : has_add (M →ₛₗ[σ₁₂] M₂) := +⟨λ f g, { to_fun := f + g, + map_add' := by simp [add_comm, add_left_comm], map_smul' := by simp [smul_add] }⟩ + +@[simp] lemma add_apply (f g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x := rfl + +lemma add_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) : + ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f := rfl + +lemma comp_add (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : + (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g := +ext $ λ _, h.map_add _ _ + +/-- The type of linear maps is an additive monoid. -/ +instance : add_comm_monoid (M →ₛₗ[σ₁₂] M₂) := +{ zero := 0, + add := (+), + add_assoc := λ f g h, linear_map.ext $ λ x, add_assoc _ _ _, + zero_add := λ f, linear_map.ext $ λ x, zero_add _, + add_zero := λ f, linear_map.ext $ λ x, add_zero _, + add_comm := λ f g, linear_map.ext $ λ x, add_comm _ _, + nsmul := λ n f, + { to_fun := λ x, n • (f x), + map_add' := λ x y, by rw [f.map_add, smul_add], + map_smul' := λ c x, + begin + rw [f.map_smulₛₗ], + simp [smul_comm n (σ₁₂ c) (f x)], + end }, + nsmul_zero' := λ f, linear_map.ext $ λ x, add_comm_monoid.nsmul_zero' _, + nsmul_succ' := λ n f, linear_map.ext $ λ x, add_comm_monoid.nsmul_succ' _ _ } + +/-- The negation of a linear map is linear. -/ +instance : has_neg (M →ₛₗ[σ₁₂] N₂) := +⟨λ f, { to_fun := -f, map_add' := by simp [add_comm], map_smul' := by simp }⟩ + +@[simp] lemma neg_apply (f : M →ₛₗ[σ₁₂] N₂) (x : M) : (- f) x = - f x := rfl + +include σ₁₃ +@[simp] lemma neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (- g).comp f = - g.comp f := rfl + +@[simp] lemma comp_neg (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (- f) = - g.comp f := +ext $ λ _, g.map_neg _ +omit σ₁₃ + +/-- The negation of a linear map is linear. -/ +instance : has_sub (M →ₛₗ[σ₁₂] N₂) := +⟨λ f g, { to_fun := f - g, + map_add' := λ x y, by simp only [pi.sub_apply, map_add, add_sub_comm], + map_smul' := λ r x, by simp [pi.sub_apply, map_smul, smul_sub] }⟩ + +@[simp] lemma sub_apply (f g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x := rfl + +include σ₁₃ +lemma sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) : + (g - h).comp f = g.comp f - h.comp f := rfl + +lemma comp_sub (f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : + h.comp (g - f) = h.comp g - h.comp f := +ext $ λ _, h.map_sub _ _ +omit σ₁₃ + +/-- The type of linear maps is an additive group. -/ +instance : add_comm_group (M →ₛₗ[σ₁₂] N₂) := +{ zero := 0, + add := (+), + neg := has_neg.neg, + sub := has_sub.sub, + sub_eq_add_neg := λ f g, linear_map.ext $ λ m, sub_eq_add_neg _ _, + add_left_neg := λ f, linear_map.ext $ λ m, add_left_neg _, + nsmul := λ n f, { + to_fun := λ x, n • (f x), + map_add' := λ x y, by rw [f.map_add, smul_add], + map_smul' := λ c x, by rw [f.map_smulₛₗ, smul_comm n (σ₁₂ c) (f x)] }, + gsmul := λ n f, { + to_fun := λ x, n • (f x), + map_add' := λ x y, by rw [f.map_add, smul_add], + map_smul' := λ c x, by rw [f.map_smulₛₗ, smul_comm n (σ₁₂ c) (f x)] }, + gsmul_zero' := λ a, linear_map.ext $ λ m, zero_smul _ _, + gsmul_succ' := λ n a, linear_map.ext $ λ m, add_comm_group.gsmul_succ' n _, + gsmul_neg' := λ n a, linear_map.ext $ λ m, add_comm_group.gsmul_neg' n _, + .. linear_map.add_comm_monoid } + +end arithmetic + +-- TODO: generalize this section to semilinear maps where possible +section actions + +variables [semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] +variables [module R M] [module R M₂] [module R M₃] + +section has_scalar +variables [monoid S] [distrib_mul_action S M₂] [smul_comm_class R S M₂] +variables [monoid T] [distrib_mul_action T M₂] [smul_comm_class R T M₂] + +instance : has_scalar S (M →ₗ[R] M₂) := +⟨λ a f, { to_fun := a • f, + map_add' := λ x y, by simp only [pi.smul_apply, f.map_add, smul_add], + map_smul' := λ c x, by simp [pi.smul_apply, f.map_smul, smul_comm c] }⟩ + +@[simp] lemma smul_apply (a : S) (f : M →ₗ[R] M₂) (x : M) : (a • f) x = a • f x := rfl + +instance [smul_comm_class S T M₂] : smul_comm_class S T (M →ₗ[R] M₂) := +⟨λ a b f, ext $ λ x, smul_comm _ _ _⟩ + +-- example application of this instance: if S -> T -> R are homomorphisms of commutative rings and +-- M and M₂ are R-modules then the S-module and T-module structures on Hom_R(M,M₂) are compatible. +instance [has_scalar S T] [is_scalar_tower S T M₂] : is_scalar_tower S T (M →ₗ[R] M₂) := +{ smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ } + +instance : distrib_mul_action S (M →ₗ[R] M₂) := +{ one_smul := λ f, ext $ λ _, one_smul _ _, + mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _, + smul_add := λ c f g, ext $ λ x, smul_add _ _ _, + smul_zero := λ c, ext $ λ x, smul_zero _ } + +theorem smul_comp (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] M₃) : (a • g).comp f = a • (g.comp f) := +rfl + +theorem comp_smul [distrib_mul_action S M₃] [smul_comm_class R S M₃] [compatible_smul M₃ M₂ S R] + (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • (g.comp f) := +ext $ λ x, g.map_smul_of_tower _ _ + +end has_scalar + +section module +variables [semiring S] [module S M₂] [smul_comm_class R S M₂] + +instance : module S (M →ₗ[R] M₂) := +{ add_smul := λ a b f, ext $ λ x, add_smul _ _ _, + zero_smul := λ f, ext $ λ x, zero_smul _ _ } + +end module + +end actions + +/-! +### Monoid structure of endomorphisms + +Lemmas about `pow` such as `linear_map.pow_apply` appear in later files. +-/ +section endomorphisms + +variables [semiring R] [add_comm_monoid M] [add_comm_group N₁] [module R M] [module R N₁] + +instance : has_one (module.End R M) := ⟨linear_map.id⟩ +instance : has_mul (module.End R M) := ⟨linear_map.comp⟩ + +lemma one_eq_id : (1 : module.End R M) = id := rfl +lemma mul_eq_comp (f g : module.End R M) : f * g = f.comp g := rfl + +@[simp] lemma one_apply (x : M) : (1 : module.End R M) x = x := rfl +@[simp] lemma mul_apply (f g : module.End R M) (x : M) : (f * g) x = f (g x) := rfl + +lemma coe_one : ⇑(1 : module.End R M) = _root_.id := rfl +lemma coe_mul (f g : module.End R M) : ⇑(f * g) = f ∘ g := rfl + +instance _root_.module.End.monoid : monoid (module.End R M) := +{ mul := (*), + one := (1 : M →ₗ[R] M), + mul_assoc := λ f g h, linear_map.ext $ λ x, rfl, + mul_one := comp_id, + one_mul := id_comp } + +instance _root_.module.End.semiring : semiring (module.End R M) := +{ mul := (*), + one := (1 : M →ₗ[R] M), + zero := 0, + add := (+), + npow := @npow_rec _ ⟨1⟩ ⟨(*)⟩, + mul_zero := comp_zero, + zero_mul := zero_comp, + left_distrib := λ f g h, comp_add _ _ _, + right_distrib := λ f g h, add_comp _ _ _, + .. _root_.module.End.monoid, + .. linear_map.add_comm_monoid } + +instance _root_.module.End.ring : ring (module.End R N₁) := +{ ..module.End.semiring, ..linear_map.add_comm_group } + +section +variables [monoid S] [distrib_mul_action S M] [smul_comm_class R S M] + +instance _root_.module.End.is_scalar_tower : + is_scalar_tower S (module.End R M) (module.End R M) := ⟨smul_comp⟩ + +instance _root_.module.End.smul_comm_class [has_scalar S R] [is_scalar_tower S R M] : + smul_comm_class S (module.End R M) (module.End R M) := +⟨λ s _ _, (comp_smul _ s _).symm⟩ + +instance _root_.module.End.smul_comm_class' [has_scalar S R] [is_scalar_tower S R M] : + smul_comm_class (module.End R M) S (module.End R M) := +smul_comm_class.symm _ _ _ + +end + +/-! ### Action by a module endomorphism. -/ + +/-- The tautological action by `module.End R M` (aka `M →ₗ[R] M`) on `M`. + +This generalizes `function.End.apply_mul_action`. -/ +instance apply_module : module (module.End R M) M := +{ smul := ($), + smul_zero := linear_map.map_zero, + smul_add := linear_map.map_add, + add_smul := linear_map.add_apply, + zero_smul := (linear_map.zero_apply : ∀ m, (0 : M →ₗ[R] M) m = 0), + one_smul := λ _, rfl, + mul_smul := λ _ _ _, rfl } + +@[simp] protected lemma smul_def (f : module.End R M) (a : M) : f • a = f a := rfl + +/-- `linear_map.apply_module` is faithful. -/ +instance apply_has_faithful_scalar : has_faithful_scalar (module.End R M) M := +⟨λ _ _, linear_map.ext⟩ + +instance apply_smul_comm_class : smul_comm_class R (module.End R M) M := +{ smul_comm := λ r e m, (e.map_smul r m).symm } + +instance apply_smul_comm_class' : smul_comm_class (module.End R M) R M := +{ smul_comm := linear_map.map_smul } + +end endomorphisms + +end linear_map diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 73fd41a958d14..321f82dd127f6 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -194,16 +194,6 @@ lemma restrict_eq_dom_restrict_cod_restrict {f : M →ₗ[R] M} {p : submodule R M} (hf : ∀ x, f x ∈ p) : f.restrict (λ x _, hf x) = (f.cod_restrict p hf).dom_restrict p := rfl -/-- The constant 0 map is linear. -/ -instance : has_zero (M →ₛₗ[σ₁₂] M₂) := -⟨{ to_fun := 0, map_add' := by simp, map_smul' := by simp }⟩ - -instance : inhabited (M →ₛₗ[σ₁₂] M₂) := ⟨0⟩ - -@[simp] lemma zero_apply (x : M) : (0 : M →ₛₗ[σ₁₂] M₂) x = 0 := rfl - -@[simp] lemma default_def : default (M →ₛₗ[σ₁₂] M₂) = 0 := rfl - instance unique_of_left [subsingleton M] : unique (M →ₛₗ[σ₁₂] M₂) := { uniq := λ f, ext $ λ x, by rw [subsingleton.elim x 0, map_zero, map_zero], .. linear_map.inhabited } @@ -211,45 +201,12 @@ instance unique_of_left [subsingleton M] : unique (M →ₛₗ[σ₁₂] M₂) : instance unique_of_right [subsingleton M₂] : unique (M →ₛₗ[σ₁₂] M₂) := coe_injective.unique -/-- The sum of two linear maps is linear. -/ -instance : has_add (M →ₛₗ[σ₁₂] M₂) := -⟨λ f g, { to_fun := f + g, - map_add' := by simp [add_comm, add_left_comm], map_smul' := by simp [smul_add] }⟩ - -@[simp] lemma add_apply (g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x := rfl - -/-- The type of linear maps is an additive monoid. -/ -instance : add_comm_monoid (M →ₛₗ[σ₁₂] M₂) := -{ zero := 0, - add := (+), - add_assoc := λ f g h, linear_map.ext $ λ x, add_assoc _ _ _, - zero_add := λ f, linear_map.ext $ λ x, zero_add _, - add_zero := λ f, linear_map.ext $ λ x, add_zero _, - add_comm := λ f g, linear_map.ext $ λ x, add_comm _ _, - nsmul := λ n f, - { to_fun := λ x, n • (f x), - map_add' := λ x y, by rw [f.map_add, smul_add], - map_smul' := λ c x, - begin - rw [f.map_smulₛₗ], - simp [smul_comm n (σ₁₂ c) (f x)], - end }, - nsmul_zero' := λ f, linear_map.ext $ λ x, add_comm_monoid.nsmul_zero' _, - nsmul_succ' := λ n f, linear_map.ext $ λ x, add_comm_monoid.nsmul_succ' _ _ } - /-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `add_monoid_hom`. -/ def eval_add_monoid_hom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂ := { to_fun := λ f, f a, map_add' := λ f g, linear_map.add_apply f g a, map_zero' := rfl } -lemma add_comp (f : M →ₛₗ[σ₁₂] M₂)(g h : M₂ →ₛₗ[σ₂₃] M₃) : - ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f := rfl - -lemma comp_add (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : - (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g := -ext $ λ _, h.map_add _ _ - /-- `linear_map.to_add_monoid_hom` promoted to an `add_monoid_hom` -/ def to_add_monoid_hom' : (M →ₛₗ[σ₁₂] M₂) →+ (M →+ M₂) := { to_fun := to_add_monoid_hom, @@ -278,37 +235,16 @@ theorem smul_right_apply (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : end smul_right -instance : has_one (M →ₗ[R] M) := ⟨linear_map.id⟩ -instance : has_mul (M →ₗ[R] M) := ⟨linear_map.comp⟩ - -lemma one_eq_id : (1 : M →ₗ[R] M) = id := rfl -lemma mul_eq_comp (f g : M →ₗ[R] M) : f * g = f.comp g := rfl - -@[simp] lemma one_apply (x : M) : (1 : M →ₗ[R] M) x = x := rfl -@[simp] lemma mul_apply (f g : M →ₗ[R] M) (x : M) : (f * g) x = f (g x) := rfl - -lemma coe_one : ⇑(1 : M →ₗ[R] M) = _root_.id := rfl -lemma coe_mul (f g : M →ₗ[R] M) : ⇑(f * g) = f ∘ g := rfl - instance [nontrivial M] : nontrivial (module.End R M) := begin obtain ⟨m, ne⟩ := (nontrivial_iff_exists_ne (0 : M)).mp infer_instance, exact nontrivial_of_ne 1 0 (λ p, ne (linear_map.congr_fun p m)), end -@[simp] theorem comp_zero : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 := -ext $ assume c, by rw [comp_apply, zero_apply, zero_apply, g.map_zero] - -@[simp] theorem zero_comp : ((0 : M₂ →ₛₗ[σ₂₃] M₃).comp f : M →ₛₗ[σ₁₃] M₃) = 0 := rfl - @[simp, norm_cast] lemma coe_fn_sum {ι : Type*} (t : finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) : ⇑(∑ i in t, f i) = ∑ i in t, (f i : M → M₂) := add_monoid_hom.map_sum ⟨@to_fun R R₂ _ _ σ₁₂ M M₂ _ _ _ _, rfl, λ x y, rfl⟩ _ _ -instance _root_.module.End.monoid : monoid (module.End R M) := -by refine_struct { mul := (*), one := (1 : M →ₗ[R] M), npow := @npow_rec _ ⟨1⟩ ⟨(*)⟩ }; -intros; try { refl }; apply linear_map.ext; simp {proj := ff} - @[simp] lemma pow_apply (f : M →ₗ[R] M) (n : ℕ) (m : M) : (f^n) m = (f^[n] m) := begin @@ -400,124 +336,6 @@ end end add_comm_monoid -section add_comm_group - -variables [semiring R] [semiring R₂] [semiring R₃] [semiring R₄] - [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_group M₃] [add_comm_group M₄] - [module R M] [module R₂ M₂] [module R₃ M₃] [module R₄ M₄] - {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₃₄ : R₃ →+* R₄} {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} - [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] - [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄] - -/-- The negation of a linear map is linear. -/ -instance : has_neg (M →ₛₗ[σ₁₃] M₃) := -⟨λ f, { to_fun := -f, map_add' := by simp [add_comm], map_smul' := by simp }⟩ - -@[simp] lemma neg_apply (f : M →ₛₗ[σ₁₃] M₃) (x : M) : (- f) x = - f x := rfl - -include σ₁₃ -@[simp] lemma neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) : (- g).comp f = - g.comp f := rfl -omit σ₁₃ - -include σ₁₄ -@[simp] lemma comp_neg (f : M →ₛₗ[σ₁₃] M₃) (g : M₃ →ₛₗ[σ₃₄] M₄) : g.comp (- f) = - g.comp f := -ext $ λ _, g.map_neg _ -omit σ₁₄ - -/-- The negation of a linear map is linear. -/ -instance : has_sub (M →ₛₗ[σ₁₃] M₃) := -⟨λ f g, { to_fun := f - g, - map_add' := λ x y, by simp only [pi.sub_apply, map_add, add_sub_comm], - map_smul' := λ r x, by simp [pi.sub_apply, map_smul, smul_sub] }⟩ - -@[simp] lemma sub_apply (f g : M →ₛₗ[σ₁₃] M₃) (x : M) : (f - g) x = f x - g x := rfl - -include σ₁₃ -lemma sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) : - (g - h).comp f = g.comp f - h.comp f := rfl -omit σ₁₃ - -include σ₁₄ -lemma comp_sub (f g : M →ₛₗ[σ₁₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) : - h.comp (g - f) = h.comp g - h.comp f := by { ext, simp } -omit σ₁₄ - -/-- The type of linear maps is an additive group. -/ -instance : add_comm_group (M →ₛₗ[σ₁₃] M₃) := -{ zero := 0, - add := (+), - neg := has_neg.neg, - sub := has_sub.sub, - sub_eq_add_neg := λ f g, linear_map.ext $ λ m, sub_eq_add_neg _ _, - add_left_neg := λ f, linear_map.ext $ λ m, add_left_neg _, - nsmul := λ n f, { - to_fun := λ x, n • (f x), - map_add' := λ x y, by rw [f.map_add, smul_add], - map_smul' := λ c x, by rw [f.map_smulₛₗ, smul_comm n (σ₁₃ c) (f x)] }, - gsmul := λ n f, { - to_fun := λ x, n • (f x), - map_add' := λ x y, by rw [f.map_add, smul_add], - map_smul' := λ c x, by rw [f.map_smulₛₗ, smul_comm n (σ₁₃ c) (f x)] }, - gsmul_zero' := λ a, linear_map.ext $ λ m, zero_smul _ _, - gsmul_succ' := λ n a, linear_map.ext $ λ m, add_comm_group.gsmul_succ' n _, - gsmul_neg' := λ n a, linear_map.ext $ λ m, add_comm_group.gsmul_neg' n _, - .. linear_map.add_comm_monoid } - -end add_comm_group - -section has_scalar -variables {S : Type*} [semiring R] [monoid S] - [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] - [module R M] [module R M₂] [module R M₃] - [distrib_mul_action S M₂] [smul_comm_class R S M₂] - (f : M →ₗ[R] M₂) - -instance : has_scalar S (M →ₗ[R] M₂) := -⟨λ a f, { to_fun := a • f, - map_add' := λ x y, by simp only [pi.smul_apply, f.map_add, smul_add], - map_smul' := λ c x, by simp [pi.smul_apply, f.map_smul, smul_comm c] }⟩ - -@[simp] lemma smul_apply (a : S) (x : M) : (a • f) x = a • f x := rfl - -instance {T : Type*} [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 →ₗ[R] M₂) := -⟨λ a b f, ext $ λ x, smul_comm _ _ _⟩ - --- example application of this instance: if S -> T -> R are homomorphisms of commutative rings and --- M and M₂ are R-modules then the S-module and T-module structures on Hom_R(M,M₂) are compatible. -instance {T : Type*} [monoid T] [has_scalar S T] [distrib_mul_action T M₂] [smul_comm_class R T M₂] - [is_scalar_tower S T M₂] : - is_scalar_tower S T (M →ₗ[R] M₂) := -{ smul_assoc := λ _ _ _, ext $ λ _, smul_assoc _ _ _ } - -instance : distrib_mul_action S (M →ₗ[R] M₂) := -{ one_smul := λ f, ext $ λ _, one_smul _ _, - mul_smul := λ c c' f, ext $ λ _, mul_smul _ _ _, - smul_add := λ c f g, ext $ λ x, smul_add _ _ _, - smul_zero := λ c, ext $ λ x, smul_zero _ } - -theorem smul_comp (a : S) (g : M₃ →ₗ[R] M₂) (f : M →ₗ[R] M₃) : (a • g).comp f = a • (g.comp f) := -rfl - -instance _root_.module.End.is_scalar_tower : - is_scalar_tower S (module.End R M₂) (module.End R M₂) := ⟨smul_comp⟩ - -theorem comp_smul [distrib_mul_action S M₃] [smul_comm_class R S M₃] [compatible_smul M₂ M₃ S R] - (g : M₂ →ₗ[R] M₃) (a : S) : - g.comp (a • f) = a • (g.comp f) := -ext $ λ _, g.map_smul_of_tower _ _ - -instance _root_.module.End.smul_comm_class [has_scalar S R] [is_scalar_tower S R M₂] : - smul_comm_class S (module.End R M₂) (module.End R M₂) := -⟨λ s _ _, (comp_smul _ _ s).symm⟩ - -instance _root_.module.End.smul_comm_class' [has_scalar S R] [is_scalar_tower S R M₂] : - smul_comm_class (module.End R M₂) S (module.End R M₂) := -smul_comm_class.symm _ _ _ - -end has_scalar - section module variables {S : Type*} [semiring R] [semiring S] @@ -526,10 +344,6 @@ variables {S : Type*} [semiring R] [semiring S] [module S M₂] [module S M₃] [smul_comm_class R S M₂] [smul_comm_class R S M₃] (f : M →ₗ[R] M₂) -instance : module S (M →ₗ[R] M₂) := -{ add_smul := λ a b f, ext $ λ x, add_smul _ _ _, - zero_smul := λ f, ext $ λ x, zero_smul _ _ } - variable (S) /-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`. @@ -604,58 +418,6 @@ def dom_restrict' end comm_semiring -section semiring - -variables [semiring R] [add_comm_monoid M] [module R M] - -instance _root_.module.End.semiring : semiring (module.End R M) := -{ mul := (*), - one := (1 : M →ₗ[R] M), - zero := 0, - add := (+), - npow := @npow_rec _ ⟨1⟩ ⟨(*)⟩, - mul_zero := comp_zero, - zero_mul := zero_comp, - left_distrib := λ f g h, comp_add _ _ _, - right_distrib := λ f g h, add_comp _ _ _, - .. _root_.module.End.monoid, - .. linear_map.add_comm_monoid } - -/-- The tautological action by `M →ₗ[R] M` on `M`. - -This generalizes `function.End.apply_mul_action`. -/ -instance apply_module : module (M →ₗ[R] M) M := -{ smul := ($), - smul_zero := linear_map.map_zero, - smul_add := linear_map.map_add, - add_smul := linear_map.add_apply, - zero_smul := (linear_map.zero_apply : ∀ m, (0 : M →ₗ[R] M) m = 0), - one_smul := λ _, rfl, - mul_smul := λ _ _ _, rfl } - -@[simp] protected lemma smul_def (f : M →ₗ[R] M) (a : M) : f • a = f a := rfl - -/-- `linear_map.apply_module` is faithful. -/ -instance apply_has_faithful_scalar : has_faithful_scalar (M →ₗ[R] M) M := -⟨λ _ _, linear_map.ext⟩ - -instance apply_smul_comm_class : smul_comm_class R (M →ₗ[R] M) M := -{ smul_comm := λ r e m, (e.map_smul r m).symm } - -instance apply_smul_comm_class' : smul_comm_class (M →ₗ[R] M) R M := -{ smul_comm := linear_map.map_smul } - -end semiring - -section ring - -variables [ring R] [add_comm_group M] [module R M] - -instance _root_.module.End.ring : ring (module.End R M) := -{ ..module.End.semiring, ..linear_map.add_comm_group } - -end ring - section comm_ring variables [comm_ring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] variables [module R M] [module R M₂] [module R M₃]