[Merged by Bors] - feat(Order): order isomorphisms from `Fin n` for small `n` by joelriou · Pull Request #21120 · leanprover-community/mathlib4

joelriou · 2025-01-27T09:49:11Z

We define order isomorphisms like Fin.orderIsoTriple from Fin 3 to the finset {a, b, c} when a < b and b < c.

depends on: [Merged by Bors] - feat(Order): Fin.orderHom_injective_iff #21119

github-actions · 2025-01-27T09:50:13Z

PR summary 93c6f50e03

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Fin.Finset` (new file)	397

Declarations diff

+ ofUnique
+ orderIsoPair
+ orderIsoPair_one
+ orderIsoPair_zero
+ orderIsoSingleton
+ orderIsoSingleton_apply
+ orderIsoTriple
+ orderIsoTriple_one
+ orderIsoTriple_two
+ orderIsoTriple_zero

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

…in-order-iso-finset

mathlib4-dependent-issues-bot · 2025-01-29T06:36:17Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Order): Fin.orderHom_injective_iff #21119~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Order/Fin/Finset.lean

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib/Order/Fin/Finset.lean

Ruben-VandeVelde

Thanks!

maintainer merge

github-actions · 2025-01-31T09:07:26Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

Vierkantor

What surprises me a bit is that we're doing this for Finsets and not Sets. I suppose we don't really have any machinery for constructing a finset, casting it to a set and then to a type, and asserting all of that is order isomorphic?

I have the feeling that the proofs are going to be annoying to generalize. If we stick with 1, 2, 3 it's going to be fine. But for 4 we'll end up copying and pasting most of the code. Wouldn't it be possible to break up the order iso into something like Fin.consOrderIso, saying that we can extend an order iso between Fin n and a (fin)set s to Fin (n + 1) and insert a s, if a is smaller than everything in s?

On the other hand, perhaps I'm already too late with these suggestions. The code here is perfectly fine for its goals at the moment. So if you want this in Mathlib quickly, then I'm okay with merging if you can write some TODO items on the two notes above.

Mathlib/Order/Fin/Finset.lean

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Mathlib/Order/Fin/Finset.lean

joelriou · 2025-01-31T11:34:39Z

I am using Finset because this is what naturally appears in the future applications of this (in simplicial homotopy theory, typically a, b and c are going to be elements in another Fin n) and there it is convenient to be able to use Finset.card.
I have added TODOs to be file.

Mathlib/Order/Fin/Finset.lean

Vierkantor

Thanks!

bors r+

We define order isomorphisms like `Fin.orderIsoTriple` from `Fin 3` to the finset `{a, b, c}` when `a < b` and `b < c`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

mathlib-bors · 2025-01-31T12:56:49Z

Pull request successfully merged into master.

Build succeeded:

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

We define order isomorphisms like `Fin.orderIsoTriple` from `Fin 3` to the finset `{a, b, c}` when `a < b` and `b < c`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

joelriou added 2 commits January 27, 2025 10:16

feat(Order/Fin): monotone maps from Fin

4b2f74c

wip

ed8de94

joelriou added the t-order Order theory label Jan 27, 2025

fixed Mathlib.lean

bee3cc0

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 27, 2025

joelriou added 4 commits January 27, 2025 15:31

Merge remote-tracking branch 'origin' into jriou-fin-monotone

d1e89f3

removed duplicates

e8df0af

better syntax

27cb75a

Merge remote-tracking branch 'origin/jriou-fin-monotone' into jriou-f…

951ea41

…in-order-iso-finset

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 29, 2025

Merge remote-tracking branch 'origin' into jriou-fin-order-iso-finset

c2e7397

joelriou added the WIP Work in progress label Jan 29, 2025

removed duplicate

8294d0a

joelriou removed the WIP Work in progress label Jan 29, 2025

Ruben-VandeVelde reviewed Jan 30, 2025

View reviewed changes

Mathlib/Order/Fin/Finset.lean Outdated Show resolved Hide resolved

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

joelriou and others added 2 commits January 30, 2025 16:53

Update Mathlib/Order/Fin/Finset.lean

eb7261a

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

better simp lemmas

9b7d8ff

joelriou commented Jan 30, 2025

View reviewed changes

Mathlib/Order/Fin/Finset.lean Show resolved Hide resolved

Update Mathlib/Order/Fin/Finset.lean

ce82e05

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

Ruben-VandeVelde approved these changes Jan 31, 2025

View reviewed changes

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

Vierkantor reviewed Jan 31, 2025

View reviewed changes

Mathlib/Order/Fin/Finset.lean Outdated Show resolved Hide resolved

Mathlib/Order/Fin/Finset.lean Outdated Show resolved Hide resolved

Mathlib/Order/Fin/Finset.lean Outdated Show resolved Hide resolved

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

joelriou and others added 2 commits January 31, 2025 12:14

Update Mathlib/Order/Fin/Finset.lean

84cafbe

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Update Mathlib/Order/Fin/Finset.lean

5227676

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Update Mathlib/Order/Fin/Finset.lean

723fcfe

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

joelriou commented Jan 31, 2025

View reviewed changes

Mathlib/Order/Fin/Finset.lean Show resolved Hide resolved

Update Mathlib/Order/Fin/Finset.lean

79311cf

joelriou commented Jan 31, 2025

View reviewed changes

Mathlib/Order/Fin/Finset.lean Show resolved Hide resolved

Update Mathlib/Order/Fin/Finset.lean

93c6f50

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

Vierkantor approved these changes Jan 31, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025

mathlib-bors bot changed the title ~~feat(Order): order isomorphisms from Fin n for small n~~ [Merged by Bors] - feat(Order): order isomorphisms from Fin n for small n Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the jriou-fin-order-iso-finset branch January 31, 2025 12:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Order): order isomorphisms from `Fin n` for small `n`#21120

[Merged by Bors] - feat(Order): order isomorphisms from `Fin n` for small `n`#21120
joelriou wants to merge 17 commits intomasterfrom
jriou-fin-order-iso-finset

joelriou commented Jan 27, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 27, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 29, 2025

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

Vierkantor left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Jan 31, 2025

Uh oh!

Uh oh!

Vierkantor left a comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

joelriou commented Jan 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 93c6f50e03

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 29, 2025

Uh oh!

Uh oh!

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Jan 31, 2025

Uh oh!

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joelriou commented Jan 27, 2025 •

edited

Loading

github-actions bot commented Jan 27, 2025 •

edited

Loading