Skip to content

[Merged by Bors] - feat(CategoryTheory): retracts of objects and morphisms#19233

Closed
mckoen wants to merge 9 commits intomasterfrom
mckoen/retract
Closed

[Merged by Bors] - feat(CategoryTheory): retracts of objects and morphisms#19233
mckoen wants to merge 9 commits intomasterfrom
mckoen/retract

Conversation

@mckoen
Copy link
Copy Markdown
Collaborator

@mckoen mckoen commented Nov 19, 2024

Defines retracts of objects and morphisms, and basic API. Used in #19135.


Open in Gitpod

@mckoen mckoen added WIP Work in progress t-category-theory Category theory labels Nov 19, 2024
@mckoen mckoen requested a review from joelriou November 19, 2024 00:10
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 19, 2024

PR summary b3e23b6de7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Retract (new file) 320
Mathlib.CategoryTheory.MorphismProperty.Retract (new file) 393

Declarations diff

+ IsStableUnderRetracts
+ IsStableUnderRetracts.epimorphisms
+ IsStableUnderRetracts.isomorphisms
+ IsStableUnderRetracts.monomorphisms
+ Retract
+ RetractArrow
+ i_w
+ instance : IsSplitEpi h.r := ⟨⟨h.splitEpi⟩⟩
+ instance : IsSplitEpi h.r.left := ⟨⟨h.left.splitEpi⟩⟩
+ instance : IsSplitEpi h.r.right := ⟨⟨h.right.splitEpi⟩⟩
+ instance : IsSplitMono h.i := ⟨⟨h.splitMono⟩⟩
+ instance : IsSplitMono h.i.left := ⟨⟨h.left.splitMono⟩⟩
+ instance : IsSplitMono h.i.right := ⟨⟨h.right.splitMono⟩⟩
+ left
+ map
+ of_retract
+ r_w
+ retract_left
+ retract_right
+ right
+ splitEpi
+ splitMono

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.


No changes to technical debt.

You can run this locally as

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

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 20, 2024
@mckoen mckoen removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 21, 2024
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 24, 2024
mckoen and others added 3 commits December 3, 2024 16:23
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mckoen mckoen removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 4, 2024
@joelriou joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 4, 2024
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@mckoen mckoen removed awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress labels Dec 5, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Dec 6, 2024

Thanks!
bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 6, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 6, 2024
Defines retracts of objects and morphisms, and basic API. Used in #19135.



Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 6, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): retracts of objects and morphisms [Merged by Bors] - feat(CategoryTheory): retracts of objects and morphisms Dec 6, 2024
@mathlib-bors mathlib-bors bot closed this Dec 6, 2024
@mathlib-bors mathlib-bors bot deleted the mckoen/retract branch December 6, 2024 07:10
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