Skip to content

[Merged by Bors] - feat(Algebra/Homology): boundaries of embeddings of complex shapes#14650

Closed
joelriou wants to merge 3 commits intomasterfrom
embedding-boundary
Closed

[Merged by Bors] - feat(Algebra/Homology): boundaries of embeddings of complex shapes#14650
joelriou wants to merge 3 commits intomasterfrom
embedding-boundary

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

In this PR, we define the lower/upper boundaries of embeddings of complex shapes. These notions shall be important when constructing canonical truncations of homological complexes.


Open in Gitpod

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

github-actions bot commented Jul 11, 2024

PR summary 5e3c3ab7ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Homology.Embedding.Boundary 672

Declarations diff

+ BoundaryGE
+ BoundaryGE.false
+ BoundaryGE.not_mem
+ BoundaryLE
+ BoundaryLE.false
+ BoundaryLE.not_mem
+ boundaryGE
+ boundaryGE_embeddingUpIntGE_iff
+ boundaryLE
+ boundaryLE_embeddingUpIntLE_iff
+ mem_next
+ mem_prev
+ next_eq_self
+ next_eq_self'
+ next_f_of_not_boundaryLE
+ not_boundaryGE_next
+ not_boundaryGE_next'
+ not_boundaryLE_prev
+ not_boundaryLE_prev'
+ prev_eq_self
+ prev_eq_self'
+ prev_f_of_not_boundaryGE

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

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 17, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 17, 2024
…14650)

In this PR, we define the lower/upper boundaries of embeddings of complex shapes. These notions shall be important when constructing canonical truncations of homological complexes.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Homology): boundaries of embeddings of complex shapes [Merged by Bors] - feat(Algebra/Homology): boundaries of embeddings of complex shapes Jul 17, 2024
@mathlib-bors mathlib-bors bot closed this Jul 17, 2024
@mathlib-bors mathlib-bors bot deleted the embedding-boundary branch July 17, 2024 21:58
@adomani adomani mentioned this pull request Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants