From 720ef195954398c359b82fbd7963fbeec8271a71 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 16:17:38 +0100 Subject: [PATCH 01/25] feat: port LinearAlgebra.Finsupp From 674df28ffb484e8812736ee9bb179ee5b1d82785 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 16:17:38 +0100 Subject: [PATCH 02/25] Initial file copy from mathport --- Mathlib/LinearAlgebra/Finsupp.lean | 1274 ++++++++++++++++++++++++++++ 1 file changed, 1274 insertions(+) create mode 100644 Mathlib/LinearAlgebra/Finsupp.lean diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean new file mode 100644 index 0000000000000..13a6211b2d883 --- /dev/null +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -0,0 +1,1274 @@ +/- +Copyright (c) 2019 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl + +! This file was ported from Lean 3 source module linear_algebra.finsupp +! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Data.Finsupp.Defs +import Mathbin.LinearAlgebra.Pi +import Mathbin.LinearAlgebra.Span + +/-! +# Properties of the module `α →₀ M` + +Given an `R`-module `M`, the `R`-module structure on `α →₀ M` is defined in +`data.finsupp.basic`. + +In this file we define `finsupp.supported s` to be the set `{f : α →₀ M | f.support ⊆ s}` +interpreted as a submodule of `α →₀ M`. We also define `linear_map` versions of various maps: + +* `finsupp.lsingle a : M →ₗ[R] ι →₀ M`: `finsupp.single a` as a linear map; + +* `finsupp.lapply a : (ι →₀ M) →ₗ[R] M`: the map `λ f, f a` as a linear map; + +* `finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a + linear map; + +* `finsupp.restrict_dom`: `finsupp.filter` as a linear map to `finsupp.supported s`; + +* `finsupp.lsum`: `finsupp.sum` or `finsupp.lift_add_hom` as a `linear_map`; + +* `finsupp.total α M R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with + coefficients `l i`; + +* `finsupp.total_on`: a restricted version of `finsupp.total` with domain `finsupp.supported R R s` + and codomain `submodule.span R (v '' s)`; + +* `finsupp.supported_equiv_finsupp`: a linear equivalence between the functions `α →₀ M` supported + on `s` and the functions `s →₀ M`; + +* `finsupp.lmap_domain`: a linear map version of `finsupp.map_domain`; + +* `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`; + +* `finsupp.lcongr`: a `linear_equiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ + β` and `e' : M ≃ₗ[R] N`. + +## Tags + +function with finite support, module, linear algebra +-/ + + +noncomputable section + +open Set LinearMap Submodule + +open Classical BigOperators + +namespace Finsupp + +variable {α : Type _} {M : Type _} {N : Type _} {P : Type _} {R : Type _} {S : Type _} + +variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] + +variable [AddCommMonoid N] [Module R N] + +variable [AddCommMonoid P] [Module R P] + +/-- Interpret `finsupp.single a` as a linear map. -/ +def lsingle (a : α) : M →ₗ[R] α →₀ M := + { Finsupp.singleAddHom a with map_smul' := fun a b => (smul_single _ _ _).symm } +#align finsupp.lsingle Finsupp.lsingle + +/-- Two `R`-linear maps from `finsupp X M` which agree on each `single x y` agree everywhere. -/ +theorem lhom_ext ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ := + LinearMap.toAddMonoidHom_injective <| addHom_ext h +#align finsupp.lhom_ext Finsupp.lhom_ext + +/-- Two `R`-linear maps from `finsupp X M` which agree on each `single x y` 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] +theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) : + φ = ψ := + lhom_ext fun a => LinearMap.congr_fun (h a) +#align finsupp.lhom_ext' Finsupp.lhom_ext' + +/-- Interpret `λ (f : α →₀ M), f a` as a linear map. -/ +def lapply (a : α) : (α →₀ M) →ₗ[R] M := + { Finsupp.applyAddHom a with map_smul' := fun a b => rfl } +#align finsupp.lapply Finsupp.lapply + +/-- Forget that a function is finitely supported. + +This is the linear version of `finsupp.to_fun`. -/ +@[simps] +def lcoeFun : (α →₀ M) →ₗ[R] α → M where + toFun := coeFn + map_add' x y := by + ext + simp + map_smul' x y := by + ext + simp +#align finsupp.lcoe_fun Finsupp.lcoeFun + +section LsubtypeDomain + +variable (s : Set α) + +/-- Interpret `finsupp.subtype_domain s` as a linear map. -/ +def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M + where + toFun := subtypeDomain fun x => x ∈ s + map_add' a b := subtypeDomain_add + map_smul' c a := ext fun a => rfl +#align finsupp.lsubtype_domain Finsupp.lsubtypeDomain + +theorem lsubtypeDomain_apply (f : α →₀ M) : + (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M) f = subtypeDomain (fun x => x ∈ s) f := + rfl +#align finsupp.lsubtype_domain_apply Finsupp.lsubtypeDomain_apply + +end LsubtypeDomain + +@[simp] +theorem lsingle_apply (a : α) (b : M) : (lsingle a : M →ₗ[R] α →₀ M) b = single a b := + rfl +#align finsupp.lsingle_apply Finsupp.lsingle_apply + +@[simp] +theorem lapply_apply (a : α) (f : α →₀ M) : (lapply a : (α →₀ M) →ₗ[R] M) f = f a := + rfl +#align finsupp.lapply_apply Finsupp.lapply_apply + +@[simp] +theorem ker_lsingle (a : α) : (lsingle a : M →ₗ[R] α →₀ M).ker = ⊥ := + ker_eq_bot_of_injective (single_injective a) +#align finsupp.ker_lsingle Finsupp.ker_lsingle + +theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) : + (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := + by + refine' supᵢ_le fun a₁ => supᵢ_le fun h₁ => range_le_iff_comap.2 _ + simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_infi, mem_infi] + intro b hb a₂ h₂ + have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, Eq.symm ▸ h₂⟩ + exact single_eq_of_ne this +#align finsupp.lsingle_range_le_ker_lapply Finsupp.lsingle_range_le_ker_lapply + +theorem infᵢ_ker_lapply_le_bot : (⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M)) ≤ ⊥ := + by + simp only [SetLike.le_def, mem_infi, mem_ker, mem_bot, lapply_apply] + exact fun a h => Finsupp.ext h +#align finsupp.infi_ker_lapply_le_bot Finsupp.infᵢ_ker_lapply_le_bot + +theorem supᵢ_lsingle_range : (⨆ a, (lsingle a : M →ₗ[R] α →₀ M).range) = ⊤ := + by + refine' eq_top_iff.2 <| SetLike.le_def.2 fun f _ => _ + rw [← sum_single f] + exact sum_mem fun a ha => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ +#align finsupp.supr_lsingle_range Finsupp.supᵢ_lsingle_range + +theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : + Disjoint (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) + (⨆ a ∈ t, (lsingle a : M →ₗ[R] α →₀ M).range) := + by + refine' + (Disjoint.mono (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right) + (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right)) + _ + rw [disjoint_iff_inf_le] + refine' le_trans (le_infᵢ fun i => _) infi_ker_lapply_le_bot + classical + by_cases his : i ∈ s + · by_cases hit : i ∈ t + · exact (hs.le_bot ⟨his, hit⟩).elim + exact inf_le_of_right_le (infᵢ_le_of_le i <| infᵢ_le _ hit) + exact inf_le_of_left_le (infᵢ_le_of_le i <| infᵢ_le _ his) +#align finsupp.disjoint_lsingle_lsingle Finsupp.disjoint_lsingle_lsingle + +theorem span_single_image (s : Set M) (a : α) : + Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by + rw [← span_image] <;> rfl +#align finsupp.span_single_image Finsupp.span_single_image + +variable (M R) + +/-- `finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/ +def supported (s : Set α) : Submodule R (α →₀ M) := + by + refine' ⟨{ p | ↑p.support ⊆ s }, _, _, _⟩ + · intro p q hp hq + refine' subset.trans (subset.trans (Finset.coe_subset.2 support_add) _) (union_subset hp hq) + rw [Finset.coe_union] + · simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply] + intro h ha + exact (ha rfl).elim + · intro a p hp + refine' subset.trans (Finset.coe_subset.2 support_smul) hp +#align finsupp.supported Finsupp.supported + +variable {M} + +theorem mem_supported {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ↑p.support ⊆ s := + Iff.rfl +#align finsupp.mem_supported Finsupp.mem_supported + +/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (x «expr ∉ » s) -/ +theorem mem_supported' {s : Set α} (p : α →₀ M) : + p ∈ supported M R s ↔ ∀ (x) (_ : x ∉ s), p x = 0 := by + haveI := Classical.decPred fun x : α => x ∈ s <;> + simp [mem_supported, Set.subset_def, not_imp_comm] +#align finsupp.mem_supported' Finsupp.mem_supported' + +theorem mem_supported_support (p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α) := by + rw [Finsupp.mem_supported] +#align finsupp.mem_supported_support Finsupp.mem_supported_support + +theorem single_mem_supported {s : Set α} {a : α} (b : M) (h : a ∈ s) : + single a b ∈ supported M R s := + Set.Subset.trans support_single_subset (Finset.singleton_subset_set_iff.2 h) +#align finsupp.single_mem_supported Finsupp.single_mem_supported + +theorem supported_eq_span_single (s : Set α) : + supported R R s = span R ((fun i => single i 1) '' s) := + by + refine' (span_eq_of_le _ _ (SetLike.le_def.2 fun l hl => _)).symm + · rintro _ ⟨_, hp, rfl⟩ + exact single_mem_supported R 1 hp + · rw [← l.sum_single] + refine' sum_mem fun i il => _ + convert @smul_mem R (α →₀ R) _ _ _ _ (single i 1) (l i) _ + · simp + apply subset_span + apply Set.mem_image_of_mem _ (hl il) +#align finsupp.supported_eq_span_single Finsupp.supported_eq_span_single + +variable (M R) + +/-- Interpret `finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/ +def restrictDom (s : Set α) : (α →₀ M) →ₗ[R] supported M R s := + LinearMap.codRestrict _ + { toFun := filter (· ∈ s) + map_add' := fun l₁ l₂ => filter_add + map_smul' := fun a l => filter_smul } fun l => + (mem_supported' _ _).2 fun x => filter_apply_neg (· ∈ s) l +#align finsupp.restrict_dom Finsupp.restrictDom + +variable {M R} + +section + +@[simp] +theorem restrictDom_apply (s : Set α) (l : α →₀ M) : + ((restrictDom M R s : (α →₀ M) →ₗ[R] supported M R s) l : α →₀ M) = Finsupp.filter (· ∈ s) l := + rfl +#align finsupp.restrict_dom_apply Finsupp.restrictDom_apply + +end + +theorem restrictDom_comp_subtype (s : Set α) : + (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := + by + ext (l a) + by_cases a ∈ s <;> simp [h] + exact ((mem_supported' R l.1).1 l.2 a h).symm +#align finsupp.restrict_dom_comp_subtype Finsupp.restrictDom_comp_subtype + +theorem range_restrictDom (s : Set α) : (restrictDom M R s).range = ⊤ := + range_eq_top.2 <| + Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s) +#align finsupp.range_restrict_dom Finsupp.range_restrictDom + +theorem supported_mono {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := fun l h => + Set.Subset.trans h st +#align finsupp.supported_mono Finsupp.supported_mono + +@[simp] +theorem supported_empty : supported M R (∅ : Set α) = ⊥ := + eq_bot_iff.2 fun l h => (Submodule.mem_bot R).2 <| by ext <;> simp_all [mem_supported'] +#align finsupp.supported_empty Finsupp.supported_empty + +@[simp] +theorem supported_univ : supported M R (Set.univ : Set α) = ⊤ := + eq_top_iff.2 fun l _ => Set.subset_univ _ +#align finsupp.supported_univ Finsupp.supported_univ + +theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : + supported M R (⋃ i, s i) = ⨆ i, supported M R (s i) := + by + refine' le_antisymm _ (supᵢ_le fun i => supported_mono <| Set.subset_unionᵢ _ _) + haveI := Classical.decPred fun x => x ∈ ⋃ i, s i + suffices + ((Submodule.subtype _).comp (restrict_dom M R (⋃ i, s i))).range ≤ ⨆ i, supported M R (s i) by + rwa [LinearMap.range_comp, range_restrict_dom, map_top, range_subtype] at this + rw [range_le_iff_comap, eq_top_iff] + rintro l ⟨⟩ + apply Finsupp.induction l + · exact zero_mem _ + refine' fun x a l hl a0 => add_mem _ + by_cases ∃ i, x ∈ s i <;> simp [h] + · cases' h with i hi + exact le_supᵢ (fun i => supported M R (s i)) i (single_mem_supported R _ hi) +#align finsupp.supported_Union Finsupp.supported_unionᵢ + +theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := + by erw [Set.union_eq_unionᵢ, supported_Union, supᵢ_bool_eq] <;> rfl +#align finsupp.supported_union Finsupp.supported_union + +theorem supported_interᵢ {ι : Type _} (s : ι → Set α) : + supported M R (⋂ i, s i) = ⨅ i, supported M R (s i) := + Submodule.ext fun x => by simp [mem_supported, subset_Inter_iff] +#align finsupp.supported_Inter Finsupp.supported_interᵢ + +theorem supported_inter (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t := + by rw [Set.inter_eq_interᵢ, supported_Inter, infᵢ_bool_eq] <;> rfl +#align finsupp.supported_inter Finsupp.supported_inter + +theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) : + Disjoint (supported M R s) (supported M R t) := + disjoint_iff.2 <| by rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty] +#align finsupp.disjoint_supported_supported Finsupp.disjoint_supported_supported + +theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : + Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t := + by + refine' ⟨fun h => set.disjoint_left.mpr fun x hx1 hx2 => _, disjoint_supported_supported⟩ + rcases exists_ne (0 : M) with ⟨y, hy⟩ + have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩ + rw [mem_bot, single_eq_zero] at this + exact hy this +#align finsupp.disjoint_supported_supported_iff Finsupp.disjoint_supported_supported_iff + +/-- Interpret `finsupp.restrict_support_equiv` as a linear equivalence between +`supported M R s` and `s →₀ M`. -/ +def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := + by + let F : supported M R s ≃ (s →₀ M) := restrict_support_equiv s M + refine' F.to_linear_equiv _ + have : + (F : supported M R s → ↥s →₀ M) = + (lsubtype_domain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) := + rfl + rw [this] + exact LinearMap.isLinear _ +#align finsupp.supported_equiv_finsupp Finsupp.supportedEquivFinsupp + +section Lsum + +variable (S) [Module S N] [SMulCommClass R S N] + +/-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to +`N` using `finsupp.sum`. This is an upgraded version of `finsupp.lift_add_hom`. + +See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. +-/ +def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N + where + toFun F := + { toFun := fun d => d.Sum fun i => F i + map_add' := (liftAddHom fun x => (F x).toAddMonoidHom).map_add + map_smul' := fun c f => by simp [sum_smul_index', smul_sum] } + invFun F x := F.comp (lsingle x) + 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 + map_smul' F G := by + ext (x y) + simp +#align finsupp.lsum Finsupp.lsum + +@[simp] +theorem coe_lsum (f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = fun d => d.Sum fun i => f i := + rfl +#align finsupp.coe_lsum Finsupp.coe_lsum + +theorem lsum_apply (f : α → M →ₗ[R] N) (l : α →₀ M) : Finsupp.lsum S f l = l.Sum fun b => f b := + rfl +#align finsupp.lsum_apply Finsupp.lsum_apply + +theorem lsum_single (f : α → M →ₗ[R] N) (i : α) (m : M) : + Finsupp.lsum S f (Finsupp.single i m) = f i m := + Finsupp.sum_single_index (f i).map_zero +#align finsupp.lsum_single Finsupp.lsum_single + +theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) : (lsum S).symm f x = f.comp (lsingle x) := + rfl +#align finsupp.lsum_symm_apply Finsupp.lsum_symm_apply + +end Lsum + +section + +variable (M) (R) (X : Type _) + +/-- A slight rearrangement from `lsum` gives us +the bijection underlying the free-forgetful adjunction for R-modules. +-/ +noncomputable def lift : (X → M) ≃+ ((X →₀ R) →ₗ[R] M) := + (AddEquiv.arrowCongr (Equiv.refl X) (ringLmapEquivSelf R ℕ M).toAddEquiv.symm).trans + (lsum _ : _ ≃ₗ[ℕ] _).toAddEquiv +#align finsupp.lift Finsupp.lift + +@[simp] +theorem lift_symm_apply (f) (x) : ((lift M R X).symm f) x = f (single x 1) := + rfl +#align finsupp.lift_symm_apply Finsupp.lift_symm_apply + +@[simp] +theorem lift_apply (f) (g) : ((lift M R X) f) g = g.Sum fun x r => r • f x := + rfl +#align finsupp.lift_apply Finsupp.lift_apply + +end + +section LmapDomain + +variable {α' : Type _} {α'' : Type _} (M R) + +/-- Interpret `finsupp.map_domain` as a linear map. -/ +def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M + where + toFun := mapDomain f + map_add' a b := mapDomain_add + map_smul' := mapDomain_smul +#align finsupp.lmap_domain Finsupp.lmapDomain + +@[simp] +theorem lmapDomain_apply (f : α → α') (l : α →₀ M) : + (lmapDomain M R f : (α →₀ M) →ₗ[R] α' →₀ M) l = mapDomain f l := + rfl +#align finsupp.lmap_domain_apply Finsupp.lmapDomain_apply + +@[simp] +theorem lmapDomain_id : (lmapDomain M R id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id := + LinearMap.ext fun l => mapDomain_id +#align finsupp.lmap_domain_id Finsupp.lmapDomain_id + +theorem lmapDomain_comp (f : α → α') (g : α' → α'') : + lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f) := + LinearMap.ext fun l => mapDomain_comp +#align finsupp.lmap_domain_comp Finsupp.lmapDomain_comp + +theorem supported_comap_lmapDomain (f : α → α') (s : Set α') : + supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f) := + fun l (hl : ↑l.support ⊆ f ⁻¹' s) => + show ↑(mapDomain f l).support ⊆ s + by + rw [← Set.image_subset_iff, ← Finset.coe_image] at hl + exact Set.Subset.trans map_domain_support hl +#align finsupp.supported_comap_lmap_domain Finsupp.supported_comap_lmapDomain + +theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : + (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := + by + inhabit α + refine' + le_antisymm + (map_le_iff_le_comap.2 <| + le_trans (supported_mono <| Set.subset_preimage_image _ _) + (supported_comap_lmap_domain _ _ _ _)) + _ + intro l hl + refine' ⟨(lmap_domain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => _, _⟩ + · rcases Finset.mem_image.1 (map_domain_support hx) with ⟨c, hc, rfl⟩ + exact Function.invFunOn_mem (by simpa using hl hc) + · rw [← LinearMap.comp_apply, ← lmap_domain_comp] + refine' (map_domain_congr fun c hc => _).trans map_domain_id + exact Function.invFunOn_eq (by simpa using hl hc) +#align finsupp.lmap_domain_supported Finsupp.lmapDomain_supported + +/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (a b «expr ∈ » s) -/ +theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} + (H : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), f a = f b → a = b) : + Disjoint (supported M R s) (lmapDomain M R f).ker := + by + rw [disjoint_iff_inf_le] + rintro l ⟨h₁, h₂⟩ + rw [SetLike.mem_coe, mem_ker, lmap_domain_apply, map_domain] at h₂ + simp; ext x + haveI := Classical.decPred fun x => x ∈ s + by_cases xs : x ∈ s + · have : Finsupp.sum l (fun a => Finsupp.single (f a)) (f x) = 0 := + by + rw [h₂] + rfl + rw [Finsupp.sum_apply, Finsupp.sum, Finset.sum_eq_single x] at this + · simpa [Finsupp.single_apply] + · intro y hy xy + simp [mt (H _ (h₁ hy) _ xs) xy] + · simp (config := { contextual := true }) + · by_contra h + exact xs (h₁ <| Finsupp.mem_support_iff.2 h) +#align finsupp.lmap_domain_disjoint_ker Finsupp.lmapDomain_disjoint_ker + +end LmapDomain + +section LcomapDomain + +variable {β : Type _} {R M} + +/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomap_domain f hf` is the linear map +sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing +`l` with `f`. + +This is the linear version of `finsupp.comap_domain`. -/ +def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M + where + toFun l := Finsupp.comapDomain f l (hf.InjOn _) + map_add' x y := by + ext + simp + map_smul' c x := by + ext + simp +#align finsupp.lcomap_domain Finsupp.lcomapDomain + +end LcomapDomain + +section Total + +variable (α) {α' : Type _} (M) {M' : Type _} (R) [AddCommMonoid M'] [Module R M'] (v : α → M) + {v' : α' → M'} + +/-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and + evaluates this linear combination. -/ +protected def total : (α →₀ R) →ₗ[R] M := + Finsupp.lsum ℕ fun i => LinearMap.id.smul_right (v i) +#align finsupp.total Finsupp.total + +variable {α M v} + +theorem total_apply (l : α →₀ R) : Finsupp.total α M R v l = l.Sum fun i a => a • v i := + rfl +#align finsupp.total_apply Finsupp.total_apply + +theorem total_apply_of_mem_supported {l : α →₀ R} {s : Finset α} + (hs : l ∈ supported R R (↑s : Set α)) : Finsupp.total α M R v l = s.Sum fun i => l i • v i := + Finset.sum_subset hs fun x _ hxg => + show l x • v x = 0 by rw [not_mem_support_iff.1 hxg, zero_smul] +#align finsupp.total_apply_of_mem_supported Finsupp.total_apply_of_mem_supported + +@[simp] +theorem total_single (c : R) (a : α) : Finsupp.total α M R v (single a c) = c • v a := by + simp [total_apply, sum_single_index] +#align finsupp.total_single Finsupp.total_single + +theorem total_zero_apply (x : α →₀ R) : (Finsupp.total α M R 0) x = 0 := by + simp [Finsupp.total_apply] +#align finsupp.total_zero_apply Finsupp.total_zero_apply + +variable (α M) + +@[simp] +theorem total_zero : Finsupp.total α M R 0 = 0 := + LinearMap.ext (total_zero_apply R) +#align finsupp.total_zero Finsupp.total_zero + +variable {α M} + +theorem apply_total (f : M →ₗ[R] M') (v) (l : α →₀ R) : + f (Finsupp.total α M R v l) = Finsupp.total α M' R (f ∘ v) l := by + apply Finsupp.induction_linear l <;> simp (config := { contextual := true }) +#align finsupp.apply_total Finsupp.apply_total + +theorem total_unique [Unique α] (l : α →₀ R) (v) : + Finsupp.total α M R v l = l default • v default := by rw [← total_single, ← unique_single l] +#align finsupp.total_unique Finsupp.total_unique + +theorem total_surjective (h : Function.Surjective v) : + Function.Surjective (Finsupp.total α M R v) := + by + intro x + obtain ⟨y, hy⟩ := h x + exact ⟨Finsupp.single y 1, by simp [hy]⟩ +#align finsupp.total_surjective Finsupp.total_surjective + +theorem total_range (h : Function.Surjective v) : (Finsupp.total α M R v).range = ⊤ := + range_eq_top.2 <| total_surjective R h +#align finsupp.total_range Finsupp.total_range + +/-- Any module is a quotient of a free module. This is stated as surjectivity of +`finsupp.total M M R id : (M →₀ R) →ₗ[R] M`. -/ +theorem total_id_surjective (M) [AddCommMonoid M] [Module R M] : + Function.Surjective (Finsupp.total M M R id) := + total_surjective R Function.surjective_id +#align finsupp.total_id_surjective Finsupp.total_id_surjective + +theorem range_total : (Finsupp.total α M R v).range = span R (range v) := + by + ext x + constructor + · intro hx + rw [LinearMap.mem_range] at hx + rcases hx with ⟨l, hl⟩ + rw [← hl] + rw [Finsupp.total_apply] + exact sum_mem fun i hi => Submodule.smul_mem _ _ (subset_span (mem_range_self i)) + · apply span_le.2 + intro x hx + rcases hx with ⟨i, hi⟩ + rw [SetLike.mem_coe, LinearMap.mem_range] + use Finsupp.single i 1 + simp [hi] +#align finsupp.range_total Finsupp.range_total + +theorem lmapDomain_total (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) : + (Finsupp.total α' M' R v').comp (lmapDomain R R f) = g.comp (Finsupp.total α M R v) := by + ext l <;> simp [total_apply, Finsupp.sum_mapDomain_index, add_smul, h] +#align finsupp.lmap_domain_total Finsupp.lmapDomain_total + +theorem total_comp_lmapDomain (f : α → α') : + (Finsupp.total α' M' R v').comp (Finsupp.lmapDomain R R f) = Finsupp.total α M' R (v' ∘ f) := + by + ext + simp +#align finsupp.total_comp_lmap_domain Finsupp.total_comp_lmapDomain + +@[simp] +theorem total_embDomain (f : α ↪ α') (l : α →₀ R) : + (Finsupp.total α' M' R v') (embDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l := by + simp [total_apply, Finsupp.sum, support_emb_domain, emb_domain_apply] +#align finsupp.total_emb_domain Finsupp.total_embDomain + +@[simp] +theorem total_mapDomain (f : α → α') (l : α →₀ R) : + (Finsupp.total α' M' R v') (mapDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l := + LinearMap.congr_fun (total_comp_lmapDomain _ _) l +#align finsupp.total_map_domain Finsupp.total_mapDomain + +@[simp] +theorem total_equivMapDomain (f : α ≃ α') (l : α →₀ R) : + (Finsupp.total α' M' R v') (equivMapDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l := by + rw [equiv_map_domain_eq_map_domain, total_map_domain] +#align finsupp.total_equiv_map_domain Finsupp.total_equivMapDomain + +/-- A version of `finsupp.range_total` which is useful for going in the other direction -/ +theorem span_eq_range_total (s : Set M) : span R s = (Finsupp.total s M R coe).range := by + rw [range_total, Subtype.range_coe_subtype, Set.setOf_mem_eq] +#align finsupp.span_eq_range_total Finsupp.span_eq_range_total + +theorem mem_span_iff_total (s : Set M) (x : M) : + x ∈ span R s ↔ ∃ l : s →₀ R, Finsupp.total s M R coe l = x := + (SetLike.ext_iff.1 <| span_eq_range_total _ _) x +#align finsupp.mem_span_iff_total Finsupp.mem_span_iff_total + +variable {R} + +theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} : + x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.Sum fun i a => a • v i) = x := by + simp only [← Finsupp.range_total, LinearMap.mem_range, Finsupp.total_apply] +#align finsupp.mem_span_range_iff_exists_finsupp Finsupp.mem_span_range_iff_exists_finsupp + +variable (R) + +theorem span_image_eq_map_total (s : Set α) : + span R (v '' s) = Submodule.map (Finsupp.total α M R v) (supported R R s) := + by + apply span_eq_of_le + · intro x hx + rw [Set.mem_image] at hx + apply Exists.elim hx + intro i hi + exact ⟨_, Finsupp.single_mem_supported R 1 hi.1, by simp [hi.2]⟩ + · refine' map_le_iff_le_comap.2 fun z hz => _ + have : ∀ i, z i • v i ∈ span R (v '' s) := by + intro c + haveI := Classical.decPred fun x => x ∈ s + by_cases c ∈ s + · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h)) + · simp [(Finsupp.mem_supported' R _).1 hz _ h] + refine' sum_mem _ + simp [this] +#align finsupp.span_image_eq_map_total Finsupp.span_image_eq_map_total + +theorem mem_span_image_iff_total {s : Set α} {x : M} : + x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, Finsupp.total α M R v l = x := + by + rw [span_image_eq_map_total] + simp +#align finsupp.mem_span_image_iff_total Finsupp.mem_span_image_iff_total + +theorem total_option (v : Option α → M) (f : Option α →₀ R) : + Finsupp.total (Option α) M R v f = + f none • v none + Finsupp.total α M R (v ∘ Option.some) f.some := + by rw [total_apply, sum_option_index_smul, total_apply] +#align finsupp.total_option Finsupp.total_option + +theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) : + Finsupp.total α M R A (Finsupp.total β (α →₀ R) R B f) = + Finsupp.total β M R (fun b => Finsupp.total α M R A (B b)) f := + by + simp only [total_apply] + apply induction_linear f + · simp only [sum_zero_index] + · intro f₁ f₂ h₁ h₂ + simp [sum_add_index, h₁, h₂, add_smul] + · simp [sum_single_index, sum_smul_index, smul_sum, mul_smul] +#align finsupp.total_total Finsupp.total_total + +@[simp] +theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := + by + ext i + apply finZeroElim i +#align finsupp.total_fin_zero Finsupp.total_fin_zero + +variable (α) (M) (v) + +/-- `finsupp.total_on M v s` interprets `p : α →₀ R` as a linear combination of a +subset of the vectors in `v`, mapping it to the span of those vectors. + +The subset is indicated by a set `s : set α` of indices. +-/ +protected def totalOn (s : Set α) : supported R R s →ₗ[R] span R (v '' s) := + LinearMap.codRestrict _ ((Finsupp.total _ _ _ v).comp (Submodule.subtype (supported R R s))) + fun ⟨l, hl⟩ => (mem_span_image_iff_total _).2 ⟨l, hl, rfl⟩ +#align finsupp.total_on Finsupp.totalOn + +variable {α} {M} {v} + +theorem totalOn_range (s : Set α) : (Finsupp.totalOn α M R v s).range = ⊤ := + by + rw [Finsupp.totalOn, LinearMap.range_eq_map, LinearMap.map_codRestrict, ← + LinearMap.range_le_iff_comap, range_subtype, map_top, LinearMap.range_comp, range_subtype] + exact (span_image_eq_map_total _ _).le +#align finsupp.total_on_range Finsupp.totalOn_range + +theorem total_comp (f : α' → α) : + Finsupp.total α' M R (v ∘ f) = (Finsupp.total α M R v).comp (lmapDomain R R f) := + by + ext + simp [total_apply] +#align finsupp.total_comp Finsupp.total_comp + +theorem total_comapDomain (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : + Finsupp.total α M R v (Finsupp.comapDomain f l hf) = + (l.support.Preimage f hf).Sum fun i => l (f i) • v i := + by rw [Finsupp.total_apply] <;> rfl +#align finsupp.total_comap_domain Finsupp.total_comapDomain + +theorem total_onFinset {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : + Finsupp.total α M R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := + by + simp only [Finsupp.total_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset] + rw [Finset.sum_filter_of_ne] + intro x hx h + contrapose! h + simp [h] +#align finsupp.total_on_finset Finsupp.total_onFinset + +end Total + +/-- An equivalence of domains induces a linear equivalence of finitely supported functions. + +This is `finsupp.dom_congr` as a `linear_equiv`. +See also `linear_map.fun_congr_left` for the case of arbitrary functions. -/ +protected def domLcongr {α₁ α₂ : Type _} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M := + (Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by + simpa only [equiv_map_domain_eq_map_domain, dom_congr_apply] using (lmap_domain M R e).map_smul +#align finsupp.dom_lcongr Finsupp.domLcongr + +@[simp] +theorem domLcongr_apply {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : + (Finsupp.domLcongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v := + rfl +#align finsupp.dom_lcongr_apply Finsupp.domLcongr_apply + +@[simp] +theorem domLcongr_refl : Finsupp.domLcongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M) := + LinearEquiv.ext fun _ => equivMapDomain_refl _ +#align finsupp.dom_lcongr_refl Finsupp.domLcongr_refl + +theorem domLcongr_trans {α₁ α₂ α₃ : Type _} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) : + (Finsupp.domLcongr f).trans (Finsupp.domLcongr f₂) = + (Finsupp.domLcongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _) := + LinearEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm +#align finsupp.dom_lcongr_trans Finsupp.domLcongr_trans + +@[simp] +theorem domLcongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : + ((Finsupp.domLcongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLcongr f.symm := + LinearEquiv.ext fun x => rfl +#align finsupp.dom_lcongr_symm Finsupp.domLcongr_symm + +@[simp] +theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (i : α₁) (m : M) : + (Finsupp.domLcongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by + simp [Finsupp.domLcongr, Finsupp.domCongr, equiv_map_domain_single] +#align finsupp.dom_lcongr_single Finsupp.domLcongr_single + +/-- An equivalence of sets induces a linear equivalence of `finsupp`s supported on those sets. -/ +noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : + supported M R s ≃ₗ[R] supported M R t := + by + haveI := Classical.decPred fun x => x ∈ s + haveI := Classical.decPred fun x => x ∈ t + refine' Finsupp.supportedEquivFinsupp s ≪≫ₗ (_ ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) + exact Finsupp.domLcongr e +#align finsupp.congr Finsupp.congr + +/-- `finsupp.map_range` as a `linear_map`. -/ +@[simps] +def mapRange.linearMap (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N := + { + mapRange.addMonoidHom + f.toAddMonoidHom with + toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N) + map_smul' := fun c v => mapRange_smul c v (f.map_smul c) } +#align finsupp.map_range.linear_map Finsupp.mapRange.linearMap + +@[simp] +theorem mapRange.linearMap_id : + mapRange.linearMap LinearMap.id = (LinearMap.id : (α →₀ M) →ₗ[R] _) := + LinearMap.ext mapRange_id +#align finsupp.map_range.linear_map_id Finsupp.mapRange.linearMap_id + +theorem mapRange.linearMap_comp (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) : + (mapRange.linearMap (f.comp f₂) : (α →₀ _) →ₗ[R] _) = + (mapRange.linearMap f).comp (mapRange.linearMap f₂) := + LinearMap.ext <| mapRange_comp _ _ _ _ _ +#align finsupp.map_range.linear_map_comp Finsupp.mapRange.linearMap_comp + +@[simp] +theorem mapRange.linearMap_toAddMonoidHom (f : M →ₗ[R] N) : + (mapRange.linearMap f).toAddMonoidHom = + (mapRange.addMonoidHom f.toAddMonoidHom : (α →₀ M) →+ _) := + AddMonoidHom.ext fun _ => rfl +#align finsupp.map_range.linear_map_to_add_monoid_hom Finsupp.mapRange.linearMap_toAddMonoidHom + +/-- `finsupp.map_range` as a `linear_equiv`. -/ +@[simps apply] +def mapRange.linearEquiv (e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ N := + { mapRange.linearMap e.toLinearMap, + mapRange.addEquiv e.toAddEquiv with + toFun := mapRange e e.map_zero + invFun := mapRange e.symm e.symm.map_zero } +#align finsupp.map_range.linear_equiv Finsupp.mapRange.linearEquiv + +@[simp] +theorem mapRange.linearEquiv_refl : + mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M) := + LinearEquiv.ext mapRange_id +#align finsupp.map_range.linear_equiv_refl Finsupp.mapRange.linearEquiv_refl + +theorem mapRange.linearEquiv_trans (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) : + (mapRange.linearEquiv (f.trans f₂) : (α →₀ _) ≃ₗ[R] _) = + (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) := + LinearEquiv.ext <| mapRange_comp _ _ _ _ _ +#align finsupp.map_range.linear_equiv_trans Finsupp.mapRange.linearEquiv_trans + +@[simp] +theorem mapRange.linearEquiv_symm (f : M ≃ₗ[R] N) : + ((mapRange.linearEquiv f).symm : (α →₀ _) ≃ₗ[R] _) = mapRange.linearEquiv f.symm := + LinearEquiv.ext fun x => rfl +#align finsupp.map_range.linear_equiv_symm Finsupp.mapRange.linearEquiv_symm + +@[simp] +theorem mapRange.linearEquiv_toAddEquiv (f : M ≃ₗ[R] N) : + (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv : (α →₀ M) ≃+ _) := + AddEquiv.ext fun _ => rfl +#align finsupp.map_range.linear_equiv_to_add_equiv Finsupp.mapRange.linearEquiv_toAddEquiv + +@[simp] +theorem mapRange.linearEquiv_toLinearMap (f : M ≃ₗ[R] N) : + (mapRange.linearEquiv f).toLinearMap = (mapRange.linearMap f.toLinearMap : (α →₀ M) →ₗ[R] _) := + LinearMap.ext fun _ => rfl +#align finsupp.map_range.linear_equiv_to_linear_map Finsupp.mapRange.linearEquiv_toLinearMap + +/-- An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the +corresponding finitely supported functions. -/ +def lcongr {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (ι →₀ M) ≃ₗ[R] κ →₀ N := + (Finsupp.domLcongr e₁).trans (mapRange.linearEquiv e₂) +#align finsupp.lcongr Finsupp.lcongr + +@[simp] +theorem lcongr_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (i : ι) (m : M) : + lcongr e₁ e₂ (Finsupp.single i m) = Finsupp.single (e₁ i) (e₂ m) := by simp [lcongr] +#align finsupp.lcongr_single Finsupp.lcongr_single + +@[simp] +theorem lcongr_apply_apply {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (f : ι →₀ M) (k : κ) : + lcongr e₁ e₂ f k = e₂ (f (e₁.symm k)) := + rfl +#align finsupp.lcongr_apply_apply Finsupp.lcongr_apply_apply + +theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) : + (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) := + by + apply_fun lcongr e₁ e₂ using (lcongr e₁ e₂).Injective + simp +#align finsupp.lcongr_symm_single Finsupp.lcongr_symm_single + +@[simp] +theorem lcongr_symm {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : + (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm := + by + ext + rfl +#align finsupp.lcongr_symm Finsupp.lcongr_symm + +section Sum + +variable (R) + +/-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`. + +This is the `linear_equiv` version of `finsupp.sum_finsupp_equiv_prod_finsupp`. -/ +@[simps apply symm_apply] +def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) := + { sumFinsuppAddEquivProdFinsupp with + map_smul' := by + intros + ext <;> + simp only [[anonymous], Prod.smul_fst, Prod.smul_snd, smul_apply, + snd_sum_finsupp_add_equiv_prod_finsupp, fst_sum_finsupp_add_equiv_prod_finsupp, + RingHom.id_apply] } +#align finsupp.sum_finsupp_lequiv_prod_finsupp Finsupp.sumFinsuppLequivProdFinsupp + +theorem fst_sumFinsuppLequivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (x : α) : + (sumFinsuppLequivProdFinsupp R f).1 x = f (Sum.inl x) := + rfl +#align finsupp.fst_sum_finsupp_lequiv_prod_finsupp Finsupp.fst_sumFinsuppLequivProdFinsupp + +theorem snd_sumFinsuppLequivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (y : β) : + (sumFinsuppLequivProdFinsupp R f).2 y = f (Sum.inr y) := + rfl +#align finsupp.snd_sum_finsupp_lequiv_prod_finsupp Finsupp.snd_sumFinsuppLequivProdFinsupp + +theorem sumFinsuppLequivProdFinsupp_symm_inl {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (x : α) : + ((sumFinsuppLequivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x := + rfl +#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl Finsupp.sumFinsuppLequivProdFinsupp_symm_inl + +theorem sumFinsuppLequivProdFinsupp_symm_inr {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (y : β) : + ((sumFinsuppLequivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y := + rfl +#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr Finsupp.sumFinsuppLequivProdFinsupp_symm_inr + +end Sum + +section Sigma + +variable {η : Type _} [Fintype η] {ιs : η → Type _} [Zero α] + +variable (R) + +/-- On a `fintype η`, `finsupp.split` is a linear equivalence between +`(Σ (j : η), ιs j) →₀ M` and `Π j, (ιs j →₀ M)`. + +This is the `linear_equiv` version of `finsupp.sigma_finsupp_add_equiv_pi_finsupp`. -/ +noncomputable def sigmaFinsuppLequivPiFinsupp {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] : ((Σj, ιs j) →₀ M) ≃ₗ[R] ∀ j, ιs j →₀ M := + { sigmaFinsuppAddEquivPiFinsupp with + map_smul' := fun c f => by + ext + simp } +#align finsupp.sigma_finsupp_lequiv_pi_finsupp Finsupp.sigmaFinsuppLequivPiFinsupp + +@[simp] +theorem sigmaFinsuppLequivPiFinsupp_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] (f : (Σj, ιs j) →₀ M) (j i) : sigmaFinsuppLequivPiFinsupp R f j i = f ⟨j, i⟩ := + rfl +#align finsupp.sigma_finsupp_lequiv_pi_finsupp_apply Finsupp.sigmaFinsuppLequivPiFinsupp_apply + +@[simp] +theorem sigmaFinsuppLequivPiFinsupp_symm_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] (f : ∀ j, ιs j →₀ M) (ji) : + (Finsupp.sigmaFinsuppLequivPiFinsupp R).symm f ji = f ji.1 ji.2 := + rfl +#align finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply Finsupp.sigmaFinsuppLequivPiFinsupp_symm_apply + +end Sigma + +section Prod + +/-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`. + +This is the `linear_equiv` version of `finsupp.finsupp_prod_equiv`. -/ +noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [Semiring R] + [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M := + { + finsuppProdEquiv with + map_add' := fun f g => by + ext + simp [finsupp_prod_equiv, curry_apply] + map_smul' := fun c f => by + ext + simp [finsupp_prod_equiv, curry_apply] } +#align finsupp.finsupp_prod_lequiv Finsupp.finsuppProdLequiv + +@[simp] +theorem finsuppProdLequiv_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] + (f : α × β →₀ M) (x y) : finsuppProdLequiv R f x y = f (x, y) := by + rw [finsupp_prod_lequiv, LinearEquiv.coe_mk, finsupp_prod_equiv, Finsupp.curry_apply] +#align finsupp.finsupp_prod_lequiv_apply Finsupp.finsuppProdLequiv_apply + +@[simp] +theorem finsuppProdLequiv_symm_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] + (f : α →₀ β →₀ M) (xy) : (finsuppProdLequiv R).symm f xy = f xy.1 xy.2 := by + conv_rhs => + rw [← (finsupp_prod_lequiv R).apply_symm_apply f, finsupp_prod_lequiv_apply, Prod.mk.eta] +#align finsupp.finsupp_prod_lequiv_symm_apply Finsupp.finsuppProdLequiv_symm_apply + +end Prod + +end Finsupp + +section Fintype + +variable {α M : Type _} (R : Type _) [Fintype α] [Semiring R] [AddCommMonoid M] [Module R M] + +variable (S : Type _) [Semiring S] [Module S M] [SMulCommClass R S M] + +variable (v : α → M) + +/-- `fintype.total R S v f` is the linear combination of vectors in `v` with weights in `f`. +This variant of `finsupp.total` is defined on fintype indexed vectors. + +This map is linear in `v` if `R` is commutative, and always linear in `f`. +See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. +-/ +protected def Fintype.total : (α → M) →ₗ[S] (α → R) →ₗ[R] M + where + toFun v := + { toFun := fun f => ∑ i, f i • v i + map_add' := fun f g => by + simp_rw [← Finset.sum_add_distrib, ← add_smul] + rfl + map_smul' := fun r f => by + simp_rw [Finset.smul_sum, smul_smul] + rfl } + map_add' u v := by + ext + simp [Finset.sum_add_distrib, Pi.add_apply, smul_add] + map_smul' r v := by + ext + simp [Finset.smul_sum, smul_comm _ r] +#align fintype.total Fintype.total + +variable {S} + +theorem Fintype.total_apply (f) : Fintype.total R S v f = ∑ i, f i • v i := + rfl +#align fintype.total_apply Fintype.total_apply + +@[simp] +theorem Fintype.total_apply_single (i : α) (r : R) : + Fintype.total R S v (Pi.single i r) = r • v i := + by + simp_rw [Fintype.total_apply, Pi.single_apply, ite_smul, zero_smul] + rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)] +#align fintype.total_apply_single Fintype.total_apply_single + +variable (S) + +theorem Finsupp.total_eq_fintype_total_apply (x : α → R) : + Finsupp.total α M R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) = Fintype.total R S v x := + by + apply Finset.sum_subset + · exact Finset.subset_univ _ + · intro x _ hx + rw [finsupp.not_mem_support_iff.mp hx] + exact zero_smul _ _ +#align finsupp.total_eq_fintype_total_apply Finsupp.total_eq_fintype_total_apply + +theorem Finsupp.total_eq_fintype_total : + (Finsupp.total α M R v).comp (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap = + Fintype.total R S v := + LinearMap.ext <| Finsupp.total_eq_fintype_total_apply R S v +#align finsupp.total_eq_fintype_total Finsupp.total_eq_fintype_total + +variable {S} + +@[simp] +theorem Fintype.range_total : (Fintype.total R S v).range = Submodule.span R (Set.range v) := by + rw [← Finsupp.total_eq_fintype_total, LinearMap.range_comp, LinearEquiv.toLinearMap_eq_coe, + LinearEquiv.range, Submodule.map_top, Finsupp.range_total] +#align fintype.range_total Fintype.range_total + +section SpanRange + +variable {v} {x : M} + +/-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`. +-/ +theorem mem_span_range_iff_exists_fun : x ∈ span R (range v) ↔ ∃ c : α → R, (∑ i, c i • v i) = x := + by + simp only [Finsupp.mem_span_range_iff_exists_finsupp, + finsupp.equiv_fun_on_finite.surjective.exists, Finsupp.equivFunOnFinite_apply] + exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _ +#align mem_span_range_iff_exists_fun mem_span_range_iff_exists_fun + +/-- A family `v : α → V` is generating `V` iff every element `(x : V)` +can be written as sum `∑ cᵢ • vᵢ = x`. +-/ +theorem top_le_span_range_iff_forall_exists_fun : + ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, (∑ i, c i • v i) = x := + by + simp_rw [← mem_span_range_iff_exists_fun] + exact ⟨fun h x => h trivial, fun h x _ => h x⟩ +#align top_le_span_range_iff_forall_exists_fun top_le_span_range_iff_forall_exists_fun + +end SpanRange + +end Fintype + +variable {R : Type _} {M : Type _} {N : Type _} + +variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] + +section + +variable (R) + +/-- Pick some representation of `x : span R w` as a linear combination in `w`, +using the axiom of choice. +-/ +irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R := + ((Finsupp.mem_span_iff_total _ _ _).mp x.2).some +#align span.repr Span.repr + +@[simp] +theorem Span.finsupp_total_repr {w : Set M} (x : span R w) : + Finsupp.total w M R coe (Span.repr R w x) = x := + by + rw [Span.repr] + exact ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose_spec +#align span.finsupp_total_repr Span.finsupp_total_repr + +end + +protected theorem Submodule.finsupp_sum_mem {ι β : Type _} [Zero β] (S : Submodule R M) (f : ι →₀ β) + (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.Sum g ∈ S := + AddSubmonoidClass.finsupp_sum_mem S f g h +#align submodule.finsupp_sum_mem Submodule.finsupp_sum_mem + +theorem LinearMap.map_finsupp_total (f : M →ₗ[R] N) {ι : Type _} {g : ι → M} (l : ι →₀ R) : + f (Finsupp.total ι M R g l) = Finsupp.total ι N R (f ∘ g) l := by + simp only [Finsupp.total_apply, Finsupp.total_apply, Finsupp.sum, f.map_sum, f.map_smul] +#align linear_map.map_finsupp_total LinearMap.map_finsupp_total + +theorem Submodule.exists_finset_of_mem_supᵢ {ι : Sort _} (p : ι → Submodule R M) {m : M} + (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := + by + have := + CompleteLattice.IsCompactElement.exists_finset_of_le_supᵢ (Submodule R M) + (Submodule.singleton_span_isCompactElement m) p + simp only [Submodule.span_singleton_le_iff_mem] at this + exact this hm +#align submodule.exists_finset_of_mem_supr Submodule.exists_finset_of_mem_supᵢ + +/-- `submodule.exists_finset_of_mem_supr` as an `iff` -/ +theorem Submodule.mem_supᵢ_iff_exists_finset {ι : Sort _} {p : ι → Submodule R M} {m : M} : + (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := + ⟨Submodule.exists_finset_of_mem_supᵢ p, fun ⟨_, hs⟩ => + supᵢ_mono (fun i => (supᵢ_const_le : _ ≤ p i)) hs⟩ +#align submodule.mem_supr_iff_exists_finset Submodule.mem_supᵢ_iff_exists_finset + +theorem mem_span_finset {s : Finset M} {x : M} : + x ∈ span R (↑s : Set M) ↔ ∃ f : M → R, (∑ i in s, f i • i) = x := + ⟨fun hx => + let ⟨v, hvs, hvx⟩ := + (Finsupp.mem_span_image_iff_total _).1 + (show x ∈ span R (id '' (↑s : Set M)) by rwa [Set.image_id]) + ⟨v, hvx ▸ (Finsupp.total_apply_of_mem_supported _ hvs).symm⟩, + fun ⟨f, hf⟩ => hf ▸ sum_mem fun i hi => smul_mem _ _ <| subset_span hi⟩ +#align mem_span_finset mem_span_finset + +/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if +`m` can be written as a finite `R`-linear combination of elements of `s`. +The implementation uses `finsupp.sum`. -/ +theorem mem_span_set {m : M} {s : Set M} : + m ∈ Submodule.span R s ↔ + ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.Sum fun mi r => r • mi) = m := + by + conv_lhs => rw [← Set.image_id s] + simp_rw [← exists_prop] + exact Finsupp.mem_span_image_iff_total R +#align mem_span_set mem_span_set + +/-- If `subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/ +@[simps] +def Module.subsingletonEquiv (R M ι : Type _) [Semiring R] [Subsingleton R] [AddCommMonoid M] + [Module R M] : M ≃ₗ[R] ι →₀ R where + toFun m := 0 + invFun f := 0 + left_inv m := by + letI := Module.subsingleton R M + simp only [eq_iff_true_of_subsingleton] + right_inv f := by simp only [eq_iff_true_of_subsingleton] + map_add' m n := (add_zero 0).symm + map_smul' r m := (smul_zero r).symm +#align module.subsingleton_equiv Module.subsingletonEquiv + +namespace LinearMap + +variable {R M} {α : Type _} + +open Finsupp Function + +-- See also `linear_map.splitting_of_fun_on_fintype_surjective` +/-- A surjective linear map to finitely supported functions has a splitting. -/ +def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : (α →₀ R) →ₗ[R] M := + Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some +#align linear_map.splitting_of_finsupp_surjective LinearMap.splittingOfFinsuppSurjective + +theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) : + f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := + by + ext (x y) + dsimp [splitting_of_finsupp_surjective] + congr + rw [sum_single_index, one_smul] + · exact (s (Finsupp.single x 1)).choose_spec + · rw [zero_smul] +#align linear_map.splitting_of_finsupp_surjective_splits LinearMap.splittingOfFinsuppSurjective_splits + +theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : + LeftInverse f (splittingOfFinsuppSurjective f s) := fun g => + LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g +#align linear_map.left_inverse_splitting_of_finsupp_surjective LinearMap.leftInverse_splittingOfFinsuppSurjective + +theorem splittingOfFinsuppSurjective_injective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : + Injective (splittingOfFinsuppSurjective f s) := + (leftInverse_splittingOfFinsuppSurjective f s).Injective +#align linear_map.splitting_of_finsupp_surjective_injective LinearMap.splittingOfFinsuppSurjective_injective + +-- See also `linear_map.splitting_of_finsupp_surjective` +/-- A surjective linear map to functions on a finite type has a splitting. -/ +def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : + (α → R) →ₗ[R] M := + (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some).comp + (linearEquivFunOnFinite R R α).symm.toLinearMap +#align linear_map.splitting_of_fun_on_fintype_surjective LinearMap.splittingOfFunOnFintypeSurjective + +theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) + (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := + by + ext (x y) + dsimp [splitting_of_fun_on_fintype_surjective] + rw [linear_equiv_fun_on_finite_symm_single, Finsupp.sum_single_index, one_smul, + (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single] + rw [zero_smul] +#align linear_map.splitting_of_fun_on_fintype_surjective_splits LinearMap.splittingOfFunOnFintypeSurjective_splits + +theorem leftInverse_splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) + (s : Surjective f) : LeftInverse f (splittingOfFunOnFintypeSurjective f s) := fun g => + LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g +#align linear_map.left_inverse_splitting_of_fun_on_fintype_surjective LinearMap.leftInverse_splittingOfFunOnFintypeSurjective + +theorem splittingOfFunOnFintypeSurjective_injective [Fintype α] (f : M →ₗ[R] α → R) + (s : Surjective f) : Injective (splittingOfFunOnFintypeSurjective f s) := + (leftInverse_splittingOfFunOnFintypeSurjective f s).Injective +#align linear_map.splitting_of_fun_on_fintype_surjective_injective LinearMap.splittingOfFunOnFintypeSurjective_injective + +end LinearMap + From 2bc67b8414c5c070094216050352cdcea896ab29 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 16:17:38 +0100 Subject: [PATCH 03/25] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/LinearAlgebra/Finsupp.lean | 102 ++++++++++------------------- 2 files changed, 36 insertions(+), 67 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 1a56951e35f6c..e370383d54401 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -779,6 +779,7 @@ import Mathlib.Lean.Meta import Mathlib.Lean.Meta.Simp import Mathlib.LinearAlgebra.AffineSpace.Basic import Mathlib.LinearAlgebra.Basic +import Mathlib.LinearAlgebra.Finsupp import Mathlib.LinearAlgebra.GeneralLinearGroup import Mathlib.LinearAlgebra.Pi import Mathlib.LinearAlgebra.Span diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 13a6211b2d883..d55191a5d93cf 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -8,9 +8,9 @@ Authors: Johannes Hölzl ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Data.Finsupp.Defs -import Mathbin.LinearAlgebra.Pi -import Mathbin.LinearAlgebra.Span +import Mathlib.Data.Finsupp.Defs +import Mathlib.LinearAlgebra.Pi +import Mathlib.LinearAlgebra.Span /-! # Properties of the module `α →₀ M` @@ -148,8 +148,7 @@ theorem ker_lsingle (a : α) : (lsingle a : M →ₗ[R] α →₀ M).ker = ⊥ : #align finsupp.ker_lsingle Finsupp.ker_lsingle theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) : - (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := - by + (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := by refine' supᵢ_le fun a₁ => supᵢ_le fun h₁ => range_le_iff_comap.2 _ simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_infi, mem_infi] intro b hb a₂ h₂ @@ -157,14 +156,12 @@ theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) : exact single_eq_of_ne this #align finsupp.lsingle_range_le_ker_lapply Finsupp.lsingle_range_le_ker_lapply -theorem infᵢ_ker_lapply_le_bot : (⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M)) ≤ ⊥ := - by +theorem infᵢ_ker_lapply_le_bot : (⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M)) ≤ ⊥ := by simp only [SetLike.le_def, mem_infi, mem_ker, mem_bot, lapply_apply] exact fun a h => Finsupp.ext h #align finsupp.infi_ker_lapply_le_bot Finsupp.infᵢ_ker_lapply_le_bot -theorem supᵢ_lsingle_range : (⨆ a, (lsingle a : M →ₗ[R] α →₀ M).range) = ⊤ := - by +theorem supᵢ_lsingle_range : (⨆ a, (lsingle a : M →ₗ[R] α →₀ M).range) = ⊤ := by refine' eq_top_iff.2 <| SetLike.le_def.2 fun f _ => _ rw [← sum_single f] exact sum_mem fun a ha => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ @@ -172,8 +169,7 @@ theorem supᵢ_lsingle_range : (⨆ a, (lsingle a : M →ₗ[R] α →₀ M).ran theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : Disjoint (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) - (⨆ a ∈ t, (lsingle a : M →ₗ[R] α →₀ M).range) := - by + (⨆ a ∈ t, (lsingle a : M →ₗ[R] α →₀ M).range) := by refine' (Disjoint.mono (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right) (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right)) @@ -196,8 +192,7 @@ theorem span_single_image (s : Set M) (a : α) : variable (M R) /-- `finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/ -def supported (s : Set α) : Submodule R (α →₀ M) := - by +def supported (s : Set α) : Submodule R (α →₀ M) := by refine' ⟨{ p | ↑p.support ⊆ s }, _, _, _⟩ · intro p q hp hq refine' subset.trans (subset.trans (Finset.coe_subset.2 support_add) _) (union_subset hp hq) @@ -232,8 +227,7 @@ theorem single_mem_supported {s : Set α} {a : α} (b : M) (h : a ∈ s) : #align finsupp.single_mem_supported Finsupp.single_mem_supported theorem supported_eq_span_single (s : Set α) : - supported R R s = span R ((fun i => single i 1) '' s) := - by + supported R R s = span R ((fun i => single i 1) '' s) := by refine' (span_eq_of_le _ _ (SetLike.le_def.2 fun l hl => _)).symm · rintro _ ⟨_, hp, rfl⟩ exact single_mem_supported R 1 hp @@ -269,8 +263,7 @@ theorem restrictDom_apply (s : Set α) (l : α →₀ M) : end theorem restrictDom_comp_subtype (s : Set α) : - (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := - by + (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := by ext (l a) by_cases a ∈ s <;> simp [h] exact ((mem_supported' R l.1).1 l.2 a h).symm @@ -296,8 +289,7 @@ theorem supported_univ : supported M R (Set.univ : Set α) = ⊤ := #align finsupp.supported_univ Finsupp.supported_univ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : - supported M R (⋃ i, s i) = ⨆ i, supported M R (s i) := - by + supported M R (⋃ i, s i) = ⨆ i, supported M R (s i) := by refine' le_antisymm _ (supᵢ_le fun i => supported_mono <| Set.subset_unionᵢ _ _) haveI := Classical.decPred fun x => x ∈ ⋃ i, s i suffices @@ -332,8 +324,7 @@ theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) : #align finsupp.disjoint_supported_supported Finsupp.disjoint_supported_supported theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : - Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t := - by + Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t := by refine' ⟨fun h => set.disjoint_left.mpr fun x hx1 hx2 => _, disjoint_supported_supported⟩ rcases exists_ne (0 : M) with ⟨y, hy⟩ have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩ @@ -343,8 +334,7 @@ theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : /-- Interpret `finsupp.restrict_support_equiv` as a linear equivalence between `supported M R s` and `s →₀ M`. -/ -def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := - by +def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := by let F : supported M R s ≃ (s →₀ M) := restrict_support_equiv s M refine' F.to_linear_equiv _ have : @@ -467,8 +457,7 @@ theorem supported_comap_lmapDomain (f : α → α') (s : Set α') : #align finsupp.supported_comap_lmap_domain Finsupp.supported_comap_lmapDomain theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : - (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := - by + (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := by inhabit α refine' le_antisymm @@ -488,8 +477,7 @@ theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : /- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (a b «expr ∈ » s) -/ theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} (H : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), f a = f b → a = b) : - Disjoint (supported M R s) (lmapDomain M R f).ker := - by + Disjoint (supported M R s) (lmapDomain M R f).ker := by rw [disjoint_iff_inf_le] rintro l ⟨h₁, h₂⟩ rw [SetLike.mem_coe, mem_ker, lmap_domain_apply, map_domain] at h₂ @@ -584,8 +572,7 @@ theorem total_unique [Unique α] (l : α →₀ R) (v) : #align finsupp.total_unique Finsupp.total_unique theorem total_surjective (h : Function.Surjective v) : - Function.Surjective (Finsupp.total α M R v) := - by + Function.Surjective (Finsupp.total α M R v) := by intro x obtain ⟨y, hy⟩ := h x exact ⟨Finsupp.single y 1, by simp [hy]⟩ @@ -602,8 +589,7 @@ theorem total_id_surjective (M) [AddCommMonoid M] [Module R M] : total_surjective R Function.surjective_id #align finsupp.total_id_surjective Finsupp.total_id_surjective -theorem range_total : (Finsupp.total α M R v).range = span R (range v) := - by +theorem range_total : (Finsupp.total α M R v).range = span R (range v) := by ext x constructor · intro hx @@ -626,8 +612,7 @@ theorem lmapDomain_total (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v #align finsupp.lmap_domain_total Finsupp.lmapDomain_total theorem total_comp_lmapDomain (f : α → α') : - (Finsupp.total α' M' R v').comp (Finsupp.lmapDomain R R f) = Finsupp.total α M' R (v' ∘ f) := - by + (Finsupp.total α' M' R v').comp (Finsupp.lmapDomain R R f) = Finsupp.total α M' R (v' ∘ f) := by ext simp #align finsupp.total_comp_lmap_domain Finsupp.total_comp_lmapDomain @@ -670,8 +655,7 @@ theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} : variable (R) theorem span_image_eq_map_total (s : Set α) : - span R (v '' s) = Submodule.map (Finsupp.total α M R v) (supported R R s) := - by + span R (v '' s) = Submodule.map (Finsupp.total α M R v) (supported R R s) := by apply span_eq_of_le · intro x hx rw [Set.mem_image] at hx @@ -690,8 +674,7 @@ theorem span_image_eq_map_total (s : Set α) : #align finsupp.span_image_eq_map_total Finsupp.span_image_eq_map_total theorem mem_span_image_iff_total {s : Set α} {x : M} : - x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, Finsupp.total α M R v l = x := - by + x ∈ span R (v '' s) ↔ ∃ l ∈ supported R R s, Finsupp.total α M R v l = x := by rw [span_image_eq_map_total] simp #align finsupp.mem_span_image_iff_total Finsupp.mem_span_image_iff_total @@ -704,8 +687,7 @@ theorem total_option (v : Option α → M) (f : Option α →₀ R) : theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) : Finsupp.total α M R A (Finsupp.total β (α →₀ R) R B f) = - Finsupp.total β M R (fun b => Finsupp.total α M R A (B b)) f := - by + Finsupp.total β M R (fun b => Finsupp.total α M R A (B b)) f := by simp only [total_apply] apply induction_linear f · simp only [sum_zero_index] @@ -715,8 +697,7 @@ theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f #align finsupp.total_total Finsupp.total_total @[simp] -theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := - by +theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := by ext i apply finZeroElim i #align finsupp.total_fin_zero Finsupp.total_fin_zero @@ -735,16 +716,14 @@ protected def totalOn (s : Set α) : supported R R s →ₗ[R] span R (v '' s) : variable {α} {M} {v} -theorem totalOn_range (s : Set α) : (Finsupp.totalOn α M R v s).range = ⊤ := - by +theorem totalOn_range (s : Set α) : (Finsupp.totalOn α M R v s).range = ⊤ := by rw [Finsupp.totalOn, LinearMap.range_eq_map, LinearMap.map_codRestrict, ← LinearMap.range_le_iff_comap, range_subtype, map_top, LinearMap.range_comp, range_subtype] exact (span_image_eq_map_total _ _).le #align finsupp.total_on_range Finsupp.totalOn_range theorem total_comp (f : α' → α) : - Finsupp.total α' M R (v ∘ f) = (Finsupp.total α M R v).comp (lmapDomain R R f) := - by + Finsupp.total α' M R (v ∘ f) = (Finsupp.total α M R v).comp (lmapDomain R R f) := by ext simp [total_apply] #align finsupp.total_comp Finsupp.total_comp @@ -756,8 +735,7 @@ theorem total_comapDomain (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f #align finsupp.total_comap_domain Finsupp.total_comapDomain theorem total_onFinset {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : - Finsupp.total α M R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := - by + Finsupp.total α M R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := by simp only [Finsupp.total_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset] rw [Finset.sum_filter_of_ne] intro x hx h @@ -807,8 +785,7 @@ theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) /-- An equivalence of sets induces a linear equivalence of `finsupp`s supported on those sets. -/ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : - supported M R s ≃ₗ[R] supported M R t := - by + supported M R s ≃ₗ[R] supported M R t := by haveI := Classical.decPred fun x => x ∈ s haveI := Classical.decPred fun x => x ∈ t refine' Finsupp.supportedEquivFinsupp s ≪≫ₗ (_ ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) @@ -901,16 +878,14 @@ theorem lcongr_apply_apply {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[ #align finsupp.lcongr_apply_apply Finsupp.lcongr_apply_apply theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) : - (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) := - by + (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) := by apply_fun lcongr e₁ e₂ using (lcongr e₁ e₂).Injective simp #align finsupp.lcongr_symm_single Finsupp.lcongr_symm_single @[simp] theorem lcongr_symm {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : - (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm := - by + (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm := by ext rfl #align finsupp.lcongr_symm Finsupp.lcongr_symm @@ -1062,8 +1037,7 @@ theorem Fintype.total_apply (f) : Fintype.total R S v f = ∑ i, f i • v i := @[simp] theorem Fintype.total_apply_single (i : α) (r : R) : - Fintype.total R S v (Pi.single i r) = r • v i := - by + Fintype.total R S v (Pi.single i r) = r • v i := by simp_rw [Fintype.total_apply, Pi.single_apply, ite_smul, zero_smul] rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)] #align fintype.total_apply_single Fintype.total_apply_single @@ -1111,8 +1085,7 @@ theorem mem_span_range_iff_exists_fun : x ∈ span R (range v) ↔ ∃ c : α can be written as sum `∑ cᵢ • vᵢ = x`. -/ theorem top_le_span_range_iff_forall_exists_fun : - ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, (∑ i, c i • v i) = x := - by + ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, (∑ i, c i • v i) = x := by simp_rw [← mem_span_range_iff_exists_fun] exact ⟨fun h x => h trivial, fun h x _ => h x⟩ #align top_le_span_range_iff_forall_exists_fun top_le_span_range_iff_forall_exists_fun @@ -1138,8 +1111,7 @@ irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R := @[simp] theorem Span.finsupp_total_repr {w : Set M} (x : span R w) : - Finsupp.total w M R coe (Span.repr R w x) = x := - by + Finsupp.total w M R coe (Span.repr R w x) = x := by rw [Span.repr] exact ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose_spec #align span.finsupp_total_repr Span.finsupp_total_repr @@ -1157,8 +1129,7 @@ theorem LinearMap.map_finsupp_total (f : M →ₗ[R] N) {ι : Type _} {g : ι #align linear_map.map_finsupp_total LinearMap.map_finsupp_total theorem Submodule.exists_finset_of_mem_supᵢ {ι : Sort _} (p : ι → Submodule R M) {m : M} - (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := - by + (hm : m ∈ ⨆ i, p i) : ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := by have := CompleteLattice.IsCompactElement.exists_finset_of_le_supᵢ (Submodule R M) (Submodule.singleton_span_isCompactElement m) p @@ -1188,8 +1159,7 @@ theorem mem_span_finset {s : Finset M} {x : M} : The implementation uses `finsupp.sum`. -/ theorem mem_span_set {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ - ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.Sum fun mi r => r • mi) = m := - by + ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.Sum fun mi r => r • mi) = m := by conv_lhs => rw [← Set.image_id s] simp_rw [← exists_prop] exact Finsupp.mem_span_image_iff_total R @@ -1222,8 +1192,7 @@ def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f #align linear_map.splitting_of_finsupp_surjective LinearMap.splittingOfFinsuppSurjective theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) : - f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := - by + f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := by ext (x y) dsimp [splitting_of_finsupp_surjective] congr @@ -1251,8 +1220,7 @@ def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s #align linear_map.splitting_of_fun_on_fintype_surjective LinearMap.splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) - (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := - by + (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by ext (x y) dsimp [splitting_of_fun_on_fintype_surjective] rw [linear_equiv_fun_on_finite_symm_single, Finsupp.sum_single_index, one_smul, From c6954fbd75c8f625b08815f488cf0f1d75d008e2 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 16:32:21 +0100 Subject: [PATCH 04/25] remove some empty lines --- Mathlib/LinearAlgebra/Finsupp.lean | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index d55191a5d93cf..aecaac336457c 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -22,32 +22,21 @@ In this file we define `finsupp.supported s` to be the set `{f : α →₀ M | f interpreted as a submodule of `α →₀ M`. We also define `linear_map` versions of various maps: * `finsupp.lsingle a : M →ₗ[R] ι →₀ M`: `finsupp.single a` as a linear map; - * `finsupp.lapply a : (ι →₀ M) →ₗ[R] M`: the map `λ f, f a` as a linear map; - * `finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a linear map; - * `finsupp.restrict_dom`: `finsupp.filter` as a linear map to `finsupp.supported s`; - * `finsupp.lsum`: `finsupp.sum` or `finsupp.lift_add_hom` as a `linear_map`; - * `finsupp.total α M R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with coefficients `l i`; - * `finsupp.total_on`: a restricted version of `finsupp.total` with domain `finsupp.supported R R s` and codomain `submodule.span R (v '' s)`; - * `finsupp.supported_equiv_finsupp`: a linear equivalence between the functions `α →₀ M` supported on `s` and the functions `s →₀ M`; - * `finsupp.lmap_domain`: a linear map version of `finsupp.map_domain`; - * `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`; - * `finsupp.lcongr`: a `linear_equiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ β` and `e' : M ≃ₗ[R] N`. @@ -60,17 +49,13 @@ function with finite support, module, linear algebra noncomputable section open Set LinearMap Submodule - open Classical BigOperators namespace Finsupp variable {α : Type _} {M : Type _} {N : Type _} {P : Type _} {R : Type _} {S : Type _} - variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] - variable [AddCommMonoid N] [Module R N] - variable [AddCommMonoid P] [Module R P] /-- Interpret `finsupp.single a` as a linear map. -/ @@ -1239,4 +1224,3 @@ theorem splittingOfFunOnFintypeSurjective_injective [Fintype α] (f : M →ₗ[R #align linear_map.splitting_of_fun_on_fintype_surjective_injective LinearMap.splittingOfFunOnFintypeSurjective_injective end LinearMap - From 0c5028d0036c14663ead95c8d242a062c9ccee59 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 16:47:24 +0100 Subject: [PATCH 05/25] fix most of first 300 lines --- Mathlib/LinearAlgebra/Finsupp.lean | 70 ++++++++++++++++-------------- 1 file changed, 37 insertions(+), 33 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index aecaac336457c..40f694fc1eb7f 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -89,7 +89,7 @@ def lapply (a : α) : (α →₀ M) →ₗ[R] M := This is the linear version of `finsupp.to_fun`. -/ @[simps] def lcoeFun : (α →₀ M) →ₗ[R] α → M where - toFun := coeFn + toFun := (⇑) map_add' x y := by ext simp @@ -128,46 +128,49 @@ theorem lapply_apply (a : α) (f : α →₀ M) : (lapply a : (α →₀ M) → #align finsupp.lapply_apply Finsupp.lapply_apply @[simp] -theorem ker_lsingle (a : α) : (lsingle a : M →ₗ[R] α →₀ M).ker = ⊥ := +theorem ker_lsingle (a : α) : ker (lsingle a : M →ₗ[R] α →₀ M) = ⊥ := ker_eq_bot_of_injective (single_injective a) #align finsupp.ker_lsingle Finsupp.ker_lsingle theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) : - (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) ≤ ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := by + (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) ≤ + ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := by refine' supᵢ_le fun a₁ => supᵢ_le fun h₁ => range_le_iff_comap.2 _ - simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_infi, mem_infi] + simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_infᵢ, mem_infᵢ] intro b hb a₂ h₂ - have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, Eq.symm ▸ h₂⟩ + have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩ exact single_eq_of_ne this #align finsupp.lsingle_range_le_ker_lapply Finsupp.lsingle_range_le_ker_lapply theorem infᵢ_ker_lapply_le_bot : (⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M)) ≤ ⊥ := by - simp only [SetLike.le_def, mem_infi, mem_ker, mem_bot, lapply_apply] + simp only [SetLike.le_def, mem_infᵢ, mem_ker, mem_bot, lapply_apply] exact fun a h => Finsupp.ext h #align finsupp.infi_ker_lapply_le_bot Finsupp.infᵢ_ker_lapply_le_bot -theorem supᵢ_lsingle_range : (⨆ a, (lsingle a : M →ₗ[R] α →₀ M).range) = ⊤ := by +theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) = ⊤ := by refine' eq_top_iff.2 <| SetLike.le_def.2 fun f _ => _ rw [← sum_single f] exact sum_mem fun a ha => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ #align finsupp.supr_lsingle_range Finsupp.supᵢ_lsingle_range -theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : - Disjoint (⨆ a ∈ s, (lsingle a : M →ₗ[R] α →₀ M).range) - (⨆ a ∈ t, (lsingle a : M →ₗ[R] α →₀ M).range) := by - refine' - (Disjoint.mono (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right) - (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right)) - _ - rw [disjoint_iff_inf_le] - refine' le_trans (le_infᵢ fun i => _) infi_ker_lapply_le_bot - classical - by_cases his : i ∈ s - · by_cases hit : i ∈ t - · exact (hs.le_bot ⟨his, hit⟩).elim - exact inf_le_of_right_le (infᵢ_le_of_le i <| infᵢ_le _ hit) - exact inf_le_of_left_le (infᵢ_le_of_le i <| infᵢ_le _ his) -#align finsupp.disjoint_lsingle_lsingle Finsupp.disjoint_lsingle_lsingle +-- AAHRG this is too slow!!! Commenting out to continue with the rest of the file + +-- theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : +-- Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) +-- (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by +-- refine' +-- (Disjoint.mono (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right) +-- (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right)) +-- _ +-- rw [disjoint_iff_inf_le] +-- refine' le_trans (le_infᵢ fun i => _) infi_ker_lapply_le_bot +-- classical +-- by_cases his : i ∈ s +-- · by_cases hit : i ∈ t +-- · exact (hs.le_bot ⟨his, hit⟩).elim +-- exact inf_le_of_right_le (infᵢ_le_of_le i <| infᵢ_le _ hit) +-- exact inf_le_of_left_le (infᵢ_le_of_le i <| infᵢ_le _ his) +-- #align finsupp.disjoint_lsingle_lsingle Finsupp.disjoint_lsingle_lsingle theorem span_single_image (s : Set M) (a : α) : Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by @@ -178,15 +181,15 @@ variable (M R) /-- `finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/ def supported (s : Set α) : Submodule R (α →₀ M) := by - refine' ⟨{ p | ↑p.support ⊆ s }, _, _, _⟩ + refine' ⟨⟨⟨{ p | ↑p.support ⊆ s }, _⟩, _⟩, _⟩ · intro p q hp hq - refine' subset.trans (subset.trans (Finset.coe_subset.2 support_add) _) (union_subset hp hq) + refine' Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) _) (union_subset hp hq) rw [Finset.coe_union] · simp only [subset_def, Finset.mem_coe, Set.mem_setOf_eq, mem_support_iff, zero_apply] intro h ha exact (ha rfl).elim · intro a p hp - refine' subset.trans (Finset.coe_subset.2 support_smul) hp + refine' Subset.trans (Finset.coe_subset.2 support_smul) hp #align finsupp.supported Finsupp.supported variable {M} @@ -224,7 +227,7 @@ theorem supported_eq_span_single (s : Set α) : apply Set.mem_image_of_mem _ (hl il) #align finsupp.supported_eq_span_single Finsupp.supported_eq_span_single -variable (M R) +variable (M) /-- Interpret `finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/ def restrictDom (s : Set α) : (α →₀ M) →ₗ[R] supported M R s := @@ -254,7 +257,7 @@ theorem restrictDom_comp_subtype (s : Set α) : exact ((mem_supported' R l.1).1 l.2 a h).symm #align finsupp.restrict_dom_comp_subtype Finsupp.restrictDom_comp_subtype -theorem range_restrictDom (s : Set α) : (restrictDom M R s).range = ⊤ := +theorem range_restrictDom (s : Set α) : LinearMap.range (restrictDom M R s) = ⊤ := range_eq_top.2 <| Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s) #align finsupp.range_restrict_dom Finsupp.range_restrictDom @@ -278,11 +281,12 @@ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : refine' le_antisymm _ (supᵢ_le fun i => supported_mono <| Set.subset_unionᵢ _ _) haveI := Classical.decPred fun x => x ∈ ⋃ i, s i suffices - ((Submodule.subtype _).comp (restrict_dom M R (⋃ i, s i))).range ≤ ⨆ i, supported M R (s i) by - rwa [LinearMap.range_comp, range_restrict_dom, map_top, range_subtype] at this + LinearMap.range ((Submodule.subtype _).comp (restrictDom M R (⋃ i, s i))) ≤ + ⨆ i, supported M R (s i) by + rwa [LinearMap.range_comp, range_restrictDom, map_top, range_subtype] at this rw [range_le_iff_comap, eq_top_iff] rintro l ⟨⟩ - apply Finsupp.induction l + induction l using Finsupp.induction · exact zero_mem _ refine' fun x a l hl a0 => add_mem _ by_cases ∃ i, x ∈ s i <;> simp [h] @@ -291,12 +295,12 @@ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : #align finsupp.supported_Union Finsupp.supported_unionᵢ theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := - by erw [Set.union_eq_unionᵢ, supported_Union, supᵢ_bool_eq] <;> rfl + by erw [Set.union_eq_unionᵢ, supported_unionᵢ, supᵢ_bool_eq] <;> rfl #align finsupp.supported_union Finsupp.supported_union theorem supported_interᵢ {ι : Type _} (s : ι → Set α) : supported M R (⋂ i, s i) = ⨅ i, supported M R (s i) := - Submodule.ext fun x => by simp [mem_supported, subset_Inter_iff] + Submodule.ext fun x => by simp [mem_supported, subset_interᵢ_iff] #align finsupp.supported_Inter Finsupp.supported_interᵢ theorem supported_inter (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t := From d55d9c8febaf2a3e6723a4fd72143bb8ecb52411 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 14 Feb 2023 20:04:42 +0100 Subject: [PATCH 06/25] fix a few more lines --- Mathlib/LinearAlgebra/Finsupp.lean | 33 +++++++++++++++--------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 40f694fc1eb7f..b3e1895ae61aa 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -153,8 +153,7 @@ theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] exact sum_mem fun a ha => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ #align finsupp.supr_lsingle_range Finsupp.supᵢ_lsingle_range --- AAHRG this is too slow!!! Commenting out to continue with the rest of the file - +#eval "AAHRG this is too slow!!! Commenting out to continue with the rest of the file" -- theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : -- Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) -- (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by @@ -304,7 +303,7 @@ theorem supported_interᵢ {ι : Type _} (s : ι → Set α) : #align finsupp.supported_Inter Finsupp.supported_interᵢ theorem supported_inter (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t := - by rw [Set.inter_eq_interᵢ, supported_Inter, infᵢ_bool_eq] <;> rfl + by rw [Set.inter_eq_interᵢ, supported_interᵢ, infᵢ_bool_eq] <;> rfl #align finsupp.supported_inter Finsupp.supported_inter theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) : @@ -314,7 +313,7 @@ theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) : theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t := by - refine' ⟨fun h => set.disjoint_left.mpr fun x hx1 hx2 => _, disjoint_supported_supported⟩ + refine' ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => _, disjoint_supported_supported⟩ rcases exists_ne (0 : M) with ⟨y, hy⟩ have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩ rw [mem_bot, single_eq_zero] at this @@ -324,11 +323,11 @@ theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : /-- Interpret `finsupp.restrict_support_equiv` as a linear equivalence between `supported M R s` and `s →₀ M`. -/ def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := by - let F : supported M R s ≃ (s →₀ M) := restrict_support_equiv s M - refine' F.to_linear_equiv _ + let F : supported M R s ≃ (s →₀ M) := restrictSupportEquiv s M + refine' F.toLinearEquiv _ have : (F : supported M R s → ↥s →₀ M) = - (lsubtype_domain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) := + (lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) := rfl rw [this] exact LinearMap.isLinear _ @@ -336,32 +335,32 @@ def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := section Lsum -variable (S) [Module S N] [SMulCommClass R S N] +variable (S) +variable [Module S N] [SMulCommClass R S N] /-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to `N` using `finsupp.sum`. This is an upgraded version of `finsupp.lift_add_hom`. See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/ -def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N - where +def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N where toFun F := - { toFun := fun d => d.Sum fun i => F i - map_add' := (liftAddHom fun x => (F x).toAddMonoidHom).map_add + { toFun := fun d => d.sum fun i => F i + map_add' := (liftAddHom (α := α) (M := M) (N := N) fun x => (F x).toAddMonoidHom).map_add map_smul' := fun c f => by simp [sum_smul_index', smul_sum] } invFun F x := F.comp (lsingle x) left_inv F := by ext (x y) - simp + -- simp right_inv F := by ext (x y) - simp + -- simp map_add' F G := by ext (x y) - simp + -- simp map_smul' F G := by ext (x y) - simp + -- simp #align finsupp.lsum Finsupp.lsum @[simp] @@ -510,6 +509,8 @@ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) → end LcomapDomain +#exit + section Total variable (α) {α' : Type _} (M) {M' : Type _} (R) [AddCommMonoid M'] [Module R M'] (v : α → M) From da30ecec9a90ec33277e878428b8ffe3f05a0886 Mon Sep 17 00:00:00 2001 From: qawbecrdtey Date: Wed, 15 Feb 2023 01:27:13 +0000 Subject: [PATCH 07/25] small fix. --- Mathlib/LinearAlgebra/Finsupp.lean | 105 ++++++++++++++++------------- 1 file changed, 57 insertions(+), 48 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index b3e1895ae61aa..059984d66953a 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -60,7 +60,7 @@ variable [AddCommMonoid P] [Module R P] /-- Interpret `finsupp.single a` as a linear map. -/ def lsingle (a : α) : M →ₗ[R] α →₀ M := - { Finsupp.singleAddHom a with map_smul' := fun a b => (smul_single _ _ _).symm } + { Finsupp.singleAddHom a with map_smul' := fun _ _ => (smul_single _ _ _).symm } #align finsupp.lsingle Finsupp.lsingle /-- Two `R`-linear maps from `finsupp X M` which agree on each `single x y` agree everywhere. -/ @@ -81,7 +81,7 @@ theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (l /-- Interpret `λ (f : α →₀ M), f a` as a linear map. -/ def lapply (a : α) : (α →₀ M) →ₗ[R] M := - { Finsupp.applyAddHom a with map_smul' := fun a b => rfl } + { Finsupp.applyAddHom a with map_smul' := fun _ _ => rfl } #align finsupp.lapply Finsupp.lapply /-- Forget that a function is finitely supported. @@ -106,8 +106,8 @@ variable (s : Set α) def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M where toFun := subtypeDomain fun x => x ∈ s - map_add' a b := subtypeDomain_add - map_smul' c a := ext fun a => rfl + map_add' _ _ := subtypeDomain_add + map_smul' _ _ := ext fun _ => rfl #align finsupp.lsubtype_domain Finsupp.lsubtypeDomain theorem lsubtypeDomain_apply (f : α →₀ M) : @@ -137,7 +137,7 @@ theorem lsingle_range_le_ker_lapply (s t : Set α) (h : Disjoint s t) : ⨅ a ∈ t, ker (lapply a : (α →₀ M) →ₗ[R] M) := by refine' supᵢ_le fun a₁ => supᵢ_le fun h₁ => range_le_iff_comap.2 _ simp only [(ker_comp _ _).symm, eq_top_iff, SetLike.le_def, mem_ker, comap_infᵢ, mem_infᵢ] - intro b hb a₂ h₂ + intro b _ a₂ h₂ have : a₁ ≠ a₂ := fun eq => h.le_bot ⟨h₁, eq.symm ▸ h₂⟩ exact single_eq_of_ne this #align finsupp.lsingle_range_le_ker_lapply Finsupp.lsingle_range_le_ker_lapply @@ -150,7 +150,7 @@ theorem infᵢ_ker_lapply_le_bot : (⨅ a, ker (lapply a : (α →₀ M) →ₗ[ theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) = ⊤ := by refine' eq_top_iff.2 <| SetLike.le_def.2 fun f _ => _ rw [← sum_single f] - exact sum_mem fun a ha => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ + exact sum_mem fun a _ => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ #align finsupp.supr_lsingle_range Finsupp.supᵢ_lsingle_range #eval "AAHRG this is too slow!!! Commenting out to continue with the rest of the file" @@ -173,7 +173,7 @@ theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] theorem span_single_image (s : Set M) (a : α) : Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by - rw [← span_image] <;> rfl + rw [← span_image]; rfl #align finsupp.span_single_image Finsupp.span_single_image variable (M R) @@ -200,8 +200,7 @@ theorem mem_supported {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ /- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (x «expr ∉ » s) -/ theorem mem_supported' {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ∀ (x) (_ : x ∉ s), p x = 0 := by - haveI := Classical.decPred fun x : α => x ∈ s <;> - simp [mem_supported, Set.subset_def, not_imp_comm] + haveI := Classical.decPred fun x : α => x ∈ s; simp [mem_supported, Set.subset_def, not_imp_comm] #align finsupp.mem_supported' Finsupp.mem_supported' theorem mem_supported_support (p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α) := by @@ -232,9 +231,9 @@ variable (M) def restrictDom (s : Set α) : (α →₀ M) →ₗ[R] supported M R s := LinearMap.codRestrict _ { toFun := filter (· ∈ s) - map_add' := fun l₁ l₂ => filter_add - map_smul' := fun a l => filter_smul } fun l => - (mem_supported' _ _).2 fun x => filter_apply_neg (· ∈ s) l + map_add' := fun _ _ => filter_add + map_smul' := fun _ _ => filter_smul } fun l => + (mem_supported' _ _).2 fun _ => filter_apply_neg (· ∈ s) l #align finsupp.restrict_dom Finsupp.restrictDom variable {M R} @@ -261,18 +260,18 @@ theorem range_restrictDom (s : Set α) : LinearMap.range (restrictDom M R s) = Function.RightInverse.surjective <| LinearMap.congr_fun (restrictDom_comp_subtype s) #align finsupp.range_restrict_dom Finsupp.range_restrictDom -theorem supported_mono {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := fun l h => +theorem supported_mono {s t : Set α} (st : s ⊆ t) : supported M R s ≤ supported M R t := fun _ h => Set.Subset.trans h st #align finsupp.supported_mono Finsupp.supported_mono @[simp] theorem supported_empty : supported M R (∅ : Set α) = ⊥ := - eq_bot_iff.2 fun l h => (Submodule.mem_bot R).2 <| by ext <;> simp_all [mem_supported'] + eq_bot_iff.2 fun l h => (Submodule.mem_bot R).2 <| by ext; simp_all [mem_supported'] #align finsupp.supported_empty Finsupp.supported_empty @[simp] theorem supported_univ : supported M R (Set.univ : Set α) = ⊤ := - eq_top_iff.2 fun l _ => Set.subset_univ _ + eq_top_iff.2 fun _ _ => Set.subset_univ _ #align finsupp.supported_univ Finsupp.supported_univ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : @@ -294,7 +293,7 @@ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : #align finsupp.supported_Union Finsupp.supported_unionᵢ theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := - by erw [Set.union_eq_unionᵢ, supported_unionᵢ, supᵢ_bool_eq] <;> rfl + by erw [Set.union_eq_unionᵢ, supported_unionᵢ, supᵢ_bool_eq]; rfl #align finsupp.supported_union Finsupp.supported_union theorem supported_interᵢ {ι : Type _} (s : ι → Set α) : @@ -303,7 +302,7 @@ theorem supported_interᵢ {ι : Type _} (s : ι → Set α) : #align finsupp.supported_Inter Finsupp.supported_interᵢ theorem supported_inter (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t := - by rw [Set.inter_eq_interᵢ, supported_interᵢ, infᵢ_bool_eq] <;> rfl + by rw [Set.inter_eq_interᵢ, supported_interᵢ, infᵢ_bool_eq]; rfl #align finsupp.supported_inter Finsupp.supported_inter theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) : @@ -364,11 +363,11 @@ def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N where #align finsupp.lsum Finsupp.lsum @[simp] -theorem coe_lsum (f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = fun d => d.Sum fun i => f i := +theorem coe_lsum (f : α → M →ₗ[R] N) : (lsum S f : (α →₀ M) → N) = fun d => d.sum fun i => f i := rfl #align finsupp.coe_lsum Finsupp.coe_lsum -theorem lsum_apply (f : α → M →ₗ[R] N) (l : α →₀ M) : Finsupp.lsum S f l = l.Sum fun b => f b := +theorem lsum_apply (f : α → M →ₗ[R] N) (l : α →₀ M) : Finsupp.lsum S f l = l.sum fun b => f b := rfl #align finsupp.lsum_apply Finsupp.lsum_apply @@ -415,7 +414,7 @@ variable {α' : Type _} {α'' : Type _} (M R) def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M where toFun := mapDomain f - map_add' a b := mapDomain_add + map_add' _ _ := mapDomain_add map_smul' := mapDomain_smul #align finsupp.lmap_domain Finsupp.lmapDomain @@ -432,7 +431,7 @@ theorem lmapDomain_id : (lmapDomain M R id : (α →₀ M) →ₗ[R] α →₀ M theorem lmapDomain_comp (f : α → α') (g : α' → α'') : lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f) := - LinearMap.ext fun l => mapDomain_comp + LinearMap.ext fun _ => mapDomain_comp #align finsupp.lmap_domain_comp Finsupp.lmapDomain_comp theorem supported_comap_lmapDomain (f : α → α') (s : Set α') : @@ -451,7 +450,7 @@ theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : le_antisymm (map_le_iff_le_comap.2 <| le_trans (supported_mono <| Set.subset_preimage_image _ _) - (supported_comap_lmap_domain _ _ _ _)) + (supported_comap_lmapDomain _ _ _ _)) _ intro l hl refine' ⟨(lmap_domain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => _, _⟩ @@ -498,13 +497,9 @@ sending `l : β →₀ M` to the finitely supported function from `α` to `M` g This is the linear version of `finsupp.comap_domain`. -/ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M where - toFun l := Finsupp.comapDomain f l (hf.InjOn _) - map_add' x y := by - ext - simp - map_smul' c x := by - ext - simp + toFun l := Finsupp.comapDomain f l (hf.injOn _) + map_add' x y := by ext; simp + map_smul' c x := by ext; simp #align finsupp.lcomap_domain Finsupp.lcomapDomain end LcomapDomain @@ -524,12 +519,12 @@ protected def total : (α →₀ R) →ₗ[R] M := variable {α M v} -theorem total_apply (l : α →₀ R) : Finsupp.total α M R v l = l.Sum fun i a => a • v i := +theorem total_apply (l : α →₀ R) : Finsupp.total α M R v l = l.sum fun i a => a • v i := rfl #align finsupp.total_apply Finsupp.total_apply theorem total_apply_of_mem_supported {l : α →₀ R} {s : Finset α} - (hs : l ∈ supported R R (↑s : Set α)) : Finsupp.total α M R v l = s.Sum fun i => l i • v i := + (hs : l ∈ supported R R (↑s : Set α)) : Finsupp.total α M R v l = s.sum fun i => l i • v i := Finset.sum_subset hs fun x _ hxg => show l x • v x = 0 by rw [not_mem_support_iff.1 hxg, zero_smul] #align finsupp.total_apply_of_mem_supported Finsupp.total_apply_of_mem_supported @@ -638,7 +633,7 @@ theorem mem_span_iff_total (s : Set M) (x : M) : variable {R} theorem mem_span_range_iff_exists_finsupp {v : α → M} {x : M} : - x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.Sum fun i a => a • v i) = x := by + x ∈ span R (range v) ↔ ∃ c : α →₀ R, (c.sum fun i a => a • v i) = x := by simp only [← Finsupp.range_total, LinearMap.mem_range, Finsupp.total_apply] #align finsupp.mem_span_range_iff_exists_finsupp Finsupp.mem_span_range_iff_exists_finsupp @@ -720,7 +715,7 @@ theorem total_comp (f : α' → α) : theorem total_comapDomain (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : Finsupp.total α M R v (Finsupp.comapDomain f l hf) = - (l.support.Preimage f hf).Sum fun i => l (f i) • v i := + (l.support.preimage f hf).sum fun i => l (f i) • v i := by rw [Finsupp.total_apply] <;> rfl #align finsupp.total_comap_domain Finsupp.total_comapDomain @@ -764,7 +759,7 @@ theorem domLcongr_trans {α₁ α₂ α₃ : Type _} (f : α₁ ≃ α₂) (f₂ @[simp] theorem domLcongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : ((Finsupp.domLcongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLcongr f.symm := - LinearEquiv.ext fun x => rfl + LinearEquiv.ext fun _ => rfl #align finsupp.dom_lcongr_symm Finsupp.domLcongr_symm @[simp] @@ -964,23 +959,23 @@ noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [ finsuppProdEquiv with map_add' := fun f g => by ext - simp [finsupp_prod_equiv, curry_apply] + simp [finsuppProdEquiv, curry_apply] map_smul' := fun c f => by ext - simp [finsupp_prod_equiv, curry_apply] } + simp [finsuppProdEquiv, curry_apply] } #align finsupp.finsupp_prod_lequiv Finsupp.finsuppProdLequiv @[simp] theorem finsuppProdLequiv_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (f : α × β →₀ M) (x y) : finsuppProdLequiv R f x y = f (x, y) := by - rw [finsupp_prod_lequiv, LinearEquiv.coe_mk, finsupp_prod_equiv, Finsupp.curry_apply] + rw [finsuppProdLequiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply] #align finsupp.finsupp_prod_lequiv_apply Finsupp.finsuppProdLequiv_apply @[simp] theorem finsuppProdLequiv_symm_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] (f : α →₀ β →₀ M) (xy) : (finsuppProdLequiv R).symm f xy = f xy.1 xy.2 := by conv_rhs => - rw [← (finsupp_prod_lequiv R).apply_symm_apply f, finsupp_prod_lequiv_apply, Prod.mk.eta] + rw [← (finsuppProdLequiv R).apply_symm_apply f, finsuppProdLequiv_apply, Prod.mk.eta] #align finsupp.finsupp_prod_lequiv_symm_apply Finsupp.finsuppProdLequiv_symm_apply end Prod @@ -1109,7 +1104,7 @@ theorem Span.finsupp_total_repr {w : Set M} (x : span R w) : end protected theorem Submodule.finsupp_sum_mem {ι β : Type _} [Zero β] (S : Submodule R M) (f : ι →₀ β) - (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.Sum g ∈ S := + (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S := AddSubmonoidClass.finsupp_sum_mem S f g h #align submodule.finsupp_sum_mem Submodule.finsupp_sum_mem @@ -1149,7 +1144,7 @@ theorem mem_span_finset {s : Finset M} {x : M} : The implementation uses `finsupp.sum`. -/ theorem mem_span_set {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ - ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.Sum fun mi r => r • mi) = m := by + ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m := by conv_lhs => rw [← Set.image_id s] simp_rw [← exists_prop] exact Finsupp.mem_span_image_iff_total R @@ -1189,17 +1184,23 @@ theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : S rw [sum_single_index, one_smul] · exact (s (Finsupp.single x 1)).choose_spec · rw [zero_smul] -#align linear_map.splitting_of_finsupp_surjective_splits LinearMap.splittingOfFinsuppSurjective_splits +#align + linear_map.splitting_of_finsupp_surjective_splits + LinearMap.splittingOfFinsuppSurjective_splits theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : LeftInverse f (splittingOfFinsuppSurjective f s) := fun g => LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g -#align linear_map.left_inverse_splitting_of_finsupp_surjective LinearMap.leftInverse_splittingOfFinsuppSurjective +#align + linear_map.left_inverse_splitting_of_finsupp_surjective + LinearMap.leftInverse_splittingOfFinsuppSurjective theorem splittingOfFinsuppSurjective_injective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : Injective (splittingOfFinsuppSurjective f s) := (leftInverse_splittingOfFinsuppSurjective f s).Injective -#align linear_map.splitting_of_finsupp_surjective_injective LinearMap.splittingOfFinsuppSurjective_injective +#align + linear_map.splitting_of_finsupp_surjective_injective + LinearMap.splittingOfFinsuppSurjective_injective -- See also `linear_map.splitting_of_finsupp_surjective` /-- A surjective linear map to functions on a finite type has a splitting. -/ @@ -1207,7 +1208,9 @@ def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s (α → R) →ₗ[R] M := (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some).comp (linearEquivFunOnFinite R R α).symm.toLinearMap -#align linear_map.splitting_of_fun_on_fintype_surjective LinearMap.splittingOfFunOnFintypeSurjective +#align + linear_map.splitting_of_fun_on_fintype_surjective + LinearMap.splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by @@ -1216,16 +1219,22 @@ theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] rw [linear_equiv_fun_on_finite_symm_single, Finsupp.sum_single_index, one_smul, (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single] rw [zero_smul] -#align linear_map.splitting_of_fun_on_fintype_surjective_splits LinearMap.splittingOfFunOnFintypeSurjective_splits +#align + linear_map.splitting_of_fun_on_fintype_surjective_splits + LinearMap.splittingOfFunOnFintypeSurjective_splits theorem leftInverse_splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : LeftInverse f (splittingOfFunOnFintypeSurjective f s) := fun g => LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g -#align linear_map.left_inverse_splitting_of_fun_on_fintype_surjective LinearMap.leftInverse_splittingOfFunOnFintypeSurjective +#align + linear_map.left_inverse_splitting_of_fun_on_fintype_surjective + LinearMap.leftInverse_splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_injective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : Injective (splittingOfFunOnFintypeSurjective f s) := - (leftInverse_splittingOfFunOnFintypeSurjective f s).Injective -#align linear_map.splitting_of_fun_on_fintype_surjective_injective LinearMap.splittingOfFunOnFintypeSurjective_injective + (leftInverse_splittingOfFunOnFintypeSurjective f s).injective +#align + linear_map.splitting_of_fun_on_fintype_surjective_injective + LinearMap.splittingOfFunOnFintypeSurjective_injective end LinearMap From 4e805ffb60be04f0c7af4dd4d5a95e8115ae0f01 Mon Sep 17 00:00:00 2001 From: Lukas Miaskiwskyi Date: Thu, 16 Feb 2023 21:28:49 +0100 Subject: [PATCH 08/25] simple fixes --- Mathlib/LinearAlgebra/Finsupp.lean | 44 ++++++++++++++++-------------- 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 059984d66953a..2951c20180a9e 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -219,10 +219,11 @@ theorem supported_eq_span_single (s : Set α) : exact single_mem_supported R 1 hp · rw [← l.sum_single] refine' sum_mem fun i il => _ - convert @smul_mem R (α →₀ R) _ _ _ _ (single i 1) (l i) _ - · simp - apply subset_span - apply Set.mem_image_of_mem _ (hl il) + -- Porting note: Needed to help this convert quite a bit replacing underscores + convert smul_mem (M := α →₀ R) (x := single i 1) (span R ((fun i => single i 1) '' s)) (l i) ?_ + · simp [span] + · apply subset_span + apply Set.mem_image_of_mem _ (hl il) #align finsupp.supported_eq_span_single Finsupp.supported_eq_span_single variable (M) @@ -284,12 +285,13 @@ theorem supported_unionᵢ {δ : Type _} (s : δ → Set α) : rwa [LinearMap.range_comp, range_restrictDom, map_top, range_subtype] at this rw [range_le_iff_comap, eq_top_iff] rintro l ⟨⟩ - induction l using Finsupp.induction + -- Porting note: Was ported as `induction l using Finsupp.induction` + refine Finsupp.induction l ?_ ?_ · exact zero_mem _ - refine' fun x a l hl a0 => add_mem _ - by_cases ∃ i, x ∈ s i <;> simp [h] - · cases' h with i hi - exact le_supᵢ (fun i => supported M R (s i)) i (single_mem_supported R _ hi) + · refine' fun x a l _ _ => add_mem _ + by_cases ∃ i, x ∈ s i <;> simp [h] + · cases' h with i hi + exact le_supᵢ (fun i => supported M R (s i)) i (single_mem_supported R _ hi) #align finsupp.supported_Union Finsupp.supported_unionᵢ theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := @@ -400,7 +402,7 @@ theorem lift_symm_apply (f) (x) : ((lift M R X).symm f) x = f (single x 1) := #align finsupp.lift_symm_apply Finsupp.lift_symm_apply @[simp] -theorem lift_apply (f) (g) : ((lift M R X) f) g = g.Sum fun x r => r • f x := +theorem lift_apply (f) (g) : ((lift M R X) f) g = g.sum fun x r => r • f x := rfl #align finsupp.lift_apply Finsupp.lift_apply @@ -425,8 +427,8 @@ theorem lmapDomain_apply (f : α → α') (l : α →₀ M) : #align finsupp.lmap_domain_apply Finsupp.lmapDomain_apply @[simp] -theorem lmapDomain_id : (lmapDomain M R id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id := - LinearMap.ext fun l => mapDomain_id +theorem lmapDomain_id : (lmapDomain M R _root_.id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id := + LinearMap.ext fun _ => mapDomain_id #align finsupp.lmap_domain_id Finsupp.lmapDomain_id theorem lmapDomain_comp (f : α → α') (g : α' → α'') : @@ -446,28 +448,28 @@ theorem supported_comap_lmapDomain (f : α → α') (s : Set α') : theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : (supported M R s).map (lmapDomain M R f) = supported M R (f '' s) := by inhabit α - refine' + refine le_antisymm (map_le_iff_le_comap.2 <| le_trans (supported_mono <| Set.subset_preimage_image _ _) - (supported_comap_lmapDomain _ _ _ _)) - _ + (supported_comap_lmapDomain M R _ _)) + ?_ intro l hl - refine' ⟨(lmap_domain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => _, _⟩ - · rcases Finset.mem_image.1 (map_domain_support hx) with ⟨c, hc, rfl⟩ + refine' ⟨(lmapDomain M R (Function.invFunOn f s) : (α' →₀ M) →ₗ[R] α →₀ M) l, fun x hx => _, _⟩ + · rcases Finset.mem_image.1 (mapDomain_support hx) with ⟨c, hc, rfl⟩ exact Function.invFunOn_mem (by simpa using hl hc) - · rw [← LinearMap.comp_apply, ← lmap_domain_comp] - refine' (map_domain_congr fun c hc => _).trans map_domain_id + · rw [← LinearMap.comp_apply, ← lmapDomain_comp] + refine' (mapDomain_congr fun c hc => _).trans mapDomain_id exact Function.invFunOn_eq (by simpa using hl hc) #align finsupp.lmap_domain_supported Finsupp.lmapDomain_supported /- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (a b «expr ∈ » s) -/ theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} (H : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), f a = f b → a = b) : - Disjoint (supported M R s) (lmapDomain M R f).ker := by + Disjoint (supported M R s) (ker (lmapDomain M R f)) := by rw [disjoint_iff_inf_le] rintro l ⟨h₁, h₂⟩ - rw [SetLike.mem_coe, mem_ker, lmap_domain_apply, map_domain] at h₂ + rw [SetLike.mem_coe, mem_ker, lmapDomain_apply, mapDomain] at h₂ simp; ext x haveI := Classical.decPred fun x => x ∈ s by_cases xs : x ∈ s From bdb8d408e5b32f945523821845921011c7cd864d Mon Sep 17 00:00:00 2001 From: Lukas Miaskiwskyi Date: Thu, 16 Feb 2023 22:02:23 +0100 Subject: [PATCH 09/25] relatively easy fixes --- Mathlib/LinearAlgebra/Finsupp.lean | 73 ++++++++++++++++-------------- 1 file changed, 38 insertions(+), 35 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 2951c20180a9e..48db6113be527 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -351,17 +351,20 @@ def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N where map_smul' := fun c f => by simp [sum_smul_index', smul_sum] } invFun F x := F.comp (lsingle x) left_inv F := by - ext (x y) - -- simp + -- Porting note: first line of the following four proofs was `ext (x y)`, applied wrong ext lemmas + apply Finsupp.lhom_ext' + simp right_inv F := by - ext (x y) - -- simp + -- Porting note: `repeat {Finsupp.lhom_ext'}` does not currently work + apply Finsupp.lhom_ext' + apply Finsupp.lhom_ext' map_add' F G := by - ext (x y) - -- simp + apply Finsupp.lhom_ext' + simp map_smul' F G := by - ext (x y) - -- simp + apply Finsupp.lhom_ext' + apply Finsupp.lhom_ext' + simp #align finsupp.lsum Finsupp.lsum @[simp] @@ -477,8 +480,8 @@ theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} by rw [h₂] rfl - rw [Finsupp.sum_apply, Finsupp.sum, Finset.sum_eq_single x] at this - · simpa [Finsupp.single_apply] + rw [Finsupp.sum_apply, Finsupp.sum, Finset.sum_eq_single x, single_eq_same] at this + · simpa · intro y hy xy simp [mt (H _ (h₁ hy) _ xs) xy] · simp (config := { contextual := true }) @@ -490,7 +493,7 @@ end LmapDomain section LcomapDomain -variable {β : Type _} {R M} +variable {β : Type _} /-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomap_domain f hf` is the linear map sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing @@ -506,17 +509,15 @@ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) → end LcomapDomain -#exit - section Total -variable (α) {α' : Type _} (M) {M' : Type _} (R) [AddCommMonoid M'] [Module R M'] (v : α → M) - {v' : α' → M'} +variable (α) {α' : Type _} (M) {M' : Type _} (R) [Semiring R] [AddCommMonoid M'] [AddCommMonoid M] + [Module R M'] [Module R M] (v : α → M) {v' : α' → M'} /-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and evaluates this linear combination. -/ protected def total : (α →₀ R) →ₗ[R] M := - Finsupp.lsum ℕ fun i => LinearMap.id.smul_right (v i) + Finsupp.lsum ℕ fun i => LinearMap.id.smulRight (v i) #align finsupp.total Finsupp.total variable {α M v} @@ -565,18 +566,18 @@ theorem total_surjective (h : Function.Surjective v) : exact ⟨Finsupp.single y 1, by simp [hy]⟩ #align finsupp.total_surjective Finsupp.total_surjective -theorem total_range (h : Function.Surjective v) : (Finsupp.total α M R v).range = ⊤ := +theorem total_range (h : Function.Surjective v) : LinearMap.range (Finsupp.total α M R v) = ⊤ := range_eq_top.2 <| total_surjective R h #align finsupp.total_range Finsupp.total_range /-- Any module is a quotient of a free module. This is stated as surjectivity of `finsupp.total M M R id : (M →₀ R) →ₗ[R] M`. -/ theorem total_id_surjective (M) [AddCommMonoid M] [Module R M] : - Function.Surjective (Finsupp.total M M R id) := + Function.Surjective (Finsupp.total M M R _root_.id) := total_surjective R Function.surjective_id #align finsupp.total_id_surjective Finsupp.total_id_surjective -theorem range_total : (Finsupp.total α M R v).range = span R (range v) := by +theorem range_total : LinearMap.range (Finsupp.total α M R v) = span R (range v) := by ext x constructor · intro hx @@ -584,7 +585,7 @@ theorem range_total : (Finsupp.total α M R v).range = span R (range v) := by rcases hx with ⟨l, hl⟩ rw [← hl] rw [Finsupp.total_apply] - exact sum_mem fun i hi => Submodule.smul_mem _ _ (subset_span (mem_range_self i)) + exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i)) · apply span_le.2 intro x hx rcases hx with ⟨i, hi⟩ @@ -595,19 +596,20 @@ theorem range_total : (Finsupp.total α M R v).range = span R (range v) := by theorem lmapDomain_total (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) : (Finsupp.total α' M' R v').comp (lmapDomain R R f) = g.comp (Finsupp.total α M R v) := by - ext l <;> simp [total_apply, Finsupp.sum_mapDomain_index, add_smul, h] + ext l + simp [total_apply, Finsupp.sum_mapDomain_index, add_smul, h] #align finsupp.lmap_domain_total Finsupp.lmapDomain_total theorem total_comp_lmapDomain (f : α → α') : (Finsupp.total α' M' R v').comp (Finsupp.lmapDomain R R f) = Finsupp.total α M' R (v' ∘ f) := by - ext + apply lhom_ext' simp #align finsupp.total_comp_lmap_domain Finsupp.total_comp_lmapDomain @[simp] theorem total_embDomain (f : α ↪ α') (l : α →₀ R) : (Finsupp.total α' M' R v') (embDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l := by - simp [total_apply, Finsupp.sum, support_emb_domain, emb_domain_apply] + simp [total_apply, Finsupp.sum, support_embDomain, embDomain_apply] #align finsupp.total_emb_domain Finsupp.total_embDomain @[simp] @@ -619,16 +621,16 @@ theorem total_mapDomain (f : α → α') (l : α →₀ R) : @[simp] theorem total_equivMapDomain (f : α ≃ α') (l : α →₀ R) : (Finsupp.total α' M' R v') (equivMapDomain f l) = (Finsupp.total α M' R (v' ∘ f)) l := by - rw [equiv_map_domain_eq_map_domain, total_map_domain] + rw [equivMapDomain_eq_mapDomain, total_mapDomain] #align finsupp.total_equiv_map_domain Finsupp.total_equivMapDomain /-- A version of `finsupp.range_total` which is useful for going in the other direction -/ -theorem span_eq_range_total (s : Set M) : span R s = (Finsupp.total s M R coe).range := by +theorem span_eq_range_total (s : Set M) : span R s = LinearMap.range (Finsupp.total s M R (↑)) := by rw [range_total, Subtype.range_coe_subtype, Set.setOf_mem_eq] #align finsupp.span_eq_range_total Finsupp.span_eq_range_total theorem mem_span_iff_total (s : Set M) (x : M) : - x ∈ span R s ↔ ∃ l : s →₀ R, Finsupp.total s M R coe l = x := + x ∈ span R s ↔ ∃ l : s →₀ R, Finsupp.total s M R (↑) l = x := (SetLike.ext_iff.1 <| span_eq_range_total _ _) x #align finsupp.mem_span_iff_total Finsupp.mem_span_iff_total @@ -669,7 +671,7 @@ theorem mem_span_image_iff_total {s : Set α} {x : M} : theorem total_option (v : Option α → M) (f : Option α →₀ R) : Finsupp.total (Option α) M R v f = f none • v none + Finsupp.total α M R (v ∘ Option.some) f.some := - by rw [total_apply, sum_option_index_smul, total_apply] + by rw [total_apply, sum_option_index_smul, total_apply]; simp #align finsupp.total_option Finsupp.total_option theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f : β →₀ R) : @@ -685,7 +687,7 @@ theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f @[simp] theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := by - ext i + apply lhom_ext' apply finZeroElim i #align finsupp.total_fin_zero Finsupp.total_fin_zero @@ -703,7 +705,7 @@ protected def totalOn (s : Set α) : supported R R s →ₗ[R] span R (v '' s) : variable {α} {M} {v} -theorem totalOn_range (s : Set α) : (Finsupp.totalOn α M R v s).range = ⊤ := by +theorem totalOn_range (s : Set α) : LinearMap.range (Finsupp.totalOn α M R v s) = ⊤ := by rw [Finsupp.totalOn, LinearMap.range_eq_map, LinearMap.map_codRestrict, ← LinearMap.range_le_iff_comap, range_subtype, map_top, LinearMap.range_comp, range_subtype] exact (span_image_eq_map_total _ _).le @@ -711,21 +713,21 @@ theorem totalOn_range (s : Set α) : (Finsupp.totalOn α M R v s).range = ⊤ := theorem total_comp (f : α' → α) : Finsupp.total α' M R (v ∘ f) = (Finsupp.total α M R v).comp (lmapDomain R R f) := by - ext + apply lhom_ext' simp [total_apply] #align finsupp.total_comp Finsupp.total_comp theorem total_comapDomain (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : Finsupp.total α M R v (Finsupp.comapDomain f l hf) = (l.support.preimage f hf).sum fun i => l (f i) • v i := - by rw [Finsupp.total_apply] <;> rfl + by rw [Finsupp.total_apply]; rfl #align finsupp.total_comap_domain Finsupp.total_comapDomain theorem total_onFinset {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : Finsupp.total α M R g (Finsupp.onFinset s f hf) = Finset.sum s fun x : α => f x • g x := by simp only [Finsupp.total_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset] rw [Finset.sum_filter_of_ne] - intro x hx h + intro x _ h contrapose! h simp [h] #align finsupp.total_on_finset Finsupp.total_onFinset @@ -738,7 +740,7 @@ This is `finsupp.dom_congr` as a `linear_equiv`. See also `linear_map.fun_congr_left` for the case of arbitrary functions. -/ protected def domLcongr {α₁ α₂ : Type _} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M := (Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by - simpa only [equiv_map_domain_eq_map_domain, dom_congr_apply] using (lmap_domain M R e).map_smul + simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul #align finsupp.dom_lcongr Finsupp.domLcongr @[simp] @@ -767,9 +769,10 @@ theorem domLcongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : @[simp] theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (i : α₁) (m : M) : (Finsupp.domLcongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by - simp [Finsupp.domLcongr, Finsupp.domCongr, equiv_map_domain_single] + simp [Finsupp.domLcongr, Finsupp.domCongr, equivMapDomain_single] #align finsupp.dom_lcongr_single Finsupp.domLcongr_single +#exit /-- An equivalence of sets induces a linear equivalence of `finsupp`s supported on those sets. -/ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : supported M R s ≃ₗ[R] supported M R t := by @@ -780,7 +783,7 @@ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) #align finsupp.congr Finsupp.congr /-- `finsupp.map_range` as a `linear_map`. -/ -@[simps] +@[simps!] def mapRange.linearMap (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N := { mapRange.addMonoidHom From 315620190280dccddf5793d0353b1f0569551587 Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 13:23:22 +0900 Subject: [PATCH 10/25] fix LinearMap.coe_mk --- 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 e98e90767d19c..55d141e5c6ea5 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -269,8 +269,8 @@ protected def Simps.apply {R S : Type _} [Semiring R] [Semiring S] (σ : R →+* initialize_simps_projections LinearMap (toAddHom_toFun → apply) @[simp] -theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) : - ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f := +theorem coe_mk {σ : R →+* S} (f : M → M₃) (h₁ h₂) : + ((LinearMap.mk (AddHom.mk f h₁) h₂ : M →ₛₗ[σ] M₃) : M → M₃) = f := rfl #align linear_map.coe_mk LinearMap.coe_mk From bc5ae5042c30caed88c1df1fbbea65e77a7e40cb Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 14:09:27 +0900 Subject: [PATCH 11/25] 51 red errors left --- Mathlib/LinearAlgebra/Finsupp.lean | 37 +++++++++++++----------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 48db6113be527..a80e2e69a0b9b 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -73,7 +73,8 @@ theorem lhom_ext ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a b, φ (singl 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] +-- Porting note: The priority should be higher than `LinearMap.ext`. +@[ext high] theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) : φ = ψ := lhom_ext fun a => LinearMap.congr_fun (h a) @@ -197,7 +198,6 @@ theorem mem_supported {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ Iff.rfl #align finsupp.mem_supported Finsupp.mem_supported -/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (x «expr ∉ » s) -/ theorem mem_supported' {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ∀ (x) (_ : x ∉ s), p x = 0 := by haveI := Classical.decPred fun x : α => x ∈ s; simp [mem_supported, Set.subset_def, not_imp_comm] @@ -351,19 +351,16 @@ def lsum : (α → M →ₗ[R] N) ≃ₗ[S] (α →₀ M) →ₗ[R] N where map_smul' := fun c f => by simp [sum_smul_index', smul_sum] } invFun F x := F.comp (lsingle x) left_inv F := by - -- Porting note: first line of the following four proofs was `ext (x y)`, applied wrong ext lemmas - apply Finsupp.lhom_ext' + ext x y simp right_inv F := by - -- Porting note: `repeat {Finsupp.lhom_ext'}` does not currently work - apply Finsupp.lhom_ext' - apply Finsupp.lhom_ext' + ext x y + simp map_add' F G := by - apply Finsupp.lhom_ext' + ext x y simp map_smul' F G := by - apply Finsupp.lhom_ext' - apply Finsupp.lhom_ext' + ext x y simp #align finsupp.lsum Finsupp.lsum @@ -441,11 +438,10 @@ theorem lmapDomain_comp (f : α → α') (g : α' → α'') : theorem supported_comap_lmapDomain (f : α → α') (s : Set α') : supported M R (f ⁻¹' s) ≤ (supported M R s).comap (lmapDomain M R f) := - fun l (hl : ↑l.support ⊆ f ⁻¹' s) => - show ↑(mapDomain f l).support ⊆ s - by + fun l (hl : (l.support : Set α) ⊆ f ⁻¹' s) => + show ↑(mapDomain f l).support ⊆ s by rw [← Set.image_subset_iff, ← Finset.coe_image] at hl - exact Set.Subset.trans map_domain_support hl + exact Set.Subset.trans mapDomain_support hl #align finsupp.supported_comap_lmap_domain Finsupp.supported_comap_lmapDomain theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : @@ -602,7 +598,7 @@ theorem lmapDomain_total (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v theorem total_comp_lmapDomain (f : α → α') : (Finsupp.total α' M' R v').comp (Finsupp.lmapDomain R R f) = Finsupp.total α M' R (v' ∘ f) := by - apply lhom_ext' + ext simp #align finsupp.total_comp_lmap_domain Finsupp.total_comp_lmapDomain @@ -658,6 +654,8 @@ theorem span_image_eq_map_total (s : Set α) : by_cases c ∈ s · exact smul_mem _ _ (subset_span (Set.mem_image_of_mem _ h)) · simp [(Finsupp.mem_supported' R _).1 hz _ h] + -- Porting note: `rw` is required to infer metavariables in `sum_mem`. + rw [mem_comap, total_apply] refine' sum_mem _ simp [this] #align finsupp.span_image_eq_map_total Finsupp.span_image_eq_map_total @@ -687,7 +685,7 @@ theorem total_total {α β : Type _} (A : α → M) (B : β → α →₀ R) (f @[simp] theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := by - apply lhom_ext' + ext i apply finZeroElim i #align finsupp.total_fin_zero Finsupp.total_fin_zero @@ -713,7 +711,7 @@ theorem totalOn_range (s : Set α) : LinearMap.range (Finsupp.totalOn α M R v s theorem total_comp (f : α' → α) : Finsupp.total α' M R (v ∘ f) = (Finsupp.total α M R v).comp (lmapDomain R R f) := by - apply lhom_ext' + ext simp [total_apply] #align finsupp.total_comp Finsupp.total_comp @@ -772,7 +770,6 @@ theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) simp [Finsupp.domLcongr, Finsupp.domCongr, equivMapDomain_single] #align finsupp.dom_lcongr_single Finsupp.domLcongr_single -#exit /-- An equivalence of sets induces a linear equivalence of `finsupp`s supported on those sets. -/ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : supported M R s ≃ₗ[R] supported M R t := by @@ -1189,9 +1186,7 @@ theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : S rw [sum_single_index, one_smul] · exact (s (Finsupp.single x 1)).choose_spec · rw [zero_smul] -#align - linear_map.splitting_of_finsupp_surjective_splits - LinearMap.splittingOfFinsuppSurjective_splits +#align linear_map.splitting_of_finsupp_surjective_splits LinearMap.splittingOfFinsuppSurjective_splits theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : LeftInverse f (splittingOfFinsuppSurjective f s) := fun g => From 9b5813416fc0af41ee32f84f28d5aa1de6e9763d Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 14:16:22 +0900 Subject: [PATCH 12/25] align --- Mathlib/LinearAlgebra/Finsupp.lean | 24 ++++++------------------ 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index a80e2e69a0b9b..b980446b23d1e 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -1191,16 +1191,12 @@ theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : S theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : LeftInverse f (splittingOfFinsuppSurjective f s) := fun g => LinearMap.congr_fun (splittingOfFinsuppSurjective_splits f s) g -#align - linear_map.left_inverse_splitting_of_finsupp_surjective - LinearMap.leftInverse_splittingOfFinsuppSurjective +#align linear_map.left_inverse_splitting_of_finsupp_surjective LinearMap.leftInverse_splittingOfFinsuppSurjective theorem splittingOfFinsuppSurjective_injective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : Injective (splittingOfFinsuppSurjective f s) := (leftInverse_splittingOfFinsuppSurjective f s).Injective -#align - linear_map.splitting_of_finsupp_surjective_injective - LinearMap.splittingOfFinsuppSurjective_injective +#align linear_map.splitting_of_finsupp_surjective_injective LinearMap.splittingOfFinsuppSurjective_injective -- See also `linear_map.splitting_of_finsupp_surjective` /-- A surjective linear map to functions on a finite type has a splitting. -/ @@ -1208,9 +1204,7 @@ def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s (α → R) →ₗ[R] M := (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some).comp (linearEquivFunOnFinite R R α).symm.toLinearMap -#align - linear_map.splitting_of_fun_on_fintype_surjective - LinearMap.splittingOfFunOnFintypeSurjective +#align linear_map.splitting_of_fun_on_fintype_surjective LinearMap.splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by @@ -1219,22 +1213,16 @@ theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] rw [linear_equiv_fun_on_finite_symm_single, Finsupp.sum_single_index, one_smul, (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single] rw [zero_smul] -#align - linear_map.splitting_of_fun_on_fintype_surjective_splits - LinearMap.splittingOfFunOnFintypeSurjective_splits +#align linear_map.splitting_of_fun_on_fintype_surjective_splits LinearMap.splittingOfFunOnFintypeSurjective_splits theorem leftInverse_splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : LeftInverse f (splittingOfFunOnFintypeSurjective f s) := fun g => LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g -#align - linear_map.left_inverse_splitting_of_fun_on_fintype_surjective - LinearMap.leftInverse_splittingOfFunOnFintypeSurjective +#align linear_map.left_inverse_splitting_of_fun_on_fintype_surjective LinearMap.leftInverse_splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_injective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : Injective (splittingOfFunOnFintypeSurjective f s) := (leftInverse_splittingOfFunOnFintypeSurjective f s).injective -#align - linear_map.splitting_of_fun_on_fintype_surjective_injective - LinearMap.splittingOfFunOnFintypeSurjective_injective +#align linear_map.splitting_of_fun_on_fintype_surjective_injective LinearMap.splittingOfFunOnFintypeSurjective_injective end LinearMap From a9c2330520f8942e5007eea5a479331b97f915fe Mon Sep 17 00:00:00 2001 From: Lukas Miaskiwskyi Date: Fri, 17 Feb 2023 10:47:17 +0100 Subject: [PATCH 13/25] simplex fixes plus docstrings --- Mathlib/LinearAlgebra/Finsupp.lean | 132 ++++++++++++++--------------- 1 file changed, 66 insertions(+), 66 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index b980446b23d1e..248945a9a9962 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -16,28 +16,28 @@ import Mathlib.LinearAlgebra.Span # Properties of the module `α →₀ M` Given an `R`-module `M`, the `R`-module structure on `α →₀ M` is defined in -`data.finsupp.basic`. +`data.Finsupp.basic`. -In this file we define `finsupp.supported s` to be the set `{f : α →₀ M | f.support ⊆ s}` -interpreted as a submodule of `α →₀ M`. We also define `linear_map` versions of various maps: +In this file we define `Finsupp.supported s` to be the set `{f : α →₀ M | f.support ⊆ s}` +interpreted as a submodule of `α →₀ M`. We also define `LinearMap` versions of various maps: -* `finsupp.lsingle a : M →ₗ[R] ι →₀ M`: `finsupp.single a` as a linear map; -* `finsupp.lapply a : (ι →₀ M) →ₗ[R] M`: the map `λ f, f a` as a linear map; -* `finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a +* `Finsupp.lsingle a : M →ₗ[R] ι →₀ M`: `Finsupp.single a` as a linear map; +* `Finsupp.lapply a : (ι →₀ M) →ₗ[R] M`: the map `λ f, f a` as a linear map; +* `Finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a linear map; -* `finsupp.restrict_dom`: `finsupp.filter` as a linear map to `finsupp.supported s`; -* `finsupp.lsum`: `finsupp.sum` or `finsupp.lift_add_hom` as a `linear_map`; -* `finsupp.total α M R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with +* `Finsupp.restrict_dom`: `Finsupp.filter` as a linear map to `Finsupp.supported s`; +* `Finsupp.lsum`: `Finsupp.sum` or `Finsupp.lift_add_hom` as a `LinearMap`; +* `Finsupp.total α M R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with coefficients `l i`; -* `finsupp.total_on`: a restricted version of `finsupp.total` with domain `finsupp.supported R R s` - and codomain `submodule.span R (v '' s)`; -* `finsupp.supported_equiv_finsupp`: a linear equivalence between the functions `α →₀ M` supported +* `Finsupp.total_on`: a restricted version of `Finsupp.total` with domain `Finsupp.supported R R s` + and codomain `Submodule.span R (v '' s)`; +* `Finsupp.supported_equiv_finsupp`: a linear equivalence between the functions `α →₀ M` supported on `s` and the functions `s →₀ M`; -* `finsupp.lmap_domain`: a linear map version of `finsupp.map_domain`; -* `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 +* `Finsupp.lmap_domain`: a linear map version of `Finsupp.map_domain`; +* `Finsupp.dom_lcongr`: a `LinearEquiv` version of `Finsupp.domCongr`; +* `Finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to `supported M R t`; -* `finsupp.lcongr`: a `linear_equiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ +* `Finsupp.lcongr`: a `LinearEquiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ β` and `e' : M ≃ₗ[R] N`. ## Tags @@ -58,17 +58,17 @@ variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] variable [AddCommMonoid N] [Module R N] variable [AddCommMonoid P] [Module R P] -/-- Interpret `finsupp.single a` as a linear map. -/ +/-- Interpret `Finsupp.single a` as a linear map. -/ def lsingle (a : α) : M →ₗ[R] α →₀ M := { Finsupp.singleAddHom a with map_smul' := fun _ _ => (smul_single _ _ _).symm } #align finsupp.lsingle Finsupp.lsingle -/-- Two `R`-linear maps from `finsupp X M` which agree on each `single x y` agree everywhere. -/ +/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere. -/ theorem lhom_ext ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a b, φ (single a b) = ψ (single a b)) : φ = ψ := LinearMap.toAddMonoidHom_injective <| addHom_ext h #align finsupp.lhom_ext Finsupp.lhom_ext -/-- Two `R`-linear maps from `finsupp X M` which agree on each `single x y` agree everywhere. +/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` 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 @@ -87,7 +87,7 @@ def lapply (a : α) : (α →₀ M) →ₗ[R] M := /-- Forget that a function is finitely supported. -This is the linear version of `finsupp.to_fun`. -/ +This is the linear version of `Finsupp.to_fun`. -/ @[simps] def lcoeFun : (α →₀ M) →ₗ[R] α → M where toFun := (⇑) @@ -103,7 +103,7 @@ section LsubtypeDomain variable (s : Set α) -/-- Interpret `finsupp.subtype_domain s` as a linear map. -/ +/-- Interpret `Finsupp.subtype_domain s` as a linear map. -/ def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M where toFun := subtypeDomain fun x => x ∈ s @@ -179,7 +179,7 @@ theorem span_single_image (s : Set M) (a : α) : variable (M R) -/-- `finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/ +/-- `Finsupp.supported M R s` is the `R`-submodule of all `p : α →₀ M` such that `p.support ⊆ s`. -/ def supported (s : Set α) : Submodule R (α →₀ M) := by refine' ⟨⟨⟨{ p | ↑p.support ⊆ s }, _⟩, _⟩, _⟩ · intro p q hp hq @@ -228,7 +228,7 @@ theorem supported_eq_span_single (s : Set α) : variable (M) -/-- Interpret `finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/ +/-- Interpret `Finsupp.filter s` as a linear map from `α →₀ M` to `supported M R s`. -/ def restrictDom (s : Set α) : (α →₀ M) →ₗ[R] supported M R s := LinearMap.codRestrict _ { toFun := filter (· ∈ s) @@ -321,7 +321,7 @@ theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : exact hy this #align finsupp.disjoint_supported_supported_iff Finsupp.disjoint_supported_supported_iff -/-- Interpret `finsupp.restrict_support_equiv` as a linear equivalence between +/-- Interpret `Finsupp.restrict_support_equiv` as a linear equivalence between `supported M R s` and `s →₀ M`. -/ def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := by let F : supported M R s ≃ (s →₀ M) := restrictSupportEquiv s M @@ -340,7 +340,7 @@ variable (S) variable [Module S N] [SMulCommClass R S N] /-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to -`N` using `finsupp.sum`. This is an upgraded version of `finsupp.lift_add_hom`. +`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.lift_add_hom`. See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/ @@ -412,7 +412,7 @@ section LmapDomain variable {α' : Type _} {α'' : Type _} (M R) -/-- Interpret `finsupp.map_domain` as a linear map. -/ +/-- Interpret `Finsupp.map_domain` as a linear map. -/ def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M where toFun := mapDomain f @@ -495,7 +495,7 @@ variable {β : Type _} sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing `l` with `f`. -This is the linear version of `finsupp.comap_domain`. -/ +This is the linear version of `Finsupp.comap_domain`. -/ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M where toFun l := Finsupp.comapDomain f l (hf.injOn _) @@ -567,7 +567,7 @@ theorem total_range (h : Function.Surjective v) : LinearMap.range (Finsupp.total #align finsupp.total_range Finsupp.total_range /-- Any module is a quotient of a free module. This is stated as surjectivity of -`finsupp.total M M R id : (M →₀ R) →ₗ[R] M`. -/ +`Finsupp.total M M R id : (M →₀ R) →ₗ[R] M`. -/ theorem total_id_surjective (M) [AddCommMonoid M] [Module R M] : Function.Surjective (Finsupp.total M M R _root_.id) := total_surjective R Function.surjective_id @@ -620,7 +620,7 @@ theorem total_equivMapDomain (f : α ≃ α') (l : α →₀ R) : rw [equivMapDomain_eq_mapDomain, total_mapDomain] #align finsupp.total_equiv_map_domain Finsupp.total_equivMapDomain -/-- A version of `finsupp.range_total` which is useful for going in the other direction -/ +/-- A version of `Finsupp.range_total` which is useful for going in the other direction -/ theorem span_eq_range_total (s : Set M) : span R s = LinearMap.range (Finsupp.total s M R (↑)) := by rw [range_total, Subtype.range_coe_subtype, Set.setOf_mem_eq] #align finsupp.span_eq_range_total Finsupp.span_eq_range_total @@ -691,7 +691,7 @@ theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := by variable (α) (M) (v) -/-- `finsupp.total_on M v s` interprets `p : α →₀ R` as a linear combination of a +/-- `Finsupp.total_on M v s` interprets `p : α →₀ R` as a linear combination of a subset of the vectors in `v`, mapping it to the span of those vectors. The subset is indicated by a set `s : set α` of indices. @@ -734,8 +734,8 @@ end Total /-- An equivalence of domains induces a linear equivalence of finitely supported functions. -This is `finsupp.dom_congr` as a `linear_equiv`. -See also `linear_map.fun_congr_left` for the case of arbitrary functions. -/ +This is `Finsupp.domCongr` as a `LinearEquiv`. +See also `LinearMap.fun_congr_left` for the case of arbitrary functions. -/ protected def domLcongr {α₁ α₂ : Type _} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M := (Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul @@ -770,7 +770,7 @@ theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) simp [Finsupp.domLcongr, Finsupp.domCongr, equivMapDomain_single] #align finsupp.dom_lcongr_single Finsupp.domLcongr_single -/-- An equivalence of sets induces a linear equivalence of `finsupp`s supported on those sets. -/ +/-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets. -/ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : supported M R s ≃ₗ[R] supported M R t := by haveI := Classical.decPred fun x => x ∈ s @@ -779,7 +779,7 @@ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) exact Finsupp.domLcongr e #align finsupp.congr Finsupp.congr -/-- `finsupp.map_range` as a `linear_map`. -/ +/-- `Finsupp.mapRange` as a `LinearMap`. -/ @[simps!] def mapRange.linearMap (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N := { @@ -808,7 +808,7 @@ theorem mapRange.linearMap_toAddMonoidHom (f : M →ₗ[R] N) : AddMonoidHom.ext fun _ => rfl #align finsupp.map_range.linear_map_to_add_monoid_hom Finsupp.mapRange.linearMap_toAddMonoidHom -/-- `finsupp.map_range` as a `linear_equiv`. -/ +/-- `Finsupp.mapRange` as a `LinearEquiv`. -/ @[simps apply] def mapRange.linearEquiv (e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ N := { mapRange.linearMap e.toLinearMap, @@ -883,7 +883,7 @@ variable (R) /-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`. -This is the `linear_equiv` version of `finsupp.sum_finsupp_equiv_prod_finsupp`. -/ +This is the `LinearEquiv` version of `Finsupp.sum_finsupp_equiv_prod_finsupp`. -/ @[simps apply symm_apply] def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) := { sumFinsuppAddEquivProdFinsupp with @@ -923,10 +923,10 @@ variable {η : Type _} [Fintype η] {ιs : η → Type _} [Zero α] variable (R) -/-- On a `fintype η`, `finsupp.split` is a linear equivalence between +/-- On a `Fintype η`, `Finsupp.split` is a linear equivalence between `(Σ (j : η), ιs j) →₀ M` and `Π j, (ιs j →₀ M)`. -This is the `linear_equiv` version of `finsupp.sigma_finsupp_add_equiv_pi_finsupp`. -/ +This is the `LinearEquiv` version of `Finsupp.sigma_finsupp_add_equiv_pi_finsupp`. -/ noncomputable def sigmaFinsuppLequivPiFinsupp {M : Type _} {ιs : η → Type _} [AddCommMonoid M] [Module R M] : ((Σj, ιs j) →₀ M) ≃ₗ[R] ∀ j, ιs j →₀ M := { sigmaFinsuppAddEquivPiFinsupp with @@ -954,7 +954,7 @@ section Prod /-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`. -This is the `linear_equiv` version of `finsupp.finsupp_prod_equiv`. -/ +This is the `LinearEquiv` version of `Finsupp.finsuppProdEquiv`. -/ noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M := { @@ -992,8 +992,8 @@ variable (S : Type _) [Semiring S] [Module S M] [SMulCommClass R S M] variable (v : α → M) -/-- `fintype.total R S v f` is the linear combination of vectors in `v` with weights in `f`. -This variant of `finsupp.total` is defined on fintype indexed vectors. +/-- `Fintype.total R S v f` is the linear combination of vectors in `v` with weights in `f`. +This variant of `Finsupp.total` is defined on fintype indexed vectors. This map is linear in `v` if `R` is commutative, and always linear in `f`. See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. @@ -1037,7 +1037,7 @@ theorem Finsupp.total_eq_fintype_total_apply (x : α → R) : apply Finset.sum_subset · exact Finset.subset_univ _ · intro x _ hx - rw [finsupp.not_mem_support_iff.mp hx] + rw [Finsupp.not_mem_support_iff.mp hx] exact zero_smul _ _ #align finsupp.total_eq_fintype_total_apply Finsupp.total_eq_fintype_total_apply @@ -1050,9 +1050,9 @@ theorem Finsupp.total_eq_fintype_total : variable {S} @[simp] -theorem Fintype.range_total : (Fintype.total R S v).range = Submodule.span R (Set.range v) := by - rw [← Finsupp.total_eq_fintype_total, LinearMap.range_comp, LinearEquiv.toLinearMap_eq_coe, - LinearEquiv.range, Submodule.map_top, Finsupp.range_total] +theorem Fintype.range_total : LinearMap.range (Fintype.total R S v) = Submodule.span R (Set.range v) := by + rw [← Finsupp.total_eq_fintype_total, LinearMap.range_comp, LinearEquiv.range, + Submodule.map_top, Finsupp.range_total] #align fintype.range_total Fintype.range_total section SpanRange @@ -1063,8 +1063,8 @@ variable {v} {x : M} -/ theorem mem_span_range_iff_exists_fun : x ∈ span R (range v) ↔ ∃ c : α → R, (∑ i, c i • v i) = x := by - simp only [Finsupp.mem_span_range_iff_exists_finsupp, - finsupp.equiv_fun_on_finite.surjective.exists, Finsupp.equivFunOnFinite_apply] + simp? [Finsupp.mem_span_range_iff_exists_finsupp, + Finsupp.equivFunOnFinite.surjective.exists, Finsupp.equivFunOnFinite_apply] exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _ #align mem_span_range_iff_exists_fun mem_span_range_iff_exists_fun @@ -1093,12 +1093,12 @@ variable (R) using the axiom of choice. -/ irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R := - ((Finsupp.mem_span_iff_total _ _ _).mp x.2).some + ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose #align span.repr Span.repr @[simp] theorem Span.finsupp_total_repr {w : Set M} (x : span R w) : - Finsupp.total w M R coe (Span.repr R w x) = x := by + Finsupp.total w M R (↑) (Span.repr R w x) = x := by rw [Span.repr] exact ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose_spec #align span.finsupp_total_repr Span.finsupp_total_repr @@ -1124,7 +1124,7 @@ theorem Submodule.exists_finset_of_mem_supᵢ {ι : Sort _} (p : ι → Submodul exact this hm #align submodule.exists_finset_of_mem_supr Submodule.exists_finset_of_mem_supᵢ -/-- `submodule.exists_finset_of_mem_supr` as an `iff` -/ +/-- `Submodule.exists_finset_of_mem_supr` as an `iff` -/ theorem Submodule.mem_supᵢ_iff_exists_finset {ι : Sort _} {p : ι → Submodule R M} {m : M} : (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := ⟨Submodule.exists_finset_of_mem_supᵢ p, fun ⟨_, hs⟩ => @@ -1136,14 +1136,14 @@ theorem mem_span_finset {s : Finset M} {x : M} : ⟨fun hx => let ⟨v, hvs, hvx⟩ := (Finsupp.mem_span_image_iff_total _).1 - (show x ∈ span R (id '' (↑s : Set M)) by rwa [Set.image_id]) + (show x ∈ span R (_root_.id '' (↑s : Set M)) by rwa [Set.image_id]) ⟨v, hvx ▸ (Finsupp.total_apply_of_mem_supported _ hvs).symm⟩, fun ⟨f, hf⟩ => hf ▸ sum_mem fun i hi => smul_mem _ _ <| subset_span hi⟩ #align mem_span_finset mem_span_finset /-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if `m` can be written as a finite `R`-linear combination of elements of `s`. -The implementation uses `finsupp.sum`. -/ +The implementation uses `Finsupp.sum`. -/ theorem mem_span_set {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m := by @@ -1152,36 +1152,36 @@ theorem mem_span_set {m : M} {s : Set M} : exact Finsupp.mem_span_image_iff_total R #align mem_span_set mem_span_set -/-- If `subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/ +/-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/ @[simps] def Module.subsingletonEquiv (R M ι : Type _) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : M ≃ₗ[R] ι →₀ R where - toFun m := 0 - invFun f := 0 + toFun _ := 0 + invFun _ := 0 left_inv m := by letI := Module.subsingleton R M simp only [eq_iff_true_of_subsingleton] right_inv f := by simp only [eq_iff_true_of_subsingleton] - map_add' m n := (add_zero 0).symm - map_smul' r m := (smul_zero r).symm + map_add' _ _ := (add_zero 0).symm + map_smul' r _ := (smul_zero r).symm #align module.subsingleton_equiv Module.subsingletonEquiv namespace LinearMap -variable {R M} {α : Type _} +variable {α : Type _} open Finsupp Function --- See also `linear_map.splitting_of_fun_on_fintype_surjective` +-- See also `LinearMap.splittingOfFunOnFintypeSurjective` /-- A surjective linear map to finitely supported functions has a splitting. -/ def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : (α →₀ R) →ₗ[R] M := - Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some + Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).choose #align linear_map.splitting_of_finsupp_surjective LinearMap.splittingOfFinsuppSurjective theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) : f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := by ext (x y) - dsimp [splitting_of_finsupp_surjective] + dsimp [splittingOfFinsuppSurjective] congr rw [sum_single_index, one_smul] · exact (s (Finsupp.single x 1)).choose_spec @@ -1195,22 +1195,22 @@ theorem leftInverse_splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) ( theorem splittingOfFinsuppSurjective_injective (f : M →ₗ[R] α →₀ R) (s : Surjective f) : Injective (splittingOfFinsuppSurjective f s) := - (leftInverse_splittingOfFinsuppSurjective f s).Injective + (leftInverse_splittingOfFinsuppSurjective f s).injective #align linear_map.splitting_of_finsupp_surjective_injective LinearMap.splittingOfFinsuppSurjective_injective --- See also `linear_map.splitting_of_finsupp_surjective` +-- See also `LinearMap.splittingOfFinsuppSurjective` /-- A surjective linear map to functions on a finite type has a splitting. -/ def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : (α → R) →ₗ[R] M := - (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).some).comp + (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).choose).comp (linearEquivFunOnFinite R R α).symm.toLinearMap #align linear_map.splitting_of_fun_on_fintype_surjective LinearMap.splittingOfFunOnFintypeSurjective theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by ext (x y) - dsimp [splitting_of_fun_on_fintype_surjective] - rw [linear_equiv_fun_on_finite_symm_single, Finsupp.sum_single_index, one_smul, + dsimp [splittingOfFunOnFintypeSurjective] + rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul, (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single] rw [zero_smul] #align linear_map.splitting_of_fun_on_fintype_surjective_splits LinearMap.splittingOfFunOnFintypeSurjective_splits From 50e397b89bb725b524c9ad8e25c29ae48b1810b9 Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 21:40:59 +0900 Subject: [PATCH 14/25] fix AAHRG --- Mathlib/LinearAlgebra/Finsupp.lean | 36 ++++++++++++++++-------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 248945a9a9962..a6f38bf6dae1f 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -154,23 +154,25 @@ theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] exact sum_mem fun a _ => Submodule.mem_supᵢ_of_mem a ⟨_, rfl⟩ #align finsupp.supr_lsingle_range Finsupp.supᵢ_lsingle_range -#eval "AAHRG this is too slow!!! Commenting out to continue with the rest of the file" --- theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : --- Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) --- (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by --- refine' --- (Disjoint.mono (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right) --- (lsingle_range_le_ker_lapply _ _ <| disjoint_compl_right)) --- _ --- rw [disjoint_iff_inf_le] --- refine' le_trans (le_infᵢ fun i => _) infi_ker_lapply_le_bot --- classical --- by_cases his : i ∈ s --- · by_cases hit : i ∈ t --- · exact (hs.le_bot ⟨his, hit⟩).elim --- exact inf_le_of_right_le (infᵢ_le_of_le i <| infᵢ_le _ hit) --- exact inf_le_of_left_le (infᵢ_le_of_le i <| infᵢ_le _ his) --- #align finsupp.disjoint_lsingle_lsingle Finsupp.disjoint_lsingle_lsingle +theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : + Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) + (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by + refine' + (Disjoint.mono + (lsingle_range_le_ker_lapply s (sᶜ) _) + (lsingle_range_le_ker_lapply t (tᶜ) _)) + _ + · apply disjoint_compl_right + · apply disjoint_compl_right + rw [disjoint_iff_inf_le] + refine' le_trans (le_infᵢ fun i => _) infᵢ_ker_lapply_le_bot + classical + by_cases his : i ∈ s + · by_cases hit : i ∈ t + · exact (hs.le_bot ⟨his, hit⟩).elim + exact inf_le_of_right_le (infᵢ_le_of_le i <| infᵢ_le _ hit) + exact inf_le_of_left_le (infᵢ_le_of_le i <| infᵢ_le _ his) +#align finsupp.disjoint_lsingle_lsingle Finsupp.disjoint_lsingle_lsingle theorem span_single_image (s : Set M) (a : α) : Submodule.span R (single a '' s) = (Submodule.span R s).map (lsingle a : M →ₗ[R] α →₀ M) := by From b2f9c0adf9d06275046cddd8de450be562ae206a Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 21:37:04 +0900 Subject: [PATCH 15/25] fix --- Mathlib/Algebra/Module/LinearMap.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 55d141e5c6ea5..bcc9c92bb5f1c 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -269,11 +269,17 @@ protected def Simps.apply {R S : Type _} [Semiring R] [Semiring S] (σ : R →+* initialize_simps_projections LinearMap (toAddHom_toFun → apply) @[simp] -theorem coe_mk {σ : R →+* S} (f : M → M₃) (h₁ h₂) : - ((LinearMap.mk (AddHom.mk f h₁) h₂ : M →ₛₗ[σ] M₃) : M → M₃) = f := +theorem coe_mk {σ : R →+* S} (f : AddHom M M₃) (h) : + ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f := rfl #align linear_map.coe_mk LinearMap.coe_mk +-- Porting note: This theorem is added. +@[simp] +theorem coe_mk' {σ : R →+* S} (f : AddHom M M₃) (h) : + ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f := + rfl + /-- Identity map as a `LinearMap` -/ def id : M →ₗ[R] M := { DistribMulActionHom.id R with toFun := _root_.id } From 40781b42762da25662ae14a461762903762d9a8b Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 21:52:37 +0900 Subject: [PATCH 16/25] porting note --- Mathlib/LinearAlgebra/Finsupp.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index a6f38bf6dae1f..f6451f437be3c 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -157,6 +157,7 @@ theorem supᵢ_lsingle_range : (⨆ a, LinearMap.range (lsingle a : M →ₗ[R] theorem disjoint_lsingle_lsingle (s t : Set α) (hs : Disjoint s t) : Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) (⨆ a ∈ t, LinearMap.range (lsingle a : M →ₗ[R] α →₀ M)) := by + -- Porting note: 2 placeholders are added to prevent timeout. refine' (Disjoint.mono (lsingle_range_le_ker_lapply s (sᶜ) _) From 92d4075b577c4143113f6474bf3bba50af1466b3 Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 22:21:42 +0900 Subject: [PATCH 17/25] notation of LinearEquiv.trans --- Mathlib/Algebra/Module/Equiv.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index 8e48ce7c2ff6d..ce8b9a013a6eb 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -322,9 +322,10 @@ variable {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) --- Note: The linter thinks the `RingHomCompTriple` argument is doubled -- it is not. +-- Porting note: The linter don't thinks the `RingHomCompTriple` argument is doubled, so +-- `nolint unusedArguments` is not necessary. /-- Linear equivalences are transitive. -/ -@[trans, nolint unusedArguments] +@[trans] def trans : M₁ ≃ₛₗ[σ₁₃] M₃ := { e₂₃.toLinearMap.comp e₁₂.toLinearMap, e₁₂.toEquiv.trans e₂₃.toEquiv with } #align linear_equiv.trans LinearEquiv.trans @@ -334,7 +335,7 @@ set_option quotPrecheck false in /-- The notation `e₁ ≪≫ₗ e₂` denotes the composition of the linear equivalences `e₁` and `e₂`. -/ infixl:80 " ≪≫ₗ " => @LinearEquiv.trans _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) - (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids RingHomCompTriple.ids + (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids From 31bb26ab2e90fc1db660ea7ccccd6c419aba690b Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 22:22:24 +0900 Subject: [PATCH 18/25] fix Finsupp.congr --- Mathlib/LinearAlgebra/Finsupp.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index f6451f437be3c..e5f2e31ba2458 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -778,8 +778,8 @@ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) supported M R s ≃ₗ[R] supported M R t := by haveI := Classical.decPred fun x => x ∈ s haveI := Classical.decPred fun x => x ∈ t - refine' Finsupp.supportedEquivFinsupp s ≪≫ₗ (_ ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) - exact Finsupp.domLcongr e + exact Finsupp.supportedEquivFinsupp s ≪≫ₗ + (Finsupp.domLcongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) #align finsupp.congr Finsupp.congr /-- `Finsupp.mapRange` as a `LinearMap`. -/ From 10efbc1787eae4881a8867376ca890688baefe54 Mon Sep 17 00:00:00 2001 From: Komyyy Date: Fri, 17 Feb 2023 23:59:59 +0900 Subject: [PATCH 19/25] other PRs --- Mathlib/Algebra/Module/Equiv.lean | 16 +++++++++++----- Mathlib/Algebra/Module/LinearMap.lean | 4 ++-- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index ce8b9a013a6eb..78b1afd1dcdf5 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -322,11 +322,17 @@ variable {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) --- Porting note: The linter don't thinks the `RingHomCompTriple` argument is doubled, so --- `nolint unusedArguments` is not necessary. +-- Porting note: Lean 4 aggressively removes unused variables declared using `variables`, so +-- we have to list all the variables explicitly here in order to match the Lean 3 signature. +set_option linter.unusedVariables false in /-- Linear equivalences are transitive. -/ -@[trans] -def trans : M₁ ≃ₛₗ[σ₁₃] M₃ := +@[trans, nolint unusedArguments] +def trans + [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] + {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} + [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} + {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] + (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : M₁ ≃ₛₗ[σ₁₃] M₃ := { e₂₃.toLinearMap.comp e₁₂.toLinearMap, e₁₂.toEquiv.trans e₂₃.toEquiv with } #align linear_equiv.trans LinearEquiv.trans @@ -335,7 +341,7 @@ set_option quotPrecheck false in /-- The notation `e₁ ≪≫ₗ e₂` denotes the composition of the linear equivalences `e₁` and `e₂`. -/ infixl:80 " ≪≫ₗ " => @LinearEquiv.trans _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) - (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids + (RingHom.id _) (RingHom.id _) (RingHom.id _) RingHomCompTriple.ids RingHomCompTriple.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids RingHomInvPair.ids diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index bcc9c92bb5f1c..7e6241a3fc570 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -274,9 +274,9 @@ theorem coe_mk {σ : R →+* S} (f : AddHom M M₃) (h) : rfl #align linear_map.coe_mk LinearMap.coe_mk --- Porting note: This theorem is added. +-- Porting note: This theorem is new. @[simp] -theorem coe_mk' {σ : R →+* S} (f : AddHom M M₃) (h) : +theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) : ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f := rfl From f37c4c3917498377287ba95c8e1626d92f41ae3a Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 00:05:07 +0900 Subject: [PATCH 20/25] 13 red errors left --- Mathlib/LinearAlgebra/Finsupp.lean | 35 ++++++++++++++++++++---------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index e5f2e31ba2458..5a39af153aa7e 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -783,15 +783,19 @@ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) #align finsupp.congr Finsupp.congr /-- `Finsupp.mapRange` as a `LinearMap`. -/ -@[simps!] def mapRange.linearMap (f : M →ₗ[R] N) : (α →₀ M) →ₗ[R] α →₀ N := - { - mapRange.addMonoidHom - f.toAddMonoidHom with + { mapRange.addMonoidHom f.toAddMonoidHom with toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N) - map_smul' := fun c v => mapRange_smul c v (f.map_smul c) } + -- Porting note: `hf` should be specified. + map_smul' := fun c v => mapRange_smul (hf := f.map_zero) c v (f.map_smul c) } #align finsupp.map_range.linear_map Finsupp.mapRange.linearMap +-- Porting note: This was generated by `simps!`. +@[simp] +theorem mapRange.linearMap_apply (f : M →ₗ[R] N) (g : α →₀ M) : + mapRange.linearMap f g = mapRange f f.map_zero g := rfl +#align finsupp.map_range.linear_map_apply Finsupp.mapRange.linearMap_apply + @[simp] theorem mapRange.linearMap_id : mapRange.linearMap LinearMap.id = (LinearMap.id : (α →₀ M) →ₗ[R] _) := @@ -801,7 +805,8 @@ theorem mapRange.linearMap_id : theorem mapRange.linearMap_comp (f : N →ₗ[R] P) (f₂ : M →ₗ[R] N) : (mapRange.linearMap (f.comp f₂) : (α →₀ _) →ₗ[R] _) = (mapRange.linearMap f).comp (mapRange.linearMap f₂) := - LinearMap.ext <| mapRange_comp _ _ _ _ _ + -- Porting note: Placeholders should be filled. + LinearMap.ext <| mapRange_comp f f.map_zero f₂ f₂.map_zero (comp f f₂).map_zero #align finsupp.map_range.linear_map_comp Finsupp.mapRange.linearMap_comp @[simp] @@ -812,7 +817,6 @@ theorem mapRange.linearMap_toAddMonoidHom (f : M →ₗ[R] N) : #align finsupp.map_range.linear_map_to_add_monoid_hom Finsupp.mapRange.linearMap_toAddMonoidHom /-- `Finsupp.mapRange` as a `LinearEquiv`. -/ -@[simps apply] def mapRange.linearEquiv (e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ N := { mapRange.linearMap e.toLinearMap, mapRange.addEquiv e.toAddEquiv with @@ -820,6 +824,12 @@ def mapRange.linearEquiv (e : M ≃ₗ[R] N) : (α →₀ M) ≃ₗ[R] α →₀ invFun := mapRange e.symm e.symm.map_zero } #align finsupp.map_range.linear_equiv Finsupp.mapRange.linearEquiv +-- Porting note: This was generated by `simps`. +@[simp] +theorem mapRange.linearEquiv_apply (e : M ≃ₗ[R] N) (g : α →₀ M) : + mapRange.linearEquiv e g = mapRange.linearMap e.toLinearMap g := rfl +#align finsupp.map_range.linear_equiv_apply Finsupp.mapRange.linearEquiv_apply + @[simp] theorem mapRange.linearEquiv_refl : mapRange.linearEquiv (LinearEquiv.refl R M) = LinearEquiv.refl R (α →₀ M) := @@ -829,7 +839,8 @@ theorem mapRange.linearEquiv_refl : theorem mapRange.linearEquiv_trans (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) : (mapRange.linearEquiv (f.trans f₂) : (α →₀ _) ≃ₗ[R] _) = (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) := - LinearEquiv.ext <| mapRange_comp _ _ _ _ _ + -- Porting note: Placeholders should be filled. + LinearEquiv.ext <| mapRange_comp f₂ f₂.map_zero f f.map_zero (f.trans f₂).map_zero #align finsupp.map_range.linear_equiv_trans Finsupp.mapRange.linearEquiv_trans @[simp] @@ -869,7 +880,7 @@ theorem lcongr_apply_apply {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[ theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) : (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) := by - apply_fun lcongr e₁ e₂ using (lcongr e₁ e₂).Injective + apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective simp #align finsupp.lcongr_symm_single Finsupp.lcongr_symm_single @@ -887,14 +898,14 @@ variable (R) /-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`. This is the `LinearEquiv` version of `Finsupp.sum_finsupp_equiv_prod_finsupp`. -/ -@[simps apply symm_apply] +@[simps apply symmApply] def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) := { sumFinsuppAddEquivProdFinsupp with map_smul' := by intros ext <;> - simp only [[anonymous], Prod.smul_fst, Prod.smul_snd, smul_apply, - snd_sum_finsupp_add_equiv_prod_finsupp, fst_sum_finsupp_add_equiv_prod_finsupp, + simp only [Prod.smul_fst, Prod.smul_snd, smul_apply, + snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp, RingHom.id_apply] } #align finsupp.sum_finsupp_lequiv_prod_finsupp Finsupp.sumFinsuppLequivProdFinsupp From a91090781f1d865849d5d9e0aeacb987de79f2db Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 11:24:51 +0900 Subject: [PATCH 21/25] no errors & script lints anymore --- Mathlib/LinearAlgebra/Finsupp.lean | 52 +++++++++++++++++------------- 1 file changed, 30 insertions(+), 22 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 5a39af153aa7e..4be6ec4b6f0c2 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -465,7 +465,6 @@ theorem lmapDomain_supported [Nonempty α] (f : α → α') (s : Set α) : exact Function.invFunOn_eq (by simpa using hl hc) #align finsupp.lmap_domain_supported Finsupp.lmapDomain_supported -/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder collection (a b «expr ∈ » s) -/ theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} (H : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), f a = f b → a = b) : Disjoint (supported M R s) (ker (lmapDomain M R f)) := by @@ -846,7 +845,7 @@ theorem mapRange.linearEquiv_trans (f : M ≃ₗ[R] N) (f₂ : N ≃ₗ[R] P) : @[simp] theorem mapRange.linearEquiv_symm (f : M ≃ₗ[R] N) : ((mapRange.linearEquiv f).symm : (α →₀ _) ≃ₗ[R] _) = mapRange.linearEquiv f.symm := - LinearEquiv.ext fun x => rfl + LinearEquiv.ext fun _x => rfl #align finsupp.map_range.linear_equiv_symm Finsupp.mapRange.linearEquiv_symm @[simp] @@ -904,7 +903,10 @@ def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R map_smul' := by intros ext <;> - simp only [Prod.smul_fst, Prod.smul_snd, smul_apply, + -- Porting note: `add_equiv.to_fun_eq_coe` → + -- `Equiv.toFun_as_coe` & `AddEquiv.coe_toEquiv` + simp only [Equiv.toFun_as_coe, AddEquiv.coe_toEquiv, Prod.smul_fst, + Prod.smul_snd, smul_apply, snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp, RingHom.id_apply] } #align finsupp.sum_finsupp_lequiv_prod_finsupp Finsupp.sumFinsuppLequivProdFinsupp @@ -942,8 +944,9 @@ variable (R) This is the `LinearEquiv` version of `Finsupp.sigma_finsupp_add_equiv_pi_finsupp`. -/ noncomputable def sigmaFinsuppLequivPiFinsupp {M : Type _} {ιs : η → Type _} [AddCommMonoid M] - [Module R M] : ((Σj, ιs j) →₀ M) ≃ₗ[R] ∀ j, ιs j →₀ M := - { sigmaFinsuppAddEquivPiFinsupp with + [Module R M] : ((Σ j, ιs j) →₀ M) ≃ₗ[R] ∀ j, ιs j →₀ M := + -- Porting note: `ιs` should be specified. + { sigmaFinsuppAddEquivPiFinsupp (ιs := ιs) with map_smul' := fun c f => by ext simp } @@ -971,8 +974,7 @@ section Prod This is the `LinearEquiv` version of `Finsupp.finsuppProdEquiv`. -/ noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M := - { - finsuppProdEquiv with + { finsuppProdEquiv with map_add' := fun f g => by ext simp [finsuppProdEquiv, curry_apply] @@ -1012,8 +1014,7 @@ This variant of `Finsupp.total` is defined on fintype indexed vectors. This map is linear in `v` if `R` is commutative, and always linear in `f`. See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/ -protected def Fintype.total : (α → M) →ₗ[S] (α → R) →ₗ[R] M - where +protected def Fintype.total : (α → M) →ₗ[S] (α → R) →ₗ[R] M where toFun v := { toFun := fun f => ∑ i, f i • v i map_add' := fun f g => by @@ -1026,8 +1027,9 @@ protected def Fintype.total : (α → M) →ₗ[S] (α → R) →ₗ[R] M ext simp [Finset.sum_add_distrib, Pi.add_apply, smul_add] map_smul' r v := by - ext - simp [Finset.smul_sum, smul_comm _ r] + ext g + -- Porting note: `smul_comm _ r` → `fun x => smul_comm (g x) r (v x)` + simp [Finset.smul_sum, fun x => smul_comm (g x) r (v x)] #align fintype.total Fintype.total variable {S} @@ -1064,7 +1066,8 @@ theorem Finsupp.total_eq_fintype_total : variable {S} @[simp] -theorem Fintype.range_total : LinearMap.range (Fintype.total R S v) = Submodule.span R (Set.range v) := by +theorem Fintype.range_total : + LinearMap.range (Fintype.total R S v) = Submodule.span R (Set.range v) := by rw [← Finsupp.total_eq_fintype_total, LinearMap.range_comp, LinearEquiv.range, Submodule.map_top, Finsupp.range_total] #align fintype.range_total Fintype.range_total @@ -1075,10 +1078,11 @@ variable {v} {x : M} /-- An element `x` lies in the span of `v` iff it can be written as sum `∑ cᵢ • vᵢ = x`. -/ -theorem mem_span_range_iff_exists_fun : x ∈ span R (range v) ↔ ∃ c : α → R, (∑ i, c i • v i) = x := - by - simp? [Finsupp.mem_span_range_iff_exists_finsupp, - Finsupp.equivFunOnFinite.surjective.exists, Finsupp.equivFunOnFinite_apply] +theorem mem_span_range_iff_exists_fun : + x ∈ span R (range v) ↔ ∃ c : α → R, (∑ i, c i • v i) = x := by + -- Porting note: `Finsupp.equivFunOnFinite.surjective.exists` should be come before `simp`. + rw [Finsupp.equivFunOnFinite.surjective.exists] + simp [Finsupp.mem_span_range_iff_exists_finsupp, Finsupp.equivFunOnFinite_apply] exact exists_congr fun c => Eq.congr_left <| Finsupp.sum_fintype _ _ fun i => zero_smul _ _ #align mem_span_range_iff_exists_fun mem_span_range_iff_exists_fun @@ -1113,7 +1117,7 @@ irreducible_def Span.repr (w : Set M) (x : span R w) : w →₀ R := @[simp] theorem Span.finsupp_total_repr {w : Set M} (x : span R w) : Finsupp.total w M R (↑) (Span.repr R w x) = x := by - rw [Span.repr] + rw [Span.repr_def] exact ((Finsupp.mem_span_iff_total _ _ _).mp x.2).choose_spec #align span.finsupp_total_repr Span.finsupp_total_repr @@ -1126,7 +1130,8 @@ protected theorem Submodule.finsupp_sum_mem {ι β : Type _} [Zero β] (S : Subm theorem LinearMap.map_finsupp_total (f : M →ₗ[R] N) {ι : Type _} {g : ι → M} (l : ι →₀ R) : f (Finsupp.total ι M R g l) = Finsupp.total ι N R (f ∘ g) l := by - simp only [Finsupp.total_apply, Finsupp.total_apply, Finsupp.sum, f.map_sum, f.map_smul] + -- Porting note: `(· ∘ ·)` is required. + simp only [Finsupp.total_apply, Finsupp.total_apply, Finsupp.sum, f.map_sum, f.map_smul, (· ∘ ·)] #align linear_map.map_finsupp_total LinearMap.map_finsupp_total theorem Submodule.exists_finset_of_mem_supᵢ {ι : Sort _} (p : ι → Submodule R M) {m : M} @@ -1162,8 +1167,9 @@ theorem mem_span_set {m : M} {s : Set M} : m ∈ Submodule.span R s ↔ ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m := by conv_lhs => rw [← Set.image_id s] - simp_rw [← exists_prop] - exact Finsupp.mem_span_image_iff_total R + -- Porting note: `simp_rw [← exists_prop]` is not necessary because of the + -- new definition of `∃ x, p x`. + exact Finsupp.mem_span_image_iff_total R (v := _root_.id (α := M)) #align mem_span_set mem_span_set /-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/ @@ -1194,7 +1200,8 @@ def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) : f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := by - ext (x y) + -- Porting note: `ext` can't find appropriate theorems. + refine lhom_ext' fun x => ext_ring <| Finsupp.ext fun y => ?_ dsimp [splittingOfFinsuppSurjective] congr rw [sum_single_index, one_smul] @@ -1222,7 +1229,8 @@ def splittingOfFunOnFintypeSurjective [Fintype α] (f : M →ₗ[R] α → R) (s theorem splittingOfFunOnFintypeSurjective_splits [Fintype α] (f : M →ₗ[R] α → R) (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by - ext (x y) + -- Porting note: `ext` can't find appropriate theorems. + refine pi_ext' fun x => ext_ring <| funext fun y => ?_ dsimp [splittingOfFunOnFintypeSurjective] rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul, (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single] From 43a5b8aae9c8a9a05a42ae9a2272356ed22b4cb1 Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 12:01:26 +0900 Subject: [PATCH 22/25] no build lints anymore --- Mathlib/LinearAlgebra/Finsupp.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 4be6ec4b6f0c2..47c966b3e7102 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -766,10 +766,10 @@ theorem domLcongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : LinearEquiv.ext fun _ => rfl #align finsupp.dom_lcongr_symm Finsupp.domLcongr_symm -@[simp] +-- @[simp] -- Porting note: simp can prove this theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (i : α₁) (m : M) : (Finsupp.domLcongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by - simp [Finsupp.domLcongr, Finsupp.domCongr, equivMapDomain_single] + simp #align finsupp.dom_lcongr_single Finsupp.domLcongr_single /-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets. -/ @@ -848,7 +848,8 @@ theorem mapRange.linearEquiv_symm (f : M ≃ₗ[R] N) : LinearEquiv.ext fun _x => rfl #align finsupp.map_range.linear_equiv_symm Finsupp.mapRange.linearEquiv_symm -@[simp] +-- Porting note: This priority should be higher than `LinearEquiv.coe_toAddEquiv`. +@[simp 1500] theorem mapRange.linearEquiv_toAddEquiv (f : M ≃ₗ[R] N) : (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv : (α →₀ M) ≃+ _) := AddEquiv.ext fun _ => rfl @@ -1107,6 +1108,11 @@ section variable (R) +-- Porting note: `irreducible_def` produces a structure. +-- When a structure is defined, an injectivity theorem of the constructor is +-- generated, which has `simp` attr, but this get a `simpNF` linter. +-- So, this option is required. +set_option genInjectivity false in /-- Pick some representation of `x : span R w` as a linear combination in `w`, using the axiom of choice. -/ From 3863a217ffd5a45bb6c020306985fa345c53db5e Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 12:24:39 +0900 Subject: [PATCH 23/25] naming conventions & edit docs & pi notations --- Mathlib/LinearAlgebra/Finsupp.lean | 166 ++++++++++++++--------------- 1 file changed, 83 insertions(+), 83 deletions(-) diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 47c966b3e7102..6463f4816ec93 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -16,25 +16,25 @@ import Mathlib.LinearAlgebra.Span # Properties of the module `α →₀ M` Given an `R`-module `M`, the `R`-module structure on `α →₀ M` is defined in -`data.Finsupp.basic`. +`Data.Finsupp.Basic`. In this file we define `Finsupp.supported s` to be the set `{f : α →₀ M | f.support ⊆ s}` interpreted as a submodule of `α →₀ M`. We also define `LinearMap` versions of various maps: * `Finsupp.lsingle a : M →ₗ[R] ι →₀ M`: `Finsupp.single a` as a linear map; * `Finsupp.lapply a : (ι →₀ M) →ₗ[R] M`: the map `λ f, f a` as a linear map; -* `Finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a +* `Finsupp.lsubtypeDomain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)`: restriction to a subtype as a linear map; -* `Finsupp.restrict_dom`: `Finsupp.filter` as a linear map to `Finsupp.supported s`; -* `Finsupp.lsum`: `Finsupp.sum` or `Finsupp.lift_add_hom` as a `LinearMap`; +* `Finsupp.restrictDom`: `Finsupp.filter` as a linear map to `Finsupp.supported s`; +* `Finsupp.lsum`: `Finsupp.sum` or `Finsupp.liftAddHom` as a `LinearMap`; * `Finsupp.total α M R (v : ι → M)`: sends `l : ι → R` to the linear combination of `v i` with coefficients `l i`; -* `Finsupp.total_on`: a restricted version of `Finsupp.total` with domain `Finsupp.supported R R s` +* `Finsupp.totalOn`: a restricted version of `Finsupp.total` with domain `Finsupp.supported R R s` and codomain `Submodule.span R (v '' s)`; -* `Finsupp.supported_equiv_finsupp`: a linear equivalence between the functions `α →₀ M` supported +* `Finsupp.supportedEquivFinsupp`: a linear equivalence between the functions `α →₀ M` supported on `s` and the functions `s →₀ M`; -* `Finsupp.lmap_domain`: a linear map version of `Finsupp.map_domain`; -* `Finsupp.dom_lcongr`: a `LinearEquiv` version of `Finsupp.domCongr`; +* `Finsupp.lmapDomain`: a linear map version of `Finsupp.mapDomain`; +* `Finsupp.domLCongr`: a `LinearEquiv` version of `Finsupp.domCongr`; * `Finsupp.congr`: if the sets `s` and `t` are equivalent, then `supported M R s` is equivalent to `supported M R t`; * `Finsupp.lcongr`: a `LinearEquiv`alence between `α →₀ M` and `β →₀ N` constructed using `e : α ≃ @@ -80,14 +80,14 @@ theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₗ[R] N⦄ (h : ∀ a, φ.comp (l lhom_ext fun a => LinearMap.congr_fun (h a) #align finsupp.lhom_ext' Finsupp.lhom_ext' -/-- Interpret `λ (f : α →₀ M), f a` as a linear map. -/ +/-- Interpret `fun f : α →₀ M ↦ f a` as a linear map. -/ def lapply (a : α) : (α →₀ M) →ₗ[R] M := { Finsupp.applyAddHom a with map_smul' := fun _ _ => rfl } #align finsupp.lapply Finsupp.lapply /-- Forget that a function is finitely supported. -This is the linear version of `Finsupp.to_fun`. -/ +This is the linear version of `Finsupp.toFun`. -/ @[simps] def lcoeFun : (α →₀ M) →ₗ[R] α → M where toFun := (⇑) @@ -99,11 +99,11 @@ def lcoeFun : (α →₀ M) →ₗ[R] α → M where simp #align finsupp.lcoe_fun Finsupp.lcoeFun -section LsubtypeDomain +section LSubtypeDomain variable (s : Set α) -/-- Interpret `Finsupp.subtype_domain s` as a linear map. -/ +/-- Interpret `Finsupp.subtypeDomain s` as a linear map. -/ def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M where toFun := subtypeDomain fun x => x ∈ s @@ -116,7 +116,7 @@ theorem lsubtypeDomain_apply (f : α →₀ M) : rfl #align finsupp.lsubtype_domain_apply Finsupp.lsubtypeDomain_apply -end LsubtypeDomain +end LSubtypeDomain @[simp] theorem lsingle_apply (a : α) (b : M) : (lsingle a : M →ₗ[R] α →₀ M) b = single a b := @@ -324,7 +324,7 @@ theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} : exact hy this #align finsupp.disjoint_supported_supported_iff Finsupp.disjoint_supported_supported_iff -/-- Interpret `Finsupp.restrict_support_equiv` as a linear equivalence between +/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between `supported M R s` and `s →₀ M`. -/ def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := by let F : supported M R s ≃ (s →₀ M) := restrictSupportEquiv s M @@ -337,13 +337,13 @@ def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M := exact LinearMap.isLinear _ #align finsupp.supported_equiv_finsupp Finsupp.supportedEquivFinsupp -section Lsum +section LSum variable (S) variable [Module S N] [SMulCommClass R S N] /-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to -`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.lift_add_hom`. +`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.liftAddHom`. See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/ @@ -385,7 +385,7 @@ theorem lsum_symm_apply (f : (α →₀ M) →ₗ[R] N) (x : α) : (lsum S).symm rfl #align finsupp.lsum_symm_apply Finsupp.lsum_symm_apply -end Lsum +end LSum section @@ -411,11 +411,11 @@ theorem lift_apply (f) (g) : ((lift M R X) f) g = g.sum fun x r => r • f x := end -section LmapDomain +section LMapDomain variable {α' : Type _} {α'' : Type _} (M R) -/-- Interpret `Finsupp.map_domain` as a linear map. -/ +/-- Interpret `Finsupp.mapDomain` as a linear map. -/ def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M where toFun := mapDomain f @@ -487,17 +487,17 @@ theorem lmapDomain_disjoint_ker (f : α → α') {s : Set α} exact xs (h₁ <| Finsupp.mem_support_iff.2 h) #align finsupp.lmap_domain_disjoint_ker Finsupp.lmapDomain_disjoint_ker -end LmapDomain +end LMapDomain -section LcomapDomain +section LComapDomain variable {β : Type _} -/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomap_domain f hf` is the linear map +/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomapDomain f hf` is the linear map sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing `l` with `f`. -This is the linear version of `Finsupp.comap_domain`. -/ +This is the linear version of `Finsupp.comapDomain`. -/ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M where toFun l := Finsupp.comapDomain f l (hf.injOn _) @@ -505,7 +505,7 @@ def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) → map_smul' c x := by ext; simp #align finsupp.lcomap_domain Finsupp.lcomapDomain -end LcomapDomain +end LComapDomain section Total @@ -693,7 +693,7 @@ theorem total_fin_zero (f : Fin 0 → M) : Finsupp.total (Fin 0) M R f = 0 := by variable (α) (M) (v) -/-- `Finsupp.total_on M v s` interprets `p : α →₀ R` as a linear combination of a +/-- `Finsupp.totalOn M v s` interprets `p : α →₀ R` as a linear combination of a subset of the vectors in `v`, mapping it to the span of those vectors. The subset is indicated by a set `s : set α` of indices. @@ -737,40 +737,40 @@ end Total /-- An equivalence of domains induces a linear equivalence of finitely supported functions. This is `Finsupp.domCongr` as a `LinearEquiv`. -See also `LinearMap.fun_congr_left` for the case of arbitrary functions. -/ -protected def domLcongr {α₁ α₂ : Type _} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M := +See also `LinearMap.funCongrLeft` for the case of arbitrary functions. -/ +protected def domLCongr {α₁ α₂ : Type _} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M := (Finsupp.domCongr e : (α₁ →₀ M) ≃+ (α₂ →₀ M)).toLinearEquiv <| by simpa only [equivMapDomain_eq_mapDomain, domCongr_apply] using (lmapDomain M R e).map_smul -#align finsupp.dom_lcongr Finsupp.domLcongr +#align finsupp.dom_lcongr Finsupp.domLCongr @[simp] -theorem domLcongr_apply {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : - (Finsupp.domLcongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v := +theorem domLCongr_apply {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : + (Finsupp.domLCongr e : _ ≃ₗ[R] _) v = Finsupp.domCongr e v := rfl -#align finsupp.dom_lcongr_apply Finsupp.domLcongr_apply +#align finsupp.dom_lcongr_apply Finsupp.domLCongr_apply @[simp] -theorem domLcongr_refl : Finsupp.domLcongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M) := +theorem domLCongr_refl : Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M) := LinearEquiv.ext fun _ => equivMapDomain_refl _ -#align finsupp.dom_lcongr_refl Finsupp.domLcongr_refl +#align finsupp.dom_lcongr_refl Finsupp.domLCongr_refl -theorem domLcongr_trans {α₁ α₂ α₃ : Type _} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) : - (Finsupp.domLcongr f).trans (Finsupp.domLcongr f₂) = - (Finsupp.domLcongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _) := +theorem domLCongr_trans {α₁ α₂ α₃ : Type _} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) : + (Finsupp.domLCongr f).trans (Finsupp.domLCongr f₂) = + (Finsupp.domLCongr (f.trans f₂) : (_ →₀ M) ≃ₗ[R] _) := LinearEquiv.ext fun _ => (equivMapDomain_trans _ _ _).symm -#align finsupp.dom_lcongr_trans Finsupp.domLcongr_trans +#align finsupp.dom_lcongr_trans Finsupp.domLCongr_trans @[simp] -theorem domLcongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : - ((Finsupp.domLcongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLcongr f.symm := +theorem domLCongr_symm {α₁ α₂ : Type _} (f : α₁ ≃ α₂) : + ((Finsupp.domLCongr f).symm : (_ →₀ M) ≃ₗ[R] _) = Finsupp.domLCongr f.symm := LinearEquiv.ext fun _ => rfl -#align finsupp.dom_lcongr_symm Finsupp.domLcongr_symm +#align finsupp.dom_lcongr_symm Finsupp.domLCongr_symm -- @[simp] -- Porting note: simp can prove this -theorem domLcongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (i : α₁) (m : M) : - (Finsupp.domLcongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by +theorem domLCongr_single {α₁ : Type _} {α₂ : Type _} (e : α₁ ≃ α₂) (i : α₁) (m : M) : + (Finsupp.domLCongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m := by simp -#align finsupp.dom_lcongr_single Finsupp.domLcongr_single +#align finsupp.dom_lcongr_single Finsupp.domLCongr_single /-- An equivalence of sets induces a linear equivalence of `Finsupp`s supported on those sets. -/ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) : @@ -778,7 +778,7 @@ noncomputable def congr {α' : Type _} (s : Set α) (t : Set α') (e : s ≃ t) haveI := Classical.decPred fun x => x ∈ s haveI := Classical.decPred fun x => x ∈ t exact Finsupp.supportedEquivFinsupp s ≪≫ₗ - (Finsupp.domLcongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) + (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm) #align finsupp.congr Finsupp.congr /-- `Finsupp.mapRange` as a `LinearMap`. -/ @@ -864,7 +864,7 @@ theorem mapRange.linearEquiv_toLinearMap (f : M ≃ₗ[R] N) : /-- An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions. -/ def lcongr {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) : (ι →₀ M) ≃ₗ[R] κ →₀ N := - (Finsupp.domLcongr e₁).trans (mapRange.linearEquiv e₂) + (Finsupp.domLCongr e₁).trans (mapRange.linearEquiv e₂) #align finsupp.lcongr Finsupp.lcongr @[simp] @@ -897,9 +897,9 @@ variable (R) /-- The linear equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`. -This is the `LinearEquiv` version of `Finsupp.sum_finsupp_equiv_prod_finsupp`. -/ +This is the `LinearEquiv` version of `Finsupp.sumFinsuppEquivProdFinsupp`. -/ @[simps apply symmApply] -def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) := +def sumFinsuppLEquivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R] (α →₀ M) × (β →₀ M) := { sumFinsuppAddEquivProdFinsupp with map_smul' := by intros @@ -910,27 +910,27 @@ def sumFinsuppLequivProdFinsupp {α β : Type _} : (Sum α β →₀ M) ≃ₗ[R Prod.smul_snd, smul_apply, snd_sumFinsuppAddEquivProdFinsupp, fst_sumFinsuppAddEquivProdFinsupp, RingHom.id_apply] } -#align finsupp.sum_finsupp_lequiv_prod_finsupp Finsupp.sumFinsuppLequivProdFinsupp +#align finsupp.sum_finsupp_lequiv_prod_finsupp Finsupp.sumFinsuppLEquivProdFinsupp -theorem fst_sumFinsuppLequivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (x : α) : - (sumFinsuppLequivProdFinsupp R f).1 x = f (Sum.inl x) := +theorem fst_sumFinsuppLEquivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (x : α) : + (sumFinsuppLEquivProdFinsupp R f).1 x = f (Sum.inl x) := rfl -#align finsupp.fst_sum_finsupp_lequiv_prod_finsupp Finsupp.fst_sumFinsuppLequivProdFinsupp +#align finsupp.fst_sum_finsupp_lequiv_prod_finsupp Finsupp.fst_sumFinsuppLEquivProdFinsupp -theorem snd_sumFinsuppLequivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (y : β) : - (sumFinsuppLequivProdFinsupp R f).2 y = f (Sum.inr y) := +theorem snd_sumFinsuppLEquivProdFinsupp {α β : Type _} (f : Sum α β →₀ M) (y : β) : + (sumFinsuppLEquivProdFinsupp R f).2 y = f (Sum.inr y) := rfl -#align finsupp.snd_sum_finsupp_lequiv_prod_finsupp Finsupp.snd_sumFinsuppLequivProdFinsupp +#align finsupp.snd_sum_finsupp_lequiv_prod_finsupp Finsupp.snd_sumFinsuppLEquivProdFinsupp -theorem sumFinsuppLequivProdFinsupp_symm_inl {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (x : α) : - ((sumFinsuppLequivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x := +theorem sumFinsuppLEquivProdFinsupp_symm_inl {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (x : α) : + ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inl x) = fg.1 x := rfl -#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl Finsupp.sumFinsuppLequivProdFinsupp_symm_inl +#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inl Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl -theorem sumFinsuppLequivProdFinsupp_symm_inr {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (y : β) : - ((sumFinsuppLequivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y := +theorem sumFinsuppLEquivProdFinsupp_symm_inr {α β : Type _} (fg : (α →₀ M) × (β →₀ M)) (y : β) : + ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y := rfl -#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr Finsupp.sumFinsuppLequivProdFinsupp_symm_inr +#align finsupp.sum_finsupp_lequiv_prod_finsupp_symm_inr Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr end Sum @@ -941,30 +941,30 @@ variable {η : Type _} [Fintype η] {ιs : η → Type _} [Zero α] variable (R) /-- On a `Fintype η`, `Finsupp.split` is a linear equivalence between -`(Σ (j : η), ιs j) →₀ M` and `Π j, (ιs j →₀ M)`. +`(Σ (j : η), ιs j) →₀ M` and `(j : η) → (ιs j →₀ M)`. -This is the `LinearEquiv` version of `Finsupp.sigma_finsupp_add_equiv_pi_finsupp`. -/ -noncomputable def sigmaFinsuppLequivPiFinsupp {M : Type _} {ιs : η → Type _} [AddCommMonoid M] - [Module R M] : ((Σ j, ιs j) →₀ M) ≃ₗ[R] ∀ j, ιs j →₀ M := +This is the `LinearEquiv` version of `Finsupp.sigmaFinsuppAddEquivPiFinsupp`. -/ +noncomputable def sigmaFinsuppLEquivPiFinsupp {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] : ((Σ j, ιs j) →₀ M) ≃ₗ[R] (j : _) → (ιs j →₀ M) := -- Porting note: `ιs` should be specified. { sigmaFinsuppAddEquivPiFinsupp (ιs := ιs) with map_smul' := fun c f => by ext simp } -#align finsupp.sigma_finsupp_lequiv_pi_finsupp Finsupp.sigmaFinsuppLequivPiFinsupp +#align finsupp.sigma_finsupp_lequiv_pi_finsupp Finsupp.sigmaFinsuppLEquivPiFinsupp @[simp] -theorem sigmaFinsuppLequivPiFinsupp_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] - [Module R M] (f : (Σj, ιs j) →₀ M) (j i) : sigmaFinsuppLequivPiFinsupp R f j i = f ⟨j, i⟩ := +theorem sigmaFinsuppLEquivPiFinsupp_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] (f : (Σj, ιs j) →₀ M) (j i) : sigmaFinsuppLEquivPiFinsupp R f j i = f ⟨j, i⟩ := rfl -#align finsupp.sigma_finsupp_lequiv_pi_finsupp_apply Finsupp.sigmaFinsuppLequivPiFinsupp_apply +#align finsupp.sigma_finsupp_lequiv_pi_finsupp_apply Finsupp.sigmaFinsuppLEquivPiFinsupp_apply @[simp] -theorem sigmaFinsuppLequivPiFinsupp_symm_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] - [Module R M] (f : ∀ j, ιs j →₀ M) (ji) : - (Finsupp.sigmaFinsuppLequivPiFinsupp R).symm f ji = f ji.1 ji.2 := +theorem sigmaFinsuppLEquivPiFinsupp_symm_apply {M : Type _} {ιs : η → Type _} [AddCommMonoid M] + [Module R M] (f : (j : _) → (ιs j →₀ M)) (ji) : + (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm f ji = f ji.1 ji.2 := rfl -#align finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply Finsupp.sigmaFinsuppLequivPiFinsupp_symm_apply +#align finsupp.sigma_finsupp_lequiv_pi_finsupp_symm_apply Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply end Sigma @@ -973,7 +973,7 @@ section Prod /-- The linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M`. This is the `LinearEquiv` version of `Finsupp.finsuppProdEquiv`. -/ -noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [Semiring R] +noncomputable def finsuppProdLEquiv {α β : Type _} (R : Type _) {M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] : (α × β →₀ M) ≃ₗ[R] α →₀ β →₀ M := { finsuppProdEquiv with map_add' := fun f g => by @@ -982,20 +982,20 @@ noncomputable def finsuppProdLequiv {α β : Type _} (R : Type _) {M : Type _} [ map_smul' := fun c f => by ext simp [finsuppProdEquiv, curry_apply] } -#align finsupp.finsupp_prod_lequiv Finsupp.finsuppProdLequiv +#align finsupp.finsupp_prod_lequiv Finsupp.finsuppProdLEquiv @[simp] -theorem finsuppProdLequiv_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] - (f : α × β →₀ M) (x y) : finsuppProdLequiv R f x y = f (x, y) := by - rw [finsuppProdLequiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply] -#align finsupp.finsupp_prod_lequiv_apply Finsupp.finsuppProdLequiv_apply +theorem finsuppProdLEquiv_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] + (f : α × β →₀ M) (x y) : finsuppProdLEquiv R f x y = f (x, y) := by + rw [finsuppProdLEquiv, LinearEquiv.coe_mk, finsuppProdEquiv, Finsupp.curry_apply] +#align finsupp.finsupp_prod_lequiv_apply Finsupp.finsuppProdLEquiv_apply @[simp] -theorem finsuppProdLequiv_symm_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] - (f : α →₀ β →₀ M) (xy) : (finsuppProdLequiv R).symm f xy = f xy.1 xy.2 := by +theorem finsuppProdLEquiv_symm_apply {α β R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M] + (f : α →₀ β →₀ M) (xy) : (finsuppProdLEquiv R).symm f xy = f xy.1 xy.2 := by conv_rhs => - rw [← (finsuppProdLequiv R).apply_symm_apply f, finsuppProdLequiv_apply, Prod.mk.eta] -#align finsupp.finsupp_prod_lequiv_symm_apply Finsupp.finsuppProdLequiv_symm_apply + rw [← (finsuppProdLEquiv R).apply_symm_apply f, finsuppProdLEquiv_apply, Prod.mk.eta] +#align finsupp.finsupp_prod_lequiv_symm_apply Finsupp.finsuppProdLEquiv_symm_apply end Prod @@ -1149,7 +1149,7 @@ theorem Submodule.exists_finset_of_mem_supᵢ {ι : Sort _} (p : ι → Submodul exact this hm #align submodule.exists_finset_of_mem_supr Submodule.exists_finset_of_mem_supᵢ -/-- `Submodule.exists_finset_of_mem_supr` as an `iff` -/ +/-- `Submodule.exists_finset_of_mem_supᵢ` as an `iff` -/ theorem Submodule.mem_supᵢ_iff_exists_finset {ι : Sort _} {p : ι → Submodule R M} {m : M} : (m ∈ ⨆ i, p i) ↔ ∃ s : Finset ι, m ∈ ⨆ i ∈ s, p i := ⟨Submodule.exists_finset_of_mem_supᵢ p, fun ⟨_, hs⟩ => From af6234094d55e222083c40c0961db2b39e0074eb Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 14:02:47 +0900 Subject: [PATCH 24/25] other PR --- Mathlib/Algebra/Module/Equiv.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index 78b1afd1dcdf5..bedd503c9f215 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -326,6 +326,8 @@ variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ -- we have to list all the variables explicitly here in order to match the Lean 3 signature. set_option linter.unusedVariables false in /-- Linear equivalences are transitive. -/ +-- Note: the `ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around +-- implicitly for lemmas like `linear_equiv.self_trans_symm`. @[trans, nolint unusedArguments] def trans [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] From 96fb6156693200b4b188fdb28b8afaf1bb9d24bf Mon Sep 17 00:00:00 2001 From: Komyyy Date: Sat, 18 Feb 2023 14:09:51 +0900 Subject: [PATCH 25/25] indent --- Mathlib/Algebra/Module/Equiv.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index bedd503c9f215..c7abfd4e55b27 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -330,11 +330,11 @@ set_option linter.unusedVariables false in -- implicitly for lemmas like `linear_equiv.self_trans_symm`. @[trans, nolint unusedArguments] def trans - [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] - {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} - [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} - {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] - (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : M₁ ≃ₛₗ[σ₁₃] M₃ := + [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] + {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} + [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} + {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] + (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) : M₁ ≃ₛₗ[σ₁₃] M₃ := { e₂₃.toLinearMap.comp e₁₂.toLinearMap, e₁₂.toEquiv.trans e₂₃.toEquiv with } #align linear_equiv.trans LinearEquiv.trans