chore(LinearAlgebra/Alternating): move currying to a new file (#24800)

The only change is removing primes from all variable names in the new files.

I plan to add more operations to the new file soon, required to define operations on differential forms.

Author: urkud

Mathlib.lean

@@ -3805,6 +3805,7 @@ import Mathlib.LinearAlgebra.AffineSpace.Pointwise
 import Mathlib.LinearAlgebra.AffineSpace.Restrict
 import Mathlib.LinearAlgebra.AffineSpace.Slope
 import Mathlib.LinearAlgebra.Alternating.Basic
+import Mathlib.LinearAlgebra.Alternating.Curry
 import Mathlib.LinearAlgebra.Alternating.DomCoprod
 import Mathlib.LinearAlgebra.AnnihilatingPolynomial
 import Mathlib.LinearAlgebra.Basis.Basic

Mathlib/Analysis/InnerProductSpace/TwoDim.lean

@@ -7,6 +7,7 @@ import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.Orientation
 import Mathlib.Data.Complex.FiniteDimensional
 import Mathlib.Data.Complex.Orientation
+import Mathlib.LinearAlgebra.Alternating.Curry
 import Mathlib.Tactic.LinearCombination
 
 /-!
@@ -92,7 +93,7 @@ irreducible_def areaForm : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := by
     AlternatingMap.constLinearEquivOfIsEmpty.symm
   let y : E [⋀^Fin 1]→ₗ[ℝ] ℝ →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
     LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
-  exact y ∘ₗ AlternatingMap.curryLeftLinearMap (R' := ℝ) o.volumeForm
+  exact y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm
 
 local notation "ω" => o.areaForm
 

Mathlib/LinearAlgebra/Alternating/Basic.lean

@@ -6,7 +6,6 @@ Authors: Eric Wieser, Zhangir Azerbayev
 import Mathlib.GroupTheory.Perm.Sign
 import Mathlib.LinearAlgebra.LinearIndependent.Defs
 import Mathlib.LinearAlgebra.Multilinear.Basis
-import Mathlib.LinearAlgebra.Multilinear.Curry
 
 /-!
 # Alternating Maps
@@ -886,90 +885,18 @@ theorem Basis.ext_alternating {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι
 
 end Basis
 
-/-! ### Currying -/
-
-
-section Currying
-
 variable {R' : Type*} {M'' M₂'' N'' N₂'' : Type*} [CommSemiring R'] [AddCommMonoid M'']
   [AddCommMonoid M₂''] [AddCommMonoid N''] [AddCommMonoid N₂''] [Module R' M''] [Module R' M₂'']
   [Module R' N''] [Module R' N₂'']
 
-namespace AlternatingMap
-
-/-- Given an alternating map `f` in `n+1` variables, split the first variable to obtain
-a linear map into alternating maps in `n` variables, given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
-It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.
-
-This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
-`AlternatingMap.curryLeftLinearMap`. -/
-@[simps]
-def curryLeft {n : ℕ} (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
-    M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
-  toFun m :=
-    { f.toMultilinearMap.curryLeft m with
-      toFun := fun v => f (Matrix.vecCons m v)
-      map_eq_zero_of_eq' := fun v i j hv hij =>
-        f.map_eq_zero_of_eq _ (by
-          rwa [Matrix.cons_val_succ, Matrix.cons_val_succ]) ((Fin.succ_injective _).ne hij) }
-  map_add' _ _ := ext fun _ => f.map_vecCons_add _ _ _
-  map_smul' _ _ := ext fun _ => f.map_vecCons_smul _ _ _
-
-@[simp]
-theorem curryLeft_zero {n : ℕ} : curryLeft (0 : M'' [⋀^Fin n.succ]→ₗ[R'] N'') = 0 :=
-  rfl
-
-@[simp]
-theorem curryLeft_add {n : ℕ} (f g : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
-    curryLeft (f + g) = curryLeft f + curryLeft g :=
-  rfl
-
-@[simp]
-theorem curryLeft_smul {n : ℕ} (r : R') (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') :
-    curryLeft (r • f) = r • curryLeft f :=
-  rfl
-
-/-- `AlternatingMap.curryLeft` as a `LinearMap`. This is a separate definition as dot notation
-does not work for this version. -/
-@[simps]
-def curryLeftLinearMap {n : ℕ} :
-    (M'' [⋀^Fin n.succ]→ₗ[R'] N'') →ₗ[R'] M'' →ₗ[R'] M'' [⋀^Fin n]→ₗ[R'] N'' where
-  toFun f := f.curryLeft
-  map_add' := curryLeft_add
-  map_smul' := curryLeft_smul
-
-/-- Currying with the same element twice gives the zero map. -/
-@[simp]
-theorem curryLeft_same {n : ℕ} (f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N'') (m : M'') :
-    (f.curryLeft m).curryLeft m = 0 :=
-  ext fun _ => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one
-
-@[simp]
-theorem curryLeft_compAlternatingMap {n : ℕ} (g : N'' →ₗ[R'] N₂'')
-    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M'') :
-    (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m) :=
-  rfl
-
-@[simp]
-theorem curryLeft_compLinearMap {n : ℕ} (g : M₂'' →ₗ[R'] M'')
-    (f : M'' [⋀^Fin n.succ]→ₗ[R'] N'') (m : M₂'') :
-    (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
-  ext fun v => congr_arg f <| funext <| by
-    refine Fin.cases ?_ ?_
-    · rfl
-    · simp
-
 /-- The space of constant maps is equivalent to the space of maps that are alternating with respect
 to an empty family. -/
 @[simps]
-def constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'') where
+def AlternatingMap.constLinearEquivOfIsEmpty [IsEmpty ι] : N'' ≃ₗ[R'] (M'' [⋀^ι]→ₗ[R'] N'') where
   toFun := AlternatingMap.constOfIsEmpty R' M'' ι
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
   invFun f := f 0
   left_inv _ := rfl
   right_inv f := ext fun _ => AlternatingMap.congr_arg f <| Subsingleton.elim _ _
 
-end AlternatingMap
-
-end Currying

Mathlib/LinearAlgebra/Alternating/Curry.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.LinearAlgebra.Alternating.Basic
+import Mathlib.LinearAlgebra.Multilinear.Curry
+
+/-!
+# Currying alternating forms
+
+In this file we define `AlternatingMap.curryLeft`
+which interprets an alternating map in `n + 1` variables
+as a linear map in the 0th variable taking values in the alternating maps in `n` variables.
+-/
+
+variable {R : Type*} {M M₂ N N₂ : Type*} [CommSemiring R] [AddCommMonoid M]
+  [AddCommMonoid M₂] [AddCommMonoid N] [AddCommMonoid N₂] [Module R M] [Module R M₂]
+  [Module R N] [Module R N₂]
+
+namespace AlternatingMap
+
+/-- Given an alternating map `f` in `n+1` variables, split the first variable to obtain
+a linear map into alternating maps in `n` variables, given by `x ↦ (m ↦ f (Matrix.vecCons x m))`.
+It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.
+
+This is `MultilinearMap.curryLeft` for `AlternatingMap`. See also
+`AlternatingMap.curryLeftLinearMap`. -/
+@[simps]
+def curryLeft {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) :
+    M →ₗ[R] M [⋀^Fin n]→ₗ[R] N where
+  toFun m :=
+    { f.toMultilinearMap.curryLeft m with
+      toFun := fun v => f (Matrix.vecCons m v)
+      map_eq_zero_of_eq' := fun v i j hv hij =>
+        f.map_eq_zero_of_eq _ (by
+          rwa [Matrix.cons_val_succ, Matrix.cons_val_succ]) ((Fin.succ_injective _).ne hij) }
+  map_add' _ _ := ext fun _ => f.map_vecCons_add _ _ _
+  map_smul' _ _ := ext fun _ => f.map_vecCons_smul _ _ _
+
+@[simp]
+theorem curryLeft_zero {n : ℕ} : curryLeft (0 : M [⋀^Fin n.succ]→ₗ[R] N) = 0 :=
+  rfl
+
+@[simp]
+theorem curryLeft_add {n : ℕ} (f g : M [⋀^Fin n.succ]→ₗ[R] N) :
+    curryLeft (f + g) = curryLeft f + curryLeft g :=
+  rfl
+
+@[simp]
+theorem curryLeft_smul {n : ℕ} (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N) :
+    curryLeft (r • f) = r • curryLeft f :=
+  rfl
+
+/-- `AlternatingMap.curryLeft` as a `LinearMap`. This is a separate definition as dot notation
+does not work for this version. -/
+@[simps]
+def curryLeftLinearMap {n : ℕ} :
+    (M [⋀^Fin n.succ]→ₗ[R] N) →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N where
+  toFun f := f.curryLeft
+  map_add' := curryLeft_add
+  map_smul' := curryLeft_smul
+
+/-- Currying with the same element twice gives the zero map. -/
+@[simp]
+theorem curryLeft_same {n : ℕ} (f : M [⋀^Fin n.succ.succ]→ₗ[R] N) (m : M) :
+    (f.curryLeft m).curryLeft m = 0 :=
+  ext fun _ => f.map_eq_zero_of_eq _ (by simp) Fin.zero_ne_one
+
+@[simp]
+theorem curryLeft_compAlternatingMap {n : ℕ} (g : N →ₗ[R] N₂)
+    (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) :
+    (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m) :=
+  rfl
+
+@[simp]
+theorem curryLeft_compLinearMap {n : ℕ} (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M₂) :
+    (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g :=
+  ext fun v => congr_arg f <| funext <| by
+    refine Fin.cases ?_ ?_
+    · rfl
+    · simp
+
+end AlternatingMap
+

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
-import Mathlib.LinearAlgebra.Alternating.Basic
+import Mathlib.LinearAlgebra.Alternating.Curry
 
 /-!
 # Exterior Algebras