feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties #10654

smorel394 · 2024-02-17T08:42:45Z

This introduces the exterior powers of a module and proves some of their basic properties, in LinearAlgebra/ExteriorPower/Basic.lean and LinearAlgebra/ExteriorPower/Generators.lean. It also adds a lemma in LinearAlgebra/LinearIndependent.lean (linearIndependent_of_dualFamily : if a family of vectors admits a "dual" family of linear forms, then it is linearly independent) and a construction in LinearAlgebra/TensorPower.lean (linearFormOfFamily : the linear form on the tensor power of M obtained by multiplying a family of linear forms on M).

Main definitions

In `LinearAlgebra/ExteriorPower/Basic.lean`:

ExteriorPower R n M is the nth exterior power of a R-module M, 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.
ExteriorPower.ιMulti is the canonical alternating map on M with values in Λ[R]^n M.
ExteriorPower.map: functoriality of exterior powers with respect to linear maps between modules.
ExteriorPower.toTensorPower: linear map from the nth exterior power to the nth
tensor power (coming from MultilinearMap.alternatization via the universal property of
exterior powers).

In `LinearAlgebra/ExteriorPower/Generators.lean`:

ExteriorPower.BasisOfBasis: If b is a basis of M (indexed by a linearly ordered type),
the basis of the nth exterior power of M formed by the n-fold exterior products of elements
of b.

Main theorems

In `LinearAlgebra/ExteriorPower/Basic.lean`:

The image of ExteriorPower.ιMulti spans Λ[R]^n M.
ExteriorPower.liftAlternatingEquiv (universal property of the nth exterior power of M):
the linear equivalence between linear maps from Λ[R]^n M to a module N and n-fold
alternating maps from M to N.
ExteriorPower.map_injective_field: If f : M →ₗ[R] N is injective and R is a field, then
ExteriorPower.map n f is injective.
ExteriorPower.map_surjective: If f : M →ₗ[R] N is surjective, then ExteriorPower.map n f
is surjective.
ExteriorPower.mem_exteriorPower_is_mem_finite: Every element of Λ[R]^n M is in the image of
Λ[R]^n P for some finitely generated submodule P of M.

In `LinearAlgebra/ExteriorPower/Generators.lean`:

ExteriorPower.Finite: The nth exterior power of a finite module is a finite module.
ExteriorPower.span_top_of_span_top and ExteriorPower.span_top_of_span_top': If a family of
vectors spans M, then the family of its n-fold exterior products spans Λ[R]^n M. (We give
versions in the exterior algebra and in the exterior power.)
ExteriorPower.FreeOfFree: If M is a free module, then so is its nth exterior power.
ExteriorPower.FinrankOfFiniteFree: If R satisfies the strong rank condition and M is
finite free of rank r, then the nth exterior power of M is of finrank Nat.choose r n.
ExteriorPower.ιMulti_family_linearIndependent_field: If R is a field, and if v is a
linearly independent family of vectors (indexed by a linearly ordered type), then the family of
its n-fold exterior products is also linearly independent.

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

eric-wieser · 2024-02-18T16:01:31Z

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

+`Λ[R]^n M` for `ExteriorPower R n M`. -/
+@[reducible]
+def ExteriorPower := (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)
+
+@[inherit_doc]
+notation:100 "Λ[" R "]^" n:arg => ExteriorPower R n


I think (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n) is already used quite a lot throughout mathlib; can you split out a PR that just adds this new def and notation, and replaces all the existing uses with the new notation?

Can do. Given that this expression already appears in LinearAlgebra/ExteriorAlgebra/Basic.lean, I guess it would make sense to introduce ExteriorPower there.

It's maybe worth waiting to see what Zulip says about the type of this expression, Right now Lean is inferring this as Submodule R (ExteriorAlgebra R M)

Suggested change

`Λ[R]^n M` for `ExteriorPower R n M`. -/

@[reducible]

def ExteriorPower := (LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

@[inherit_doc]

notation:100 "Λ[" R "]^" n:arg => ExteriorPower R n

`Λ[R]^n M` for `ExteriorPower R n M`. -/

@[reducible]

def ExteriorPower : Submodule R (ExteriorAlgebra R M) :=

(LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n)

@[inherit_doc]

notation:100 "Λ[" R "]^" n:arg => ExteriorPower R n

but this goes against the naming convention, since ExteriorPower is not a type.

Either we should make it a type (in which case it won't actually work as a substitute in a handful of places), or we should rename it to exteriorPower.

Right, I am actually using that it's a submodule of the exterior algebra in a few places. Anyway, I started a new branch that defined ExteriorPower earlier and started substituting it there, and it's creating timeouts in ExteriorAlgebra/Grading.lean. I need to play around with it more to see if I can figure out what happened.

Okay, I changed all the ExteriorPowers to exteriorPowers and created PR #10744 to introduce the definition and notation. (But it does have that annoying instance synthesization problem.)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

mattrobball · 2024-02-18T16:15:18Z

!bench

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

leanprover-bot · 2024-02-18T16:38:16Z

Here are the benchmark results for commit 3c3d7f9.
There were no significant changes against commit 29c27c3.

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

…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>

leanprover-community-mathlib4-bot · 2024-02-29T11:47:19Z

This PR/issue depends on:

~~[Merged by Bors] - refactor(LinearAlgebra/ExteriorAlgebra/{Basic,Grading}): add a definition and notation for the exterior powers of a module #10744~~
feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of PiTensorProduct #11156
By Dependent Issues (🤖). Happy coding!

eric-wieser · 2024-03-01T12:51:01Z

Mathlib/LinearAlgebra/TensorPower.lean

+
+/-- A family `f` of linear forms on `M` indexed by `Fin n` defines a linear form on
+`⨂[R]^n M`, by multiplying the components of `f`. -/
+noncomputable def linearFormOfFamily (f : (_ : Fin n) → (M →ₗ[R] R)) : (⨂[R]^n) M →ₗ[R] R :=


Suggested change

noncomputable def linearFormOfFamily (f : (_ : Fin n) → (M →ₗ[R] R)) : (⨂[R]^n) M →ₗ[R] R :=

noncomputable def linearFormOfFamily (f : (_ : Fin n) → Module.Dual R M) : Module.Dual R (⨂[R]^n M) :=

I think this holds more generally for the n-ary tensor products, rather than just tensor powers; can you add that definition instead?

I don't think that it should make it more complicated, so I'll try.
You suggested having a name that contains dual instead of linearFormOfFamily, and I'm not against that, but I don't feel very inspired.

TensorProduct.dualDistrib seems pretty analogous to this result; ideally we would bundle this map slightly further, and use the same name.

You're right, my linearFormOfFamily is basically PiTensorProduct.dualDistrib applied to the case of a constant family. PiTensorProduct.dualDistrib doesn't exist yet, but I'll get to work on it.
I don't know if you were also suggesting to unify the case of the tensor product of two modules and that of the tensor product of a finite family of modules; if so, I don't know how to do that.

Okay, so there is no PiTensorProduct.map, I have to define that too... I am making this into another PR, because I am afraid that it will grow.

I started working in a new branch. Let's hope this doesn't grow too large.

I don't know if you were also suggesting to unify the case of the tensor product of two modules and that of the tensor product of a finite family of modules; if so, I don't know how to do that.

No, I am certainly not suggesting this! Just that we should try to match the names of the AP

I started working in a new branch. Let's hope this doesn't grow too large.

It looks like you haven't pushed this branch yet.

I did push it, but I didn't create a PR yet. I also got my link wrong somehow. Let's try again.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…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>

bustercopley

I'm really looking forward to this.

bustercopley · 2024-03-02T22:28:54Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+theorem finite [Module.Finite R M]: Module.Finite R (⋀[R]^n M) :=
+  Module.Finite.mk ((Submodule.fg_top _).mpr (Submodule.FG.pow (by
+  rw [LinearMap.range_eq_map]; exact Submodule.FG.map _  (Module.finite_def.mp inferInstance)) _ ))


Suggested change

theorem finite [Module.Finite R M]: Module.Finite R (⋀[R]^n M) :=

Module.Finite.mk ((Submodule.fg_top _).mpr (Submodule.FG.pow (by

rw [LinearMap.range_eq_map]; exact Submodule.FG.map _ (Module.finite_def.mp inferInstance)) _ ))

instance instFinite [Module.Finite R M]: Module.Finite R (⋀[R]^n M) :=

Module.Finite.mk ((Submodule.fg_top _).mpr (Submodule.FG.pow (by

rw [LinearMap.range_eq_map]; exact Submodule.FG.map _ (Module.finite_def.mp inferInstance)) _ ))

bustercopley · 2024-03-02T22:29:42Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+
+/-- If `b` is a basis of `M` (indexed by a linearly ordered type), the basis of the `n`th
+exterior power of `M` formed by the `n`-fold exterior products of elements of `b`. -/
+noncomputable def BasisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :


Suggested change

noncomputable def BasisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :

noncomputable def basisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :

and throughout

or _root_.Basis.exteriorPower?

bustercopley · 2024-03-02T22:30:17Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+  (by rw [span_top_of_span_top']; rw [Basis.span_eq])
+
+@[simp]
+lemma BasisOfBasis_coe {I : Type*} [LinearOrder I] (b : Basis I R M) :


Suggested change

lemma BasisOfBasis_coe {I : Type*} [LinearOrder I] (b : Basis I R M) :

lemma coe_basisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :

and throughout

bustercopley · 2024-03-02T22:31:22Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+lemma FreeOfFree (hfree : Module.Free R M) : Module.Free R (⋀[R]^n M) :=
+  let ⟨I, b⟩ := (Classical.choice hfree.exists_basis)
+  letI := WellFounded.wellOrderExtension (emptyWf (α := I)).wf
+  Module.Free.of_basis (BasisOfBasis R n b)


Suggested change

lemma FreeOfFree (hfree : Module.Free R M) : Module.Free R (⋀[R]^n M) :=

let ⟨I, b⟩ := (Classical.choice hfree.exists_basis)

letI := WellFounded.wellOrderExtension (emptyWf (α := I)).wf

Module.Free.of_basis (BasisOfBasis R n b)

instance instFree [hfree : Module.Free R M] : Module.Free R (⋀[R]^n M) :=

let ⟨I, b⟩ := hfree.exists_basis

letI := WellFounded.wellOrderExtension (emptyWf (α := I)).wf

Module.Free.of_basis (basisOfBasis R n b)

bustercopley · 2024-03-02T22:33:42Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+lemma nonemptyOfNonempty {I : Type*} [LinearOrder I]
+    (hne : Nonempty {v : I → E // LinearIndependent K v}) :
+    Nonempty {v : {s : Finset I // Finset.card s = n} →
+    (⋀[K]^n) E // LinearIndependent K v} :=
+  let v := Classical.choice hne
+  Nonempty.intro ⟨ιMulti_family K n v, ιMulti_family_linearIndependent_field n v.2⟩


Suggested change

lemma nonemptyOfNonempty {I : Type*} [LinearOrder I]

(hne : Nonempty {v : I → E // LinearIndependent K v}) :

Nonempty {v : {s : Finset I // Finset.card s = n} →

(⋀[K]^n) E // LinearIndependent K v} :=

let v := Classical.choice hne

Nonempty.intro ⟨ιMulti_family K n v, ιMulti_family_linearIndependent_field n v.2⟩

instance instNonempty {I : Type*} [LinearOrder I] [Nonempty {v : I → E // LinearIndependent K v}] :

Nonempty {v : {s : Finset I // Finset.card s = n} → (⋀[K]^n) E // LinearIndependent K v} :=

Nonempty.map (fun v : {v : I → E // LinearIndependent K v} ↦

⟨ιMulti_family K n v, ιMulti_family_linearIndependent_field n v.2⟩) ‹_›

bustercopley · 2024-03-02T22:42:32Z

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

+lemma FinrankOfFiniteFree (hfree : Module.Free R M) [Module.Finite R M] :
+    FiniteDimensional.finrank R (⋀[R]^n M) =
+    Nat.choose (FiniteDimensional.finrank R M) n :=
+  letI := WellFounded.wellOrderExtension (emptyWf (α := hfree.ChooseBasisIndex)).wf
+  let B :=  BasisOfBasis R n (hfree.chooseBasis)
+  by rw [FiniteDimensional.finrank_eq_card_basis hfree.chooseBasis,
+    FiniteDimensional.finrank_eq_card_basis B, Fintype.card_finset_len]


Suggested change

lemma FinrankOfFiniteFree (hfree : Module.Free R M) [Module.Finite R M] :

FiniteDimensional.finrank R (⋀[R]^n M) =

Nat.choose (FiniteDimensional.finrank R M) n :=

letI := WellFounded.wellOrderExtension (emptyWf (α := hfree.ChooseBasisIndex)).wf

let B := BasisOfBasis R n (hfree.chooseBasis)

by rw [FiniteDimensional.finrank_eq_card_basis hfree.chooseBasis,

FiniteDimensional.finrank_eq_card_basis B, Fintype.card_finset_len]

lemma finrank_eq_of_finite_free [hfree : Module.Free R M] [Module.Finite R M] :

FiniteDimensional.finrank R (⋀[R]^n M) =

Nat.choose (FiniteDimensional.finrank R M) n := by

letI := WellFounded.wellOrderExtension (emptyWf (α := hfree.ChooseBasisIndex)).wf

let B := basisOfBasis R n hfree.chooseBasis

rw [FiniteDimensional.finrank_eq_card_basis hfree.chooseBasis,

FiniteDimensional.finrank_eq_card_basis B, Fintype.card_finset_len]

or just finrank_eq?

* `exteriorPower.BasisOfBases` -> `Basis.exteriorPower` * `exteriorPower.BasisOfBasis_coe` -> `exteriorPower.coe_basis` * `exteriorPower.BasisOfBasis_apply` -> `exteriorPower.basis_apply` * `exteriorPower.BasisOfBasis_coord` -> `exteriorPower.basis_coord` * `FinrankOfFiniteFree` -> `finrank_eq` * `theorem finite` -> `instance instFinite` * `theorem FreeOfFree` -> `instance instFree` Use instance-implicit arguments for `Module.Free` and `Nonempty`.

bustercopley · 2024-03-04T00:09:06Z

I've made those changes, along with a separate golf commit, on [edit: deleted branch]. Feel free to use any or all of it if you want.

smorel394 · 2024-03-04T06:05:38Z

I've made those changes, along with a separate golf commit, on branch https://github.com/leanprover-community/mathlib4/commits/RC/ExteriorPower/ . Feel free to use any or all of it if you want.

Thanks ! I'm happy to use all of them, you can make them directly here if you want, otherwise I'll try to get to it this evening.
Sorry, yesterday I was concentrating on the tensor power stuff, generalizing linearFormOfFamily as Eric Wieser suggested, and it turns out there's a lot of stuff that is only done for TensorProduct and not PiTensorProduct, so I was writing some of it.

eric-wieser · 2024-03-04T08:54:41Z

turns out there's a lot of stuff that is only done for TensorProduct and not PiTensorProduct, so I was writing some of it.

Don't feel like you have to write everything that's missing, especially not in one go; the changes in PiTensorProduct.lean alone would make a good standalone PR, and I think cover most of what you actually need in this one.

smorel394 · 2024-03-04T16:44:52Z

turns out there's a lot of stuff that is only done for TensorProduct and not PiTensorProduct, so I was writing some of it.

Don't feel like you have to write everything that's missing, especially not in one go; the changes in PiTensorProduct.lean alone would make a good standalone PR, and I think cover most of what you actually need in this one.

I got slightly carried away...
Anyway, I realized that the functoriality of PiTensorProducts (i.e. PiTensorProduct.map) had been recently added to mathlib, but there were still some missing features of it, so I added them there: #11152

But I also constructed a basis of the PiTensorProduct, and for this proved that it distributes over DirectSums, and... I an preparing the PRs now.

smorel394 · 2024-03-04T18:55:03Z

But I also constructed a basis of the PiTensorProduct, and for this proved that it distributes over DirectSums, and... I > an preparing the PRs now.

Here is the PR proving that PiTensorProducts distribute over DirectSums: #11155
The final part is the construction of PiTensorProduct.dualDistrib and the proof that finite PiTensorProducts of finite free modules commute with taking duals; this is in PR #11156, which depends on the two previous ones.

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

…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>

morel added 3 commits February 16, 2024 21:34

initial commit

68f51a3

update Mathlib.lean

c689f02

add documentation

7709eec

smorel394 added awaiting-review t-algebra Algebra (groups, rings, fields etc) labels Feb 17, 2024

smorel394 mentioned this pull request Feb 17, 2024

[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation #9718

Closed

eric-wieser self-assigned this Feb 17, 2024

YaelDillies reviewed Feb 18, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Feb 18, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean Outdated Show resolved Hide resolved

Update Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

84f4e44

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

eric-wieser reviewed Feb 18, 2024

View reviewed changes

Update Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

3c3d7f9

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

eric-wieser reviewed Feb 18, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean Outdated Show resolved Hide resolved

Ruben-VandeVelde reviewed Feb 18, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean Outdated Show resolved Hide resolved

Ruben-VandeVelde reviewed Feb 18, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean Outdated Show resolved Hide resolved

eric-wieser and others added 5 commits February 18, 2024 16:42

golf map

9a527a7

remove useless liftAlternating_aux

6d6d736

Update Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

c4d9fe0

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Update Mathlib/LinearAlgebra/ExteriorPower/Generators.lean

1939452

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

change ExteriorPower to exteriorPower

506232b

smorel394 mentioned this pull request Feb 20, 2024

[Merged by Bors] - refactor(LinearAlgebra/ExteriorAlgebra/{Basic,Grading}): add a definition and notation for the exterior powers of a module #10744

Closed

smorel394 added the blocked-by-other-PR This PR depends on another PR to Mathlib label Feb 26, 2024

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Feb 29, 2024

eric-wieser added 2 commits February 29, 2024 13:57

Merge remote-tracking branch 'origin/master' into SM.ExteriorPower

1543eea

fix notation

d94a919

eric-wieser reviewed Mar 1, 2024

View reviewed changes

smorel394 and others added 2 commits March 1, 2024 15:56

Update Mathlib/LinearAlgebra/TensorPower.lean

fdc24cf

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

add import

505df1e

linter stuff

de83305

bustercopley reviewed Mar 2, 2024

View reviewed changes

bustercopley added 2 commits March 3, 2024 17:53

Golf and tidy up

3d78df6

golf

97d6301

bustercopley added 4 commits March 5, 2024 11:35

Merge remote-tracking branch 'origin/master' into SM.ExteriorPower

ae33569

fix notation for alternating map (bigwedge)

2bb8027

fix for "simp no longer unfolds lets"

a341ad7

golf

1f343ea

github-actions bot reviewed Mar 6, 2024

View reviewed changes

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean Outdated Show resolved Hide resolved

Mathlib/LinearAlgebra/ExteriorPower/Generators.lean Outdated Show resolved Hide resolved

oops, wrong dot (reviewdog)

b17c1b9

smorel394 added the blocked-by-other-PR This PR depends on another PR to Mathlib label Mar 14, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR label May 27, 2024

YaelDillies removed the blocked-by-other-PR label May 28, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR label May 28, 2024

YaelDillies removed the blocked-by-other-PR label May 28, 2024

semorrison removed the awaiting-review label Jul 9, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties #10654

feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties #10654

smorel394 commented Feb 17, 2024 •

edited

Loading

eric-wieser Feb 18, 2024

smorel394 Feb 18, 2024 •

edited

Loading

eric-wieser Feb 18, 2024 •

edited

Loading

smorel394 Feb 18, 2024

smorel394 Feb 20, 2024

mattrobball commented Feb 18, 2024

leanprover-bot commented Feb 18, 2024

leanprover-community-mathlib4-bot commented Feb 29, 2024 •

edited

Loading

eric-wieser Mar 1, 2024

smorel394 Mar 1, 2024

eric-wieser Mar 1, 2024 •

edited

Loading

smorel394 Mar 1, 2024

smorel394 Mar 1, 2024

smorel394 Mar 1, 2024

eric-wieser Mar 1, 2024

eric-wieser Mar 1, 2024

smorel394 Mar 2, 2024 •

edited

Loading

bustercopley left a comment

bustercopley Mar 2, 2024

bustercopley Mar 2, 2024

bustercopley Mar 3, 2024

bustercopley Mar 2, 2024

bustercopley Mar 2, 2024

bustercopley Mar 2, 2024 •

edited

Loading

bustercopley Mar 2, 2024

bustercopley commented Mar 4, 2024 •

edited

Loading

smorel394 commented Mar 4, 2024

eric-wieser commented Mar 4, 2024 •

edited

Loading

smorel394 commented Mar 4, 2024

smorel394 commented Mar 4, 2024 •

edited

Loading

	noncomputable def linearFormOfFamily (f : (_ : Fin n) → (M →ₗ[R] R)) : (⨂[R]^n) M →ₗ[R] R :=
	noncomputable def linearFormOfFamily (f : (_ : Fin n) → Module.Dual R M) : Module.Dual R (⨂[R]^n M) :=

	noncomputable def BasisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :
	noncomputable def basisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :

	lemma BasisOfBasis_coe {I : Type*} [LinearOrder I] (b : Basis I R M) :
	lemma coe_basisOfBasis {I : Type*} [LinearOrder I] (b : Basis I R M) :

feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties #10654

Are you sure you want to change the base?

feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties #10654

Conversation

smorel394 commented Feb 17, 2024 • edited Loading

Main definitions

In LinearAlgebra/ExteriorPower/Basic.lean:

In LinearAlgebra/ExteriorPower/Generators.lean:

Main theorems

In LinearAlgebra/ExteriorPower/Basic.lean:

In LinearAlgebra/ExteriorPower/Generators.lean:

Choose a reason for hiding this comment

smorel394 Feb 18, 2024 • edited Loading

Choose a reason for hiding this comment

eric-wieser Feb 18, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattrobball commented Feb 18, 2024

leanprover-bot commented Feb 18, 2024

leanprover-community-mathlib4-bot commented Feb 29, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Mar 1, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smorel394 Mar 2, 2024 • edited Loading

Choose a reason for hiding this comment

bustercopley left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bustercopley Mar 2, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bustercopley commented Mar 4, 2024 • edited Loading

smorel394 commented Mar 4, 2024

eric-wieser commented Mar 4, 2024 • edited Loading

smorel394 commented Mar 4, 2024

smorel394 commented Mar 4, 2024 • edited Loading

smorel394 commented Feb 17, 2024 •

edited

Loading

In `LinearAlgebra/ExteriorPower/Basic.lean`:

In `LinearAlgebra/ExteriorPower/Generators.lean`:

In `LinearAlgebra/ExteriorPower/Basic.lean`:

In `LinearAlgebra/ExteriorPower/Generators.lean`:

smorel394 Feb 18, 2024 •

edited

Loading

eric-wieser Feb 18, 2024 •

edited

Loading

leanprover-community-mathlib4-bot commented Feb 29, 2024 •

edited

Loading

eric-wieser Mar 1, 2024 •

edited

Loading

smorel394 Mar 2, 2024 •

edited

Loading

bustercopley Mar 2, 2024 •

edited

Loading

bustercopley commented Mar 4, 2024 •

edited

Loading

eric-wieser commented Mar 4, 2024 •

edited

Loading

smorel394 commented Mar 4, 2024 •

edited

Loading