feat: linear order is isomorphic to lexicographic sum of two intervals #20409

vihdzp · 2025-01-03T02:07:49Z

The material in this PR was previously in #18893.

github-actions · 2025-01-03T02:08:41Z

PR summary 962da91995

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Hom.Lex` (new file)	349

Declarations diff

+ sumCongr
+ sumCongr_symm
+ sumLexComplLeft
+ sumLexComplLeft_apply
+ sumLexComplLeft_symm_apply
+ sumLexComplRight
+ sumLexComplRight_apply
+ sumLexComplRight_symm_apply
+ sumLexCongr
+ sumLexCongr_symm
+ sumLexIicIoi
+ sumLexIicIoi_apply_inl
+ sumLexIicIoi_apply_inr
+ sumLexIicIoi_symm_apply_Iic
+ sumLexIicIoi_symm_apply_Ioi
+ sumLexIicIoi_symm_apply_of_le
+ sumLexIicIoi_symm_apply_of_lt
+ sumLexIioIci
+ sumLexIioIci_apply_inl
+ sumLexIioIci_apply_inr
+ sumLexIioIci_symm_apply_Ici
+ sumLexIioIci_symm_apply_Iio
+ sumLexIioIci_symm_apply_of_le
+ sumLexIioIci_symm_apply_of_lt

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/Order/RelIso/Set.lean

YaelDillies

Can we have the specialisation to preorders?

Mathlib/Order/RelIso/Set.lean

vihdzp · 2025-01-04T09:40:27Z

Can we have the specialisation to preorders?

This adds a bunch of imports and makes the PR twice as big. But I think they're an useful addition, so I've done a few changes to accomodate it: mainly, I've moved all of this to its own file.

Mathlib/Data/Sum/Order.lean

eric-wieser · 2025-01-04T22:25:14Z

Mathlib/Data/Sum/Order.lean

+  map_rel_iff' := by simp_rw [Lex.forall]; rintro (a | a) (b | b) <;> simp
+
+@[simp]
+theorem sumLexCongr_symm {α₁ α₂ β₁ β₂ : Type*} [LE α₁] [LE α₂] [LE β₁] [LE β₂]


It would be nice to have the trans and refl versions of this too.

eric-wieser · 2025-01-04T22:26:11Z

Mathlib/Order/Hom/Lex.lean

+variable (r x) in
+/-- A relation is isomorphic to the lexicographic sum of elements less than `x` and elements not
+less than `x`. -/
+-- The explicit type signature stops `simp` from complaining.


Where does this complaining happen? If you're able to make a mwe, can you file an issue with it?

This complaining is addressed in #20479, I can make this a dependent PR so that this doesn't come up

Do you mean #20475?

Mathlib/Order/Hom/Lex.lean

eric-wieser · 2025-01-05T12:06:58Z

Mathlib/Order/Hom/Lex.lean

+greater or equal to `x`. -/
+def sumLexIioIci : Iio x ⊕ₗ Ici x ≃o α :=
+  (sumLexCongr (refl _) (setCongr (Ici x) {y | ¬ y < x} (by ext; simp))).trans <|
+    ofRelIsoLT (RelIso.sumLexComplLeft (· < ·) x)


I think you should be composing with ofLex here somehow. Do we have ofLex as a RelIso for Sum?

There's some pretty subtle def-eq finagling going on here: the reason ofRelIsoLT works is because Sum.Lex (· < ·) (· < ·) (Iio x) (Ici x) is def-eq to the < relation on Iio x ⊕ₗ Ici x. I'm not sure this can be made less abusive by just inserting ofLex.

In any case things should probably be fine as long as we keep the actual API free of def-eq abuse.

I think we should introduce a Sum.toLexRelIso : Sum.Lex (. < .) (. < .) ≃r (fun a b : Lex (Sum _ _) => a < b) or whatever the true version is, with simp lemmas reducing to toLex, and cast through that here

eric-wieser · 2025-01-05T12:07:22Z

Mathlib/Order/Hom/Lex.lean

+theorem sumLexIioIci_apply_inl (a : Iio x) : sumLexIioIci x (Sum.inl a) = a :=
+  rfl
+
+@[simp]
+theorem sumLexIioIci_apply_inr (a : Ici x) : sumLexIioIci x (Sum.inr a) = a :=
+  rfl


Suggested change

theorem sumLexIioIci_apply_inl (a : Iio x) : sumLexIioIci x (Sum.inl a) = a :=

rfl

@[simp]

theorem sumLexIioIci_apply_inr (a : Ici x) : sumLexIioIci x (Sum.inr a) = a :=

rfl

theorem sumLexIioIci_apply_inl (a : Iio x) : sumLexIioIci x (ofLex <| Sum.inl a) = a :=

rfl

@[simp]

theorem sumLexIioIci_apply_inr (a : Ici x) : sumLexIioIci x (ofLex <| Sum.inr a) = a :=

rfl

It'd be better for simp to instead put toLex on the RHS.

That suggestion doesn't make any sense to me, the type of this bundled map is Lex (Sum (Iio x) (Ici x)) ≃o α, so when applying the map to a Sum you have to call toLex first.

(I realize I made a type above too...)

Oh nevermind, I see why what I was saying is nonsense. And in fact I'm missing some other ofLex elsewhere.

Update Set.lean

04a003f

vihdzp added the t-order Order theory label Jan 3, 2025

vihdzp requested a review from YaelDillies January 3, 2025 02:07

vihdzp mentioned this pull request Jan 3, 2025

feat(Order/InitialSeg): InitialSeg.exists_relIso_sum #18893

Open

2 tasks

eric-wieser reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/RelIso/Set.lean Outdated Show resolved Hide resolved

subrel strikes again

72ab07d

YaelDillies reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/RelIso/Set.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 3, 2025

tweaks

fc82690

YaelDillies reviewed Jan 4, 2025

View reviewed changes

Mathlib/Data/Sum/Order.lean Outdated Show resolved Hide resolved

vihdzp added 3 commits January 4, 2025 03:45

Update Lex.lean

7927732

Update Order.lean

b141ca9

Update Mathlib.lean

07e8f1c

vihdzp removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 4, 2025

eric-wieser reviewed Jan 4, 2025

View reviewed changes

vihdzp added 3 commits January 4, 2025 19:41

Merge branch 'master' into vi.sumLexStuff

357b405

Update Lex.lean

863d897

fix stuff

e5aa9e2

eric-wieser reviewed Jan 5, 2025

View reviewed changes

vihdzp added 2 commits January 5, 2025 14:16

apply suggestions

35a7326

Merge branch 'master' into vi.sumLexStuff

962da91

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: linear order is isomorphic to lexicographic sum of two intervals #20409

feat: linear order is isomorphic to lexicographic sum of two intervals #20409

vihdzp commented Jan 3, 2025

github-actions bot commented Jan 3, 2025 •

edited

Loading

Declarations diff

YaelDillies left a comment

vihdzp commented Jan 4, 2025

eric-wieser Jan 4, 2025

eric-wieser Jan 4, 2025

vihdzp Jan 4, 2025

eric-wieser Jan 4, 2025

eric-wieser Jan 5, 2025

vihdzp Jan 5, 2025 •

edited

Loading

eric-wieser Jan 5, 2025 •

edited

Loading

eric-wieser Jan 5, 2025

vihdzp Jan 5, 2025

eric-wieser Jan 5, 2025

vihdzp Jan 5, 2025 •

edited

Loading

feat: linear order is isomorphic to lexicographic sum of two intervals #20409

Are you sure you want to change the base?

feat: linear order is isomorphic to lexicographic sum of two intervals #20409

Conversation

vihdzp commented Jan 3, 2025

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

PR summary 962da91995

Import changes for modified files

Declarations diff

YaelDillies left a comment

Choose a reason for hiding this comment

vihdzp commented Jan 4, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vihdzp Jan 5, 2025 • edited Loading

Choose a reason for hiding this comment

eric-wieser Jan 5, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vihdzp Jan 5, 2025 • edited Loading

Choose a reason for hiding this comment

github-actions bot commented Jan 3, 2025 •

edited

Loading

vihdzp Jan 5, 2025 •

edited

Loading

eric-wieser Jan 5, 2025 •

edited

Loading

vihdzp Jan 5, 2025 •

edited

Loading