From 13a104d9f0dae261dc52c75065f91de9a8d54ea1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 2 Nov 2020 18:45:02 +0000 Subject: [PATCH] chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to its own file (#4873) This makes the layout of files about `dfinsupp` resemble those of `finsupp` a little better. This also: * Renames type arguments to match the names of those in finsupp * Adjusts argument explicitness to match those in finsupp * Adds `dfinsupp.lapply` to match `finsupp.lapply` --- src/data/dfinsupp.lean | 50 ---------- src/linear_algebra/dfinsupp.lean | 107 ++++++++++++++++++++++ src/linear_algebra/direct_sum_module.lean | 15 ++- src/linear_algebra/finsupp.lean | 2 +- 4 files changed, 114 insertions(+), 60 deletions(-) create mode 100644 src/linear_algebra/dfinsupp.lean diff --git a/src/data/dfinsupp.lean b/src/data/dfinsupp.lean index 35810fb2c7b79..83c3116ed84e2 100644 --- a/src/data/dfinsupp.lean +++ b/src/data/dfinsupp.lean @@ -7,7 +7,6 @@ import algebra.module.linear_map import algebra.module.pi import algebra.big_operators.basic import data.set.finite -import linear_algebra.basic /-! # Dependent functions with finite support @@ -504,35 +503,6 @@ ext $ λ i, by simp only [smul_apply, mk_apply]; split_ifs; [refl, rw smul_zero] single i (c • x) = c • single i x := ext $ λ i, by simp only [smul_apply, single_apply]; split_ifs; [cases h, rw smul_zero]; refl -variable β -/-- `dfinsupp.mk` as a `linear_map`. -/ -def lmk (s : finset ι) : (Π i : (↑s : set ι), β i.1) →ₗ[γ] Π₀ i, β i := -⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul γ x]⟩ - -/-- `dfinsupp.single` as a `linear_map` -/ -def lsingle (i) : β i →ₗ[γ] Π₀ i, β i := -⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩ -variable {β} - -/-- Two `R`-linear maps from `Π₀ i, β i` which agree on each `single i x` agree everywhere. -/ -lemma lhom_ext {δ : Type*} [add_comm_monoid δ] [semimodule γ δ] ⦃φ ψ : (Π₀ i, β i) →ₗ[γ] δ⦄ - (h : ∀ i x, φ (single i x) = ψ (single i x)) : - φ = ψ := -linear_map.to_add_monoid_hom_injective $ add_hom_ext h - -/-- Two `R`-linear maps from `Π₀ i, β i` which agree on each `single i x` agree everywhere. - -We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)` -so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these -maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/ -@[ext] lemma lhom_ext' {δ : Type*} [add_comm_monoid δ] [semimodule γ δ] ⦃φ ψ : (Π₀ i, β i) →ₗ[γ] δ⦄ - (h : ∀ i, φ.comp (lsingle β γ i) = ψ.comp (lsingle β γ i)) : - φ = ψ := -lhom_ext γ $ λ i, linear_map.congr_fun (h i) - -@[simp] lemma lmk_apply {s : finset ι} {x} : lmk β γ s x = mk s x := rfl - -@[simp] lemma lsingle_apply {i : ι} {x : β i} : lsingle β γ i x = single i x := rfl end section support_basic @@ -952,26 +922,6 @@ begin exact this, end -/-- The `dfinsupp` version of `finsupp.lsum`,-/ -@[simps apply symm_apply] -def lsum {R : Type*} [semiring R] [Π i, add_comm_monoid (β i)] [Π i, semimodule R (β i)] - [add_comm_monoid γ] [semimodule R γ] : - (Π i, β i →ₗ[R] γ) ≃+ ((Π₀ i, β i) →ₗ[R] γ) := -{ to_fun := λ F, { - to_fun := sum_add_hom (λ i, (F i).to_add_monoid_hom), - map_add' := (lift_add_hom (λ i, (F i).to_add_monoid_hom)).map_add, - map_smul' := λ c f, by { - apply dfinsupp.induction f, - { rw [smul_zero, add_monoid_hom.map_zero, smul_zero] }, - { intros a b f ha hb hf, - rw [smul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, smul_add, hf, ←single_smul, - sum_add_hom_single, sum_add_hom_single, linear_map.to_add_monoid_hom_coe, - linear_map.map_smul], } } }, - inv_fun := λ F i, F.comp (lsingle β R i), - left_inv := λ F, by { ext x y, simp }, - right_inv := λ F, by { ext x y, simp }, - map_add' := λ F G, by { ext x y, simp } } - @[to_additive] lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)] [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p] diff --git a/src/linear_algebra/dfinsupp.lean b/src/linear_algebra/dfinsupp.lean new file mode 100644 index 0000000000000..79c3edefc2503 --- /dev/null +++ b/src/linear_algebra/dfinsupp.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2018 Kenny Lau. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Johannes Hölzl, Kenny Lau +-/ +import data.dfinsupp +import linear_algebra.basic + +/-! +# Properties of the semimodule `Π₀ i, M i` + +Given an indexed collection of `R`-semimodules `M i`, the `R`-semimodule structure on `Π₀ i, M i` +is defined in `data.dfinsupp`. + +In this file we define `linear_map` versions of various maps: + +* `dfinsupp.lsingle a : M →ₗ[R] Π₀ i, M i`: `dfinsupp.single a` as a linear map; + +* `dfinsupp.lmk s : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i`: `dfinsupp.single a` as a linear map; + +* `dfinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M`: the map `λ f, f i` as a linear map; + +* `dfinsupp.lsum`: `dfinsupp.sum` or `dfinsupp.lift_add_hom` as a `linear_map`; + +## Implementation notes + +This file should try to mirror `linear_algebra.finsupp` where possible. The API of `finsupp` is +much more developed, but many lemmas in that file should be eligible to copy over. + +## Tags + +function with finite support, semimodule, linear algebra +-/ + +variables {ι : Type*} {R : Type*} {M : ι → Type*} {N : Type*} + +variables [dec_ι : decidable_eq ι] +variables [semiring R] [Π i, add_comm_monoid (M i)] [Π i, semimodule R (M i)] +variables [add_comm_monoid N] [semimodule R N] + +namespace dfinsupp + +include dec_ι + +/-- `dfinsupp.mk` as a `linear_map`. -/ +def lmk (s : finset ι) : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i := +⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul R x]⟩ + +/-- `dfinsupp.single` as a `linear_map` -/ +def lsingle (i) : M i →ₗ[R] Π₀ i, M i := +⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩ + +/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. -/ +lemma lhom_ext ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ + (h : ∀ i x, φ (single i x) = ψ (single i x)) : + φ = ψ := +linear_map.to_add_monoid_hom_injective $ add_hom_ext h + +/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. + +We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)` +so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these +maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/ +@[ext] lemma lhom_ext' ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ + (h : ∀ i, φ.comp (lsingle i) = ψ.comp (lsingle i)) : + φ = ψ := +lhom_ext $ λ i, linear_map.congr_fun (h i) + +omit dec_ι + +/-- Interpret `λ (f : Π₀ i, M i), f i` as a linear map. -/ +def lapply (i : ι) : (Π₀ i, M i) →ₗ[R] M i := +{ to_fun := λ f, f i, + map_add' := λ f g, add_apply f g i, + map_smul' := λ c f, smul_apply c f i} + +include dec_ι + +@[simp] lemma lmk_apply (s : finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x := rfl + +@[simp] lemma lsingle_apply (i : ι) (x : M i) : (lsingle i : _ →ₗ[R] _) x = single i x := rfl + +omit dec_ι + +@[simp] lemma lapply_apply (i : ι) (f : Π₀ i, M i) : (lapply i : _ →ₗ[R] _) f = f i := rfl + +include dec_ι + +/-- The `dfinsupp` version of `finsupp.lsum`. -/ +@[simps apply symm_apply] +def lsum : (Π i, M i →ₗ[R] N) ≃+ ((Π₀ i, M i) →ₗ[R] N) := +{ to_fun := λ F, { + to_fun := sum_add_hom (λ i, (F i).to_add_monoid_hom), + map_add' := (lift_add_hom (λ i, (F i).to_add_monoid_hom)).map_add, + map_smul' := λ c f, by { + apply dfinsupp.induction f, + { rw [smul_zero, add_monoid_hom.map_zero, smul_zero] }, + { intros a b f ha hb hf, + rw [smul_add, add_monoid_hom.map_add, add_monoid_hom.map_add, smul_add, hf, ←single_smul, + sum_add_hom_single, sum_add_hom_single, linear_map.to_add_monoid_hom_coe, + linear_map.map_smul], } } }, + inv_fun := λ F i, F.comp (lsingle i), + left_inv := λ F, by { ext x y, simp }, + right_inv := λ F, by { ext x y, simp }, + map_add' := λ F G, by { ext x y, simp } } + +end dfinsupp diff --git a/src/linear_algebra/direct_sum_module.lean b/src/linear_algebra/direct_sum_module.lean index e61309c37bfbb..e4cbcfd483f24 100644 --- a/src/linear_algebra/direct_sum_module.lean +++ b/src/linear_algebra/direct_sum_module.lean @@ -6,7 +6,7 @@ Authors: Kenny Lau Direct sum of modules over commutative rings, indexed by a discrete type. -/ import algebra.direct_sum -import linear_algebra.basic +import linear_algebra.dfinsupp /-! # Direct sum of modules over commutative rings, indexed by a discrete type. @@ -46,11 +46,11 @@ include dec_ι variables R ι M /-- Create the direct sum given a family `M` of `R` semimodules indexed over `ι`. -/ def lmk : Π s : finset ι, (Π i : (↑s : set ι), M i.val) →ₗ[R] (⨁ i, M i) := -dfinsupp.lmk M R +dfinsupp.lmk /-- Inclusion of each component into the direct sum. -/ def lof : Π i : ι, M i →ₗ[R] (⨁ i, M i) := -dfinsupp.lsingle M R +dfinsupp.lsingle variables {ι M} lemma single_eq_lof (i : ι) (b : M i) : @@ -94,7 +94,7 @@ variables {ψ} {ψ' : (⨁ i, M i) →ₗ[R] N} theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) (f : ⨁ i, M i) : ψ f = ψ' f := -by rw dfinsupp.lhom_ext' R H +by rw dfinsupp.lhom_ext' H /-- The inclusion of a subset of the direct summands @@ -107,7 +107,6 @@ to_module R _ _ $ λ i, lof R T (λ (i : subtype T), M i) ⟨i, H i.prop⟩ omit dec_ι /-- The natural linear equivalence between `⨁ _ : ι, M` and `M` when `unique ι`. -/ --- TODO: generalize this to arbitrary index type `ι` with `unique ι` protected def lid (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [semimodule R M] [unique ι] : (⨁ (_ : ι), M) ≃ₗ M := @@ -117,9 +116,7 @@ protected def lid (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [semimo variables (ι M) /-- The projection map onto one component, as a linear map. -/ def component (i : ι) : (⨁ i, M i) →ₗ[R] M i := -{ to_fun := λ f, f i, - map_add' := λ f g, dfinsupp.add_apply f g i, - map_smul' := λ c f, dfinsupp.smul_apply c f i} +dfinsupp.lapply i variables {ι M} @@ -137,7 +134,7 @@ lemma ext_iff {f g : ⨁ i, M i} : f = g ↔ include dec_ι @[simp] lemma lof_apply (i : ι) (b : M i) : ((lof R ι M i) b) i = b := -by rw [lof, dfinsupp.lsingle_apply, dfinsupp.single_apply, dif_pos rfl] +dfinsupp.single_eq_same @[simp] lemma component.lof_self (i : ι) (b : M i) : component R ι M i ((lof R ι M i) b) = b := diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean index d7c683c26bf5c..452c0c9a1252c 100644 --- a/src/linear_algebra/finsupp.lean +++ b/src/linear_algebra/finsupp.lean @@ -40,7 +40,7 @@ interpreted as a submodule of `α →₀ M`. We also define `linear_map` version * `finsupp.dom_lcongr`: a `linear_equiv` version of `finsupp.dom_congr`; * `finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to - `supported M R t`; + `supported M R t`; * `finsupp.lcongr`: a `linear_equiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ β` and `e' : M ≃ₗ[R] N`.