Skip to content

feat(Homology): interaction of projective and injective dimension and SES#36643

Open
Thmoas-Guan wants to merge 17 commits intoleanprover-community:masterfrom
Thmoas-Guan:projective-and-injective-dimension-in-SES
Open

feat(Homology): interaction of projective and injective dimension and SES#36643
Thmoas-Guan wants to merge 17 commits intoleanprover-community:masterfrom
Thmoas-Guan:projective-and-injective-dimension-in-SES

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

@Thmoas-Guan Thmoas-Guan commented Mar 14, 2026

In this PR, we directly implemented the relation of projectiveDimension and injectiveDimension in SES.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 14, 2026

PR summary 4ec5d95aa6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Injective.injectiveDimension_le_zero
+ Projective.projectiveDimension_le_zero
+ add_one_le_iff'
+ add_one_le_natCast_iff
+ add_one_le_zero_iff
+ coe_eq_natCast
+ hasProjectiveDimension_X₁_succ_le_sup
+ hasinjectiveDimension_X₃_succ_le_sup
+ injectiveDimension_X₁_le_sup
+ injectiveDimension_X₂_le_sup
+ injectiveDimension_X₃_eq_succ_of_not_projective
+ lt_zero_iff_eq_bot
+ projectiveDimension_X₂_le_sup
+ projectiveDimension_X₃_eq_succ_of_not_projective
+ projectiveDimension_X₃_le_sup

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.


No changes to technical debt.

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).

@Thmoas-Guan Thmoas-Guan requested a review from joelriou March 16, 2026 07:03
@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 18, 2026
@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 2, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

This PR/issue depends on:

@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant