Commit 2023-05-11 05:53 799bb95b

View on Github →

feat: port CategoryTheory.Sites.Pushforward (#3899)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Pushforward.lean

added def CategoryTheory.Sites.pullbackPushforwardAdjunction

added def CategoryTheory.Sites.pushforward