[Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves by joelriou · Pull Request #21047 · leanprover-community/mathlib4

joelriou · 2025-01-25T10:06:00Z

github-actions · 2025-01-25T10:06:56Z

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

Mathlib/CategoryTheory/Subpresheaf/Image.lean

erdOne · 2025-01-26T12:29:01Z

Thanks!
maintainer merge

github-actions · 2025-01-26T12:29:20Z

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

riccardobrasca · 2025-01-27T09:39:57Z

Thanks!

bors merge

…es (#21047)

mathlib-bors · 2025-01-27T10:03:57Z

Pull request successfully merged into master.

Build succeeded:

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

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. 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) ...

`imagePresheaf` was renamed `Subpresheaf.range` in #21047. This PR fixes the names of the lemmas referring to the old name.

…21090) Some new API is introduced for subcomplexes of the standard simplex: any `S : Finset (Fin (n + 1))` defines a subcomplex `face S` of `Δ[n]`, and this face is isomorphic to `Δ[m]` when `Fin (m + 1) ≃o S`. Then, boundaries and horns are redefined as subcomplexes of the standard simplex and it is shown that they are unions of certain codimension one faces of the standard simplex. - [x] depends on: #21543 - [x] depends on: #21540 - [x] depends on: #21542 - [x] depends on: #21303 - [x] depends on: #21047 - [x] depends on: #20840 - [x] depends on: #21096 Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

fixing the build

f39ad92

joelriou added the t-category-theory Category theory label Jan 25, 2025

removed blank line

1ab7d00

fixing the build

e96834b

erdOne reviewed Jan 25, 2025

View reviewed changes

Mathlib/CategoryTheory/Subpresheaf/Image.lean Show resolved Hide resolved

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 25, 2025

added preimage_comp and preimage_id

530dd84

joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 25, 2025

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 26, 2025

ghost 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

feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheav…

d17e5f6

…es (#21047)

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 bot closed this Jan 27, 2025

mathlib-bors bot deleted the subpresheaf-preimage branch January 27, 2025 10:04

joelriou mentioned this pull request Feb 7, 2025

[Merged by Bors] - chore(CategoryTheory/Sites): fix names #21540

Closed

mathlib-bors bot pushed a commit that referenced this pull request Feb 7, 2025

chore(CategoryTheory/Sites): fix names (#21540)

4429112

`imagePresheaf` was renamed `Subpresheaf.range` in #21047. This PR fixes the names of the lemmas referring to the old name.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

[Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves#21047
joelriou wants to merge 4 commits intomasterfrom
subpresheaf-preimage

joelriou commented Jan 25, 2025

Uh oh!

github-actions bot commented Jan 25, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

erdOne commented Jan 26, 2025

Uh oh!

github-actions bot commented Jan 26, 2025

Uh oh!

riccardobrasca commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

joelriou commented Jan 25, 2025

Uh oh!

github-actions bot commented Jan 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 530dd846e6

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

erdOne commented Jan 26, 2025

Uh oh!

github-actions bot commented Jan 26, 2025

Uh oh!

riccardobrasca commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented Jan 25, 2025 •

edited

Loading