From 2c784466afc13d3d312f1efbe533df6d429b2c06 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Mon, 16 Jan 2023 13:49:25 +0100 Subject: [PATCH 1/9] feat: port Algebra.Module.LinearMap From 6b81eb2b6f54832b5638d14395577523d9a04f0d Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Mon, 16 Jan 2023 13:49:26 +0100 Subject: [PATCH 2/9] Initial file copy from mathport --- Mathlib/Algebra/Module/LinearMap.lean | 1285 +++++++++++++++++++++++++ 1 file changed, 1285 insertions(+) create mode 100644 Mathlib/Algebra/Module/LinearMap.lean diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean new file mode 100644 index 0000000000000..c0ccea93bc6c7 --- /dev/null +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -0,0 +1,1285 @@ +/- +Copyright (c) 2020 Anne Baanen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne Baanen, + Frédéric Dupuis, Heather Macbeth + +! This file was ported from Lean 3 source module algebra.module.linear_map +! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Algebra.Hom.GroupAction +import Mathbin.Algebra.Module.Pi +import Mathbin.Algebra.Star.Basic +import Mathbin.Data.Set.Pointwise.Smul +import Mathbin.Algebra.Ring.CompTypeclasses + +/-! +# (Semi)linear maps + +In this file we define + +* `linear_map σ M M₂`, `M →ₛₗ[σ] M₂` : a semilinear map between two `module`s. Here, + `σ` is a `ring_hom` from `R` to `R₂` and an `f : M →ₛₗ[σ] M₂` satisfies + `f (c • x) = (σ c) • (f x)`. We recover plain linear maps by choosing `σ` to be `ring_hom.id R`. + This is denoted by `M →ₗ[R] M₂`. We also add the notation `M →ₗ⋆[R] M₂` for star-linear maps. + +* `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 +`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 + by `f`, `g`, etc. + +## TODO + +* Parts of this file have not yet been generalized to semilinear maps (i.e. `compatible_smul`) + +## Tags + +linear map +-/ + + +assert_not_exists Submonoid + +assert_not_exists finset + +open Function + +universe u u' v w x y z + +variable {R : Type _} {R₁ : Type _} {R₂ : Type _} {R₃ : Type _} + +variable {k : Type _} {S : Type _} {S₃ : Type _} {T : Type _} + +variable {M : Type _} {M₁ : Type _} {M₂ : Type _} {M₃ : Type _} + +variable {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 +property. A bundled version is available with `linear_map`, and should be favored over +`is_linear_map` most of the time. -/ +structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] + [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) : Prop where + map_add : ∀ x y, f (x + y) = f x + f y + map_smul : ∀ (c : R) (x), f (c • x) = c • f x +#align is_linear_map IsLinearMap + +section + +/-- 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. -/ +structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type _) + (M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends + AddHom M M₂ where + map_smul' : ∀ (r : R) (x : M), to_fun (r • x) = σ r • to_fun x +#align linear_map LinearMap + +/-- The `add_hom` underlying a `linear_map`. -/ +add_decl_doc LinearMap.toAddHom + +-- mathport name: «expr →ₛₗ[ ] » +notation:25 M " →ₛₗ[" σ:25 "] " M₂:0 => LinearMap σ M M₂ + +-- mathport name: «expr →ₗ[ ] » +notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂ + +-- mathport name: «expr →ₗ⋆[ ] » +notation:25 M " →ₗ⋆[" R:25 "] " M₂:0 => LinearMap (starRingEnd R) M M₂ + +/-- `semilinear_map_class F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`. + +See also `linear_map_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`. -/ +class SemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S] + (σ : outParam <| R →+* S) (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂] + [Module R M] [Module S M₂] extends AddHomClass F M M₂ where + map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x +#align semilinear_map_class SemilinearMapClass + +end + +-- `σ` becomes a metavariable but that's fine because it's an `out_param` +attribute [nolint dangerous_instance] SemilinearMapClass.toAddHomClass + +export SemilinearMapClass (map_smulₛₗ) + +attribute [simp] map_smulₛₗ + +/-- `linear_map_class F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`. + +This is an abbreviation for `semilinear_map_class F (ring_hom.id R) M M₂`. +-/ +abbrev LinearMapClass (F : Type _) (R M M₂ : outParam (Type _)) [Semiring R] [AddCommMonoid M] + [AddCommMonoid M₂] [Module R M] [Module R M₂] := + SemilinearMapClass F (RingHom.id R) M M₂ +#align linear_map_class LinearMapClass + +namespace SemilinearMapClass + +variable (F : Type _) + +variable [Semiring R] [Semiring S] + +variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] + +variable [Module R M] [Module R M₂] [Module S M₃] + +variable {σ : R →+* S} + +-- `σ` is an `out_param` so it's not dangerous +@[nolint dangerous_instance] +instance (priority := 100) [SemilinearMapClass F σ M M₃] : AddMonoidHomClass F M M₃ := + { + SemilinearMapClass.toAddHomClass F σ M + M₃ with + coe := fun f => (f : M → M₃) + map_zero := fun f => + show f 0 = 0 by + rw [← zero_smul R (0 : M), map_smulₛₗ] + simp } + +-- `R` is an `out_param` so it's not dangerous +@[nolint dangerous_instance] +instance (priority := 100) [LinearMapClass F R M M₂] : DistribMulActionHomClass F R M M₂ := + { + SemilinearMapClass.addMonoidHomClass + F with + coe := fun f => (f : M → M₂) + map_smul := fun f c x => by rw [map_smulₛₗ, RingHom.id_apply] } + +variable {F} (f : F) [i : SemilinearMapClass F σ M M₃] + +include i + +theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : + c • f x = f (σ' c • x) := by simp +#align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv + +end SemilinearMapClass + +namespace LinearMap + +section AddCommMonoid + +variable [Semiring R] [Semiring S] + +section + +variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] + +variable [Module R M] [Module R M₂] [Module S M₃] + +variable {σ : R →+* S} + +instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ + where + coe := LinearMap.toFun + coe_injective' f g h := by cases f <;> cases g <;> congr + map_add := LinearMap.map_add' + map_smulₛₗ := LinearMap.map_smul' + +/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` +directly. +-/ +instance : CoeFun (M →ₛₗ[σ] M₃) fun _ => M → M₃ := + ⟨fun f => f⟩ + +/-- The `distrib_mul_action_hom` underlying a `linear_map`. -/ +def toDistribMulActionHom (f : M →ₗ[R] M₂) : DistribMulActionHom R M M₂ := + { f with map_zero' := show f 0 = 0 from map_zero f } +#align linear_map.to_distrib_mul_action_hom LinearMap.toDistribMulActionHom + +@[simp] +theorem to_fun_eq_coe {f : M →ₛₗ[σ] M₃} : f.toFun = (f : M → M₃) := + rfl +#align linear_map.to_fun_eq_coe LinearMap.to_fun_eq_coe + +@[ext] +theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g := + FunLike.ext f g h +#align linear_map.ext LinearMap.ext + +/-- Copy of a `linear_map` with a new `to_fun` equal to the old one. Useful to fix definitional +equalities. -/ +protected def copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃ + where + toFun := f' + map_add' := h.symm ▸ f.map_add' + map_smul' := h.symm ▸ f.map_smul' +#align linear_map.copy LinearMap.copy + +@[simp] +theorem coe_copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' := + rfl +#align linear_map.coe_copy LinearMap.coe_copy + +theorem copy_eq (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : f.copy f' h = f := + FunLike.ext' h +#align linear_map.copy_eq LinearMap.copy_eq + +/-- See Note [custom simps projection]. -/ +protected def Simps.apply {R S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M M₃ : Type _) + [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] (f : M →ₛₗ[σ] M₃) : M → M₃ := + f +#align linear_map.simps.apply LinearMap.Simps.apply + +initialize_simps_projections LinearMap (toFun → apply) + +@[simp] +theorem coe_mk {σ : R →+* S} (f : M → M₃) (h₁ h₂) : + ((LinearMap.mk f h₁ h₂ : M →ₛₗ[σ] M₃) : M → M₃) = f := + rfl +#align linear_map.coe_mk LinearMap.coe_mk + +/-- Identity map as a `linear_map` -/ +def id : M →ₗ[R] M := + { DistribMulActionHom.id R with toFun := id } +#align linear_map.id LinearMap.id + +theorem id_apply (x : M) : @id R M _ _ _ x = x := + rfl +#align linear_map.id_apply LinearMap.id_apply + +@[simp, norm_cast] +theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id := + rfl +#align linear_map.id_coe LinearMap.id_coe + +end + +section + +variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] + +variable [Module R M] [Module R M₂] [Module S M₃] + +variable (σ : R →+* S) + +variable (fₗ gₗ : M →ₗ[R] M₂) (f g : M →ₛₗ[σ] M₃) + +theorem isLinear : IsLinearMap R fₗ := + ⟨fₗ.map_add', fₗ.map_smul'⟩ +#align linear_map.is_linear LinearMap.isLinear + +variable {fₗ gₗ f g σ} + +theorem coe_injective : @Injective (M →ₛₗ[σ] M₃) (M → M₃) coeFn := + FunLike.coe_injective +#align linear_map.coe_injective LinearMap.coe_injective + +protected theorem congr_arg {x x' : M} : x = x' → f x = f x' := + FunLike.congr_arg f +#align linear_map.congr_arg LinearMap.congr_arg + +/-- If two linear maps are equal, they are equal at each point. -/ +protected theorem congr_fun (h : f = g) (x : M) : f x = g x := + FunLike.congr_fun h x +#align linear_map.congr_fun LinearMap.congr_fun + +theorem ext_iff : f = g ↔ ∀ x, f x = g x := + FunLike.ext_iff +#align linear_map.ext_iff LinearMap.ext_iff + +@[simp] +theorem mk_coe (f : M →ₛₗ[σ] M₃) (h₁ h₂) : (LinearMap.mk f h₁ h₂ : M →ₛₗ[σ] M₃) = f := + ext fun _ => rfl +#align linear_map.mk_coe LinearMap.mk_coe + +variable (fₗ gₗ f g) + +protected theorem map_add (x y : M) : f (x + y) = f x + f y := + map_add f x y +#align linear_map.map_add LinearMap.map_add + +protected theorem map_zero : f 0 = 0 := + map_zero f +#align linear_map.map_zero LinearMap.map_zero + +-- TODO: `simp` isn't picking up `map_smulₛₗ` for `linear_map`s without specifying `map_smulₛₗ f` +@[simp] +protected theorem map_smulₛₗ (c : R) (x : M) : f (c • x) = σ c • f x := + map_smulₛₗ f c x +#align linear_map.map_smulₛₗ LinearMap.map_smulₛₗ + +protected theorem map_smul (c : R) (x : M) : fₗ (c • x) = c • fₗ x := + map_smul fₗ c x +#align linear_map.map_smul LinearMap.map_smul + +protected theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : + c • f x = f (σ' c • x) := by simp +#align linear_map.map_smul_inv LinearMap.map_smul_inv + +-- TODO: generalize to `zero_hom_class` +@[simp] +theorem map_eq_zero_iff (h : Function.Injective f) {x : M} : f x = 0 ↔ x = 0 := + ⟨fun w => by + apply h + simp [w], fun w => by + subst w + simp⟩ +#align linear_map.map_eq_zero_iff LinearMap.map_eq_zero_iff + +section Pointwise + +open Pointwise + +variable (M M₃ σ) {F : Type _} (h : F) + +@[simp] +theorem image_smul_setₛₗ [SemilinearMapClass F σ M M₃] (c : R) (s : Set M) : + h '' (c • s) = σ c • h '' s := by + apply Set.Subset.antisymm + · rintro x ⟨y, ⟨z, zs, rfl⟩, rfl⟩ + exact ⟨h z, Set.mem_image_of_mem _ zs, (map_smulₛₗ _ _ _).symm⟩ + · rintro x ⟨y, ⟨z, hz, rfl⟩, rfl⟩ + exact (Set.mem_image _ _ _).2 ⟨c • z, Set.smul_mem_smul_set hz, map_smulₛₗ _ _ _⟩ +#align image_smul_setₛₗ image_smul_setₛₗ + +theorem preimage_smul_setₛₗ [SemilinearMapClass F σ M M₃] {c : R} (hc : IsUnit c) (s : Set M₃) : + h ⁻¹' (σ c • s) = c • h ⁻¹' s := by + apply Set.Subset.antisymm + · rintro x ⟨y, ys, hy⟩ + refine' ⟨(hc.unit.inv : R) • x, _, _⟩ + · + simp only [← hy, smul_smul, Set.mem_preimage, Units.inv_eq_val_inv, map_smulₛₗ h, ← map_mul, + IsUnit.val_inv_mul, one_smul, map_one, ys] + · simp only [smul_smul, IsUnit.mul_val_inv, one_smul, Units.inv_eq_val_inv] + · rintro x ⟨y, hy, rfl⟩ + refine' ⟨h y, hy, by simp only [RingHom.id_apply, map_smulₛₗ h]⟩ +#align preimage_smul_setₛₗ preimage_smul_setₛₗ + +variable (R M₂) + +theorem image_smul_set [LinearMapClass F R M M₂] (c : R) (s : Set M) : h '' (c • s) = c • h '' s := + image_smul_setₛₗ _ _ _ h c s +#align image_smul_set image_smul_set + +theorem preimage_smul_set [LinearMapClass F R M M₂] {c : R} (hc : IsUnit c) (s : Set M₂) : + h ⁻¹' (c • s) = c • h ⁻¹' s := + preimage_smul_setₛₗ _ _ _ h hc s +#align preimage_smul_set preimage_smul_set + +end Pointwise + +variable (M M₂) + +/-- A typeclass for `has_smul` 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. +-/ +class CompatibleSmul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] + [Module S M₂] where + map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x +#align linear_map.compatible_smul LinearMap.CompatibleSmul + +variable {M M₂} + +instance (priority := 100) IsScalarTower.compatibleSmul {R S : Type _} [Semiring S] [SMul R S] + [SMul R M] [Module S M] [IsScalarTower R S M] [SMul R M₂] [Module S M₂] [IsScalarTower R S M₂] : + CompatibleSmul M M₂ R S := + ⟨fun fₗ c x => by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩ +#align linear_map.is_scalar_tower.compatible_smul LinearMap.IsScalarTower.compatibleSmul + +@[simp] +theorem map_smul_of_tower {R S : Type _} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] + [Module S M₂] [CompatibleSmul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : + fₗ (c • x) = c • fₗ x := + CompatibleSmul.map_smul fₗ c x +#align linear_map.map_smul_of_tower LinearMap.map_smul_of_tower + +/-- convert a linear map to an additive map -/ +def toAddMonoidHom : M →+ M₃ where + toFun := f + map_zero' := f.map_zero + map_add' := f.map_add +#align linear_map.to_add_monoid_hom LinearMap.toAddMonoidHom + +@[simp] +theorem to_add_monoid_hom_coe : ⇑f.toAddMonoidHom = f := + rfl +#align linear_map.to_add_monoid_hom_coe LinearMap.to_add_monoid_hom_coe + +section RestrictScalars + +variable (R) [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] + +/-- 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`. -/ +def restrictScalars (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂ + where + toFun := fₗ + map_add' := fₗ.map_add + map_smul' := fₗ.map_smul_of_tower +#align linear_map.restrict_scalars LinearMap.restrictScalars + +@[simp] +theorem coe_restrict_scalars (fₗ : M →ₗ[S] M₂) : ⇑(restrictScalars R fₗ) = fₗ := + rfl +#align linear_map.coe_restrict_scalars LinearMap.coe_restrict_scalars + +theorem restrict_scalars_apply (fₗ : M →ₗ[S] M₂) (x) : restrictScalars R fₗ x = fₗ x := + rfl +#align linear_map.restrict_scalars_apply LinearMap.restrict_scalars_apply + +theorem restrict_scalars_injective : + Function.Injective (restrictScalars R : (M →ₗ[S] M₂) → M →ₗ[R] M₂) := fun fₗ gₗ h => + ext (LinearMap.congr_fun h : _) +#align linear_map.restrict_scalars_injective LinearMap.restrict_scalars_injective + +@[simp] +theorem restrict_scalars_inj (fₗ gₗ : M →ₗ[S] M₂) : + fₗ.restrictScalars R = gₗ.restrictScalars R ↔ fₗ = gₗ := + (restrict_scalars_injective R).eq_iff +#align linear_map.restrict_scalars_inj LinearMap.restrict_scalars_inj + +end RestrictScalars + +variable {R} + +theorem to_add_monoid_hom_injective : + Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun f g h => + ext <| AddMonoidHom.congr_fun h +#align linear_map.to_add_monoid_hom_injective LinearMap.to_add_monoid_hom_injective + +/-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/ +@[ext] +theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g := + ext fun x => by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h] +#align linear_map.ext_ring LinearMap.ext_ring + +theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1 = g 1 := + ⟨fun h => h ▸ rfl, ext_ring⟩ +#align linear_map.ext_ring_iff LinearMap.ext_ring_iff + +@[ext] +theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g := + ext fun x => by rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h] +#align linear_map.ext_ring_op LinearMap.ext_ring_op + +end + +/-- Interpret a `ring_hom` `f` as an `f`-semilinear map. -/ +@[simps] +def RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S := + { f with + toFun := f + map_smul' := f.map_mul } +#align ring_hom.to_semilinear_map RingHom.toSemilinearMap + +section + +variable [Semiring R₁] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} + +variable {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} + +variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + +variable (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) + +include module_M₁ module_M₂ module_M₃ + +/-- Composition of two linear maps is a linear map -/ +def comp : M₁ →ₛₗ[σ₁₃] M₃ where + toFun := f ∘ g + map_add' := by simp only [map_add, forall_const, eq_self_iff_true, comp_app] + map_smul' r x := by rw [comp_app, map_smulₛₗ, map_smulₛₗ, RingHomCompTriple.comp_apply] +#align linear_map.comp LinearMap.comp + +omit module_M₁ module_M₂ module_M₃ + +-- mathport name: «expr ∘ₗ » +infixr:80 " ∘ₗ " => + @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) + RingHomCompTriple.ids + +include σ₁₃ + +theorem comp_apply (x : M₁) : f.comp g x = f (g x) := + rfl +#align linear_map.comp_apply LinearMap.comp_apply + +omit σ₁₃ + +include σ₁₃ + +@[simp, norm_cast] +theorem coe_comp : (f.comp g : M₁ → M₃) = f ∘ g := + rfl +#align linear_map.coe_comp LinearMap.coe_comp + +omit σ₁₃ + +@[simp] +theorem comp_id : f.comp id = f := + LinearMap.ext fun x => rfl +#align linear_map.comp_id LinearMap.comp_id + +@[simp] +theorem id_comp : id.comp f = f := + LinearMap.ext fun x => rfl +#align linear_map.id_comp LinearMap.id_comp + +variable {f g} {f' : M₂ →ₛₗ[σ₂₃] M₃} {g' : M₁ →ₛₗ[σ₁₂] M₂} + +include σ₁₃ + +theorem cancel_right (hg : Function.Surjective g) : f.comp g = f'.comp g ↔ f = f' := + ⟨fun h => ext <| hg.forall.2 (ext_iff.1 h), fun h => h ▸ rfl⟩ +#align linear_map.cancel_right LinearMap.cancel_right + +theorem cancel_left (hf : Function.Injective f) : f.comp g = f.comp g' ↔ g = g' := + ⟨fun h => ext fun x => hf <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩ +#align linear_map.cancel_left LinearMap.cancel_left + +omit σ₁₃ + +end + +variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] + +/-- If a function `g` is a left and right inverse of a linear map `f`, then `g` is linear itself. -/ +def inverse [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] + (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : M₂ →ₛₗ[σ'] M := + by + dsimp [left_inverse, Function.RightInverse] at h₁ h₂ <;> + exact + { toFun := g + map_add' := fun x y => by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)] <;> simp [h₂] + map_smul' := fun a b => by + rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)] + simp [h₂] } +#align linear_map.inverse LinearMap.inverse + +end AddCommMonoid + +section AddCommGroup + +variable [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] + +variable {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} + +variable (f : M →ₛₗ[σ] M₂) + +protected theorem map_neg (x : M) : f (-x) = -f x := + map_neg f x +#align linear_map.map_neg LinearMap.map_neg + +protected theorem map_sub (x y : M) : f (x - y) = f x - f y := + map_sub f x y +#align linear_map.map_sub LinearMap.map_sub + +instance CompatibleSmul.intModule {S : Type _} [Semiring S] [Module S M] [Module S M₂] : + CompatibleSmul M M₂ ℤ S := + ⟨fun fₗ c x => by + induction c using Int.induction_on + case hz => simp + case hp n ih => simp [add_smul, ih] + case hn n ih => simp [sub_smul, ih]⟩ +#align linear_map.compatible_smul.int_module LinearMap.CompatibleSmul.intModule + +instance CompatibleSmul.units {R S : Type _} [Monoid R] [MulAction R M] [MulAction R M₂] + [Semiring S] [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] : CompatibleSmul M M₂ Rˣ S := + ⟨fun fₗ c x => (CompatibleSmul.map_smul fₗ (c : R) x : _)⟩ +#align linear_map.compatible_smul.units LinearMap.CompatibleSmul.units + +end AddCommGroup + +end LinearMap + +namespace Module + +/-- `g : R →+* S` is `R`-linear when the module structure on `S` is `module.comp_hom S g` . -/ +@[simps] +def compHom.toLinearMap {R S : Type _} [Semiring R] [Semiring S] (g : R →+* S) : + haveI := comp_hom S g + R →ₗ[R] S + where + toFun := (g : R → S) + map_add' := g.map_add + map_smul' := g.map_mul +#align module.comp_hom.to_linear_map Module.compHom.toLinearMap + +end Module + +namespace DistribMulActionHom + +variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] + +/-- A `distrib_mul_action_hom` between two modules is a linear map. -/ +def toLinearMap (fₗ : M →+[R] M₂) : M →ₗ[R] M₂ := + { fₗ with } +#align distrib_mul_action_hom.to_linear_map DistribMulActionHom.toLinearMap + +instance : Coe (M →+[R] M₂) (M →ₗ[R] M₂) := + ⟨toLinearMap⟩ + +@[simp] +theorem to_linear_map_eq_coe (f : M →+[R] M₂) : f.toLinearMap = ↑f := + rfl +#align distrib_mul_action_hom.to_linear_map_eq_coe DistribMulActionHom.to_linear_map_eq_coe + +@[simp, norm_cast] +theorem coe_to_linear_map (f : M →+[R] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f := + rfl +#align distrib_mul_action_hom.coe_to_linear_map DistribMulActionHom.coe_to_linear_map + +theorem to_linear_map_injective {f g : M →+[R] M₂} (h : (f : M →ₗ[R] M₂) = (g : M →ₗ[R] M₂)) : + f = g := by + ext m + exact LinearMap.congr_fun h m +#align distrib_mul_action_hom.to_linear_map_injective DistribMulActionHom.to_linear_map_injective + +end DistribMulActionHom + +namespace IsLinearMap + +section AddCommMonoid + +variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] + +variable [Module R M] [Module R M₂] + +include R + +/-- Convert an `is_linear_map` predicate to a `linear_map` -/ +def mk' (f : M → M₂) (H : IsLinearMap R f) : M →ₗ[R] M₂ + where + toFun := f + map_add' := H.1 + map_smul' := H.2 +#align is_linear_map.mk' IsLinearMap.mk' + +@[simp] +theorem mk'_apply {f : M → M₂} (H : IsLinearMap R f) (x : M) : mk' f H x = f x := + rfl +#align is_linear_map.mk'_apply IsLinearMap.mk'_apply + +theorem isLinearMapSmul {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : + IsLinearMap R fun z : M => c • z := + by + refine' IsLinearMap.mk (smul_add c) _ + intro _ _ + simp only [smul_smul, mul_comm] +#align is_linear_map.is_linear_map_smul IsLinearMap.isLinearMapSmul + +theorem isLinearMapSmul' {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : + IsLinearMap R fun c : R => c • a := + IsLinearMap.mk (fun x y => add_smul x y a) fun x y => mul_smul x y a +#align is_linear_map.is_linear_map_smul' IsLinearMap.isLinearMapSmul' + +variable {f : M → M₂} (lin : IsLinearMap R f) + +include M M₂ lin + +theorem map_zero : f (0 : M) = (0 : M₂) := + (lin.mk' f).map_zero +#align is_linear_map.map_zero IsLinearMap.map_zero + +end AddCommMonoid + +section AddCommGroup + +variable [Semiring R] [AddCommGroup M] [AddCommGroup M₂] + +variable [Module R M] [Module R M₂] + +include R + +theorem isLinearMapNeg : IsLinearMap R fun z : M => -z := + IsLinearMap.mk neg_add fun x y => (smul_neg x y).symm +#align is_linear_map.is_linear_map_neg IsLinearMap.isLinearMapNeg + +variable {f : M → M₂} (lin : IsLinearMap R f) + +include M M₂ lin + +theorem map_neg (x : M) : f (-x) = -f x := + (lin.mk' f).map_neg x +#align is_linear_map.map_neg IsLinearMap.map_neg + +theorem map_sub (x y) : f (x - y) = f x - f y := + (lin.mk' f).map_sub x y +#align is_linear_map.map_sub IsLinearMap.map_sub + +end AddCommGroup + +end IsLinearMap + +/-- Linear endomorphisms of a module, with associated ring structure +`module.End.semiring` and algebra structure `module.End.algebra`. -/ +abbrev Module.EndCat (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] := + M →ₗ[R] M +#align module.End Module.EndCat + +/-- Reinterpret an additive homomorphism as a `ℕ`-linear map. -/ +def AddMonoidHom.toNatLinearMap [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂ + where + toFun := f + map_add' := f.map_add + map_smul' := map_nsmul f +#align add_monoid_hom.to_nat_linear_map AddMonoidHom.toNatLinearMap + +theorem AddMonoidHom.to_nat_linear_map_injective [AddCommMonoid M] [AddCommMonoid M₂] : + Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _) := + by + intro f g h + ext + exact LinearMap.congr_fun h x +#align add_monoid_hom.to_nat_linear_map_injective AddMonoidHom.to_nat_linear_map_injective + +/-- Reinterpret an additive homomorphism as a `ℤ`-linear map. -/ +def AddMonoidHom.toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂ + where + toFun := f + map_add' := f.map_add + map_smul' := map_zsmul f +#align add_monoid_hom.to_int_linear_map AddMonoidHom.toIntLinearMap + +theorem AddMonoidHom.to_int_linear_map_injective [AddCommGroup M] [AddCommGroup M₂] : + Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _) := + by + intro f g h + ext + exact LinearMap.congr_fun h x +#align add_monoid_hom.to_int_linear_map_injective AddMonoidHom.to_int_linear_map_injective + +@[simp] +theorem AddMonoidHom.coe_to_int_linear_map [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : + ⇑f.toIntLinearMap = f := + rfl +#align add_monoid_hom.coe_to_int_linear_map AddMonoidHom.coe_to_int_linear_map + +/-- Reinterpret an additive homomorphism as a `ℚ`-linear map. -/ +def AddMonoidHom.toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] + (f : M →+ M₂) : M →ₗ[ℚ] M₂ := + { f with map_smul' := map_rat_smul f } +#align add_monoid_hom.to_rat_linear_map AddMonoidHom.toRatLinearMap + +theorem AddMonoidHom.to_rat_linear_map_injective [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] + [Module ℚ M₂] : Function.Injective (@AddMonoidHom.toRatLinearMap M M₂ _ _ _ _) := + by + intro f g h + ext + exact LinearMap.congr_fun h x +#align add_monoid_hom.to_rat_linear_map_injective AddMonoidHom.to_rat_linear_map_injective + +@[simp] +theorem AddMonoidHom.coe_to_rat_linear_map [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] + [Module ℚ M₂] (f : M →+ M₂) : ⇑f.toRatLinearMap = f := + rfl +#align add_monoid_hom.coe_to_rat_linear_map AddMonoidHom.coe_to_rat_linear_map + +namespace LinearMap + +section SMul + +variable [Semiring R] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] + +variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + +variable [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] + +variable [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] + +variable [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] + +instance : SMul S (M →ₛₗ[σ₁₂] M₂) := + ⟨fun a f => + { toFun := a • f + map_add' := fun x y => by simp only [Pi.smul_apply, f.map_add, smul_add] + map_smul' := fun c x => by simp [Pi.smul_apply, smul_comm (σ₁₂ c)] }⟩ + +@[simp] +theorem smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x := + rfl +#align linear_map.smul_apply LinearMap.smul_apply + +theorem coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ⇑(a • f) = a • f := + rfl +#align linear_map.coe_smul LinearMap.coe_smul + +instance [SMulCommClass S T M₂] : SMulCommClass S T (M →ₛₗ[σ₁₂] M₂) := + ⟨fun a b f => ext fun 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 [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂) + where smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _ + +instance [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] : + IsCentralScalar S (M →ₛₗ[σ₁₂] M₂) where op_smul_eq_smul a b := ext fun x => op_smul_eq_smul _ _ + +end SMul + +/-! ### Arithmetic on the codomain -/ + + +section Arithmetic + +variable [Semiring R₁] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₃] + +variable [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] + +variable [Module R₁ N₁] [Module R₂ N₂] [Module R₃ N₃] + +variable {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + +/-- The constant 0 map is linear. -/ +instance : Zero (M →ₛₗ[σ₁₂] M₂) := + ⟨{ toFun := 0 + map_add' := by simp + map_smul' := by simp }⟩ + +@[simp] +theorem zero_apply (x : M) : (0 : M →ₛₗ[σ₁₂] M₂) x = 0 := + rfl +#align linear_map.zero_apply LinearMap.zero_apply + +@[simp] +theorem comp_zero (g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 := + ext fun c => by rw [comp_apply, zero_apply, zero_apply, g.map_zero] +#align linear_map.comp_zero LinearMap.comp_zero + +@[simp] +theorem zero_comp (f : M →ₛₗ[σ₁₂] M₂) : ((0 : M₂ →ₛₗ[σ₂₃] M₃).comp f : M →ₛₗ[σ₁₃] M₃) = 0 := + rfl +#align linear_map.zero_comp LinearMap.zero_comp + +instance : Inhabited (M →ₛₗ[σ₁₂] M₂) := + ⟨0⟩ + +@[simp] +theorem default_def : (default : M →ₛₗ[σ₁₂] M₂) = 0 := + rfl +#align linear_map.default_def LinearMap.default_def + +/-- The sum of two linear maps is linear. -/ +instance : Add (M →ₛₗ[σ₁₂] M₂) := + ⟨fun f g => + { toFun := f + g + map_add' := by simp [add_comm, add_left_comm] + map_smul' := by simp [smul_add] }⟩ + +@[simp] +theorem add_apply (f g : M →ₛₗ[σ₁₂] M₂) (x : M) : (f + g) x = f x + g x := + rfl +#align linear_map.add_apply LinearMap.add_apply + +theorem add_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) : + ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f := + rfl +#align linear_map.add_comp LinearMap.add_comp + +theorem comp_add (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : + (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g := + ext fun _ => h.map_add _ _ +#align linear_map.comp_add LinearMap.comp_add + +/-- The type of linear maps is an additive monoid. -/ +instance : AddCommMonoid (M →ₛₗ[σ₁₂] M₂) := + FunLike.coe_injective.AddCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl + +/-- The negation of a linear map is linear. -/ +instance : Neg (M →ₛₗ[σ₁₂] N₂) := + ⟨fun f => + { toFun := -f + map_add' := by simp [add_comm] + map_smul' := by simp }⟩ + +@[simp] +theorem neg_apply (f : M →ₛₗ[σ₁₂] N₂) (x : M) : (-f) x = -f x := + rfl +#align linear_map.neg_apply LinearMap.neg_apply + +include σ₁₃ + +@[simp] +theorem neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f := + rfl +#align linear_map.neg_comp LinearMap.neg_comp + +@[simp] +theorem comp_neg (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (-f) = -g.comp f := + ext fun _ => g.map_neg _ +#align linear_map.comp_neg LinearMap.comp_neg + +omit σ₁₃ + +/-- The negation of a linear map is linear. -/ +instance : Sub (M →ₛₗ[σ₁₂] N₂) := + ⟨fun f g => + { toFun := f - g + map_add' := fun x y => by simp only [Pi.sub_apply, map_add, add_sub_add_comm] + map_smul' := fun r x => by simp [Pi.sub_apply, map_smul, smul_sub] }⟩ + +@[simp] +theorem sub_apply (f g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x := + rfl +#align linear_map.sub_apply LinearMap.sub_apply + +include σ₁₃ + +theorem sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) : + (g - h).comp f = g.comp f - h.comp f := + rfl +#align linear_map.sub_comp LinearMap.sub_comp + +theorem comp_sub (f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : + h.comp (g - f) = h.comp g - h.comp f := + ext fun _ => h.map_sub _ _ +#align linear_map.comp_sub LinearMap.comp_sub + +omit σ₁₃ + +/-- The type of linear maps is an additive group. -/ +instance : AddCommGroup (M →ₛₗ[σ₁₂] N₂) := + FunLike.coe_injective.AddCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) + (fun _ _ => rfl) fun _ _ => rfl + +end Arithmetic + +section Actions + +variable [Semiring R] [Semiring R₂] [Semiring R₃] + +variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] + +variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] + +variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] + +section SMul + +variable [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] + +variable [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] + +variable [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] + +instance : DistribMulAction S (M →ₛₗ[σ₁₂] M₂) + where + one_smul f := ext fun _ => one_smul _ _ + mul_smul c c' f := ext fun _ => mul_smul _ _ _ + smul_add c f g := ext fun x => smul_add _ _ _ + smul_zero c := ext fun x => smul_zero _ + +include σ₁₃ + +theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : + (a • g).comp f = a • g.comp f := + rfl +#align linear_map.smul_comp LinearMap.smul_comp + +omit σ₁₃ + +-- TODO: generalize this to semilinear maps +theorem comp_smul [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] + [SMulCommClass R S M₃] [CompatibleSmul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : + g.comp (a • f) = a • g.comp f := + ext fun x => g.map_smul_of_tower _ _ +#align linear_map.comp_smul LinearMap.comp_smul + +end SMul + +section Module + +variable [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] + +instance : Module S (M →ₛₗ[σ₁₂] M₂) + where + add_smul a b f := ext fun x => add_smul _ _ _ + zero_smul f := ext fun x => zero_smul _ _ + +instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂) := + coe_injective.NoZeroSmulDivisors _ rfl coe_smul + +end Module + +end Actions + +/-! +### Monoid structure of endomorphisms + +Lemmas about `pow` such as `linear_map.pow_apply` appear in later files. +-/ + + +section Endomorphisms + +variable [Semiring R] [AddCommMonoid M] [AddCommGroup N₁] [Module R M] [Module R N₁] + +instance : One (Module.EndCat R M) := + ⟨LinearMap.id⟩ + +instance : Mul (Module.EndCat R M) := + ⟨LinearMap.comp⟩ + +theorem one_eq_id : (1 : Module.EndCat R M) = id := + rfl +#align linear_map.one_eq_id LinearMap.one_eq_id + +theorem mul_eq_comp (f g : Module.EndCat R M) : f * g = f.comp g := + rfl +#align linear_map.mul_eq_comp LinearMap.mul_eq_comp + +@[simp] +theorem one_apply (x : M) : (1 : Module.EndCat R M) x = x := + rfl +#align linear_map.one_apply LinearMap.one_apply + +@[simp] +theorem mul_apply (f g : Module.EndCat R M) (x : M) : (f * g) x = f (g x) := + rfl +#align linear_map.mul_apply LinearMap.mul_apply + +theorem coe_one : ⇑(1 : Module.EndCat R M) = _root_.id := + rfl +#align linear_map.coe_one LinearMap.coe_one + +theorem coe_mul (f g : Module.EndCat R M) : ⇑(f * g) = f ∘ g := + rfl +#align linear_map.coe_mul LinearMap.coe_mul + +instance Module.EndCat.monoid : Monoid (Module.EndCat R M) + where + mul := (· * ·) + one := (1 : M →ₗ[R] M) + mul_assoc f g h := LinearMap.ext fun x => rfl + mul_one := comp_id + one_mul := id_comp +#align module.End.monoid Module.EndCat.monoid + +instance Module.EndCat.semiring : Semiring (Module.EndCat R M) := + { AddMonoidWithOne.unary, Module.EndCat.monoid, + LinearMap.addCommMonoid with + mul := (· * ·) + one := (1 : M →ₗ[R] M) + zero := 0 + add := (· + ·) + mul_zero := comp_zero + zero_mul := zero_comp + left_distrib := fun f g h => comp_add _ _ _ + right_distrib := fun f g h => add_comp _ _ _ + natCast := fun n => n • 1 + nat_cast_zero := AddMonoid.nsmul_zero _ + nat_cast_succ := fun n => (AddMonoid.nsmul_succ n 1).trans (add_comm _ _) } +#align module.End.semiring Module.EndCat.semiring + +/-- See also `module.End.nat_cast_def`. -/ +@[simp] +theorem Module.EndCat.nat_cast_apply (n : ℕ) (m : M) : (↑n : Module.EndCat R M) m = n • m := + rfl +#align module.End.nat_cast_apply Module.EndCat.nat_cast_apply + +instance Module.EndCat.ring : Ring (Module.EndCat R N₁) := + { Module.EndCat.semiring, + LinearMap.addCommGroup with + intCast := fun z => z • 1 + int_cast_of_nat := of_nat_zsmul _ + int_cast_neg_succ_of_nat := negSucc_zsmul _ } +#align module.End.ring Module.EndCat.ring + +/-- See also `module.End.int_cast_def`. -/ +@[simp] +theorem Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (↑z : Module.EndCat R N₁) m = z • m := + rfl +#align module.End.int_cast_apply Module.EndCat.int_cast_apply + +section + +variable [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] + +instance Module.EndCat.is_scalar_tower : IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := + ⟨smul_comp⟩ +#align module.End.is_scalar_tower Module.EndCat.is_scalar_tower + +instance Module.EndCat.smul_comm_class [SMul S R] [IsScalarTower S R M] : + SMulCommClass S (Module.EndCat R M) (Module.EndCat R M) := + ⟨fun s _ _ => (comp_smul _ s _).symm⟩ +#align module.End.smul_comm_class Module.EndCat.smul_comm_class + +instance Module.EndCat.smul_comm_class' [SMul S R] [IsScalarTower S R M] : + SMulCommClass (Module.EndCat R M) S (Module.EndCat R M) := + SMulCommClass.symm _ _ _ +#align module.End.smul_comm_class' Module.EndCat.smul_comm_class' + +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 applyModule : Module (Module.EndCat R M) M + where + smul := (· <| ·) + smul_zero := LinearMap.map_zero + smul_add := LinearMap.map_add + add_smul := LinearMap.add_apply + zero_smul := (LinearMap.zero_apply : ∀ m, (0 : M →ₗ[R] M) m = 0) + one_smul _ := rfl + mul_smul _ _ _ := rfl +#align linear_map.apply_module LinearMap.applyModule + +@[simp] +protected theorem smul_def (f : Module.EndCat R M) (a : M) : f • a = f a := + rfl +#align linear_map.smul_def LinearMap.smul_def + +/-- `linear_map.apply_module` is faithful. -/ +instance apply_has_faithful_smul : FaithfulSMul (Module.EndCat R M) M := + ⟨fun _ _ => LinearMap.ext⟩ +#align linear_map.apply_has_faithful_smul LinearMap.apply_has_faithful_smul + +instance apply_smul_comm_class : SMulCommClass R (Module.EndCat R M) M + where smul_comm r e m := (e.map_smul r m).symm +#align linear_map.apply_smul_comm_class LinearMap.apply_smul_comm_class + +instance apply_smul_comm_class' : SMulCommClass (Module.EndCat R M) R M + where smul_comm := LinearMap.map_smul +#align linear_map.apply_smul_comm_class' LinearMap.apply_smul_comm_class' + +instance apply_is_scalar_tower {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] : + IsScalarTower R (Module.EndCat R M) M := + ⟨fun t f m => rfl⟩ +#align linear_map.apply_is_scalar_tower LinearMap.apply_is_scalar_tower + +end Endomorphisms + +end LinearMap + +/-! ### Actions as module endomorphisms -/ + + +namespace DistribMulAction + +variable (R M) [Semiring R] [AddCommMonoid M] [Module R M] + +variable [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] + +/-- Each element of the monoid defines a linear map. + +This is a stronger version of `distrib_mul_action.to_add_monoid_hom`. -/ +@[simps] +def toLinearMap (s : S) : M →ₗ[R] M where + toFun := SMul.smul s + map_add' := smul_add s + map_smul' a b := smul_comm _ _ _ +#align distrib_mul_action.to_linear_map DistribMulAction.toLinearMap + +/-- Each element of the monoid defines a module endomorphism. + +This is a stronger version of `distrib_mul_action.to_add_monoid_End`. -/ +@[simps] +def toModuleEnd : S →* Module.EndCat R M + where + toFun := toLinearMap R M + map_one' := LinearMap.ext <| one_smul _ + map_mul' a b := LinearMap.ext <| mul_smul _ _ +#align distrib_mul_action.to_module_End DistribMulAction.toModuleEnd + +end DistribMulAction + +namespace Module + +variable (R M) [Semiring R] [AddCommMonoid M] [Module R M] + +variable [Semiring S] [Module S M] [SMulCommClass S R M] + +/-- Each element of the semiring defines a module endomorphism. + +This is a stronger version of `distrib_mul_action.to_module_End`. -/ +@[simps] +def toModuleEnd : S →+* Module.EndCat R M := + { + DistribMulAction.toModuleEnd R + M with + toFun := DistribMulAction.toLinearMap R M + map_zero' := LinearMap.ext <| zero_smul _ + map_add' := fun f g => LinearMap.ext <| add_smul _ _ } +#align module.to_module_End Module.toModuleEnd + +/-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `module.End R R` induced by the right +multiplication. -/ +@[simps] +def moduleEndSelf : Rᵐᵒᵖ ≃+* Module.EndCat R R := + { Module.toModuleEnd R R with + toFun := DistribMulAction.toLinearMap R R + invFun := fun f => MulOpposite.op (f 1) + left_inv := mul_one + right_inv := fun f => LinearMap.ext_ring <| one_mul _ } +#align module.module_End_self Module.moduleEndSelf + +/-- The canonical (semi)ring isomorphism from `R` to `module.End Rᵐᵒᵖ R` induced by the left +multiplication. -/ +@[simps] +def moduleEndSelfOp : R ≃+* Module.EndCat Rᵐᵒᵖ R := + { Module.toModuleEnd _ _ with + toFun := DistribMulAction.toLinearMap _ _ + invFun := fun f => f 1 + left_inv := mul_one + right_inv := fun f => LinearMap.ext_ring_op <| mul_one _ } +#align module.module_End_self_op Module.moduleEndSelfOp + +theorem EndCat.nat_cast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : + (↑n : Module.EndCat R N₁) = Module.toModuleEnd R N₁ n := + rfl +#align module.End.nat_cast_def Module.EndCat.nat_cast_def + +theorem EndCat.int_cast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] : + (↑z : Module.EndCat R N₁) = Module.toModuleEnd R N₁ z := + rfl +#align module.End.int_cast_def Module.EndCat.int_cast_def + +end Module + From 5342facc2f60e5258fd05341880d4b0c0c9deb47 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Mon, 16 Jan 2023 13:49:26 +0100 Subject: [PATCH 3/9] Mathbin -> Mathlib; add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Algebra/Module/LinearMap.lean | 10 +++++----- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 1cd361e60a7d9..bf11a77546931 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -69,6 +69,7 @@ import Mathlib.Algebra.Homology.ComplexShape import Mathlib.Algebra.Invertible import Mathlib.Algebra.Module.Basic import Mathlib.Algebra.Module.Hom +import Mathlib.Algebra.Module.LinearMap import Mathlib.Algebra.Module.Pi import Mathlib.Algebra.Module.PointwisePi import Mathlib.Algebra.Module.Prod diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index c0ccea93bc6c7..a9aa6e4e92930 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -9,11 +9,11 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Algebra.Hom.GroupAction -import Mathbin.Algebra.Module.Pi -import Mathbin.Algebra.Star.Basic -import Mathbin.Data.Set.Pointwise.Smul -import Mathbin.Algebra.Ring.CompTypeclasses +import Mathlib.Algebra.Hom.GroupAction +import Mathlib.Algebra.Module.Pi +import Mathlib.Algebra.Star.Basic +import Mathlib.Data.Set.Pointwise.Smul +import Mathlib.Algebra.Ring.CompTypeclasses /-! # (Semi)linear maps From a3672122d11e888a3817351897f10963dfe9a357 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Mon, 16 Jan 2023 15:19:19 +0100 Subject: [PATCH 4/9] WIP: works until the Ring instance --- Mathlib/Algebra/Module/LinearMap.lean | 402 ++++++++++++-------------- 1 file changed, 177 insertions(+), 225 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index a9aa6e4e92930..9bc0533f3aa08 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -12,7 +12,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne import Mathlib.Algebra.Hom.GroupAction import Mathlib.Algebra.Module.Pi import Mathlib.Algebra.Star.Basic -import Mathlib.Data.Set.Pointwise.Smul +import Mathlib.Data.Set.Pointwise.SMul import Mathlib.Algebra.Ring.CompTypeclasses /-! @@ -58,20 +58,20 @@ linear map -/ +-- Porting note: `assert_not_exists` is not defined yet +/- assert_not_exists Submonoid assert_not_exists finset +-/ open Function universe u u' v w x y z variable {R : Type _} {R₁ : Type _} {R₂ : Type _} {R₃ : Type _} - variable {k : Type _} {S : Type _} {S₃ : Type _} {T : Type _} - variable {M : Type _} {M₁ : Type _} {M₂ : Type _} {M₃ : Type _} - variable {N₁ : Type _} {N₂ : Type _} {N₃ : Type _} {ι : Type _} /-- A map `f` between modules over a semiring is linear if it satisfies the two properties @@ -80,7 +80,9 @@ property. A bundled version is available with `linear_map`, and should be favore `is_linear_map` most of the time. -/ structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) : Prop where + /-- A linear map preserves addition. -/ map_add : ∀ x y, f (x + y) = f x + f y + /-- A linear map preserves scalar multiplication. -/ map_smul : ∀ (c : R) (x), f (c • x) = c • f x #align is_linear_map IsLinearMap @@ -93,20 +95,25 @@ is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `σ = 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. -/ structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type _) - (M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends - AddHom M M₂ where - map_smul' : ∀ (r : R) (x : M), to_fun (r • x) = σ r • to_fun x + (M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends + AddHom M M₂ where + /-- A linear map preserves scalar multiplication. + We prefer the spelling `_root_.map_smul` instead. -/ + map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x #align linear_map LinearMap /-- The `add_hom` underlying a `linear_map`. -/ add_decl_doc LinearMap.toAddHom -- mathport name: «expr →ₛₗ[ ] » +/-- `M →ₛₗ[σ] N` is the type of `σ`-semilinear maps from `M` to `N`. -/ notation:25 M " →ₛₗ[" σ:25 "] " M₂:0 => LinearMap σ M M₂ +/-- `M →ₗ[R] N` is the type of `R`-linear maps from `M` to `N`. -/ -- mathport name: «expr →ₗ[ ] » notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂ +/-- `M →ₗ⋆[R] N` is the type of `R`-conjugate-linear maps from `M` to `N`. -/ -- mathport name: «expr →ₗ⋆[ ] » notation:25 M " →ₗ⋆[" R:25 "] " M₂:0 => LinearMap (starRingEnd R) M M₂ @@ -118,15 +125,18 @@ A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and `f (c • x) = (σ c) • f x`. -/ class SemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S] - (σ : outParam <| R →+* S) (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂] + (σ : outParam (R →+* S)) (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHomClass F M M₂ where + /-- A semilinear map preserves scalar multiplication up to some ring homomorphism `σ`. + See also `_root_.map_smul` for the case where `σ` is the identity. -/ map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x #align semilinear_map_class SemilinearMapClass end --- `σ` becomes a metavariable but that's fine because it's an `out_param` -attribute [nolint dangerous_instance] SemilinearMapClass.toAddHomClass +-- Porting note: `dangerousInstance` linter has become smarter about `outParam`s +-- `σ` becomes a metavariable but that's fine because it's an `outParam` +-- attribute [nolint dangerousInstance] SemilinearMapClass.toAddHomClass export SemilinearMapClass (map_smulₛₗ) @@ -144,41 +154,36 @@ abbrev LinearMapClass (F : Type _) (R M M₂ : outParam (Type _)) [Semiring R] [ namespace SemilinearMapClass variable (F : Type _) - -variable [Semiring R] [Semiring S] - -variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] - -variable [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] - -variable [Module R M] [Module R M₂] [Module S M₃] - +variable {_ : Semiring R} {_ : Semiring S} +variable {_ : AddCommMonoid M} {_ : AddCommMonoid M₁} {_ : AddCommMonoid M₂} {_ : AddCommMonoid M₃} +variable {_ : AddCommMonoid N₁} {_ : AddCommMonoid N₂} {_ : AddCommMonoid N₃} +variable {_ : Module R M} {_ : Module R M₂} {_ : Module S M₃} variable {σ : R →+* S} --- `σ` is an `out_param` so it's not dangerous -@[nolint dangerous_instance] -instance (priority := 100) [SemilinearMapClass F σ M M₃] : AddMonoidHomClass F M M₃ := - { - SemilinearMapClass.toAddHomClass F σ M - M₃ with - coe := fun f => (f : M → M₃) - map_zero := fun f => +-- Porting note: the `dangerousInstance` linter has become smarter about `outParam`s +-- @[nolint dangerousInstance] -- `σ` is an `outParam` so it's not dangerous +instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] : + AddMonoidHomClass F M M₃ := + { SemilinearMapClass.toAddHomClass with + coe := fun f ↦ (f : M → M₃) + map_zero := fun f ↦ show f 0 = 0 by rw [← zero_smul R (0 : M), map_smulₛₗ] simp } --- `R` is an `out_param` so it's not dangerous -@[nolint dangerous_instance] -instance (priority := 100) [LinearMapClass F R M M₂] : DistribMulActionHomClass F R M M₂ := - { - SemilinearMapClass.addMonoidHomClass - F with - coe := fun f => (f : M → M₂) - map_smul := fun f c x => by rw [map_smulₛₗ, RingHom.id_apply] } +-- The `Semiring` should be an instance parameter but depends on outParams. +-- If Lean 4 gets better support for instance params depending on outParams, +-- we should be able to remove this nolint. +@[nolint dangerousInstance] +instance (priority := 100) distribMulActionHomClass [LinearMapClass F R M M₂] : + DistribMulActionHomClass F R M M₂ := + { SemilinearMapClass.addMonoidHomClass F with + coe := fun f ↦ (f : M → M₂) + map_smul := fun f c x ↦ by rw [map_smulₛₗ, RingHom.id_apply] } variable {F} (f : F) [i : SemilinearMapClass F σ M M₃] -include i +set_option pp.all true in theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x) := by simp @@ -204,18 +209,20 @@ variable {σ : R →+* S} instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ where - coe := LinearMap.toFun - coe_injective' f g h := by cases f <;> cases g <;> congr - map_add := LinearMap.map_add' + coe f := f.toFun + coe_injective' f g h := by + cases f + cases g + congr + apply FunLike.coe_injective' + exact h + map_add f := f.map_add' map_smulₛₗ := LinearMap.map_smul' -/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` -directly. --/ -instance : CoeFun (M →ₛₗ[σ] M₃) fun _ => M → M₃ := - ⟨fun f => f⟩ +-- Porting note: we don't port specialized `CoeFun` instances if there is `FunLike` instead +#noalign linear_map.has_coe_to_fun -/-- The `distrib_mul_action_hom` underlying a `linear_map`. -/ +/-- The `DistribMulActionHom` underlying a `linear_map`. -/ def toDistribMulActionHom (f : M →ₗ[R] M₂) : DistribMulActionHom R M M₂ := { f with map_zero' := show f 0 = 0 from map_zero f } #align linear_map.to_distrib_mul_action_hom LinearMap.toDistribMulActionHom @@ -230,7 +237,7 @@ theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g := FunLike.ext f g h #align linear_map.ext LinearMap.ext -/-- Copy of a `linear_map` with a new `to_fun` equal to the old one. Useful to fix definitional +/-- Copy of a `linear_map` with a new `toFun` equal to the old one. Useful to fix definitional equalities. -/ protected def copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃ where @@ -254,17 +261,17 @@ protected def Simps.apply {R S : Type _} [Semiring R] [Semiring S] (σ : R →+* f #align linear_map.simps.apply LinearMap.Simps.apply -initialize_simps_projections LinearMap (toFun → apply) +initialize_simps_projections LinearMap (toAddHom_toFun → apply) @[simp] -theorem coe_mk {σ : R →+* S} (f : M → M₃) (h₁ h₂) : - ((LinearMap.mk f h₁ h₂ : M →ₛₗ[σ] M₃) : M → M₃) = f := +theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) : + ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f := rfl #align linear_map.coe_mk LinearMap.coe_mk /-- Identity map as a `linear_map` -/ def id : M →ₗ[R] M := - { DistribMulActionHom.id R with toFun := id } + { DistribMulActionHom.id R with toFun := _root_.id } #align linear_map.id LinearMap.id theorem id_apply (x : M) : @id R M _ _ _ x = x := @@ -290,13 +297,13 @@ variable (σ : R →+* S) variable (fₗ gₗ : M →ₗ[R] M₂) (f g : M →ₛₗ[σ] M₃) -theorem isLinear : IsLinearMap R fₗ := +theorem is_linear : IsLinearMap R fₗ := ⟨fₗ.map_add', fₗ.map_smul'⟩ -#align linear_map.is_linear LinearMap.isLinear +#align linear_map.is_linear LinearMap.is_linear variable {fₗ gₗ f g σ} -theorem coe_injective : @Injective (M →ₛₗ[σ] M₃) (M → M₃) coeFn := +theorem coe_injective : Injective (FunLike.coe : (M →ₛₗ[σ] M₃) → _) := FunLike.coe_injective #align linear_map.coe_injective LinearMap.coe_injective @@ -314,8 +321,8 @@ theorem ext_iff : f = g ↔ ∀ x, f x = g x := #align linear_map.ext_iff LinearMap.ext_iff @[simp] -theorem mk_coe (f : M →ₛₗ[σ] M₃) (h₁ h₂) : (LinearMap.mk f h₁ h₂ : M →ₛₗ[σ] M₃) = f := - ext fun _ => rfl +theorem mk_coe (f : M →ₛₗ[σ] M₃) (h) : (LinearMap.mk f h : M →ₛₗ[σ] M₃) = f := + ext fun _ ↦ rfl #align linear_map.mk_coe LinearMap.mk_coe variable (fₗ gₗ f g) @@ -328,8 +335,9 @@ protected theorem map_zero : f 0 = 0 := map_zero f #align linear_map.map_zero LinearMap.map_zero --- TODO: `simp` isn't picking up `map_smulₛₗ` for `linear_map`s without specifying `map_smulₛₗ f` -@[simp] +-- Porting note: `simp` wasn't picking up `map_smulₛₗ` for `linear_map`s without specifying +-- `map_smulₛₗ f`, so we marked this as `@[simp]` in Mathlib3. +-- For Mathlib4, let's try without the `@[simp]` attribute and hope it won't need to be re-enabled. protected theorem map_smulₛₗ (c : R) (x : M) : f (c • x) = σ c • f x := map_smulₛₗ f c x #align linear_map.map_smulₛₗ LinearMap.map_smulₛₗ @@ -342,14 +350,9 @@ protected theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) c • f x = f (σ' c • x) := by simp #align linear_map.map_smul_inv LinearMap.map_smul_inv --- TODO: generalize to `zero_hom_class` @[simp] theorem map_eq_zero_iff (h : Function.Injective f) {x : M} : f x = 0 ↔ x = 0 := - ⟨fun w => by - apply h - simp [w], fun w => by - subst w - simp⟩ + _root_.map_eq_zero_iff f h #align linear_map.map_eq_zero_iff LinearMap.map_eq_zero_iff section Pointwise @@ -359,7 +362,7 @@ open Pointwise variable (M M₃ σ) {F : Type _} (h : F) @[simp] -theorem image_smul_setₛₗ [SemilinearMapClass F σ M M₃] (c : R) (s : Set M) : +theorem _root_.image_smul_setₛₗ [SemilinearMapClass F σ M M₃] (c : R) (s : Set M) : h '' (c • s) = σ c • h '' s := by apply Set.Subset.antisymm · rintro x ⟨y, ⟨z, zs, rfl⟩, rfl⟩ @@ -368,7 +371,8 @@ theorem image_smul_setₛₗ [SemilinearMapClass F σ M M₃] (c : R) (s : Set M exact (Set.mem_image _ _ _).2 ⟨c • z, Set.smul_mem_smul_set hz, map_smulₛₗ _ _ _⟩ #align image_smul_setₛₗ image_smul_setₛₗ -theorem preimage_smul_setₛₗ [SemilinearMapClass F σ M M₃] {c : R} (hc : IsUnit c) (s : Set M₃) : +theorem _root_.preimage_smul_setₛₗ [SemilinearMapClass F σ M M₃] {c : R} (hc : IsUnit c) + (s : Set M₃) : h ⁻¹' (σ c • s) = c • h ⁻¹' s := by apply Set.Subset.antisymm · rintro x ⟨y, ys, hy⟩ @@ -383,11 +387,12 @@ theorem preimage_smul_setₛₗ [SemilinearMapClass F σ M M₃] {c : R} (hc : I variable (R M₂) -theorem image_smul_set [LinearMapClass F R M M₂] (c : R) (s : Set M) : h '' (c • s) = c • h '' s := +theorem _root_.image_smul_set [LinearMapClass F R M M₂] (c : R) (s : Set M) : + h '' (c • s) = c • h '' s := image_smul_setₛₗ _ _ _ h c s #align image_smul_set image_smul_set -theorem preimage_smul_set [LinearMapClass F R M M₂] {c : R} (hc : IsUnit c) (s : Set M₂) : +theorem _root_.preimage_smul_set [LinearMapClass F R M M₂] {c : R} (hc : IsUnit c) (s : Set M₂) : h ⁻¹' (c • s) = c • h ⁻¹' s := preimage_smul_setₛₗ _ _ _ h hc s #align preimage_smul_set preimage_smul_set @@ -403,6 +408,7 @@ we can also add an instance for `add_comm_group.int_module`, allowing `z •` to -/ class CompatibleSmul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] where + /-- Scalar multiplication by `R` of `M` can be moved through linear maps. -/ map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x #align linear_map.compatible_smul LinearMap.CompatibleSmul @@ -411,7 +417,7 @@ variable {M M₂} instance (priority := 100) IsScalarTower.compatibleSmul {R S : Type _} [Semiring S] [SMul R S] [SMul R M] [Module S M] [IsScalarTower R S M] [SMul R M₂] [Module S M₂] [IsScalarTower R S M₂] : CompatibleSmul M M₂ R S := - ⟨fun fₗ c x => by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩ + ⟨fun fₗ c x ↦ by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩ #align linear_map.is_scalar_tower.compatible_smul LinearMap.IsScalarTower.compatibleSmul @[simp] @@ -435,7 +441,8 @@ theorem to_add_monoid_hom_coe : ⇑f.toAddMonoidHom = f := section RestrictScalars -variable (R) [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] +variable (R) +variable [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] /-- 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 @@ -459,7 +466,7 @@ theorem restrict_scalars_apply (fₗ : M →ₗ[S] M₂) (x) : restrictScalars R #align linear_map.restrict_scalars_apply LinearMap.restrict_scalars_apply theorem restrict_scalars_injective : - Function.Injective (restrictScalars R : (M →ₗ[S] M₂) → M →ₗ[R] M₂) := fun fₗ gₗ h => + Function.Injective (restrictScalars R : (M →ₗ[S] M₂) → M →ₗ[R] M₂) := fun _ _ h ↦ ext (LinearMap.congr_fun h : _) #align linear_map.restrict_scalars_injective LinearMap.restrict_scalars_injective @@ -471,33 +478,33 @@ theorem restrict_scalars_inj (fₗ gₗ : M →ₗ[S] M₂) : end RestrictScalars -variable {R} - theorem to_add_monoid_hom_injective : - Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun f g h => - ext <| AddMonoidHom.congr_fun h + Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun fₗ gₗ h ↦ + ext <| (FunLike.congr_fun h : ∀ x, fₗ.toAddMonoidHom x = gₗ.toAddMonoidHom x) #align linear_map.to_add_monoid_hom_injective LinearMap.to_add_monoid_hom_injective /-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/ @[ext] theorem ext_ring {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g := - ext fun x => by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h] + ext fun x ↦ by rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h] #align linear_map.ext_ring LinearMap.ext_ring theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1 = g 1 := - ⟨fun h => h ▸ rfl, ext_ring⟩ + ⟨fun h ↦ h ▸ rfl, ext_ring⟩ #align linear_map.ext_ring_iff LinearMap.ext_ring_iff +-- **TODO**: figure out `mul_opposite` trickery @[ext] -theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : f = g := - ext fun x => by rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h] +theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : + f = g := + ext fun x ↦ by rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, ← g.map_smulₛₗ] #align linear_map.ext_ring_op LinearMap.ext_ring_op end /-- Interpret a `ring_hom` `f` as an `f`-semilinear map. -/ @[simps] -def RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S := +def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S := { f with toFun := f map_smul' := f.map_mul } @@ -506,29 +513,21 @@ def RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S := section variable [Semiring R₁] [Semiring R₂] [Semiring R₃] - variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] - variable {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} - variable {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} - variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] - variable (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) -include module_M₁ module_M₂ module_M₃ - /-- Composition of two linear maps is a linear map -/ def comp : M₁ →ₛₗ[σ₁₃] M₃ where toFun := f ∘ g - map_add' := by simp only [map_add, forall_const, eq_self_iff_true, comp_app] - map_smul' r x := by rw [comp_app, map_smulₛₗ, map_smulₛₗ, RingHomCompTriple.comp_apply] + map_add' := by simp only [map_add, forall_const, Function.comp_apply] + map_smul' r x := by simp only [Function.comp_apply, map_smulₛₗ, RingHomCompTriple.comp_apply] #align linear_map.comp LinearMap.comp -omit module_M₁ module_M₂ module_M₃ - -- mathport name: «expr ∘ₗ » +set_option quotPrecheck false in -- Porting note: error message suggested to do this infixr:80 " ∘ₗ " => @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids @@ -539,41 +538,31 @@ theorem comp_apply (x : M₁) : f.comp g x = f (g x) := rfl #align linear_map.comp_apply LinearMap.comp_apply -omit σ₁₃ - -include σ₁₃ - @[simp, norm_cast] theorem coe_comp : (f.comp g : M₁ → M₃) = f ∘ g := rfl #align linear_map.coe_comp LinearMap.coe_comp -omit σ₁₃ - @[simp] theorem comp_id : f.comp id = f := - LinearMap.ext fun x => rfl + LinearMap.ext fun _ ↦ rfl #align linear_map.comp_id LinearMap.comp_id @[simp] theorem id_comp : id.comp f = f := - LinearMap.ext fun x => rfl + LinearMap.ext fun _ ↦ rfl #align linear_map.id_comp LinearMap.id_comp variable {f g} {f' : M₂ →ₛₗ[σ₂₃] M₃} {g' : M₁ →ₛₗ[σ₁₂] M₂} -include σ₁₃ - theorem cancel_right (hg : Function.Surjective g) : f.comp g = f'.comp g ↔ f = f' := - ⟨fun h => ext <| hg.forall.2 (ext_iff.1 h), fun h => h ▸ rfl⟩ + ⟨fun h ↦ ext <| hg.forall.2 (ext_iff.1 h), fun h ↦ h ▸ rfl⟩ #align linear_map.cancel_right LinearMap.cancel_right theorem cancel_left (hf : Function.Injective f) : f.comp g = f.comp g' ↔ g = g' := - ⟨fun h => ext fun x => hf <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩ + ⟨fun h ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply], fun h ↦ h ▸ rfl⟩ #align linear_map.cancel_left LinearMap.cancel_left -omit σ₁₃ - end variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] @@ -582,13 +571,14 @@ variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMon def inverse [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂ → M) (h₁ : LeftInverse g f) (h₂ : RightInverse g f) : M₂ →ₛₗ[σ'] M := by - dsimp [left_inverse, Function.RightInverse] at h₁ h₂ <;> - exact - { toFun := g - map_add' := fun x y => by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)] <;> simp [h₂] - map_smul' := fun a b => by - rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)] - simp [h₂] } + dsimp [LeftInverse, Function.RightInverse] at h₁ h₂ + exact + { toFun := g + map_add' := fun x y ↦ by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)] ; simp [h₂] + map_smul' := fun a b ↦ by + dsimp only + rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)] + simp [h₂] } #align linear_map.inverse LinearMap.inverse end AddCommMonoid @@ -611,7 +601,7 @@ protected theorem map_sub (x y : M) : f (x - y) = f x - f y := instance CompatibleSmul.intModule {S : Type _} [Semiring S] [Module S M] [Module S M₂] : CompatibleSmul M M₂ ℤ S := - ⟨fun fₗ c x => by + ⟨fun fₗ c x ↦ by induction c using Int.induction_on case hz => simp case hp n ih => simp [add_smul, ih] @@ -620,7 +610,7 @@ instance CompatibleSmul.intModule {S : Type _} [Semiring S] [Module S M] [Module instance CompatibleSmul.units {R S : Type _} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] : CompatibleSmul M M₂ Rˣ S := - ⟨fun fₗ c x => (CompatibleSmul.map_smul fₗ (c : R) x : _)⟩ + ⟨fun fₗ c x ↦ (CompatibleSmul.map_smul fₗ (c : R) x : _)⟩ #align linear_map.compatible_smul.units LinearMap.CompatibleSmul.units end AddCommGroup @@ -632,12 +622,11 @@ namespace Module /-- `g : R →+* S` is `R`-linear when the module structure on `S` is `module.comp_hom S g` . -/ @[simps] def compHom.toLinearMap {R S : Type _} [Semiring R] [Semiring S] (g : R →+* S) : - haveI := comp_hom S g - R →ₗ[R] S - where - toFun := (g : R → S) + letI := compHom S g; R →ₗ[R] S := +letI := compHom S g +{ toFun := (g : R → S) map_add' := g.map_add - map_smul' := g.map_mul + map_smul' := g.map_mul } #align module.comp_hom.to_linear_map Module.compHom.toLinearMap end Module @@ -646,7 +635,7 @@ namespace DistribMulActionHom variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] -/-- A `distrib_mul_action_hom` between two modules is a linear map. -/ +/-- A `DistribMulActionHom` between two modules is a linear map. -/ def toLinearMap (fₗ : M →+[R] M₂) : M →ₗ[R] M₂ := { fₗ with } #align distrib_mul_action_hom.to_linear_map DistribMulActionHom.toLinearMap @@ -659,7 +648,9 @@ theorem to_linear_map_eq_coe (f : M →+[R] M₂) : f.toLinearMap = ↑f := rfl #align distrib_mul_action_hom.to_linear_map_eq_coe DistribMulActionHom.to_linear_map_eq_coe -@[simp, norm_cast] +-- Porting note: removed @[norm_cast] attribute due to error: +-- norm_cast: badly shaped lemma, rhs can't start with coe +@[simp] theorem coe_to_linear_map (f : M →+[R] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f := rfl #align distrib_mul_action_hom.coe_to_linear_map DistribMulActionHom.coe_to_linear_map @@ -677,11 +668,8 @@ namespace IsLinearMap section AddCommMonoid variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] - variable [Module R M] [Module R M₂] -include R - /-- Convert an `is_linear_map` predicate to a `linear_map` -/ def mk' (f : M → M₂) (H : IsLinearMap R f) : M →ₗ[R] M₂ where @@ -696,7 +684,7 @@ theorem mk'_apply {f : M → M₂} (H : IsLinearMap R f) (x : M) : mk' f H x = f #align is_linear_map.mk'_apply IsLinearMap.mk'_apply theorem isLinearMapSmul {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : - IsLinearMap R fun z : M => c • z := + IsLinearMap R fun z : M ↦ c • z := by refine' IsLinearMap.mk (smul_add c) _ intro _ _ @@ -704,14 +692,12 @@ theorem isLinearMapSmul {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Modul #align is_linear_map.is_linear_map_smul IsLinearMap.isLinearMapSmul theorem isLinearMapSmul' {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : - IsLinearMap R fun c : R => c • a := - IsLinearMap.mk (fun x y => add_smul x y a) fun x y => mul_smul x y a + IsLinearMap R fun c : R ↦ c • a := + IsLinearMap.mk (fun x y ↦ add_smul x y a) fun x y ↦ mul_smul x y a #align is_linear_map.is_linear_map_smul' IsLinearMap.isLinearMapSmul' variable {f : M → M₂} (lin : IsLinearMap R f) -include M M₂ lin - theorem map_zero : f (0 : M) = (0 : M₂) := (lin.mk' f).map_zero #align is_linear_map.map_zero IsLinearMap.map_zero @@ -721,19 +707,14 @@ end AddCommMonoid section AddCommGroup variable [Semiring R] [AddCommGroup M] [AddCommGroup M₂] - variable [Module R M] [Module R M₂] -include R - -theorem isLinearMapNeg : IsLinearMap R fun z : M => -z := - IsLinearMap.mk neg_add fun x y => (smul_neg x y).symm +theorem isLinearMapNeg : IsLinearMap R fun z : M ↦ -z := + IsLinearMap.mk neg_add fun x y ↦ (smul_neg x y).symm #align is_linear_map.is_linear_map_neg IsLinearMap.isLinearMapNeg variable {f : M → M₂} (lin : IsLinearMap R f) -include M M₂ lin - theorem map_neg (x : M) : f (-x) = -f x := (lin.mk' f).map_neg x #align is_linear_map.map_neg IsLinearMap.map_neg @@ -764,7 +745,7 @@ theorem AddMonoidHom.to_nat_linear_map_injective [AddCommMonoid M] [AddCommMonoi Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _) := by intro f g h - ext + ext x exact LinearMap.congr_fun h x #align add_monoid_hom.to_nat_linear_map_injective AddMonoidHom.to_nat_linear_map_injective @@ -780,7 +761,7 @@ theorem AddMonoidHom.to_int_linear_map_injective [AddCommGroup M] [AddCommGroup Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _) := by intro f g h - ext + ext x exact LinearMap.congr_fun h x #align add_monoid_hom.to_int_linear_map_injective AddMonoidHom.to_int_linear_map_injective @@ -800,7 +781,7 @@ theorem AddMonoidHom.to_rat_linear_map_injective [AddCommGroup M] [Module ℚ M] [Module ℚ M₂] : Function.Injective (@AddMonoidHom.toRatLinearMap M M₂ _ _ _ _) := by intro f g h - ext + ext x exact LinearMap.congr_fun h x #align add_monoid_hom.to_rat_linear_map_injective AddMonoidHom.to_rat_linear_map_injective @@ -815,24 +796,19 @@ namespace LinearMap section SMul variable [Semiring R] [Semiring R₂] [Semiring R₃] - variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] - variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] - variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] - variable [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] - variable [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] - variable [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] instance : SMul S (M →ₛₗ[σ₁₂] M₂) := - ⟨fun a f => - { toFun := a • f - map_add' := fun x y => by simp only [Pi.smul_apply, f.map_add, smul_add] - map_smul' := fun c x => by simp [Pi.smul_apply, smul_comm (σ₁₂ c)] }⟩ + ⟨fun a f ↦ + { toFun := a • (f : M → M₂) + map_add' := fun x y ↦ by simp only [Pi.smul_apply, f.map_add, smul_add] + -- Porting note: **TODO** `simp` did not pick up `smul_comm` + map_smul' := fun c x ↦ by simp only [Pi.smul_apply, map_smulₛₗ]; rw [← smul_comm] }⟩ @[simp] theorem smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x := @@ -844,15 +820,15 @@ theorem coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ⇑(a • f) = a • #align linear_map.coe_smul LinearMap.coe_smul instance [SMulCommClass S T M₂] : SMulCommClass S T (M →ₛₗ[σ₁₂] M₂) := - ⟨fun a b f => ext fun x => smul_comm _ _ _⟩ + ⟨fun _ _ _ ↦ ext fun _ ↦ 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 [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂) - where smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _ + where smul_assoc _ _ _ := ext fun _ ↦ smul_assoc _ _ _ instance [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] : - IsCentralScalar S (M →ₛₗ[σ₁₂] M₂) where op_smul_eq_smul a b := ext fun x => op_smul_eq_smul _ _ + IsCentralScalar S (M →ₛₗ[σ₁₂] M₂) where op_smul_eq_smul _ _ := ext fun _ ↦ op_smul_eq_smul _ _ end SMul @@ -862,15 +838,10 @@ end SMul section Arithmetic variable [Semiring R₁] [Semiring R₂] [Semiring R₃] - variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] - variable [AddCommGroup N₁] [AddCommGroup N₂] [AddCommGroup N₃] - variable [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] - variable [Module R₁ N₁] [Module R₂ N₂] [Module R₃ N₃] - variable {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] /-- The constant 0 map is linear. -/ @@ -886,7 +857,7 @@ theorem zero_apply (x : M) : (0 : M →ₛₗ[σ₁₂] M₂) x = 0 := @[simp] theorem comp_zero (g : M₂ →ₛₗ[σ₂₃] M₃) : (g.comp (0 : M →ₛₗ[σ₁₂] M₂) : M →ₛₗ[σ₁₃] M₃) = 0 := - ext fun c => by rw [comp_apply, zero_apply, zero_apply, g.map_zero] + ext fun c ↦ by rw [comp_apply, zero_apply, zero_apply, g.map_zero] #align linear_map.comp_zero LinearMap.comp_zero @[simp] @@ -904,7 +875,7 @@ theorem default_def : (default : M →ₛₗ[σ₁₂] M₂) = 0 := /-- The sum of two linear maps is linear. -/ instance : Add (M →ₛₗ[σ₁₂] M₂) := - ⟨fun f g => + ⟨fun f g ↦ { toFun := f + g map_add' := by simp [add_comm, add_left_comm] map_smul' := by simp [smul_add] }⟩ @@ -921,16 +892,16 @@ theorem add_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃ theorem comp_add (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) : (h.comp (f + g) : M →ₛₗ[σ₁₃] M₃) = h.comp f + h.comp g := - ext fun _ => h.map_add _ _ + ext fun _ ↦ h.map_add _ _ #align linear_map.comp_add LinearMap.comp_add /-- The type of linear maps is an additive monoid. -/ -instance : AddCommMonoid (M →ₛₗ[σ₁₂] M₂) := - FunLike.coe_injective.AddCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl +instance addCommMonoid : AddCommMonoid (M →ₛₗ[σ₁₂] M₂) := + FunLike.coe_injective.addCommMonoid _ rfl (fun _ _ ↦ rfl) fun _ _ ↦ rfl /-- The negation of a linear map is linear. -/ instance : Neg (M →ₛₗ[σ₁₂] N₂) := - ⟨fun f => + ⟨fun f ↦ { toFun := -f map_add' := by simp [add_comm] map_smul' := by simp }⟩ @@ -940,8 +911,6 @@ theorem neg_apply (f : M →ₛₗ[σ₁₂] N₂) (x : M) : (-f) x = -f x := rfl #align linear_map.neg_apply LinearMap.neg_apply -include σ₁₃ - @[simp] theorem neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) : (-g).comp f = -g.comp f := rfl @@ -949,25 +918,21 @@ theorem neg_comp (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] @[simp] theorem comp_neg (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) : g.comp (-f) = -g.comp f := - ext fun _ => g.map_neg _ + ext fun _ ↦ g.map_neg _ #align linear_map.comp_neg LinearMap.comp_neg -omit σ₁₃ - /-- The negation of a linear map is linear. -/ instance : Sub (M →ₛₗ[σ₁₂] N₂) := - ⟨fun f g => + ⟨fun f g ↦ { toFun := f - g - map_add' := fun x y => by simp only [Pi.sub_apply, map_add, add_sub_add_comm] - map_smul' := fun r x => by simp [Pi.sub_apply, map_smul, smul_sub] }⟩ + map_add' := fun x y ↦ by simp only [Pi.sub_apply, map_add, add_sub_add_comm] + map_smul' := fun r x ↦ by simp [Pi.sub_apply, map_smul, smul_sub] }⟩ @[simp] theorem sub_apply (f g : M →ₛₗ[σ₁₂] N₂) (x : M) : (f - g) x = f x - g x := rfl #align linear_map.sub_apply LinearMap.sub_apply -include σ₁₃ - theorem sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] N₃) : (g - h).comp f = g.comp f - h.comp f := rfl @@ -975,57 +940,46 @@ theorem sub_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃ theorem comp_sub (f g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) : h.comp (g - f) = h.comp g - h.comp f := - ext fun _ => h.map_sub _ _ + ext fun _ ↦ h.map_sub _ _ #align linear_map.comp_sub LinearMap.comp_sub -omit σ₁₃ - /-- The type of linear maps is an additive group. -/ -instance : AddCommGroup (M →ₛₗ[σ₁₂] N₂) := - FunLike.coe_injective.AddCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) - (fun _ _ => rfl) fun _ _ => rfl +instance addCommGroup : AddCommGroup (M →ₛₗ[σ₁₂] N₂) := + FunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) + (fun _ _ ↦ rfl) fun _ _ ↦ rfl end Arithmetic section Actions variable [Semiring R] [Semiring R₂] [Semiring R₃] - variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] - variable [Module R M] [Module R₂ M₂] [Module R₃ M₃] - variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] section SMul variable [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] - variable [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] - variable [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] instance : DistribMulAction S (M →ₛₗ[σ₁₂] M₂) where - one_smul f := ext fun _ => one_smul _ _ - mul_smul c c' f := ext fun _ => mul_smul _ _ _ - smul_add c f g := ext fun x => smul_add _ _ _ - smul_zero c := ext fun x => smul_zero _ - -include σ₁₃ + one_smul _ := ext fun _ ↦ one_smul _ _ + mul_smul _ _ _ := ext fun _ ↦ mul_smul _ _ _ + smul_add _ _ _ := ext fun _ ↦ smul_add _ _ _ + smul_zero _ := ext fun _ ↦ smul_zero _ theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) : (a • g).comp f = a • g.comp f := rfl #align linear_map.smul_comp LinearMap.smul_comp -omit σ₁₃ - -- TODO: generalize this to semilinear maps theorem comp_smul [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃] [CompatibleSmul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • g.comp f := - ext fun x => g.map_smul_of_tower _ _ + ext fun _ ↦ g.map_smul_of_tower _ _ #align linear_map.comp_smul LinearMap.comp_smul end SMul @@ -1036,11 +990,11 @@ variable [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] instance : Module S (M →ₛₗ[σ₁₂] M₂) where - add_smul a b f := ext fun x => add_smul _ _ _ - zero_smul f := ext fun x => zero_smul _ _ + add_smul _ _ _ := ext fun _ ↦ add_smul _ _ _ + zero_smul _ := ext fun _ ↦ zero_smul _ _ instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂) := - coe_injective.NoZeroSmulDivisors _ rfl coe_smul + coe_injective.noZeroSMulDivisors _ rfl coe_smul end Module @@ -1089,48 +1043,46 @@ theorem coe_mul (f g : Module.EndCat R M) : ⇑(f * g) = f ∘ g := rfl #align linear_map.coe_mul LinearMap.coe_mul -instance Module.EndCat.monoid : Monoid (Module.EndCat R M) +instance _root_.Module.EndCat.monoid : Monoid (Module.EndCat R M) where mul := (· * ·) one := (1 : M →ₗ[R] M) - mul_assoc f g h := LinearMap.ext fun x => rfl + mul_assoc f g h := LinearMap.ext fun x ↦ rfl mul_one := comp_id one_mul := id_comp #align module.End.monoid Module.EndCat.monoid -instance Module.EndCat.semiring : Semiring (Module.EndCat R M) := - { AddMonoidWithOne.unary, Module.EndCat.monoid, - LinearMap.addCommMonoid with +instance _root_.Module.EndCat.semiring : Semiring (Module.EndCat R M) := + { AddMonoidWithOne.unary, Module.EndCat.monoid, LinearMap.addCommMonoid with mul := (· * ·) one := (1 : M →ₗ[R] M) - zero := 0 + zero := (0 : M →ₗ[R] M) add := (· + ·) mul_zero := comp_zero zero_mul := zero_comp - left_distrib := fun f g h => comp_add _ _ _ - right_distrib := fun f g h => add_comp _ _ _ - natCast := fun n => n • 1 - nat_cast_zero := AddMonoid.nsmul_zero _ - nat_cast_succ := fun n => (AddMonoid.nsmul_succ n 1).trans (add_comm _ _) } + left_distrib := fun _ _ _ ↦ comp_add _ _ _ + right_distrib := fun _ _ _ ↦ add_comp _ _ _ + natCast := fun n ↦ n • (1 : M →ₗ[R] M) + natCast_zero := zero_smul ℕ (1 : M →ₗ[R] M) + natCast_succ := fun n ↦ (AddMonoid.nsmul_succ n (1 : M →ₗ[R] M)).trans (add_comm _ _) } #align module.End.semiring Module.EndCat.semiring /-- See also `module.End.nat_cast_def`. -/ @[simp] -theorem Module.EndCat.nat_cast_apply (n : ℕ) (m : M) : (↑n : Module.EndCat R M) m = n • m := +theorem _root_.Module.EndCat.nat_cast_apply (n : ℕ) (m : M) : (↑n : Module.EndCat R M) m = n • m := rfl #align module.End.nat_cast_apply Module.EndCat.nat_cast_apply -instance Module.EndCat.ring : Ring (Module.EndCat R N₁) := - { Module.EndCat.semiring, - LinearMap.addCommGroup with - intCast := fun z => z • 1 - int_cast_of_nat := of_nat_zsmul _ - int_cast_neg_succ_of_nat := negSucc_zsmul _ } +instance _root_.Module.EndCat.ring : Ring (Module.EndCat R N₁) := + { Module.EndCat.semiring, LinearMap.addCommGroup with + intCast := fun z ↦ z • (1 : M →ₗ[R] M) + intCast_ofNat := of_nat_zsmul _ + intCast_negSucc := negSucc_zsmul _ } #align module.End.ring Module.EndCat.ring /-- See also `module.End.int_cast_def`. -/ @[simp] -theorem Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (↑z : Module.EndCat R N₁) m = z • m := +theorem _root_.Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (↑z : Module.EndCat R N₁) m = z • m := rfl #align module.End.int_cast_apply Module.EndCat.int_cast_apply @@ -1138,16 +1090,16 @@ section variable [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] -instance Module.EndCat.is_scalar_tower : IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := +instance _root_.Module.EndCat.is_scalar_tower : IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := ⟨smul_comp⟩ #align module.End.is_scalar_tower Module.EndCat.is_scalar_tower -instance Module.EndCat.smul_comm_class [SMul S R] [IsScalarTower S R M] : +instance _root_.Module.EndCat.smul_comm_class [SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.EndCat R M) (Module.EndCat R M) := - ⟨fun s _ _ => (comp_smul _ s _).symm⟩ + ⟨fun s _ _ ↦ (comp_smul _ s _).symm⟩ #align module.End.smul_comm_class Module.EndCat.smul_comm_class -instance Module.EndCat.smul_comm_class' [SMul S R] [IsScalarTower S R M] : +instance _root_.Module.EndCat.smul_comm_class' [SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.EndCat R M) S (Module.EndCat R M) := SMulCommClass.symm _ _ _ #align module.End.smul_comm_class' Module.EndCat.smul_comm_class' @@ -1178,7 +1130,7 @@ protected theorem smul_def (f : Module.EndCat R M) (a : M) : f • a = f a := /-- `linear_map.apply_module` is faithful. -/ instance apply_has_faithful_smul : FaithfulSMul (Module.EndCat R M) M := - ⟨fun _ _ => LinearMap.ext⟩ + ⟨fun _ _ ↦ LinearMap.ext⟩ #align linear_map.apply_has_faithful_smul LinearMap.apply_has_faithful_smul instance apply_smul_comm_class : SMulCommClass R (Module.EndCat R M) M @@ -1191,7 +1143,7 @@ instance apply_smul_comm_class' : SMulCommClass (Module.EndCat R M) R M instance apply_is_scalar_tower {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] : IsScalarTower R (Module.EndCat R M) M := - ⟨fun t f m => rfl⟩ + ⟨fun t f m ↦ rfl⟩ #align linear_map.apply_is_scalar_tower LinearMap.apply_is_scalar_tower end Endomorphisms @@ -1246,7 +1198,7 @@ def toModuleEnd : S →+* Module.EndCat R M := M with toFun := DistribMulAction.toLinearMap R M map_zero' := LinearMap.ext <| zero_smul _ - map_add' := fun f g => LinearMap.ext <| add_smul _ _ } + map_add' := fun f g ↦ LinearMap.ext <| add_smul _ _ } #align module.to_module_End Module.toModuleEnd /-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `module.End R R` induced by the right @@ -1255,9 +1207,9 @@ multiplication. -/ def moduleEndSelf : Rᵐᵒᵖ ≃+* Module.EndCat R R := { Module.toModuleEnd R R with toFun := DistribMulAction.toLinearMap R R - invFun := fun f => MulOpposite.op (f 1) + invFun := fun f ↦ MulOpposite.op (f 1) left_inv := mul_one - right_inv := fun f => LinearMap.ext_ring <| one_mul _ } + right_inv := fun f ↦ LinearMap.ext_ring <| one_mul _ } #align module.module_End_self Module.moduleEndSelf /-- The canonical (semi)ring isomorphism from `R` to `module.End Rᵐᵒᵖ R` induced by the left @@ -1266,9 +1218,9 @@ multiplication. -/ def moduleEndSelfOp : R ≃+* Module.EndCat Rᵐᵒᵖ R := { Module.toModuleEnd _ _ with toFun := DistribMulAction.toLinearMap _ _ - invFun := fun f => f 1 + invFun := fun f ↦ f 1 left_inv := mul_one - right_inv := fun f => LinearMap.ext_ring_op <| mul_one _ } + right_inv := fun f ↦ LinearMap.ext_ring_op <| mul_one _ } #align module.module_End_self_op Module.moduleEndSelfOp theorem EndCat.nat_cast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : From f9023fe354b2f7984203176a1b562ec7306c3c98 Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Tue, 17 Jan 2023 10:53:35 +0000 Subject: [PATCH 5/9] More fixing; works except for timeouts in `ext_ring_op` and `Module.EndCat.ring` --- Mathlib/Algebra/Module/LinearMap.lean | 59 +++++++++++++++++---------- 1 file changed, 37 insertions(+), 22 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 9bc0533f3aa08..81ac610558989 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -183,8 +183,6 @@ instance (priority := 100) distribMulActionHomClass [LinearMapClass F R M M₂] variable {F} (f : F) [i : SemilinearMapClass F σ M M₃] -set_option pp.all true in - theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) : c • f x = f (σ' c • x) := by simp #align semilinear_map_class.map_smul_inv SemilinearMapClass.map_smul_inv @@ -222,6 +220,10 @@ instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ -- Porting note: we don't port specialized `CoeFun` instances if there is `FunLike` instead #noalign linear_map.has_coe_to_fun +-- Porting note: adding this instance prevents a timeout in `ext_ring_op` +instance {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M (λ _ ↦ M₃) := + { AddHomClass.toFunLike with } + /-- The `DistribMulActionHom` underlying a `linear_map`. -/ def toDistribMulActionHom (f : M →ₗ[R] M₂) : DistribMulActionHom R M M₂ := { f with map_zero' := show f 0 = 0 from map_zero f } @@ -493,11 +495,18 @@ theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1 ⟨fun h ↦ h ▸ rfl, ext_ring⟩ #align linear_map.ext_ring_iff LinearMap.ext_ring_iff --- **TODO**: figure out `mul_opposite` trickery +-- *TODO*: why are you still timing out? +set_option maxHeartbeats 300000 in @[ext] -theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) : +theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : f (1 : R) = g (1 : R)) : f = g := - ext fun x ↦ by rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, ← g.map_smulₛₗ] + ext fun x ↦ by + -- Porting note: replaced the oneliner `rw` proof with a partially term-mode proof + -- because `rw` was giving "motive is type incorrect" errors + rw [← one_mul x, ← op_smul_eq_mul] + refine (f.map_smulₛₗ (MulOpposite.op x) 1).trans ?_ + rw [h] + exact (g.map_smulₛₗ (MulOpposite.op x) 1).symm #align linear_map.ext_ring_op LinearMap.ext_ring_op end @@ -528,6 +537,8 @@ def comp : M₁ →ₛₗ[σ₁₃] M₃ where -- mathport name: «expr ∘ₗ » set_option quotPrecheck false in -- Porting note: error message suggested to do this +/-- `∘ₗ` is notation for composition of two linear (not semilinear!) maps into a linear map. +This is useful when Lean is struggling to infer the `RingHomCompTriple` instance. -/ infixr:80 " ∘ₗ " => @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids @@ -636,6 +647,7 @@ namespace DistribMulActionHom variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] /-- A `DistribMulActionHom` between two modules is a linear map. -/ +@[coe] def toLinearMap (fₗ : M →+[R] M₂) : M →ₗ[R] M₂ := { fₗ with } #align distrib_mul_action_hom.to_linear_map DistribMulActionHom.toLinearMap @@ -643,10 +655,8 @@ def toLinearMap (fₗ : M →+[R] M₂) : M →ₗ[R] M₂ := instance : Coe (M →+[R] M₂) (M →ₗ[R] M₂) := ⟨toLinearMap⟩ -@[simp] -theorem to_linear_map_eq_coe (f : M →+[R] M₂) : f.toLinearMap = ↑f := - rfl -#align distrib_mul_action_hom.to_linear_map_eq_coe DistribMulActionHom.to_linear_map_eq_coe +-- Porting note: because coercions get unfolded, there is no need for this rewrite +#noalign distrib_mul_action_hom.to_linear_map_eq_coe -- Porting note: removed @[norm_cast] attribute due to error: -- norm_cast: badly shaped lemma, rhs can't start with coe @@ -815,7 +825,7 @@ theorem smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) rfl #align linear_map.smul_apply LinearMap.smul_apply -theorem coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : ⇑(a • f) = a • f := +theorem coe_smul (a : S) (f : M →ₛₗ[σ₁₂] M₂) : (a • f : M →ₛₗ[σ₁₂] M₂) = a • (f : M → M₂) := rfl #align linear_map.coe_smul LinearMap.coe_smul @@ -1073,16 +1083,22 @@ theorem _root_.Module.EndCat.nat_cast_apply (n : ℕ) (m : M) : (↑n : Module.E rfl #align module.End.nat_cast_apply Module.EndCat.nat_cast_apply +-- *TODO*: why are you still timing out? +set_option maxHeartbeats 300000 in instance _root_.Module.EndCat.ring : Ring (Module.EndCat R N₁) := { Module.EndCat.semiring, LinearMap.addCommGroup with - intCast := fun z ↦ z • (1 : M →ₗ[R] M) - intCast_ofNat := of_nat_zsmul _ + mul := (· * ·) + one := (1 : N₁ →ₗ[R] N₁) + zero := (0 : N₁ →ₗ[R] N₁) + add := (· + ·) + intCast := fun z ↦ z • (1 : N₁ →ₗ[R] N₁) + intCast_ofNat := ofNat_zsmul _ intCast_negSucc := negSucc_zsmul _ } #align module.End.ring Module.EndCat.ring /-- See also `module.End.int_cast_def`. -/ @[simp] -theorem _root_.Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (↑z : Module.EndCat R N₁) m = z • m := +theorem _root_.Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (z : Module.EndCat R N₁) m = z • m := rfl #align module.End.int_cast_apply Module.EndCat.int_cast_apply @@ -1130,7 +1146,7 @@ protected theorem smul_def (f : Module.EndCat R M) (a : M) : f • a = f a := /-- `linear_map.apply_module` is faithful. -/ instance apply_has_faithful_smul : FaithfulSMul (Module.EndCat R M) M := - ⟨fun _ _ ↦ LinearMap.ext⟩ + ⟨LinearMap.ext⟩ #align linear_map.apply_has_faithful_smul LinearMap.apply_has_faithful_smul instance apply_smul_comm_class : SMulCommClass R (Module.EndCat R M) M @@ -1143,7 +1159,7 @@ instance apply_smul_comm_class' : SMulCommClass (Module.EndCat R M) R M instance apply_is_scalar_tower {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] : IsScalarTower R (Module.EndCat R M) M := - ⟨fun t f m ↦ rfl⟩ + ⟨fun _ _ _ ↦ rfl⟩ #align linear_map.apply_is_scalar_tower LinearMap.apply_is_scalar_tower end Endomorphisms @@ -1166,7 +1182,7 @@ This is a stronger version of `distrib_mul_action.to_add_monoid_hom`. -/ def toLinearMap (s : S) : M →ₗ[R] M where toFun := SMul.smul s map_add' := smul_add s - map_smul' a b := smul_comm _ _ _ + map_smul' _ _ := smul_comm _ _ _ #align distrib_mul_action.to_linear_map DistribMulAction.toLinearMap /-- Each element of the monoid defines a module endomorphism. @@ -1177,7 +1193,7 @@ def toModuleEnd : S →* Module.EndCat R M where toFun := toLinearMap R M map_one' := LinearMap.ext <| one_smul _ - map_mul' a b := LinearMap.ext <| mul_smul _ _ + map_mul' _ _ := LinearMap.ext <| mul_smul _ _ #align distrib_mul_action.to_module_End DistribMulAction.toModuleEnd end DistribMulAction @@ -1198,7 +1214,7 @@ def toModuleEnd : S →+* Module.EndCat R M := M with toFun := DistribMulAction.toLinearMap R M map_zero' := LinearMap.ext <| zero_smul _ - map_add' := fun f g ↦ LinearMap.ext <| add_smul _ _ } + map_add' := fun _ _ ↦ LinearMap.ext <| add_smul _ _ } #align module.to_module_End Module.toModuleEnd /-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `module.End R R` induced by the right @@ -1209,7 +1225,7 @@ def moduleEndSelf : Rᵐᵒᵖ ≃+* Module.EndCat R R := toFun := DistribMulAction.toLinearMap R R invFun := fun f ↦ MulOpposite.op (f 1) left_inv := mul_one - right_inv := fun f ↦ LinearMap.ext_ring <| one_mul _ } + right_inv := fun _ ↦ LinearMap.ext_ring <| one_mul _ } #align module.module_End_self Module.moduleEndSelf /-- The canonical (semi)ring isomorphism from `R` to `module.End Rᵐᵒᵖ R` induced by the left @@ -1220,7 +1236,7 @@ def moduleEndSelfOp : R ≃+* Module.EndCat Rᵐᵒᵖ R := toFun := DistribMulAction.toLinearMap _ _ invFun := fun f ↦ f 1 left_inv := mul_one - right_inv := fun f ↦ LinearMap.ext_ring_op <| mul_one _ } + right_inv := fun _ ↦ LinearMap.ext_ring_op <| mul_one _ } #align module.module_End_self_op Module.moduleEndSelfOp theorem EndCat.nat_cast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : @@ -1229,9 +1245,8 @@ theorem EndCat.nat_cast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : #align module.End.nat_cast_def Module.EndCat.nat_cast_def theorem EndCat.int_cast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] : - (↑z : Module.EndCat R N₁) = Module.toModuleEnd R N₁ z := + (z : Module.EndCat R N₁) = Module.toModuleEnd R N₁ z := rfl #align module.End.int_cast_def Module.EndCat.int_cast_def end Module - From 7946a03a305c25bc2b7b607aa6b84f616730bc3a Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Tue, 17 Jan 2023 11:19:10 +0000 Subject: [PATCH 6/9] Revert expansion, now it works again for some reason --- Mathlib/Algebra/Module/LinearMap.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 81ac610558989..ee409ba35e6e7 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -817,8 +817,7 @@ instance : SMul S (M →ₛₗ[σ₁₂] M₂) := ⟨fun a f ↦ { toFun := a • (f : M → M₂) map_add' := fun x y ↦ by simp only [Pi.smul_apply, f.map_add, smul_add] - -- Porting note: **TODO** `simp` did not pick up `smul_comm` - map_smul' := fun c x ↦ by simp only [Pi.smul_apply, map_smulₛₗ]; rw [← smul_comm] }⟩ + map_smul' := fun c x ↦ by simp [Pi.smul_apply, smul_comm] }⟩ @[simp] theorem smul_apply (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) : (a • f) x = a • f x := From 901f7dc06e87ec7c7473d52cefaef30e583d6569 Mon Sep 17 00:00:00 2001 From: qawbecrdtey Date: Fri, 20 Jan 2023 12:21:30 +0000 Subject: [PATCH 7/9] <= 100 --- Mathlib/Algebra/Module/LinearMap.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index ee409ba35e6e7..c196fc1dbd39e 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -1105,7 +1105,8 @@ section variable [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] -instance _root_.Module.EndCat.is_scalar_tower : IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := +instance _root_.Module.EndCat.is_scalar_tower : + IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := ⟨smul_comp⟩ #align module.End.is_scalar_tower Module.EndCat.is_scalar_tower From d27c19c4f6db68c4871c56148bf4f84a25dfa33d Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Fri, 20 Jan 2023 14:08:42 +0000 Subject: [PATCH 8/9] Fix names --- Mathlib/Algebra/Module/LinearMap.lean | 216 +++++++++++++------------- 1 file changed, 108 insertions(+), 108 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index c196fc1dbd39e..d570318396fce 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -20,19 +20,19 @@ import Mathlib.Algebra.Ring.CompTypeclasses In this file we define -* `linear_map σ M M₂`, `M →ₛₗ[σ] M₂` : a semilinear map between two `module`s. Here, - `σ` is a `ring_hom` from `R` to `R₂` and an `f : M →ₛₗ[σ] M₂` satisfies - `f (c • x) = (σ c) • (f x)`. We recover plain linear maps by choosing `σ` to be `ring_hom.id R`. +* `LinearMap σ M M₂`, `M →ₛₗ[σ] M₂` : a semilinear map between two `Module`s. Here, + `σ` is a `RingHom` from `R` to `R₂` and an `f : M →ₛₗ[σ] M₂` satisfies + `f (c • x) = (σ c) • (f x)`. We recover plain linear maps by choosing `σ` to be `RingHom.id R`. This is denoted by `M →ₗ[R] M₂`. We also add the notation `M →ₗ⋆[R] M₂` for star-linear maps. -* `is_linear_map R f` : predicate saying that `f : M → M₂` is a linear map. (Note that this +* `IsLinearMap 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: +We then provide `LinearMap` with the following instances: -* `linear_map.add_comm_monoid` and `linear_map.add_comm_group`: the elementwise addition structures +* `LinearMap.addCommMonoid` and `LinearMap.AddCommGroup`: the elementwise addition structures corresponding to addition in the codomain -* `linear_map.distrib_mul_action` and `linear_map.module`: the elementwise scalar action structures +* `LinearMap.distribMulAction` and `LinearMap.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. @@ -40,8 +40,8 @@ We then provide `linear_map` with the following instances: ## 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`. +`RingHomCompTriple`, `RingHomInvPair` and `RingHomSurjective` from +`Mathlib.Algebra.Ring.CompTypeclasses`. ## Notation @@ -50,7 +50,7 @@ To ensure that composition works smoothly for semilinear maps, we use the typecl ## TODO -* Parts of this file have not yet been generalized to semilinear maps (i.e. `compatible_smul`) +* Parts of this file have not yet been generalized to semilinear maps (i.e. `CompatibleSMul`) ## Tags @@ -75,9 +75,9 @@ variable {M : Type _} {M₁ : Type _} {M₂ : Type _} {M₃ : Type _} variable {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 -property. A bundled version is available with `linear_map`, and should be favored over -`is_linear_map` most of the time. -/ +`f (x + y) = f x + f y` and `f (c • x) = c • f x`. The predicate `IsLinearMap R f` asserts this +property. A bundled version is available with `LinearMap`, and should be favored over +`IsLinearMap` most of the time. -/ structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M → M₂) : Prop where /-- A linear map preserves addition. -/ @@ -90,19 +90,19 @@ section /-- 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 +`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ 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. -/ +`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear +maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. -/ structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type _) (M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHom M M₂ where /-- A linear map preserves scalar multiplication. We prefer the spelling `_root_.map_smul` instead. -/ map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x -#align linear_map LinearMap +#align LinearMap LinearMap -/-- The `add_hom` underlying a `linear_map`. -/ +/-- The `add_hom` underlying a `LinearMap`. -/ add_decl_doc LinearMap.toAddHom -- mathport name: «expr →ₛₗ[ ] » @@ -117,9 +117,9 @@ notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂ -- mathport name: «expr →ₗ⋆[ ] » notation:25 M " →ₗ⋆[" R:25 "] " M₂:0 => LinearMap (starRingEnd R) M M₂ -/-- `semilinear_map_class F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`. +/-- `SemilinearMapClass F σ M M₂` asserts `F` is a type of bundled `σ`-semilinear maps `M → M₂`. -See also `linear_map_class F R M M₂` for the case where `σ` is the identity map on `R`. +See also `LinearMapClass 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 @@ -142,9 +142,9 @@ export SemilinearMapClass (map_smulₛₗ) attribute [simp] map_smulₛₗ -/-- `linear_map_class F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`. +/-- `LinearMapClass F R M M₂` asserts `F` is a type of bundled `R`-linear maps `M → M₂`. -This is an abbreviation for `semilinear_map_class F (ring_hom.id R) M M₂`. +This is an abbreviation for `semilinear_map_class F (RingHom.id R) M M₂`. -/ abbrev LinearMapClass (F : Type _) (R M M₂ : outParam (Type _)) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] := @@ -218,13 +218,13 @@ instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ map_smulₛₗ := LinearMap.map_smul' -- Porting note: we don't port specialized `CoeFun` instances if there is `FunLike` instead -#noalign linear_map.has_coe_to_fun +#noalign LinearMap.has_coe_to_fun -- Porting note: adding this instance prevents a timeout in `ext_ring_op` instance {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M (λ _ ↦ M₃) := { AddHomClass.toFunLike with } -/-- The `DistribMulActionHom` underlying a `linear_map`. -/ +/-- The `DistribMulActionHom` underlying a `LinearMap`. -/ def toDistribMulActionHom (f : M →ₗ[R] M₂) : DistribMulActionHom R M M₂ := { f with map_zero' := show f 0 = 0 from map_zero f } #align linear_map.to_distrib_mul_action_hom LinearMap.toDistribMulActionHom @@ -239,7 +239,7 @@ theorem ext {f g : M →ₛₗ[σ] M₃} (h : ∀ x, f x = g x) : f = g := FunLike.ext f g h #align linear_map.ext LinearMap.ext -/-- Copy of a `linear_map` with a new `toFun` equal to the old one. Useful to fix definitional +/-- Copy of a `LinearMap` with a new `toFun` equal to the old one. Useful to fix definitional equalities. -/ protected def copy (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f) : M →ₛₗ[σ] M₃ where @@ -271,7 +271,7 @@ theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) : rfl #align linear_map.coe_mk LinearMap.coe_mk -/-- Identity map as a `linear_map` -/ +/-- Identity map as a `LinearMap` -/ def id : M →ₗ[R] M := { DistribMulActionHom.id R with toFun := _root_.id } #align linear_map.id LinearMap.id @@ -337,7 +337,7 @@ protected theorem map_zero : f 0 = 0 := map_zero f #align linear_map.map_zero LinearMap.map_zero --- Porting note: `simp` wasn't picking up `map_smulₛₗ` for `linear_map`s without specifying +-- Porting note: `simp` wasn't picking up `map_smulₛₗ` for `LinearMap`s without specifying -- `map_smulₛₗ f`, so we marked this as `@[simp]` in Mathlib3. -- For Mathlib4, let's try without the `@[simp]` attribute and hope it won't need to be re-enabled. protected theorem map_smulₛₗ (c : R) (x : M) : f (c • x) = σ c • f x := @@ -403,30 +403,30 @@ end Pointwise variable (M M₂) -/-- A typeclass for `has_smul` 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 +/-- A typeclass for `has_smul` structures which can be moved through a `LinearMap`. +This typeclass is generated automatically from a `IsScalarTower` instance, but exists so that +we can also add an instance for `AddCommGroup.intModule`, allowing `z •` to be moved even if `R` does not support negation. -/ -class CompatibleSmul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] +class CompatibleSMul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] where /-- Scalar multiplication by `R` of `M` can be moved through linear maps. -/ map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x -#align linear_map.compatible_smul LinearMap.CompatibleSmul +#align linear_map.compatible_smul LinearMap.CompatibleSMul variable {M M₂} -instance (priority := 100) IsScalarTower.compatibleSmul {R S : Type _} [Semiring S] [SMul R S] +instance (priority := 100) IsScalarTower.compatibleSMul {R S : Type _} [Semiring S] [SMul R S] [SMul R M] [Module S M] [IsScalarTower R S M] [SMul R M₂] [Module S M₂] [IsScalarTower R S M₂] : - CompatibleSmul M M₂ R S := + CompatibleSMul M M₂ R S := ⟨fun fₗ c x ↦ by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]⟩ -#align linear_map.is_scalar_tower.compatible_smul LinearMap.IsScalarTower.compatibleSmul +#align linear_map.is_scalar_tower.compatible_smul LinearMap.IsScalarTower.compatibleSMul @[simp] theorem map_smul_of_tower {R S : Type _} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] - [Module S M₂] [CompatibleSmul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : + [Module S M₂] [CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) : fₗ (c • x) = c • fₗ x := - CompatibleSmul.map_smul fₗ c x + CompatibleSMul.map_smul fₗ c x #align linear_map.map_smul_of_tower LinearMap.map_smul_of_tower /-- convert a linear map to an additive map -/ @@ -437,20 +437,20 @@ def toAddMonoidHom : M →+ M₃ where #align linear_map.to_add_monoid_hom LinearMap.toAddMonoidHom @[simp] -theorem to_add_monoid_hom_coe : ⇑f.toAddMonoidHom = f := +theorem toAddMonoidHom_coe : ⇑f.toAddMonoidHom = f := rfl -#align linear_map.to_add_monoid_hom_coe LinearMap.to_add_monoid_hom_coe +#align linear_map.to_add_monoid_hom_coe LinearMap.toAddMonoidHom_coe section RestrictScalars variable (R) -variable [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] +variable [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] /-- 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`. -/ +See also `LinearMap.map_smul_of_tower`. -/ def restrictScalars (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂ where toFun := fₗ @@ -459,31 +459,31 @@ def restrictScalars (fₗ : M →ₗ[S] M₂) : M →ₗ[R] M₂ #align linear_map.restrict_scalars LinearMap.restrictScalars @[simp] -theorem coe_restrict_scalars (fₗ : M →ₗ[S] M₂) : ⇑(restrictScalars R fₗ) = fₗ := +theorem coe_restrictScalars (fₗ : M →ₗ[S] M₂) : ⇑(restrictScalars R fₗ) = fₗ := rfl -#align linear_map.coe_restrict_scalars LinearMap.coe_restrict_scalars +#align linear_map.coe_restrict_scalars LinearMap.coe_restrictScalars -theorem restrict_scalars_apply (fₗ : M →ₗ[S] M₂) (x) : restrictScalars R fₗ x = fₗ x := +theorem restrictScalars_apply (fₗ : M →ₗ[S] M₂) (x) : restrictScalars R fₗ x = fₗ x := rfl -#align linear_map.restrict_scalars_apply LinearMap.restrict_scalars_apply +#align linear_map.restrict_scalars_apply LinearMap.restrictScalars_apply -theorem restrict_scalars_injective : +theorem restrictScalars_injective : Function.Injective (restrictScalars R : (M →ₗ[S] M₂) → M →ₗ[R] M₂) := fun _ _ h ↦ ext (LinearMap.congr_fun h : _) -#align linear_map.restrict_scalars_injective LinearMap.restrict_scalars_injective +#align linear_map.restrict_scalars_injective LinearMap.restrictScalars_injective @[simp] -theorem restrict_scalars_inj (fₗ gₗ : M →ₗ[S] M₂) : +theorem restrictScalars_inj (fₗ gₗ : M →ₗ[S] M₂) : fₗ.restrictScalars R = gₗ.restrictScalars R ↔ fₗ = gₗ := - (restrict_scalars_injective R).eq_iff -#align linear_map.restrict_scalars_inj LinearMap.restrict_scalars_inj + (restrictScalars_injective R).eq_iff +#align linear_map.restrict_scalars_inj LinearMap.restrictScalars_inj end RestrictScalars -theorem to_add_monoid_hom_injective : +theorem toAddMonoidHom_injective : Function.Injective (toAddMonoidHom : (M →ₛₗ[σ] M₃) → M →+ M₃) := fun fₗ gₗ h ↦ ext <| (FunLike.congr_fun h : ∀ x, fₗ.toAddMonoidHom x = gₗ.toAddMonoidHom x) -#align linear_map.to_add_monoid_hom_injective LinearMap.to_add_monoid_hom_injective +#align linear_map.to_add_monoid_hom_injective LinearMap.toAddMonoidHom_injective /-- If two `σ`-linear maps from `R` are equal on `1`, then they are equal. -/ @[ext] @@ -511,7 +511,7 @@ theorem ext_ring_op {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M₃} (h : end -/-- Interpret a `ring_hom` `f` as an `f`-semilinear map. -/ +/-- Interpret a `RingHom` `f` as an `f`-semilinear map. -/ @[simps] def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S := { f with @@ -610,19 +610,19 @@ protected theorem map_sub (x y : M) : f (x - y) = f x - f y := map_sub f x y #align linear_map.map_sub LinearMap.map_sub -instance CompatibleSmul.intModule {S : Type _} [Semiring S] [Module S M] [Module S M₂] : - CompatibleSmul M M₂ ℤ S := +instance CompatibleSMul.intModule {S : Type _} [Semiring S] [Module S M] [Module S M₂] : + CompatibleSMul M M₂ ℤ S := ⟨fun fₗ c x ↦ by induction c using Int.induction_on case hz => simp case hp n ih => simp [add_smul, ih] case hn n ih => simp [sub_smul, ih]⟩ -#align linear_map.compatible_smul.int_module LinearMap.CompatibleSmul.intModule +#align linear_map.compatible_smul.int_module LinearMap.CompatibleSMul.intModule -instance CompatibleSmul.units {R S : Type _} [Monoid R] [MulAction R M] [MulAction R M₂] - [Semiring S] [Module S M] [Module S M₂] [CompatibleSmul M M₂ R S] : CompatibleSmul M M₂ Rˣ S := - ⟨fun fₗ c x ↦ (CompatibleSmul.map_smul fₗ (c : R) x : _)⟩ -#align linear_map.compatible_smul.units LinearMap.CompatibleSmul.units +instance CompatibleSMul.units {R S : Type _} [Monoid R] [MulAction R M] [MulAction R M₂] + [Semiring S] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] : CompatibleSMul M M₂ Rˣ S := + ⟨fun fₗ c x ↦ (CompatibleSMul.map_smul fₗ (c : R) x : _)⟩ +#align linear_map.compatible_smul.units LinearMap.CompatibleSMul.units end AddCommGroup @@ -661,15 +661,15 @@ instance : Coe (M →+[R] M₂) (M →ₗ[R] M₂) := -- Porting note: removed @[norm_cast] attribute due to error: -- norm_cast: badly shaped lemma, rhs can't start with coe @[simp] -theorem coe_to_linear_map (f : M →+[R] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f := +theorem coe_toLinearMap (f : M →+[R] M₂) : ((f : M →ₗ[R] M₂) : M → M₂) = f := rfl -#align distrib_mul_action_hom.coe_to_linear_map DistribMulActionHom.coe_to_linear_map +#align distrib_mul_action_hom.coe_to_linear_map DistribMulActionHom.coe_toLinearMap -theorem to_linear_map_injective {f g : M →+[R] M₂} (h : (f : M →ₗ[R] M₂) = (g : M →ₗ[R] M₂)) : +theorem toLinearMap_injective {f g : M →+[R] M₂} (h : (f : M →ₗ[R] M₂) = (g : M →ₗ[R] M₂)) : f = g := by ext m exact LinearMap.congr_fun h m -#align distrib_mul_action_hom.to_linear_map_injective DistribMulActionHom.to_linear_map_injective +#align distrib_mul_action_hom.to_linear_map_injective DistribMulActionHom.toLinearMap_injective end DistribMulActionHom @@ -680,7 +680,7 @@ section AddCommMonoid variable [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] variable [Module R M] [Module R M₂] -/-- Convert an `is_linear_map` predicate to a `linear_map` -/ +/-- Convert an `IsLinearMap` predicate to a `LinearMap` -/ def mk' (f : M → M₂) (H : IsLinearMap R f) : M →ₗ[R] M₂ where toFun := f @@ -693,18 +693,18 @@ theorem mk'_apply {f : M → M₂} (H : IsLinearMap R f) (x : M) : mk' f H x = f rfl #align is_linear_map.mk'_apply IsLinearMap.mk'_apply -theorem isLinearMapSmul {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : +theorem isLinearMap_smul {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) : IsLinearMap R fun z : M ↦ c • z := by refine' IsLinearMap.mk (smul_add c) _ intro _ _ simp only [smul_smul, mul_comm] -#align is_linear_map.is_linear_map_smul IsLinearMap.isLinearMapSmul +#align is_linear_map.is_linear_map_smul IsLinearMap.isLinearMap_smul -theorem isLinearMapSmul' {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : +theorem isLinearMap_smul' {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) : IsLinearMap R fun c : R ↦ c • a := IsLinearMap.mk (fun x y ↦ add_smul x y a) fun x y ↦ mul_smul x y a -#align is_linear_map.is_linear_map_smul' IsLinearMap.isLinearMapSmul' +#align is_linear_map.is_linear_map_smul' IsLinearMap.isLinearMap_smul' variable {f : M → M₂} (lin : IsLinearMap R f) @@ -719,9 +719,9 @@ section AddCommGroup variable [Semiring R] [AddCommGroup M] [AddCommGroup M₂] variable [Module R M] [Module R M₂] -theorem isLinearMapNeg : IsLinearMap R fun z : M ↦ -z := +theorem isLinearMap_neg : IsLinearMap R fun z : M ↦ -z := IsLinearMap.mk neg_add fun x y ↦ (smul_neg x y).symm -#align is_linear_map.is_linear_map_neg IsLinearMap.isLinearMapNeg +#align is_linear_map.is_linear_map_neg IsLinearMap.isLinearMap_neg variable {f : M → M₂} (lin : IsLinearMap R f) @@ -751,13 +751,13 @@ def AddMonoidHom.toNatLinearMap [AddCommMonoid M] [AddCommMonoid M₂] (f : M map_smul' := map_nsmul f #align add_monoid_hom.to_nat_linear_map AddMonoidHom.toNatLinearMap -theorem AddMonoidHom.to_nat_linear_map_injective [AddCommMonoid M] [AddCommMonoid M₂] : +theorem AddMonoidHom.toNatLinearMap_injective [AddCommMonoid M] [AddCommMonoid M₂] : Function.Injective (@AddMonoidHom.toNatLinearMap M M₂ _ _) := by intro f g h ext x exact LinearMap.congr_fun h x -#align add_monoid_hom.to_nat_linear_map_injective AddMonoidHom.to_nat_linear_map_injective +#align add_monoid_hom.to_nat_linear_map_injective AddMonoidHom.toNatLinearMap_injective /-- Reinterpret an additive homomorphism as a `ℤ`-linear map. -/ def AddMonoidHom.toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : M →ₗ[ℤ] M₂ @@ -767,19 +767,19 @@ def AddMonoidHom.toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ map_smul' := map_zsmul f #align add_monoid_hom.to_int_linear_map AddMonoidHom.toIntLinearMap -theorem AddMonoidHom.to_int_linear_map_injective [AddCommGroup M] [AddCommGroup M₂] : +theorem AddMonoidHom.toIntLinearMap_injective [AddCommGroup M] [AddCommGroup M₂] : Function.Injective (@AddMonoidHom.toIntLinearMap M M₂ _ _) := by intro f g h ext x exact LinearMap.congr_fun h x -#align add_monoid_hom.to_int_linear_map_injective AddMonoidHom.to_int_linear_map_injective +#align add_monoid_hom.to_int_linear_map_injective AddMonoidHom.toIntLinearMap_injective @[simp] -theorem AddMonoidHom.coe_to_int_linear_map [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : +theorem AddMonoidHom.coe_toIntLinearMap [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) : ⇑f.toIntLinearMap = f := rfl -#align add_monoid_hom.coe_to_int_linear_map AddMonoidHom.coe_to_int_linear_map +#align add_monoid_hom.coe_to_int_linear_map AddMonoidHom.coe_toIntLinearMap /-- Reinterpret an additive homomorphism as a `ℚ`-linear map. -/ def AddMonoidHom.toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] @@ -787,19 +787,19 @@ def AddMonoidHom.toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M { f with map_smul' := map_rat_smul f } #align add_monoid_hom.to_rat_linear_map AddMonoidHom.toRatLinearMap -theorem AddMonoidHom.to_rat_linear_map_injective [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] +theorem AddMonoidHom.toRatLinearMap_injective [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] : Function.Injective (@AddMonoidHom.toRatLinearMap M M₂ _ _ _ _) := by intro f g h ext x exact LinearMap.congr_fun h x -#align add_monoid_hom.to_rat_linear_map_injective AddMonoidHom.to_rat_linear_map_injective +#align add_monoid_hom.to_rat_linear_map_injective AddMonoidHom.toRatLinearMap_injective @[simp] -theorem AddMonoidHom.coe_to_rat_linear_map [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] +theorem AddMonoidHom.coe_toRatLinearMap [AddCommGroup M] [Module ℚ M] [AddCommGroup M₂] [Module ℚ M₂] (f : M →+ M₂) : ⇑f.toRatLinearMap = f := rfl -#align add_monoid_hom.coe_to_rat_linear_map AddMonoidHom.coe_to_rat_linear_map +#align add_monoid_hom.coe_to_rat_linear_map AddMonoidHom.coe_toRatLinearMap namespace LinearMap @@ -986,7 +986,7 @@ theorem smul_comp (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛ -- TODO: generalize this to semilinear maps theorem comp_smul [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] - [SMulCommClass R S M₃] [CompatibleSmul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : + [SMulCommClass R S M₃] [CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • g.comp f := ext fun _ ↦ g.map_smul_of_tower _ _ #align linear_map.comp_smul LinearMap.comp_smul @@ -1012,7 +1012,7 @@ end Actions /-! ### Monoid structure of endomorphisms -Lemmas about `pow` such as `linear_map.pow_apply` appear in later files. +Lemmas about `pow` such as `LinearMap.pow_apply` appear in later files. -/ @@ -1078,9 +1078,9 @@ instance _root_.Module.EndCat.semiring : Semiring (Module.EndCat R M) := /-- See also `module.End.nat_cast_def`. -/ @[simp] -theorem _root_.Module.EndCat.nat_cast_apply (n : ℕ) (m : M) : (↑n : Module.EndCat R M) m = n • m := +theorem _root_.Module.EndCat.natCast_apply (n : ℕ) (m : M) : (↑n : Module.EndCat R M) m = n • m := rfl -#align module.End.nat_cast_apply Module.EndCat.nat_cast_apply +#align module.End.nat_cast_apply Module.EndCat.natCast_apply -- *TODO*: why are you still timing out? set_option maxHeartbeats 300000 in @@ -1097,28 +1097,28 @@ instance _root_.Module.EndCat.ring : Ring (Module.EndCat R N₁) := /-- See also `module.End.int_cast_def`. -/ @[simp] -theorem _root_.Module.EndCat.int_cast_apply (z : ℤ) (m : N₁) : (z : Module.EndCat R N₁) m = z • m := +theorem _root_.Module.EndCat.intCast_apply (z : ℤ) (m : N₁) : (z : Module.EndCat R N₁) m = z • m := rfl -#align module.End.int_cast_apply Module.EndCat.int_cast_apply +#align module.End.int_cast_apply Module.EndCat.intCast_apply section variable [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] -instance _root_.Module.EndCat.is_scalar_tower : +instance _root_.Module.EndCat.isScalarTower : IsScalarTower S (Module.EndCat R M) (Module.EndCat R M) := ⟨smul_comp⟩ -#align module.End.is_scalar_tower Module.EndCat.is_scalar_tower +#align module.End.is_scalar_tower Module.EndCat.isScalarTower -instance _root_.Module.EndCat.smul_comm_class [SMul S R] [IsScalarTower S R M] : +instance _root_.Module.EndCat.smulCommClass [SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.EndCat R M) (Module.EndCat R M) := ⟨fun s _ _ ↦ (comp_smul _ s _).symm⟩ -#align module.End.smul_comm_class Module.EndCat.smul_comm_class +#align module.End.smul_comm_class Module.EndCat.smulCommClass -instance _root_.Module.EndCat.smul_comm_class' [SMul S R] [IsScalarTower S R M] : +instance _root_.Module.EndCat.smulCommClass' [SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.EndCat R M) S (Module.EndCat R M) := SMulCommClass.symm _ _ _ -#align module.End.smul_comm_class' Module.EndCat.smul_comm_class' +#align module.End.smul_comm_class' Module.EndCat.smulCommClass' end @@ -1145,22 +1145,22 @@ protected theorem smul_def (f : Module.EndCat R M) (a : M) : f • a = f a := #align linear_map.smul_def LinearMap.smul_def /-- `linear_map.apply_module` is faithful. -/ -instance apply_has_faithful_smul : FaithfulSMul (Module.EndCat R M) M := +instance apply_faithfulSMul : FaithfulSMul (Module.EndCat R M) M := ⟨LinearMap.ext⟩ -#align linear_map.apply_has_faithful_smul LinearMap.apply_has_faithful_smul +#align linear_map.apply_has_faithful_smul LinearMap.apply_faithfulSMul -instance apply_smul_comm_class : SMulCommClass R (Module.EndCat R M) M +instance apply_smulCommClass : SMulCommClass R (Module.EndCat R M) M where smul_comm r e m := (e.map_smul r m).symm -#align linear_map.apply_smul_comm_class LinearMap.apply_smul_comm_class +#align linear_map.apply_smul_comm_class LinearMap.apply_smulCommClass -instance apply_smul_comm_class' : SMulCommClass (Module.EndCat R M) R M +instance apply_smulCommClass' : SMulCommClass (Module.EndCat R M) R M where smul_comm := LinearMap.map_smul -#align linear_map.apply_smul_comm_class' LinearMap.apply_smul_comm_class' +#align linear_map.apply_smul_comm_class' LinearMap.apply_smulCommClass' -instance apply_is_scalar_tower {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] : +instance apply_isScalarTower {R M : Type _} [CommSemiring R] [AddCommMonoid M] [Module R M] : IsScalarTower R (Module.EndCat R M) M := ⟨fun _ _ _ ↦ rfl⟩ -#align linear_map.apply_is_scalar_tower LinearMap.apply_is_scalar_tower +#align linear_map.apply_is_scalar_tower LinearMap.apply_isScalarTower end Endomorphisms @@ -1177,7 +1177,7 @@ variable [Monoid S] [DistribMulAction S M] [SMulCommClass S R M] /-- Each element of the monoid defines a linear map. -This is a stronger version of `distrib_mul_action.to_add_monoid_hom`. -/ +This is a stronger version of `DistribMulAction.to_add_monoid_hom`. -/ @[simps] def toLinearMap (s : S) : M →ₗ[R] M where toFun := SMul.smul s @@ -1187,7 +1187,7 @@ def toLinearMap (s : S) : M →ₗ[R] M where /-- Each element of the monoid defines a module endomorphism. -This is a stronger version of `distrib_mul_action.to_add_monoid_End`. -/ +This is a stronger version of `DistribMulAction.to_add_monoid_End`. -/ @[simps] def toModuleEnd : S →* Module.EndCat R M where @@ -1206,7 +1206,7 @@ variable [Semiring S] [Module S M] [SMulCommClass S R M] /-- Each element of the semiring defines a module endomorphism. -This is a stronger version of `distrib_mul_action.to_module_End`. -/ +This is a stronger version of `DistribMulAction.to_module_End`. -/ @[simps] def toModuleEnd : S →+* Module.EndCat R M := { @@ -1239,14 +1239,14 @@ def moduleEndSelfOp : R ≃+* Module.EndCat Rᵐᵒᵖ R := right_inv := fun _ ↦ LinearMap.ext_ring_op <| mul_one _ } #align module.module_End_self_op Module.moduleEndSelfOp -theorem EndCat.nat_cast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : +theorem EndCat.natCast_def (n : ℕ) [AddCommMonoid N₁] [Module R N₁] : (↑n : Module.EndCat R N₁) = Module.toModuleEnd R N₁ n := rfl -#align module.End.nat_cast_def Module.EndCat.nat_cast_def +#align module.End.nat_cast_def Module.EndCat.natCast_def -theorem EndCat.int_cast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] : +theorem EndCat.intCast_def (z : ℤ) [AddCommGroup N₁] [Module R N₁] : (z : Module.EndCat R N₁) = Module.toModuleEnd R N₁ z := rfl -#align module.End.int_cast_def Module.EndCat.int_cast_def +#align module.End.int_cast_def Module.EndCat.intCast_def end Module From da3d315775b539da4fcad60e49fec4fd51406436 Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Fri, 20 Jan 2023 15:08:28 +0000 Subject: [PATCH 9/9] Fix naming convention Co-authored-by: Johan Commelin --- Mathlib/Algebra/Module/LinearMap.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index d570318396fce..cd14878b19bcc 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -299,9 +299,9 @@ variable (σ : R →+* S) variable (fₗ gₗ : M →ₗ[R] M₂) (f g : M →ₛₗ[σ] M₃) -theorem is_linear : IsLinearMap R fₗ := +theorem isLinear : IsLinearMap R fₗ := ⟨fₗ.map_add', fₗ.map_smul'⟩ -#align linear_map.is_linear LinearMap.is_linear +#align linear_map.is_linear LinearMap.isLinear variable {fₗ gₗ f g σ}