[Merged by Bors] - feat(Algebra/Module): characterizations of free modules in terms of their presentations by joelriou · Pull Request #18327 · leanprover-community/mathlib4

joelriou · 2024-10-28T10:46:50Z

In this PR, the API for the presentations of modules is slightly developed (uniqueness up to a linear equivalence of the module defined by generators and relations, constructor for the property IsPresentation), and this is used to show that a module is free iff it admits a presentation with generators and no relation.

depends on: [Merged by Bors] - feat(Algebra/Module): presentation of modules #18295

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…nto unbundled-module-presentation-more-api

github-actions · 2024-10-28T10:47:40Z

PR summary 3febfb1960

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Module.Presentation.Free`	962

Declarations diff

+ IsPresentationCore
+ Presentation.ofIsPresentation
+ Quotient.linearMap_ext
+ Solution.IsPresentation.free
+ congr_postcomp
+ congr_var
+ desc_var
+ down
+ free_iff_exists_presentation
+ fromQuotient_toQuotient
+ instance : AddCommGroup relations.Quotient := by
+ instance : Module A relations.Quotient := by
+ isPresentation
+ ofLinearEquiv
+ postcomp_comp
+ postcomp_desc
+ postcomp_id
+ postcomp_uniq
+ postcomp_uniq_symm
+ presentationFinsupp
+ solutionFinsupp
+ solutionFinsupp.isPresentationCore
+ solutionFinsupp_isPresentation
+ uniq
+ uniq_symm_var
+ uniq_var
- fromQuotient_mk

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.

…nto unbundled-module-presentation-more-api

mathlib4-dependent-issues-bot · 2024-10-28T14:02:45Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Algebra/Module): presentation of modules #18295~~
By Dependent Issues (🤖). Happy coding!

…ion-more-api

erdOne

I feel that if you have a constructor of Presentation R M accepting an indexed family var spanning M and indexed family relations spanning the kernel of solution, you can the Freefile more easily without developingIsPresentationCore. But if you have other plans on IsPresentationCore` then this current approach works too.

Mathlib/Algebra/Module/Presentation/Basic.lean

joelriou · 2024-10-28T18:54:06Z

I feel that if you have a constructor of Presentation R M accepting an indexed family var spanning M and indexed family relations spanning the kernel of solution, you can the Freefile more easily without developingIsPresentationCore. But if you have other plans on IsPresentationCore` then this current approach works too.

The case of free modules is a toy example for the IsPresentationCore API, for which I will have other applications (like the cokernel in #18332). At some point, I will also introduce the constructor you suggest so as to make the connection with Module.FinitePresentation.

erdOne

LGTM

Mathlib/Algebra/Module/Presentation/Free.lean

…ion-more-api

erdOne · 2024-10-29T22:33:52Z

Thanks
maintainer merge

github-actions · 2024-10-29T22:34:10Z

🚀 Pull request has been placed on the maintainer queue by erdOne.

jcommelin

Thanks 🎉

bors merge

…heir presentations (#18327) In this PR, the API for the presentations of modules is slightly developed (uniqueness up to a linear equivalence of the module defined by generators and relations, constructor for the property `IsPresentation`), and this is used to show that a module is free iff it admits a presentation with generators and no relation. - [x] depends on: #18295 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2024-10-30T05:53:59Z

Pull request successfully merged into master.

Build succeeded:

…heir presentations (#18327) In this PR, the API for the presentations of modules is slightly developed (uniqueness up to a linear equivalence of the module defined by generators and relations, constructor for the property `IsPresentation`), and this is used to show that a module is free iff it admits a presentation with generators and no relation. - [x] depends on: #18295 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou and others added 15 commits October 27, 2024 17:42

feat(Algebra/Module): presentation of modules

ebc8248

cleaning up

2da3406

mv

6cdfaa6

typos

c018772

add TODO

e8d691e

better docstring

6a0590a

added exactness

3e2ff82

Merge remote-tracking branch 'origin' into unbundled-module-presentation

dfbc8b8

Merge remote-tracking branch 'origin' into unbundled-module-presentation

c626b04

Update Mathlib/Algebra/Module/Presentation/Basic.lean

a9dac92

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

suggestions by erdOne

7a177a5

wip

eb6fc18

fix

2a00e70

Merge remote-tracking branch 'origin/unbundled-module-presentation' i…

ff59b86

…nto unbundled-module-presentation-more-api

characterizations of free modules

7ea3bf9

joelriou added the WIP Work in progress label Oct 28, 2024

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 28, 2024

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 28, 2024

joelriou mentioned this pull request Oct 28, 2024

[Merged by Bors] - feat(Algebra/Module): presentation of the cokernel of a linear map #18332

Closed

3 tasks

joelriou added 3 commits October 28, 2024 14:21

Merge remote-tracking branch 'origin' into unbundled-module-presentation

f26a964

fix

4c36db3

Merge remote-tracking branch 'origin/unbundled-module-presentation' i…

0bc03e6

…nto unbundled-module-presentation-more-api

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 28, 2024

joelriou added 4 commits October 28, 2024 15:23

Merge remote-tracking branch 'origin' into unbundled-module-presentat…

123bf6e

…ion-more-api

fixed Mathlib.lean

8446bc4

typo

4f53344

added docstring

444fd2d

joelriou removed the WIP Work in progress label Oct 28, 2024

erdOne reviewed Oct 28, 2024

View reviewed changes

Mathlib/Algebra/Module/Presentation/Basic.lean Show resolved Hide resolved

removed some Submodule.Quotient API leaks

5c18c5e

erdOne approved these changes Oct 29, 2024

View reviewed changes

Mathlib/Algebra/Module/Presentation/Free.lean Outdated Show resolved Hide resolved

joelriou added 2 commits October 29, 2024 23:19

Merge remote-tracking branch 'origin' into unbundled-module-presentat…

a8a6615

…ion-more-api

added explicit universe

3febfb1

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 29, 2024

jcommelin reviewed Oct 30, 2024

View reviewed changes

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

mathlib-bors bot changed the title ~~feat(Algebra/Module): characterizations of free modules in terms of their presentations~~ [Merged by Bors] - feat(Algebra/Module): characterizations of free modules in terms of their presentations Oct 30, 2024

mathlib-bors bot closed this Oct 30, 2024

mathlib-bors bot deleted the unbundled-module-presentation-more-api branch October 30, 2024 05:54

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Algebra/Module): characterizations of free modules in terms of their presentations#18327

[Merged by Bors] - feat(Algebra/Module): characterizations of free modules in terms of their presentations#18327
joelriou wants to merge 25 commits intomasterfrom
unbundled-module-presentation-more-api

joelriou commented Oct 28, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Oct 28, 2024 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Oct 28, 2024

Uh oh!

erdOne left a comment

Uh oh!

Uh oh!

joelriou commented Oct 28, 2024

Uh oh!

erdOne left a comment

Uh oh!

Uh oh!

erdOne commented Oct 29, 2024

Uh oh!

github-actions bot commented Oct 29, 2024

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Oct 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 3febfb1960

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Oct 28, 2024

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

joelriou commented Oct 28, 2024

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

erdOne commented Oct 29, 2024

Uh oh!

github-actions bot commented Oct 29, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Oct 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joelriou commented Oct 28, 2024 •

edited

Loading

github-actions bot commented Oct 28, 2024 •

edited

Loading