[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power by joelriou · Pull Request #18590 · leanprover-community/mathlib4

joelriou · 2024-11-03T22:30:56Z

We obtain the universal property of the nth exterior power of a module M: linear maps from this exterior power identify to n-alternating maps from M. This is also phrased as the data of a presentation of the exterior power by generators and relations.

Co-authored-by: sophie.morel@ens-lyon.fr

This is partly extracted from #10654, with some modifications. Mostly, what was named liftAlternatingEquiv is alternatingMapLinearEquiv here.

github-actions · 2024-11-03T22:31:45Z

PR summary 604d5be7a8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.ExteriorPower.Basic` (new file)	1414

Declarations diff

+ Rels
+ alternatingMapLinearEquiv
+ alternatingMapLinearEquiv_apply_ιMulti
+ alternatingMapLinearEquiv_comp
+ alternatingMapLinearEquiv_comp_ιMulti
+ alternatingMapLinearEquiv_symm_apply
+ alternatingMapLinearEquiv_ιMulti
+ isPresentationCore
+ linearMap_eq_iff_of_eq_span
+ linearMap_eq_iff_of_span_eq_top
+ linearMap_eq_zero_iff_of_eq_span
+ linearMap_eq_zero_iff_of_span_eq_top
+ linearMap_ext
+ presentation
+ relations
+ relationsSolutionEquiv
+ ιMulti
+ ιMulti_apply_coe
+ ιMulti_span
+ ιMulti_span_fixedDegree

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.

Increase in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
1525	3	erw

Current commit 604d5be7a8
Reference commit 2f1fb1baba

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…wer-basic

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

jcommelin

Apart from the stylistic issue pointed out by Eric, I think this all looks very reasonable. But I would be happy to hear more thoughts from Eric.

…wer-basic

jcommelin

bors d+

Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

mathlib-bors · 2024-12-03T15:06:59Z

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2024-12-03T19:20:33Z

Mathlib/LinearAlgebra/Span/Basic.lean

+
+variable {N : Type*} [AddCommMonoid N] [Module R N]
+
+lemma linearMap_eq_iff_of_eq_span {V : Submodule R M} (f g : V →ₗ[R] N)


Should this be called LinearMap.submodule_ext_iff_of_eq_span or something?

I do not think so.

Should this be called LinearMap.submodule_ext_iff_of_eq_span or something?

I like this name too. It enables dot notation, and by covnention the iff version of extensionality lemmas are usually called ext_iff, e.g. MvPolynomial.funext_iff, DFunLike.ext_iff.

Co-authored-by: Johan Commelin <johan@commelin.net>

joelriou · 2024-12-04T19:42:47Z

Thanks!

bors merge

…rior power (#18590) We obtain the universal property of the `n`th exterior power of a module `M`: linear maps from this exterior power identify to `n`-alternating maps from `M`. This is also phrased as the data of a presentation of the exterior power by generators and relations. Co-authored-by: sophie.morel@ens-lyon.fr Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2024-12-04T20:12:42Z

Pull request successfully merged into master.

Build succeeded:

wip

25f1ac2

joelriou added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Nov 3, 2024

joelriou mentioned this pull request Nov 3, 2024

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

Closed

3 tasks

joelriou added 2 commits November 3, 2024 23:37

fixed imports

a59d0fd

moved code about submodules

3ae2e5f

joelriou removed the WIP Work in progress label Nov 3, 2024

This was referenced Nov 4, 2024

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the exterior powers, as functors #18596

Closed

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the zeroth and first exterior powers #18624

Closed

Merge remote-tracking branch 'origin' into linear-algebra-exterior-po…

0613837

…wer-basic

This was referenced Nov 5, 2024

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the pairing between the exterior power of the dual and the exterior power #18651

Closed

feat(LinearAlgebra/ExteriorPower): generators of the exterior powers #18662

Open

joelriou added 3 commits November 6, 2024 16:50

Merge remote-tracking branch 'origin' into linear-algebra-exterior-po…

4efffb7

…wer-basic

fixing the build

4358b2e

Merge remote-tracking branch 'origin' into linear-algebra-exterior-po…

50acb61

…wer-basic

This was referenced Nov 7, 2024

feat(Algebra/Module): presentation of the exterior power #18735

Open

feat(LinearAlgebra/ExteriorPower): exterior powers of free modules are free #18771

Open

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 15, 2024

Merge remote-tracking branch 'origin' into linear-algebra-exterior-po…

513350f

…wer-basic

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 15, 2024

jcommelin assigned eric-wieser Nov 28, 2024

jcommelin requested a review from eric-wieser November 28, 2024 15:03

jcommelin assigned jcommelin and unassigned eric-wieser Nov 28, 2024

eric-wieser reviewed Nov 28, 2024

View reviewed changes

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

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 29, 2024

jcommelin reviewed Nov 30, 2024

View reviewed changes

joelriou added 2 commits December 3, 2024 14:56

Merge remote-tracking branch 'origin' into linear-algebra-exterior-po…

4c8b7fa

…wer-basic

fixed parentheses

c49bf81

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 3, 2024

jcommelin reviewed Dec 3, 2024

View reviewed changes

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

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 3, 2024

eric-wieser reviewed Dec 3, 2024

View reviewed changes

Update Mathlib/LinearAlgebra/ExteriorPower/Basic.lean

604d5be

Co-authored-by: Johan Commelin <johan@commelin.net>

ghost added the ready-to-merge This PR has been sent to bors. label Dec 4, 2024

mathlib-bors bot changed the title ~~feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power~~ [Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power Dec 4, 2024

mathlib-bors bot closed this Dec 4, 2024

mathlib-bors bot deleted the linear-algebra-exterior-power-basic branch December 4, 2024 20:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power#18590

[Merged by Bors] - feat(LinearAlgebra/ExteriorPower): the universal property of the exterior power#18590
joelriou wants to merge 11 commits intomasterfrom
linear-algebra-exterior-power-basic

joelriou commented Nov 3, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 3, 2024 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

jcommelin left a comment

Uh oh!

jcommelin left a comment

Uh oh!

Uh oh!

mathlib-bors bot commented Dec 3, 2024

Uh oh!

eric-wieser Dec 3, 2024 •

edited

Loading

Uh oh!

joelriou Dec 4, 2024

Uh oh!

alreadydone Dec 5, 2024 •

edited

Loading

Uh oh!

joelriou commented Dec 4, 2024

Uh oh!

mathlib-bors bot commented Dec 4, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants


		variable {N : Type*} [AddCommMonoid N] [Module R N]

		lemma linearMap_eq_iff_of_eq_span {V : Submodule R M} (f g : V →ₗ[R] N)

Conversation

joelriou commented Nov 3, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 3, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 604d5be7a8

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Dec 3, 2024

Uh oh!

eric-wieser Dec 3, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joelriou Dec 4, 2024

Choose a reason for hiding this comment

Uh oh!

alreadydone Dec 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joelriou commented Dec 4, 2024

Uh oh!

mathlib-bors bot commented Dec 4, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

joelriou commented Nov 3, 2024 •

edited

Loading

github-actions bot commented Nov 3, 2024 •

edited

Loading

eric-wieser Dec 3, 2024 •

edited

Loading

alreadydone Dec 5, 2024 •

edited

Loading