Skip to content

feat(Algebra): category version Baer criterion#32058

Open
Thmoas-Guan wants to merge 75 commits intoleanprover-community:masterfrom
Thmoas-Guan:category-version-Baer-criterion
Open

feat(Algebra): category version Baer criterion#32058
Thmoas-Guan wants to merge 75 commits intoleanprover-community:masterfrom
Thmoas-Guan:category-version-Baer-criterion

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

@Thmoas-Guan Thmoas-Guan commented Nov 24, 2025 •
edited
Loading

In this PR, we added the cateory version of Baer criterion stating that M is injective iff Ext^1(R/I, M) vanish for all ideal I.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 24, 2025 •
edited
Loading

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Category.ModuleCat.Baer (new file) 1918

Declarations diff

+ LinearEquiv.conj_symm_exact_iff_exact
+ _root_.LinearEquiv.postcomp_exact_iff_exact
+ _root_.LinearEquiv.precomp_exact_iff_exact
+ ext_quotient_one_subsingleton_iff
+ ext_subsingleton_of_quotients
+ ext_subsingleton_of_quotients'
+ injective_of_subsingleton_ext_quotient_one

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type
6902 1 backward.isDefEq.respectTransparency

Current commit 358b3b2922
Reference commit 6ef8cc2731

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Nov 24, 2025
@Thmoas-Guan Thmoas-Guan mentioned this pull request Nov 25, 2025
Open
3 tasks
@joelriou joelriou added the t-category-theory Category theory label Dec 1, 2025
joelriou
joelriou reviewed Dec 1, 2025
View reviewed changes
joelriou
joelriou reviewed Dec 1, 2025
View reviewed changes
Mathlib/Algebra/Category/ModuleCat/Baer.lean
Comment on lines +41 to +43
lemma injective_of_subsingleton_ext_quotient_one [Small.{v} R] (M : ModuleCat.{v} R)
(h : ∀ (I : Ideal R), Subsingleton (Ext.{w} (ModuleCat.of R (Shrink.{v, u} (R ⧸ I))) M 1)) :
Injective M := by
Copy link
Copy Markdown
Contributor

@joelriou joelriou Dec 1, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be nice to make a separate iff lemma giving the concrete condition under which Subsingleton (Ext (ModuleCat.of R (Shrink.{v, u} (R ⧸ I))) M 1)) hold for a single ideal I.
Also, with my suggestion to only use the universe v for Ext, it becomes possible to state that there is an exact sequence M -> Hom(I, M) -> Ext^1(R/I, M) -> 0 in ModuleCat.{v} R.

@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 1, 2025
@mathlib4-dependent-issues-bot 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 Dec 5, 2025
@dagurtomas dagurtomas mentioned this pull request Mar 5, 2026
Closed
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 6, 2026
@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Mar 12, 2026

Please extract everything from the long proof that could be general API, as we've discussed on this PR and #35882

@dagurtomas dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 12, 2026
@Thmoas-Guan
Copy link
Copy Markdown
Collaborator Author

Thmoas-Guan commented Mar 13, 2026

I am already planning some systematic addition on APIs about Function.Exact and usage in long exact sequence of Ext, but it may take some time.

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator Author

Thmoas-Guan commented Mar 22, 2026

@dagurtomas what do you think of the current proof? (Or maybe we should work with the new APIs first?)
The problem left is that the equivalence between surjectivity of shrunk modules and the original one isn't that straight forward in any sense, I didn't find a bigger framework to fit it in. The current one working on element is the best I can have now.

@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 22, 2026
@Thmoas-Guan Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 22, 2026
@Thmoas-Guan Thmoas-Guan requested a review from dagurtomas March 24, 2026 03:09
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 4, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Apr 4, 2026

This PR/issue depends on:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

@dagurtomas dagurtomas Awaiting requested review from dagurtomas

Assignees

@dagurtomas dagurtomas

Labels

t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@Thmoas-Guan @mathlib4-merge-conflict-bot @dagurtomas @joelriou @mathlib4-dependent-issues-bot