Conversation
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
| `Λ[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 |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
Can do. Given that this expression already appears in LinearAlgebra/ExteriorAlgebra/Basic.lean, I guess it would make sense to introduce ExteriorPower there.
There was a problem hiding this comment.
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)
| `Λ[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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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>
|
!bench |
|
Here are the benchmark results for commit 3c3d7f9. |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
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>
…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>
…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>
…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>
PR summary 504113759aImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.LinearAlgebra.TensorPower | 888 | 1297 | +409 (+46.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.FreeProduct.Basic |
345 |
Mathlib.LinearAlgebra.TensorPower |
409 |
Mathlib.LinearAlgebra.ExteriorPower.Basic |
1341 |
Mathlib.LinearAlgebra.ExteriorPower.Generators |
1344 |
Declarations diff
+ _root_.Basis.exteriorPower
+ alternatingFormOfFamily
+ alternatingFormOfFamily_apply
+ basis_apply
+ basis_coord
+ coe_basis
+ finrank_eq
+ instFinite
+ instFree
+ instNonempty
+ lhom_ext
+ liftAlternating
+ liftAlternatingEquiv
+ liftAlternatingEquiv_apply
+ liftAlternatingEquiv_symm_apply
+ liftAlternating_apply_ιMulti
+ liftAlternating_comp
+ liftAlternating_comp_ιMulti
+ liftAlternating_ιMulti
+ linearFormOfBasis
+ linearFormOfBasis_apply_diag
+ linearFormOfBasis_apply_nondiag
+ linearFormOfBasis_apply_nondiag_aux
+ linearFormOfBasis_apply_ιMulti
+ linearFormOfFamily_apply
+ linearFormOfFamily_apply_tprod
+ linearFormOfFamily_apply_ιMulti
+ linearFormOfFamily_comp_map
+ linearFormOfFamily_comp_map_apply
+ linearIndependent_of_dualFamily
+ map
+ map_apply_ιMulti
+ map_comp_map
+ map_comp_ιMulti
+ map_id
+ map_injective
+ map_injective_field
+ map_surjective
+ map_ιMulti_family
+ mem_exteriorPower_is_mem_finite
+ span_of_span
+ span_top_of_span_top
+ span_top_of_span_top'
+ sum_range_map
+ toTensorPower
+ toTensorPower_apply_ιMulti
+ ιMulti
+ ιMulti_apply
+ ιMulti_family
+ ιMulti_family_coe
+ ιMulti_family_linearIndependent_field
+ ιMulti_family_linearIndependent_ofBasis
+ ιMulti_span
+ ιMulti_span_fixedDegree
++ linearFormOfFamily
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
|
In the branch https://github.com/leanprover-community/mathlib4/tree/SM.ExteriorPower_jriou I have merged this with master and the two new PRs #18590 and #18596. If there is no objection, I could merge |
…roduct of a family of vectors (#21397) This splits the definition of `ιMulti_family` from PR #10654 along with a few basic lemmas that do not rely on other parts of the PR. The `ιMulti_family` definition allows taking the product of a subset of a family of vectors, which is useful when the number of vectors is different from the degree of the exterior power. In particular, this is useful for working with a collection of basis or spanning vectors.
…roduct of a family of vectors (#21397) This splits the definition of `ιMulti_family` from PR #10654 along with a few basic lemmas that do not rely on other parts of the PR. The `ιMulti_family` definition allows taking the product of a subset of a family of vectors, which is useful when the number of vectors is different from the degree of the exterior power. In particular, this is useful for working with a collection of basis or spanning vectors.
|
Any updates on this? My team and I are looking to use |
|
Thanks to a series of PRs from @morrison-daniel ending with #32708 I believe we now have all of the material from this PR in master 🎉 |
This introduces the exterior powers of a module and proves some of their basic properties, in
LinearAlgebra/ExteriorPower/Basic.leanandLinearAlgebra/ExteriorPower/Generators.lean. It also adds a lemma inLinearAlgebra/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 inLinearAlgebra/TensorPower.lean(linearFormOfFamily: the linear form on the tensor power ofMobtained by multiplying a family of linear forms onM).Main definitions
In
LinearAlgebra/ExteriorPower/Basic.lean:ExteriorPower R n Mis thenth exterior power of aR-moduleM, defined asLinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n. We also introduce the notationΛ[R]^n MforExteriorPower R n M.ExteriorPower.ιMultiis the canonical alternating map onMwith values inΛ[R]^n M.ExteriorPower.map: functoriality of exterior powers with respect to linear maps between modules.ExteriorPower.toTensorPower: linear map from thenth exterior power to thenthtensor power (coming from
MultilinearMap.alternatizationvia the universal property ofexterior powers).
In
LinearAlgebra/ExteriorPower/Generators.lean:ExteriorPower.BasisOfBasis: Ifbis a basis ofM(indexed by a linearly ordered type),the basis of the
nth exterior power ofMformed by then-fold exterior products of elementsof
b.Main theorems
In
LinearAlgebra/ExteriorPower/Basic.lean:The image of
ExteriorPower.ιMultispansΛ[R]^n M.ExteriorPower.liftAlternatingEquiv(universal property of thenth exterior power ofM):the linear equivalence between linear maps from
Λ[R]^n Mto a moduleNandn-foldalternating maps from
MtoN.ExteriorPower.map_injective_field: Iff : M →ₗ[R] Nis injective andRis a field, thenExteriorPower.map n fis injective.ExteriorPower.map_surjective: Iff : M →ₗ[R] Nis surjective, thenExteriorPower.map n fis surjective.
ExteriorPower.mem_exteriorPower_is_mem_finite: Every element ofΛ[R]^n Mis in the image ofΛ[R]^n Pfor some finitely generated submodulePofM.In
LinearAlgebra/ExteriorPower/Generators.lean:ExteriorPower.Finite: Thenth exterior power of a finite module is a finite module.ExteriorPower.span_top_of_span_topandExteriorPower.span_top_of_span_top': If a family ofvectors spans
M, then the family of itsn-fold exterior products spansΛ[R]^n M. (We giveversions in the exterior algebra and in the exterior power.)
ExteriorPower.FreeOfFree: IfMis a free module, then so is itsnth exterior power.ExteriorPower.FinrankOfFiniteFree: IfRsatisfies the strong rank condition andMisfinite free of rank
r, then thenth exterior power ofMis of finrankNat.choose r n.ExteriorPower.ιMulti_family_linearIndependent_field: IfRis a field, and ifvis alinearly independent family of vectors (indexed by a linearly ordered type), then the family of
its
n-fold exterior products is also linearly independent.PiTensorProduct#11156