[Merged by Bors] - feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups by pechersky · Pull Request #22420 · leanprover-community/mathlib4

pechersky · 2025-03-01T01:21:03Z

depends on: [Merged by Bors] - chore(Algebra/Order/Hom): initliaze simps for Order(Add)MonoidFoo #22402
depends on: [Merged by Bors] - feat(GroupWithZero): monoid with zero homs to (co)products #25466
depends on: [Merged by Bors] - feat(GroupWithZero/WithZero): injectivity and monotonicity of WithZero.map' #25660

and define `Order(Add)MonoidIso.symm` bringing along a copy of lemmas from MulEquiv clean up the simps

…nd projections into prod of ordered groups with a TODO about creating the associated categories

github-actions · 2025-03-01T01:22:06Z

PR summary 124c4b2dbc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Prod.Lex.Hom` (new file)	223
`Mathlib.Algebra.Order.Monoid.Lex` (new file)	410
`Mathlib.Algebra.Order.GroupWithZero.Lex` (new file)	417

Declarations diff

+ Prod.Lex.toLexOrderHom
+ coe_symm_toLexMulEquiv
+ coe_toLexMulEquiv
+ commute_inl_inr
+ commute_inlₗ_inrₗ
+ fst_comp_inr
+ fstₗ
+ fstₗ_comp_inlₗ
+ inl_eq_coe_inlₗ
+ inl_mul_inr_eq_coe_toLex
+ inl_mul_inr_eq_mk
+ inlₗ
+ inlₗ_mul_inrₗ_eq_toLex
+ inr_eq_coe_inrₗ
+ inrₗ
+ snd
+ snd_comp_inl
+ snd_comp_inr
+ toEquiv_symm_toLexMulEquiv
+ toEquiv_toLexMulEquiv
+ toLexMulEquiv
+ toMonoidWithZeroHom_coe
+ toMonoidWithZeroHom_mk
+ toOrderMonoidHom_comp
++ fst
++ fst_comp_inl
++ fst_mono
++ inl
++ inl_mono
++ inl_strictMono
++ inr
++ inr_mono
++ inr_strictMono
++ snd_mono

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

can't have the `fst_comp_inr` without a "send everything to one except zero" hom

Mathlib/Order/Prod/Lex/Hom.lean

Mathlib/Order/Prod/Lex/Monoid.lean

Mathlib/Order/Prod/Lex/GroupWithZero.lean

Factored out from #22420

mathlib4-dependent-issues-bot · 2025-06-11T15:49:53Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/Order/Hom): initliaze simps for Order(Add)MonoidFoo #22402~~
~~[Merged by Bors] - feat(GroupWithZero): monoid with zero homs to (co)products #25466~~
~~[Merged by Bors] - feat(GroupWithZero/WithZero): injectivity and monotonicity of WithZero.map' #25660~~
By Dependent Issues (🤖). Happy coding!

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

…r-community#25466) Factored out from leanprover-community#22420

…ro.map'` (leanprover-community#25660) factored out of leanprover-community#22420 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…r-community#25466) Factored out from leanprover-community#22420

…ro.map'` (leanprover-community#25660) factored out of leanprover-community#22420 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

Thanks!

maintainer delegate

YaelDillies · 2025-06-15T20:29:22Z

Mathlib/Algebra/Order/Monoid/Lex.lean

+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
+homomorphism from N to the lexicographic M ×ₗ N."]
+def inrₗ : β →*o (α ×ₗ β) where
+  __ := (Prod.Lex.toLexOrderHom).comp (inr α β)


That's evil!

Which is the evil part?

I would have expected

Suggested change

__ := (Prod.Lex.toLexOrderHom).comp (inr α β)

__ := Prod.Lex.toLexOrderHom.comp (inr α β)

YaelDillies · 2025-06-15T20:29:54Z

Mathlib/Algebra/Order/Monoid/Lex.lean

+The product of ordered monoids `α × β` is an ordered monoid itself with both natural inclusions
+and projections, making it the coproduct as well.
+
+TODO: Create the "OrdCommMon" category.


Suggested change

TODO: Create the "OrdCommMon" category.

## TODO

Create the "OrdCommMon" category.

YaelDillies · 2025-06-15T20:30:34Z

Mathlib/Algebra/Order/Hom/Monoid.lean

  rfl

+@[simp]
+lemma comp_coe_orderMonoidHom (f : β →*₀o γ) (g : α →*₀o β) :


I would suggest

Suggested change

lemma comp_coe_orderMonoidHom (f : β →*₀o γ) (g : α →*₀o β) :

lemma toOrderMonoidHom_comp (f : β →*₀o γ) (g : α →*₀o β) :

for clarity

YaelDillies · 2025-06-15T20:31:31Z

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

+  simp
+
+theorem inlₗ_mul_inrₗ_eq_coe_toLex {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0) :
+    (inl α β m * inr α β n) = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by


Suggested change

(inl α β m * inr α β n) = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by

inl α β m * inr α β n = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by

Is there no inrₗ_mul_inlₗ version?

Not sure what that would give differently, since this is over a commgroup

github-actions · 2025-06-15T20:32:21Z

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

jcommelin · 2025-06-16T06:43:14Z

bors d+

mathlib-bors · 2025-06-16T06:43:16Z

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

pechersky · 2025-06-16T15:21:29Z

bors r+

…d projections of prod of ordered groups (#22420)

mathlib-bors · 2025-06-16T16:23:13Z

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

…d projections of prod of ordered groups (#22420)

mathlib-bors · 2025-06-16T16:52:54Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…d projections of prod of ordered groups (leanprover-community#22420)

…r-community#25466) Factored out from leanprover-community#22420

…ro.map'` (leanprover-community#25660) factored out of leanprover-community#22420 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…d projections of prod of ordered groups (leanprover-community#22420)

pechersky added 2 commits February 28, 2025 09:39

chore(Algebra/Order/Hom): initliaze simps for Order(Add)MonoidFoo

7b03e85

and define `Order(Add)MonoidIso.symm` bringing along a copy of lemmas from MulEquiv clean up the simps

feat(Order/Prod/Lex/{Hom,Monoid,GroupWithZero}): ordered inclusoins a…

506bc5f

…nd projections into prod of ordered groups with a TODO about creating the associated categories

pechersky added t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Mar 1, 2025

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 Mar 1, 2025

pechersky added 4 commits March 2, 2025 15:48

remove simp

a8463c8

shake thanks to explicit types

b14da2a

switch to OrderedMonoidWithZeroHom

6bc9a81

spec lemmas

88d7332

can't have the `fst_comp_inr` without a "send everything to one except zero" hom

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 Apr 7, 2025

Merge branch 'master' into pechersky/lin-ord-g-w-zero-prod

7ea6195

grunweg assigned YaelDillies May 8, 2025

eric-wieser reviewed May 8, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/Hom.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 8, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/Hom.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 8, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/Monoid.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 8, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/GroupWithZero.lean Outdated Show resolved Hide resolved

YaelDillies reviewed May 9, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/GroupWithZero.lean Outdated Show resolved Hide resolved

YaelDillies reviewed May 9, 2025

View reviewed changes

Mathlib/Order/Prod/Lex/GroupWithZero.lean Outdated Show resolved Hide resolved

pechersky added 8 commits May 12, 2025 21:34

rename

315bd58

direct lemma

74f79be

lex syntax

9ab6eda

Merge branch 'master' into pechersky/lin-ord-g-w-zero-prod

6cba8eb

generalize with unbundled

3059eef

Prod.one_eq_mk

a397cba

explicit mono lemmas

c769623

rfl proofs

6a66db7

pechersky added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 4, 2025

feat(GroupWithZero): monoid with zero homs to (co)products

e9e206d

Factored out from #22420

pechersky mentioned this pull request Jun 5, 2025

[Merged by Bors] - feat(GroupWithZero): monoid with zero homs to (co)products #25466

Closed

YaelDillies reviewed Jun 11, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 11, 2025

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025

feat(GroupWithZero): monoid with zero homs to (co)products (leanprove…

95282b9

…r-community#25466) Factored out from leanprover-community#22420

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025

feat(GroupWithZero): monoid with zero homs to (co)products (leanprove…

29893d1

…r-community#25466) Factored out from leanprover-community#22420

feedback

a30753b

pechersky removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 15, 2025

YaelDillies approved these changes Jun 15, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 15, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 16, 2025

cleanup

1b61419

mathlib-bors bot pushed a commit that referenced this pull request Jun 16, 2025

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions an…

088da2e

…d projections of prod of ordered groups (#22420)

mathlib-bors bot pushed a commit that referenced this pull request Jun 16, 2025

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions an…

1f40b9f

…d projections of prod of ordered groups (#22420)

mathlib-bors bot changed the title ~~feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups~~ [Merged by Bors] - feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups Jun 16, 2025

mathlib-bors bot closed this Jun 16, 2025

mathlib-bors bot deleted the pechersky/lin-ord-g-w-zero-prod branch June 16, 2025 16:52

Rida-Hamadani pushed a commit to Rida-Hamadani/mathlib4 that referenced this pull request Jun 24, 2025

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions an…

f4b4af6

…d projections of prod of ordered groups (leanprover-community#22420)

callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025

feat(GroupWithZero): monoid with zero homs to (co)products (leanprove…

ed10daf

…r-community#25466) Factored out from leanprover-community#22420

callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025

feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions an…

adaee8d

…d projections of prod of ordered groups (leanprover-community#22420)

wwylele mentioned this pull request Aug 6, 2025

[Merged by Bors] - feat(Algebra/Order): LinearEquiv version of toLex/ofLex #27711

Closed

	__ := (Prod.Lex.toLexOrderHom).comp (inr α β)
	__ := Prod.Lex.toLexOrderHom.comp (inr α β)

	lemma comp_coe_orderMonoidHom (f : β →₀o γ) (g : α →₀o β) :
	lemma toOrderMonoidHom_comp (f : β →₀o γ) (g : α →₀o β) :

	(inl α β m * inr α β n) = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by
	inl α β m * inr α β n = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by

Conversation

pechersky commented Mar 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 124c4b2dbc

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jun 11, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

pechersky Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 15, 2025

Choose a reason for hiding this comment

Uh oh!

pechersky Jun 16, 2025

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jun 15, 2025

Uh oh!

jcommelin commented Jun 16, 2025

Uh oh!

mathlib-bors bot commented Jun 16, 2025

Uh oh!

pechersky commented Jun 16, 2025

Uh oh!

mathlib-bors bot commented Jun 16, 2025

Uh oh!

mathlib-bors bot commented Jun 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

pechersky commented Mar 1, 2025 •

edited

Loading

github-actions bot commented Mar 1, 2025 •

edited

Loading