mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: morphisms of presheaves that are locally injective for a Grothendieck topology

Open joelriou opened this issue 1 year ago • 1 comments

This PR creates the file CategoryTheory.Sites.LocallyInjective which develops the basic API of locally injective morphisms of presheaves. The file CategoryTheory.Sites.Surjective is renamed CategoryTheory.Sites.LocallySurjective and shall be expanded in a future PR.

  • [x] depends on: #12332

Open in Gitpod

joelriou avatar Mar 27 '24 09:03 joelriou

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#12332~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 24 '24 09:05 leanprover-community-mathlib4-bot

Thanks! maintainer merge

erdOne avatar May 28 '24 17:05 erdOne

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

github-actions[bot] avatar May 28 '24 17:05 github-actions[bot]

Thanks!

bors merge

riccardobrasca avatar May 28 '24 19:05 riccardobrasca

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 28 '24 19:05 mathlib-bors[bot]