Skip to content

[Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): epi and mono in the category of presheaves of modules#18159

Closed
joelriou wants to merge 2 commits intomasterfrom
presheaf-of-modules-epimono
Closed

[Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): epi and mono in the category of presheaves of modules#18159
joelriou wants to merge 2 commits intomasterfrom
presheaf-of-modules-epimono

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 24, 2024

In the category of presheaves of modules, epi and mono can be characterized in terms of surjective/injective maps.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Oct 24, 2024
@joelriou joelriou mentioned this pull request Oct 24, 2024
Closed
5 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 24, 2024 •
edited
Loading

PR summary 57bb57eb99

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono 1211

Declarations diff

+ epi_iff_surjective
+ epi_of_surjective
+ injective_of_mono
+ instance [Epi f] (X : Cᵒᵖ) : Epi (f.app X)
+ instance [Mono f] (X : Cᵒᵖ) : Mono (f.app X)
+ mono_iff_surjective
+ mono_of_injective
+ surjective_of_epi

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.

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 24, 2024
@joelriou joelriou mentioned this pull request Oct 24, 2024
Closed
1 task
TwoFX
TwoFX approved these changes Oct 24, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@TwoFX TwoFX 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 r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 24, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 24, 2024
@joelriou
feat(Algebra/Category/ModuleCat/Presheaf): epi and mono in the catego…
0a0178f 
…ry of presheaves of modules (#18159)

In the category of presheaves of modules, epi and mono can be characterized in terms of surjective/injective maps.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Category/ModuleCat/Presheaf): epi and mono in the category of presheaves of modules [Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): epi and mono in the category of presheaves of modules Oct 24, 2024
@mathlib-bors mathlib-bors bot closed this Oct 24, 2024
@mathlib-bors mathlib-bors bot deleted the presheaf-of-modules-epimono branch October 24, 2024 10:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@joelriou @TwoFX