Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves #21047

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves #21047

wants to merge 4 commits into from

Conversation

joelriou
Copy link
Collaborator

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jan 25, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 25, 2025 •
edited
Loading

PR summary 530dd846e6

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Sheaf.image
+ Sheaf.imageι
+ Sheaf.toImage
+ Sheaf.toImage_ι
+ Subpresheaf.le_def
+ Subpresheaf.toRangeSheafify
+ epi_iff_range_eq_top
+ fromPreimage
+ fromPreimage_ι
+ image
+ image_comp
+ image_le_iff
+ image_top
+ instance : Epi (toRange p) := by simp [epi_iff_range_eq_top]
+ instance [Mono p] : IsIso (toRange p) := by
+ instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (Sheaf.toImage f) := by
+ instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (Sheaf.imageι f)
+ lift
+ lift_ι
+ preimage
+ preimage_comp
+ preimage_eq_top_iff
+ preimage_id
+ preimage_image_of_epi
+ range
+ range_comp
+ range_comp_le
+ range_id
+ range_toRange
+ range_ι
+ toRange
+ toRange_app_val
+ toRange_ι
- Subpresheaf.lift
- Subpresheaf.lift_ι
- instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (toImageSheaf f) := by
- instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (imageSheafι f)
- isIso_toImagePresheaf

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

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 25, 2025
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 25, 2025
@erdOne
Copy link
Member

erdOne commented Jan 26, 2025

Thanks!
maintainer merge

@github-actions GitHub Actions
Copy link

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

This was referenced Jan 26, 2025
Open
Open
Open
@riccardobrasca
Copy link
Member

Thanks!

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 27, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 27, 2025
@joelriou
feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheav…
d17e5f6 
…es (#21047)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 27, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves [Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves Jan 27, 2025
@mathlib-bors mathlib-bors bot closed this Jan 27, 2025
@mathlib-bors mathlib-bors bot deleted the subpresheaf-preimage branch January 27, 2025 10:04
Julian added a commit that referenced this pull request Jan 28, 2025
@Julian
Merge remote-tracking branch 'origin/master' into polynomial-sequences
c572510 
* origin/master: (294 commits)
  feat: equalizers and coequalizers in the category of ind-objects (#21139)
  doc: turn more links to Stacks into `@[stacks]` tags (#21135)
  feat(Asymptotics): prove `IsLittleOTVS.add` (#20578)
  feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062)
  chore: import Std in Mathlib.lean (#21126)
  feat(Data/Matroid/Circuit): fundamental circuits and extensionality  (#21145)
  feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140)
  feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109)
  feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042)
  doc: fixed notation error in customizing category composition (#21132)
  feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143)
  chore(SupIndep): speedup the `Decidable` instance (#21114)
  fix(CI): use `Elab.async=false` for late importers workflow (#21147)
  feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687)
  feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921)
  feat(Algebra): `Pi.single_induction` (#21141)
  chore(BigOperators/Fin): golf a proof (#21131)
  feat: generalize tangent cone lemmas to TVS (#20859)
  feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136)
  refactor: unapply matrix lemmas (#21091)
  chore(Algebra/Category): `erw` -> `rw` (#21130)
  feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128)
  feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125)
  feat: PSum of finite sorts is finite (#20285)
  feat: inequality on the integral of a convex function of a RN derivative (#21093)
  feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058)
  chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317)
  feat: a `RelHom` preserves directedness (#20080)
  feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677)
  chore(Data/Matrix/PEquiv): clean up names (#21108)
  feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815)
  feat: define Descriptive.Tree (#18763)
  chore(Data/Complex/Exponential): split trig functions to new file (#21075)
  feat(Logic/IsEmpty/Relator): empty on sides (#20319)
  feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121)
  feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661)
  feat(RingTheory/LaurentSeries): add algebraEquiv (#21004)
  chore(SetTheory/Game/Impartial): golf two proofs (#21074)
  feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)
  feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023)
  feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994)
  feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970)
  feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084)
  feat: separating set in the category of ind-objects (#21082)
  feat: derivWithin lemmas (#21092)
  chore(Fintype): golf a proof (#21113)
  chore: golf using `funext₂` (#21106)
  chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067)
  doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101)
  doc(ComputeDegree): typos (#21095)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@erdOne erdOne erdOne left review comments

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@joelriou @erdOne @riccardobrasca @leanprover-community-mathlib4-bot