Skip to content

[Merged by Bors] - feat(Algebra/Homology): the canonical truncation truncGE#14734

Closed
joelriou wants to merge 7 commits intomasterfrom
embedding-truncge
Closed

[Merged by Bors] - feat(Algebra/Homology): the canonical truncation truncGE#14734
joelriou wants to merge 7 commits intomasterfrom
embedding-truncge

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jul 14, 2024 •
edited by kim-em
Loading

We construct the canonical truncation truncGE of homological complexes relative to an embedding e of complex shapes which satisfies e.IsTruncGE.

Open in Gitpod

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

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

PR summary dcb6209aad

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Homology.Embedding.TruncGE 927

Declarations diff

+ BoundaryGE.false_of_isTruncLE
+ BoundaryLE.false_of_isTruncGE
+ X
+ XIso
+ XIsoOpcycles
+ d
+ d_comp_d
+ truncGE
+ truncGE'
+ truncGE'XIso
+ truncGE'XIsoOpcycles
+ truncGE'_d_eq
+ truncGE'_d_eq_fromOpcycles
+ truncGEXIso
+ truncGEXIsoOpcycles
- BoundaryGE.false
- BoundaryLE.false

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>

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 14, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 17, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jul 17, 2024

This PR/issue depends on:

erdOne
erdOne reviewed Jul 20, 2024
View reviewed changes
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jul 26, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 26, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 26, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jul 26, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 26, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 26, 2024
@joelriou
feat(Algebra/Homology): the canonical truncation truncGE (#14734)
c387e3e 
We construct the canonical truncation `truncGE` of homological complexes relative to an embedding `e` of complex shapes which satisfies `e.IsTruncGE`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): the canonical truncation truncGE [Merged by Bors] - feat(Algebra/Homology): the canonical truncation truncGE Jul 26, 2024
@mathlib-bors mathlib-bors bot closed this Jul 26, 2024
@mathlib-bors mathlib-bors bot deleted the embedding-truncge branch July 26, 2024 08:36
@adomani adomani mentioned this pull request Aug 1, 2024
Open
@joelriou joelriou mentioned this pull request Nov 27, 2024
Closed
4 tasks
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2025
@joelriou
feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#…
1af2507 
…19550)

We dualize for `truncLE` the definitions and lemmas obtained for `truncGE` in PR  #14734, #19543 and #19544.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

3 participants

@joelriou @erdOne @riccardobrasca