Skip to content

[Merged by Bors] - feat(CategoryTheory): creation of finite limits#21320

Closed
TwoFX wants to merge 4 commits intomasterfrom
fme-202-split
Closed

[Merged by Bors] - feat(CategoryTheory): creation of finite limits#21320
TwoFX wants to merge 4 commits intomasterfrom
fme-202-split

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Feb 1, 2025

Open in Gitpod

@github-actions github-actions bot added the t-category-theory Category theory label Feb 1, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 1, 2025 •
edited
Loading

PR summary a438bf014c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite (new file) 529

Declarations diff

+ CreatesColimitsOfSize.createsFiniteColimits
+ CreatesFiniteColimits
+ CreatesFiniteCoproducts
+ CreatesFiniteLimits
+ CreatesFiniteProducts
+ CreatesLimitsOfSize.createsFiniteLimits
+ compCreatesFiniteColimits
+ compCreatesFiniteCoproducts
+ compCreatesFiniteLimits
+ compCreatesFiniteProducts
+ createsColimitsOfShapeOfEquiv
+ createsFiniteColimitsOfCreatesFiniteColimitsOfSize
+ createsFiniteColimitsOfNatIso
+ createsFiniteCoproductsOfNatIso
+ createsFiniteLimitsOfCreatesFiniteLimitsOfSize
+ createsFiniteLimitsOfNatIso
+ createsFiniteProductsOfNatIso
+ createsLimitsOfShapeOfEquiv
+ instance (F : C ⥤ D) [CreatesFiniteColimits F] : CreatesFiniteCoproducts F
+ instance (F : C ⥤ D) [CreatesFiniteLimits F] : CreatesFiniteProducts F
+ instance (priority := 100) CreatesColimits.createsFiniteColimits (F : C ⥤ D)
+ instance (priority := 100) CreatesLimits.createsFiniteLimits (F : C ⥤ D)
+ instance (priority := 100) createsColimitsOfShapeOfCreatesFiniteColimits (F : C ⥤ D)
+ instance (priority := 100) createsColimitsOfShapeOfCreatesFiniteProducts (F : C ⥤ D)
+ instance (priority := 100) createsLimitsOfShapeOfCreatesFiniteLimits (F : C ⥤ D)
+ instance (priority := 100) createsLimitsOfShapeOfCreatesFiniteProducts (F : C ⥤ D)
+ instance (priority := 120) CreatesColimitsOfSize0.createsFiniteColimits (F : C ⥤ D)
+ instance (priority := 120) CreatesLimitsOfSize0.createsFiniteLimits (F : C ⥤ D)

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

@TwoFX TwoFX mentioned this pull request Feb 1, 2025
Closed
1 task
joelriou
joelriou reviewed Feb 1, 2025
View reviewed changes
joelriou
joelriou reviewed Feb 1, 2025
View reviewed changes
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Feb 1, 2025

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 1, 2025

✌️ TwoFX can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@joelriou joelriou changed the title feat: creation of finite limits feat(CategoryTheory): creation of finite limits Feb 1, 2025
@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 1, 2025
TwoFX and others added 2 commits February 1, 2025 22:22
@TwoFX @joelriou
Update Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
f516c31 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@TwoFX @joelriou
Update Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean
a438bf0 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@TwoFX
Copy link
Copy Markdown
Member Author

TwoFX commented Feb 1, 2025

Thanks for the review!
bors r+

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 1, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2025
@TwoFX
feat(CategoryTheory): creation of finite limits (#21320)
388ed47 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 1, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): creation of finite limits [Merged by Bors] - feat(CategoryTheory): creation of finite limits Feb 1, 2025
@mathlib-bors mathlib-bors bot closed this Feb 1, 2025
@mathlib-bors mathlib-bors bot deleted the fme-202-split branch February 1, 2025 21:53
Julian added a commit that referenced this pull request Feb 2, 2025
@Julian
Merge branch 'factorial-dvd-int' into bhargava-factorial
4aa075f 
* factorial-dvd-int: (143 commits)
  Apply suggestions from code review
  feat(Factorial): k! divides the product of any k successive integers
  feat(CategoryTheory): creation of finite limits (#21320)
  chore: update Mathlib dependencies 2025-02-01 (#21328)
  chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314)
  feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306)
  chore: cleanup imports in Archive/IfNormalization (#21318)
  doc: fix several typos (#21315)
  feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310)
  chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271)
  feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084)
  chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308)
  feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522)
  feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168)
  chore: update Mathlib dependencies 2025-02-01 (#21312)
  chore: update Mathlib dependencies 2025-01-31 (#21311)
  feat: generalize `mem_dite` to `Membership α β` (#21262)
  feat: Lemmas for some monomial orders (#16177)
  feat(CategoryTheory): the localized category is monoidal (#12728)
  feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289)
  feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295)
  feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284)
  fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299)
  feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199)
  refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653)
  feat(RingTheory/PowerSeries): binomial series (#20192)
  chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff  (#21290)
  chore (RingTheory/HahnSeries): fix names that use coeff (#21279)
  feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233)
  chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273)
  feat(CategoryTheory): the monoidal category structure on a localization (#20951)
  feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009)
  feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)
  feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486)
  feat: Function.const as a PartialEquiv (#21137)
  chore(NonZeroDivisors): don't import rings (#20871)
  feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267)
  feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190)
  feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285)
  perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179)
  feat(Order): order isomorphisms from `Fin n` for small `n` (#21120)
  refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740)
  feat: Sylow's first theorem for elementary `p`-groups (#21072)
  chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748)
  refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)
  feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186)
  feat(Algebra/Group/Action): add definition of equidecomposition (#16936)
  feat(CategoryTheory/Subpresheaf): equalizer (#21096)
  feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204)
  chore: update Mathlib dependencies 2025-01-31 (#21282)
  ...
jt496 pushed a commit that referenced this pull request Feb 3, 2025
@TwoFX @jt496
feat(CategoryTheory): creation of finite limits (#21320)
9e58b67 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

2 participants

@TwoFX @joelriou