chore(Finsupp): move mapRange.equiv earlier (#31324)

Move `mapRange.equiv` to `Data.Finsupp.Defs` and `mapRange.addEquiv` to `Algebra.Group.Finsupp`. This lets us not import fields when defining `finsuppAntidiag`.

As previously, I am basing myself off the idea that `Finsupp` will at some point in the future be generalised to other base points (rather than just `0` as it is now), and that therefore anything under `Data.Finsupp` should not be algebraic (apart from mentioning `0`).

Author: YaelDillies

Mathlib/Algebra/Group/Finsupp.lean

@@ -23,11 +23,24 @@ variable {ι F M N O G H : Type*}
 
 namespace Finsupp
 section Zero
-variable [Zero M] [Zero N]
+variable [Zero M] [Zero N] [Zero O]
 
 lemma apply_single [FunLike F M N] [ZeroHomClass F M N] (e : F) (i : ι) (m : M) (b : ι) :
     e (single i m b) = single i (e m) b := apply_single' e (map_zero e) i m b
 
+/-- Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism
+on functions. -/
+@[simps]
+def mapRange.zeroHom (f : ZeroHom M N) : ZeroHom (ι →₀ M) (ι →₀ N) where
+  toFun := Finsupp.mapRange f f.map_zero
+  map_zero' := mapRange_zero
+
+@[simp] lemma mapRange.zeroHom_id : mapRange.zeroHom (.id M) = .id (ι →₀ M) := by ext; simp
+
+lemma mapRange.zeroHom_comp (f : ZeroHom N O) (f₂ : ZeroHom M N) :
+    mapRange.zeroHom (ι := ι) (f.comp f₂) = (mapRange.zeroHom f).comp (mapRange.zeroHom f₂) := by
+  ext; simp
+
 end Zero
 
 section AddZeroClass
@@ -327,7 +340,7 @@ instance instIsAddTorsionFree [IsAddTorsionFree M] : IsAddTorsionFree (ι →₀
 end AddMonoid
 
 section AddCommMonoid
-variable [AddCommMonoid M]
+variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid O]
 
 instance instAddCommMonoid : AddCommMonoid (ι →₀ M) :=
   fast_instance% DFunLike.coe_injective.addCommMonoid
@@ -340,6 +353,52 @@ lemma single_add_single_eq_single_add_single {k l m n : ι} {u v : M} (hu : u 
     simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
     exact Pi.single_add_single_eq_single_add_single hu hv
 
+/-- Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.
+-/
+@[simps]
+def mapRange.addMonoidHom (f : M →+ N) : (ι →₀ M) →+ ι →₀ N where
+  toFun := mapRange f f.map_zero
+  map_zero' := mapRange_zero
+  map_add' := mapRange_add f.map_add
+
+@[simp]
+lemma mapRange.addMonoidHom_id :
+    mapRange.addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (ι →₀ M) :=
+  AddMonoidHom.ext mapRange_id
+
+lemma mapRange.addMonoidHom_comp (f : N →+ O) (g : M →+ N) :
+    mapRange.addMonoidHom (ι := ι) (f.comp g) =
+      (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom g) := by ext; simp
+
+@[simp]
+lemma mapRange.addMonoidHom_toZeroHom (f : M →+ N) :
+    (mapRange.addMonoidHom f).toZeroHom = mapRange.zeroHom (ι := ι) f.toZeroHom := rfl
+
+/-- `Finsupp.mapRange.AddMonoidHom` as an equiv. -/
+@[simps! apply]
+def mapRange.addEquiv (em' : M ≃+ N) : (ι →₀ M) ≃+ (ι →₀ N) where
+  toEquiv := mapRange.equiv em' em'.map_zero
+  __ := mapRange.addMonoidHom em'.toAddMonoidHom
+
+@[simp]
+lemma mapRange.addEquiv_refl : mapRange.addEquiv (.refl M) = .refl (ι →₀ M) := by ext; simp
+
+lemma mapRange.addEquiv_trans (e₁ : M ≃+ N) (e₂ : N ≃+ O) :
+    mapRange.addEquiv (ι := ι) (e₁.trans e₂) =
+      (mapRange.addEquiv e₁).trans (mapRange.addEquiv e₂) := by ext; simp
+
+@[simp]
+lemma mapRange.addEquiv_symm (e : M ≃+ N) :
+    (mapRange.addEquiv (ι := ι) e).symm = mapRange.addEquiv e.symm := rfl
+
+@[simp]
+lemma mapRange.addEquiv_toAddMonoidHom (e : M ≃+ N) :
+    mapRange.addEquiv (ι := ι) e = mapRange.addMonoidHom (ι := ι) e.toAddMonoidHom := rfl
+
+@[simp]
+lemma mapRange.addEquiv_toEquiv (e : M ≃+ N) :
+    mapRange.addEquiv (ι := ι) e = mapRange.equiv (ι := ι) (e : M ≃ N) e.map_zero := rfl
+
 end AddCommMonoid
 
 instance instNeg [NegZeroClass G] : Neg (ι →₀ G) where neg := mapRange Neg.neg neg_zero

Mathlib/Algebra/Order/Antidiag/Finsupp.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Eric Wieser, Bhavik Mehta,
   Yaël Dillies
 -/
+import Mathlib.Algebra.BigOperators.Finsupp.Basic
 import Mathlib.Algebra.Order.Antidiag.Pi
-import Mathlib.Data.Finsupp.Basic
 
 /-!
 # Antidiagonal of finitely supported functions as finsets
@@ -26,6 +26,8 @@ We define it using `Finset.piAntidiag s n`, the corresponding antidiagonal in `
 
 -/
 
+assert_not_exists Field
+
 open Finsupp Function
 
 variable {ι μ μ' : Type*}

Mathlib/Data/Finsupp/Basic.lean

@@ -38,7 +38,7 @@ noncomputable section
 
 open Finset Function
 
-variable {α β γ ι M M' N P G H R S : Type*}
+variable {α β γ ι M N P G H R S : Type*}
 
 namespace Finsupp
 
@@ -112,94 +112,9 @@ end Finsupp
 section MapRange
 
 namespace Finsupp
-
-section Equiv
-
-variable [Zero M] [Zero N] [Zero P]
-
-/-- `Finsupp.mapRange` as an equiv. -/
-@[simps apply]
-def mapRange.equiv (f : M ≃ N) (hf : f 0 = 0) (hf' : f.symm 0 = 0) : (α →₀ M) ≃ (α →₀ N) where
-  toFun := (mapRange f hf : (α →₀ M) → α →₀ N)
-  invFun := (mapRange f.symm hf' : (α →₀ N) → α →₀ M)
-  left_inv x := by
-    rw [← mapRange_comp] <;> simp_rw [Equiv.symm_comp_self]
-    · exact mapRange_id _
-    · rfl
-  right_inv x := by
-    rw [← mapRange_comp] <;> simp_rw [Equiv.self_comp_symm]
-    · exact mapRange_id _
-    · rfl
-
-@[simp]
-theorem mapRange.equiv_refl : mapRange.equiv (Equiv.refl M) rfl rfl = Equiv.refl (α →₀ M) :=
-  Equiv.ext mapRange_id
-
-theorem mapRange.equiv_trans (f : M ≃ N) (hf : f 0 = 0) (hf') (f₂ : N ≃ P) (hf₂ : f₂ 0 = 0) (hf₂') :
-    (mapRange.equiv (f.trans f₂) (by rw [Equiv.trans_apply, hf, hf₂])
-          (by rw [Equiv.symm_trans_apply, hf₂', hf']) :
-        (α →₀ _) ≃ _) =
-      (mapRange.equiv f hf hf').trans (mapRange.equiv f₂ hf₂ hf₂') :=
-  Equiv.ext <| mapRange_comp f₂ hf₂ f hf ((congrArg f₂ hf).trans hf₂)
-
-@[simp]
-theorem mapRange.equiv_symm (f : M ≃ N) (hf hf') :
-    ((mapRange.equiv f hf hf').symm : (α →₀ _) ≃ _) = mapRange.equiv f.symm hf' hf :=
-  Equiv.ext fun _ => rfl
-
-end Equiv
-
-section ZeroHom
-
-variable [Zero M] [Zero N] [Zero P]
-
-/-- Composition with a fixed zero-preserving homomorphism is itself a zero-preserving homomorphism
-on functions. -/
-@[simps]
-def mapRange.zeroHom (f : ZeroHom M N) : ZeroHom (α →₀ M) (α →₀ N) where
-  toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
-  map_zero' := mapRange_zero
-
-@[simp]
-theorem mapRange.zeroHom_id : mapRange.zeroHom (ZeroHom.id M) = ZeroHom.id (α →₀ M) :=
-  ZeroHom.ext mapRange_id
-
-theorem mapRange.zeroHom_comp (f : ZeroHom N P) (f₂ : ZeroHom M N) :
-    (mapRange.zeroHom (f.comp f₂) : ZeroHom (α →₀ _) _) =
-      (mapRange.zeroHom f).comp (mapRange.zeroHom f₂) :=
-  ZeroHom.ext <| mapRange_comp f (map_zero f) f₂ (map_zero f₂) (by simp only [comp_apply, map_zero])
-
-end ZeroHom
-
-section AddMonoidHom
-
-variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
+variable [AddCommMonoid M] [AddCommMonoid N]
 variable {F : Type*} [FunLike F M N] [AddMonoidHomClass F M N]
 
-/-- Composition with a fixed additive homomorphism is itself an additive homomorphism on functions.
--/
-@[simps]
-def mapRange.addMonoidHom (f : M →+ N) : (α →₀ M) →+ α →₀ N where
-  toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
-  map_zero' := mapRange_zero
-  map_add' := mapRange_add f.map_add
-
-@[simp]
-theorem mapRange.addMonoidHom_id :
-    mapRange.addMonoidHom (AddMonoidHom.id M) = AddMonoidHom.id (α →₀ M) :=
-  AddMonoidHom.ext mapRange_id
-
-theorem mapRange.addMonoidHom_comp (f : N →+ P) (f₂ : M →+ N) :
-    (mapRange.addMonoidHom (f.comp f₂) : (α →₀ _) →+ _) =
-      (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂) :=
-  AddMonoidHom.ext <|
-    mapRange_comp f (map_zero f) f₂ (map_zero f₂) (by simp only [comp_apply, map_zero])
-
-@[simp]
-theorem mapRange.addMonoidHom_toZeroHom (f : M →+ N) :
-    (mapRange.addMonoidHom f).toZeroHom = (mapRange.zeroHom f.toZeroHom : ZeroHom (α →₀ _) _) :=
-  ZeroHom.ext fun _ => rfl
-
 theorem mapRange_multiset_sum (f : F) (m : Multiset (α →₀ M)) :
     mapRange f (map_zero f) m.sum = (m.map fun x => mapRange f (map_zero f) x).sum :=
   (mapRange.addMonoidHom (f : M →+ N) : (α →₀ _) →+ _).map_multiset_sum _
@@ -208,49 +123,6 @@ theorem mapRange_finset_sum (f : F) (s : Finset ι) (g : ι → α →₀ M) :
     mapRange f (map_zero f) (∑ x ∈ s, g x) = ∑ x ∈ s, mapRange f (map_zero f) (g x) :=
   map_sum (mapRange.addMonoidHom (f : M →+ N)) _ _
 
-/-- `Finsupp.mapRange.AddMonoidHom` as an equiv. -/
-@[simps apply]
-def mapRange.addEquiv (f : M ≃+ N) : (α →₀ M) ≃+ (α →₀ N) :=
-  { mapRange.addMonoidHom f.toAddMonoidHom with
-    toFun := (mapRange f f.map_zero : (α →₀ M) → α →₀ N)
-    invFun := (mapRange f.symm f.symm.map_zero : (α →₀ N) → α →₀ M)
-    left_inv := fun x => by
-      rw [← mapRange_comp] <;> simp_rw [AddEquiv.symm_comp_self]
-      · exact mapRange_id _
-      · rfl
-    right_inv := fun x => by
-      rw [← mapRange_comp] <;> simp_rw [AddEquiv.self_comp_symm]
-      · exact mapRange_id _
-      · rfl }
-
-@[simp]
-theorem mapRange.addEquiv_refl : mapRange.addEquiv (AddEquiv.refl M) = AddEquiv.refl (α →₀ M) :=
-  AddEquiv.ext mapRange_id
-
-theorem mapRange.addEquiv_trans (f : M ≃+ N) (f₂ : N ≃+ P) :
-    (mapRange.addEquiv (f.trans f₂) : (α →₀ M) ≃+ (α →₀ P)) =
-      (mapRange.addEquiv f).trans (mapRange.addEquiv f₂) :=
-  AddEquiv.ext (mapRange_comp _ f₂.map_zero _ f.map_zero (by simp))
-
-@[simp]
-theorem mapRange.addEquiv_symm (f : M ≃+ N) :
-    ((mapRange.addEquiv f).symm : (α →₀ _) ≃+ _) = mapRange.addEquiv f.symm :=
-  AddEquiv.ext fun _ => rfl
-
-@[simp]
-theorem mapRange.addEquiv_toAddMonoidHom (f : M ≃+ N) :
-    ((mapRange.addEquiv f : (α →₀ _) ≃+ _) : _ →+ _) =
-      (mapRange.addMonoidHom f.toAddMonoidHom : (α →₀ _) →+ _) :=
-  AddMonoidHom.ext fun _ => rfl
-
-@[simp]
-theorem mapRange.addEquiv_toEquiv (f : M ≃+ N) :
-    ↑(mapRange.addEquiv f : (α →₀ _) ≃+ _) =
-      (mapRange.equiv (f : M ≃ N) f.map_zero f.symm.map_zero : (α →₀ _) ≃ _) :=
-  Equiv.ext fun _ => rfl
-
-end AddMonoidHom
-
 end Finsupp
 
 end MapRange

Mathlib/Data/Finsupp/Defs.lean

@@ -52,18 +52,15 @@ This file adds `α →₀ M` as a global notation for `Finsupp α M`.
 
 We also use the following convention for `Type*` variables in this file
 
-* `α`, `β`, `γ`: types with no additional structure that appear as the first argument to `Finsupp`
+* `α`, `β`: types with no additional structure that appear as the first argument to `Finsupp`
   somewhere in the statement;
 
 * `ι` : an auxiliary index type;
 
-* `M`, `M'`, `N`, `P`: types with `Zero` or `(Add)(Comm)Monoid` structure; `M` is also used
-  for a (semi)module over a (semi)ring.
+* `M`, `N`, `O`: types with `Zero` or `(Add)(Comm)Monoid` structure;
 
 * `G`, `H`: groups (commutative or not, multiplicative or additive);
 
-* `R`, `S`: (semi)rings.
-
 ## Implementation notes
 
 This file is a `noncomputable theory` and uses classical logic throughout.
@@ -80,7 +77,7 @@ noncomputable section
 
 open Finset Function
 
-variable {α β γ ι M M' N P G H R S : Type*}
+variable {α β ι M N O G H : Type*}
 
 /-- `Finsupp α M`, denoted `α →₀ M`, is the type of functions `f : α → M` such that
   `f x = 0` for all but finitely many `x`. -/
@@ -279,7 +276,7 @@ end OfSupportFinite
 
 section MapRange
 
-variable [Zero M] [Zero N] [Zero P]
+variable [Zero M] [Zero N] [Zero O]
 
 /-- The composition of `f : M → N` and `g : α →₀ M` is `mapRange f hf g : α →₀ N`,
 which is well-defined when `f 0 = 0`.
@@ -311,12 +308,12 @@ theorem mapRange_zero {f : M → N} {hf : f 0 = 0} : mapRange f hf (0 : α →
 theorem mapRange_id (g : α →₀ M) : mapRange id rfl g = g :=
   ext fun _ => rfl
 
-theorem mapRange_comp (f : N → P) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f ∘ f₂) 0 = 0)
+theorem mapRange_comp (f : N → O) (hf : f 0 = 0) (f₂ : M → N) (hf₂ : f₂ 0 = 0) (h : (f ∘ f₂) 0 = 0)
     (g : α →₀ M) : mapRange (f ∘ f₂) h g = mapRange f hf (mapRange f₂ hf₂ g) :=
   ext fun _ => rfl
 
 @[simp]
-lemma mapRange_mapRange (e₁ : N → P) (e₂ : M → N) (he₁ he₂) (f : α →₀ M) :
+lemma mapRange_mapRange (e₁ : N → O) (e₂ : M → N) (he₁ he₂) (f : α →₀ M) :
     mapRange e₁ he₁ (mapRange e₂ he₂ f) = mapRange (e₁ ∘ e₂) (by simp [*]) f := ext fun _ ↦ rfl
 
 theorem support_mapRange {f : M → N} {hf : f 0 = 0} {g : α →₀ M} :
@@ -359,6 +356,28 @@ lemma mapRange_surjective (e : M → N) (he₀ : e 0 = 0) (he : Surjective e) :
 
 end MapRange
 
+section Equiv
+variable [Zero M] [Zero N] [Zero O]
+
+/-- `Finsupp.mapRange` as an equiv. -/
+@[simps apply]
+def mapRange.equiv (e : M ≃ N) (hf : e 0 = 0) : (ι →₀ M) ≃ (ι →₀ N) where
+  toFun := mapRange e hf
+  invFun := mapRange e.symm <| by simp [← hf]
+  left_inv x := by ext; simp
+  right_inv x := by ext; simp
+
+@[simp] lemma mapRange.equiv_refl : mapRange.equiv (.refl M) rfl = .refl (ι →₀ M) := by ext; simp
+
+lemma mapRange.equiv_trans (e : M ≃ N) (hf) (f₂ : N ≃ O) (hf₂) :
+    mapRange.equiv (ι := ι) (e.trans f₂) (by rw [Equiv.trans_apply, hf, hf₂]) =
+      (mapRange.equiv e hf).trans (mapRange.equiv f₂ hf₂) := by ext; simp
+
+@[simp] lemma mapRange.equiv_symm (e : M ≃ N) (hf) :
+    (mapRange.equiv (ι := ι) e hf).symm = mapRange.equiv e.symm (by simp [← hf]) := rfl
+
+end Equiv
+
 /-! ### Declarations about `embDomain` -/
 
 
@@ -438,12 +457,12 @@ end EmbDomain
 
 section ZipWith
 
-variable [Zero M] [Zero N] [Zero P]
+variable [Zero M] [Zero N] [Zero O]
 
-/-- Given finitely supported functions `g₁ : α →₀ M` and `g₂ : α →₀ N` and function `f : M → N → P`,
-`Finsupp.zipWith f hf g₁ g₂` is the finitely supported function `α →₀ P` satisfying
+/-- Given finitely supported functions `g₁ : α →₀ M` and `g₂ : α →₀ N` and function `f : M → N → O`,
+`Finsupp.zipWith f hf g₁ g₂` is the finitely supported function `α →₀ O` satisfying
 `zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, which is well-defined when `f 0 0 = 0`. -/
-def zipWith (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P :=
+def zipWith (f : M → N → O) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ O :=
   onFinset
     (haveI := Classical.decEq α; g₁.support ∪ g₂.support)
     (fun a => f (g₁ a) (g₂ a))
@@ -453,11 +472,11 @@ def zipWith (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α
       rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H; exact H hf
 
 @[simp]
-theorem zipWith_apply {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
+theorem zipWith_apply {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M} {g₂ : α →₀ N} {a : α} :
     zipWith f hf g₁ g₂ a = f (g₁ a) (g₂ a) :=
   rfl
 
-theorem support_zipWith [D : DecidableEq α] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M}
+theorem support_zipWith [D : DecidableEq α] {f : M → N → O} {hf : f 0 0 = 0} {g₁ : α →₀ M}
     {g₂ : α →₀ N} : (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support := by
   convert support_onFinset_subset
 

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -132,8 +132,8 @@ lemma of_ringEquiv {R R' M M'} [Semiring R] [AddCommMonoid M] [Module R M]
   let I := Module.Free.ChooseBasisIndex R M
   obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M
   let e : M' ≃+ (I →₀ R') :=
-    (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv)
-  have he (x) : e x = Finsupp.mapRange.addEquiv (α := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
+    (e₂.symm.trans e₃).toAddEquiv.trans (Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv)
+  have he (x) : e x = Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
   let e' : M' ≃ₗ[R'] (I →₀ R') :=
     { __ := e, map_smul' := fun m x ↦ Finsupp.ext fun i ↦ by simp [he, map_smulₛₗ] }
   exact of_basis (.ofRepr e')

Mathlib/RingTheory/Polynomial/Opposites.lean

@@ -81,7 +81,7 @@ theorem coeff_opRingEquiv (p : R[X]ᵐᵒᵖ) (n : ℕ) :
 
 @[simp]
 theorem support_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).support = (unop p).support :=
-  Finsupp.support_mapRange_of_injective (map_zero _) _ op_injective
+  Finsupp.support_mapRange_of_injective (by simp) _ op_injective
 
 @[simp]
 theorem natDegree_opRingEquiv (p : R[X]ᵐᵒᵖ) : (opRingEquiv R p).natDegree = (unop p).natDegree := by