refactor(LinearAlgebra/ExteriorAlgebra/{Basic,Grading}): add a defini…

…tion and notation for the exterior powers of a module (#10744)

This is split off from PR #10654 (that actually proves some properties of the exterior powers). It introduces the reducible definition `exteriorPower R n M` for the `n`th exterior power of the `R`-module `M`; this is of type `Submodule R (ExteriorAlgebra R M)` and defined as `LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n`. 
It also introduces the notation `Λ[R]^n M` for `exteriorPower R n M`.

Note: for a reason that I don't understand, Lean becomes unable to synthesize the `SetLike.GradedMonoid` instance on `fun (i : ℕ) ↦ (Λ[R]^i) M`, so I added it manually in `ExteriorAlgebra/Graded.lean`. I am far from sure that this is the correct solution.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Richard Copley <buster@buster.me.uk>

Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean

@@ -18,6 +18,11 @@ We construct the exterior algebra of a module `M` over a commutative semiring `R
 The exterior algebra of the `R`-module `M` is denoted as `ExteriorAlgebra R M`.
 It is endowed with the structure of an `R`-algebra.
 
+The `n`th exterior power of the `R`-module `M` is denoted by `exteriorPower R n M`;
+it is of type `Submodule R (ExteriorAlgebra R M)` and defined as
+`LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n`.
+We also introduce the notation `⋀[R]^n M` for `exteriorPower R n M`.
+
 Given a linear morphism `f : M → A` from a module `M` to another `R`-algebra `A`, such that
 `cond : ∀ m : M, f m * f m = 0`, there is a (unique) lift of `f` to an `R`-algebra morphism,
 which is denoted `ExteriorAlgebra.lift R f cond`.
@@ -66,6 +71,21 @@ def ι : M →ₗ[R] ExteriorAlgebra R M :=
   CliffordAlgebra.ι _
 #align exterior_algebra.ι ExteriorAlgebra.ι
 
+section exteriorPower
+
+-- New variables `n` and `M`, to get the correct order of variables in the notation.
+variable (n : ℕ) (M : Type u2) [AddCommGroup M] [Module R M]
+
+/-- Definition of the `n`th exterior power of a `R`-module `N`. We introduce the notation
+`⋀[R]^n M` for `exteriorPower R n M`. -/
+abbrev exteriorPower : Submodule R (ExteriorAlgebra R M) :=
+  LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n
+
+@[inherit_doc exteriorPower]
+notation:max "⋀[" R "]^" n:arg => exteriorPower R n
+
+end exteriorPower
+
 variable {R}
 
 /-- As well as being linear, `ι m` squares to zero. -/
@@ -333,7 +353,7 @@ variable (R)
 
 /-- The image of `ExteriorAlgebra.ιMulti R n` is contained in the `n`th exterior power. -/
 lemma ιMulti_range (n : ℕ) :
-    Set.range (ιMulti R n (M := M)) ⊆ ↑(LinearMap.range (ι R (M := M)) ^ n) := by
+    Set.range (ιMulti R n (M := M)) ⊆ ↑(⋀[R]^n M) := by
   rw [Set.range_subset_iff]
   intro v
   rw [ιMulti_apply]
@@ -344,10 +364,9 @@ lemma ιMulti_range (n : ℕ) :
 /-- The image of `ExteriorAlgebra.ιMulti R n` spans the `n`th exterior power, as a submodule
 of the exterior algebra. -/
 lemma ιMulti_span_fixedDegree (n : ℕ) :
-    Submodule.span R (Set.range (ιMulti R n)) =
-    LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n := by
+    Submodule.span R (Set.range (ιMulti R n)) = ⋀[R]^n M := by
   refine le_antisymm (Submodule.span_le.2 (ιMulti_range R n)) ?_
-  rw [Submodule.pow_eq_span_pow_set, Submodule.span_le]
+  rw [exteriorPower, Submodule.pow_eq_span_pow_set, Submodule.span_le]
   refine fun u hu ↦ Submodule.subset_span ?_
   obtain ⟨f, rfl⟩ := Set.mem_pow.mp hu
   refine ⟨fun i => ιInv (f i).1, ?_⟩

Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

@@ -17,7 +17,6 @@ The main result is `ExteriorAlgebra.gradedAlgebra`, which says that the exterior
 ℕ-graded algebra.
 -/
 
-
 namespace ExteriorAlgebra
 
 variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
@@ -30,18 +29,24 @@ open scoped DirectSum
 primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`. -/
 -- porting note: protected
 protected def GradedAlgebra.ι :
-    M →ₗ[R] ⨁ i : ℕ, ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i) :=
-  DirectSum.lof R ℕ (fun i => ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) 1 ∘ₗ
+    M →ₗ[R] ⨁ i : ℕ, ⋀[R]^i M :=
+  DirectSum.lof R ℕ (fun i => ⋀[R]^i M) 1 ∘ₗ
     (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m
 #align exterior_algebra.graded_algebra.ι ExteriorAlgebra.GradedAlgebra.ι
 
 theorem GradedAlgebra.ι_apply (m : M) :
     GradedAlgebra.ι R M m =
-      DirectSum.of (fun i : ℕ => ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)) 1
+      DirectSum.of (fun i : ℕ => ⋀[R]^i M) 1
         ⟨ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ :=
   rfl
 #align exterior_algebra.graded_algebra.ι_apply ExteriorAlgebra.GradedAlgebra.ι_apply
 
+-- Defining this instance manually, because Lean doesn't seem to be able to synthesize it.
+-- Strangely, this problem only appears when we use the abbreviation or notation for the
+-- exterior powers.
+instance : SetLike.GradedMonoid fun i : ℕ ↦ ⋀[R]^i M :=
+  Submodule.nat_power_gradedMonoid (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))
+
 -- Porting note: Lean needs to be reminded of this instance otherwise it cannot
 -- synthesize 0 in the next theorem
 attribute [instance 1100] MulZeroClass.toZero in
@@ -53,18 +58,12 @@ theorem GradedAlgebra.ι_sq_zero (m : M) : GradedAlgebra.ι R M m * GradedAlgebr
 /-- `ExteriorAlgebra.GradedAlgebra.ι` lifted to exterior algebra. This is
 primarily an auxiliary construction used to provide `ExteriorAlgebra.gradedAlgebra`. -/
 def GradedAlgebra.liftι :
-    ExteriorAlgebra R M →ₐ[R] ⨁ i : ℕ,
-    (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i : Submodule R (ExteriorAlgebra R M)) :=
+    ExteriorAlgebra R M →ₐ[R] ⨁ i : ℕ, ⋀[R]^i M :=
   lift R ⟨by apply GradedAlgebra.ι R M, GradedAlgebra.ι_sq_zero R M⟩
 #align exterior_algebra.graded_algebra.lift_ι ExteriorAlgebra.GradedAlgebra.liftι
 
-theorem GradedAlgebra.liftι_eq (i : ℕ)
-    (x : (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i :
-      Submodule R (ExteriorAlgebra R M))) :
-    GradedAlgebra.liftι R M x =
-    DirectSum.of (fun i =>
-      ↥(LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i :
-      Submodule R (ExteriorAlgebra R M))) i x := by
+theorem GradedAlgebra.liftι_eq (i : ℕ) (x : ⋀[R]^i M) :
+    GradedAlgebra.liftι R M x = DirectSum.of (fun i => ⋀[R]^i M) i x := by
   cases' x with x hx
   dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
   -- Porting note: original statement was
@@ -83,8 +82,7 @@ theorem GradedAlgebra.liftι_eq (i : ℕ)
 #align exterior_algebra.graded_algebra.lift_ι_eq ExteriorAlgebra.GradedAlgebra.liftι_eq
 
 /-- The exterior algebra is graded by the powers of the submodule `(ExteriorAlgebra.ι R).range`. -/
-instance gradedAlgebra :
-    GradedAlgebra (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ · : ℕ → Submodule R _) :=
+instance gradedAlgebra : GradedAlgebra (fun i : ℕ ↦ ⋀[R]^i M) :=
   GradedAlgebra.ofAlgHom _
     (-- while not necessary, the `by apply` makes this elaborate faster
     by apply GradedAlgebra.liftι R M)
@@ -103,8 +101,7 @@ lemma ιMulti_span :
     Submodule.span R (Set.range fun x : Σ n, (Fin n → M) => ιMulti R x.1 x.2) = ⊤ := by
   rw [Submodule.eq_top_iff']
   intro x
-  induction x
-    using DirectSum.Decomposition.inductionOn fun i => LinearMap.range (ι R (M := M)) ^ i with
+  induction x using DirectSum.Decomposition.inductionOn fun i => ⋀[R]^i M with
   | h_zero => exact Submodule.zero_mem _
   | h_add _ _ hm hm' => exact Submodule.add_mem _ hm hm'
   | h_homogeneous hm =>