Skip to content

[Merged by Bors] - feat(Algebra/Homology): the Ext class of a short exact sequence#14793

Closed
joelriou wants to merge 17 commits intomasterfrom
ext-class-of-short-exact
Closed

[Merged by Bors] - feat(Algebra/Homology): the Ext class of a short exact sequence#14793
joelriou wants to merge 17 commits intomasterfrom
ext-class-of-short-exact

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jul 16, 2024

In this PR, we construct the class in Ext S.X₃ S.X₁ 1 that is attached to a short exact short complex S in an abelian category.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jul 16, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 16, 2024 •
edited
Loading

PR summary b4eb866ec3

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Homology.DerivedCategory.Ext -1108
Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic 1108
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass 1115

Declarations diff

+ comp_assoc_of_second_deg_zero
+ comp_assoc_of_third_deg_zero
+ comp_extClass
+ extClass
+ extClass_comp
+ extClass_hom
+ hasSmallLocalizedHom_iff_source
+ hasSmallLocalizedHom_iff_target
+ hasSmallLocalizedShiftedHom_iff_source
+ hasSmallLocalizedShiftedHom_iff_target
+ instance : HasSmallLocalizedShiftedHom.{w} W ℤ (S').X₃ (S').X₁ := by
+ shift
+ singleFunctorsPostcompQIso_hom_hom
+ singleFunctorsPostcompQIso_inv_hom

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.

@joelriou joelriou mentioned this pull request Jul 16, 2024
Closed
3 tasks
erdOne
erdOne reviewed Jul 16, 2024
View reviewed changes
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 16, 2024
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 18, 2024
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 20, 2024

Perhaps the new material belongs in a new file? Happy to defer here.

@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@joelriou joelriou added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 22, 2024
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jul 22, 2024 •
edited
Loading

Perhaps the new material belongs in a new file? Happy to defer here.

Thanks for the suggestion. Ext now becomes Ext.Basic, and the definition of the class in Ext^1 is now in the file Ext.ExtClass.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 22, 2024
@joelriou joelriou mentioned this pull request Jul 24, 2024
Closed
3 tasks
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 24, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 24, 2024
@joelriou joelriou mentioned this pull request Jul 24, 2024
Closed
8 tasks
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 27, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 28, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 31, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 8, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 9, 2024
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 12, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2024
jcommelin
jcommelin reviewed Aug 23, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 23, 2024
@joelriou
feat(Algebra/Homology): the Ext class of a short exact sequence (#14793)
c378552 
In this PR, we construct the class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact short complex `S` in an abelian category.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): the Ext class of a short exact sequence [Merged by Bors] - feat(Algebra/Homology): the Ext class of a short exact sequence Aug 23, 2024
@mathlib-bors mathlib-bors bot closed this Aug 23, 2024
@mathlib-bors mathlib-bors bot deleted the ext-class-of-short-exact branch August 23, 2024 15:37
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@joelriou @bjoernkjoshanssen
feat(Algebra/Homology): the Ext class of a short exact sequence (#14793)
a0f1e50 
In this PR, we construct the class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact short complex `S` in an abelian category.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@joelriou @bjoernkjoshanssen
feat(Algebra/Homology): the Ext class of a short exact sequence (#14793)
11947e5 
In this PR, we construct the class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact short complex `S` in an abelian category.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@joelriou @bjoernkjoshanssen
feat(Algebra/Homology): the Ext class of a short exact sequence (#14793)
e6d74df 
In this PR, we construct the class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact short complex `S` in an abelian category.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @kim-em @jcommelin @erdOne