feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas #24533

robertmaxton42 · 2025-05-02T00:52:54Z

Adds the convenience def ULift.conj x := down (f (up x))`, and corresponding basic lemmas
Adds lemmas showing that ULift.up and .down commute with casts and preserve HEq.

github-actions · 2025-05-02T00:54:03Z

PR summary 0d63fa4ea4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ cast_up
+ conj
+ conj_map
+ down_cast
+ ext_heq
+ ext_heq_iff
+ map_conj

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

eric-wieser · 2025-05-02T03:02:28Z

Mathlib/Data/ULift.lean

  Function.rec_update up_injective (ULift.rec ·) (fun _ _ => rfl) (fun
    | _, _, .up _, h => (h _ rfl).elim) _ _ _

+def conj {α β : Type*} (f : ULift α → ULift β) : α → β := fun x => (f ⟨x⟩).down


What do you need this for? Can you just use Equiv.ulift.conj in your application instead?

Convenience and clarity. It's not strictly necessary but it gets annoying writing the definition out too often. And, we do have ULift.map, so it'd be good to have its inverse.

I don't think so. Equiv.ulift.conj would have type (ULift α → ULift α) ≃ (α → α), there's no good way to introduce a β there.

Mathlib/Data/ULift.lean

Co-authored-by: Eric Wieser <[email protected]>

eric-wieser · 2025-05-02T03:26:23Z

Mathlib/Data/ULift.lean

+lemma conj_map {α β : Type*} (f : α → β) : conj (ULift.map f) = f := by
+  ext x; rfl
+
+lemma down_heq_inj {α β : Type u} (x : ULift.{u'} α) (y : ULift.{u'} β)


This looks like ext_heq to me, comparing to ULift.ext

eric-wieser · 2025-05-02T03:26:53Z

Mathlib/Data/ULift.lean

+  cases x; cases y; cases h; rfl
+
+@[simp]
+lemma down_heq_inj_iff {α β : Type u} (h : α = β)


This is either heq_iff or ext_heq_iff; maybe see if you can find any precedent either way.

There are no existing ext_heqs in the library, so no real precedent I don't think. I'm going to lean towards ext_heq_iff.

eric-wieser · 2025-05-02T03:28:33Z

Mathlib/Data/ULift.lean

+  cases h; cases h'; rfl
+
+@[simp]
+lemma cast_up_comm {α β} {a : α} (h : α = β) (h' : ULift α = ULift β := congrArg ULift h)


The naming convention says this is cast_up, or up_cast only if you change the statement to be reversed.

What's your rationale for choosing to push cast to the inside instead of pulling it to the outside as in the lemma below?

cast_up it is, I suppose, though I thought of this as "commuting cast and ULift.up when I wrote it".

The thing that is likely to have cast lemmas permitting further simplification is the "bare" object, the thing inside the ULift wrapper. Both lemmas are therefore written so that the cast is applied to something not ULifted.

eric-wieser · 2025-05-02T03:28:44Z

Mathlib/Data/ULift.lean

+
+@[simp]
+lemma cast_up_comm {α β} {a : α} (h : α = β) (h' : ULift α = ULift β := congrArg ULift h)
+    : (cast h' ⟨a⟩) = ⟨cast h a⟩ := by


The prevailing style is that the : goes on the previous line.

eric-wieser · 2025-05-02T04:57:47Z

Mathlib/Data/ULift.lean

+  cases h; cases h'; rfl
+
+@[simp]
+lemma cast_down {α β} {a : ULift α} (h : α = β) (h' : ULift α = ULift β := congrArg ULift h) :


I think this one is down_cast, because the down is on the outside of the cast

I suppose. I'm a little concerned about discoverability, but sure, I guess.

grunweg · 2025-08-27T17:17:42Z

@eric-wieser Would you like to finish reviewing this? (If not, I'll try to find somebody else.)

eric-wieser · 2025-08-28T00:19:44Z

Mathlib/Data/ULift.lean

+
+@[simp]
+lemma ext_heq_iff {α β : Type u} (h : α = β)
+    (x : ULift.{u'} α) (y : ULift.{u'} β) : HEq x y ↔ HEq x.down y.down := by


This should use the new HEq notation

eric-wieser · 2025-08-28T00:21:29Z

@grunweg: happy for you to assign someone else. My feeling is that we don't want conj without more justification (e.g. a downstream PR), but the other lemmas are close to ready.

robertmaxton42 · 2025-08-28T07:40:56Z

As the name implies, all PRs in the quiv-helpers series are helper lemmas used in the construction of limits and colimits in Quiv; I haven't added the downstream PRs because I'm still rather unfamiliar with git and would prefer not to deal with git's unfortunate inconveniences around PRs that depend on other PRs.

grunweg · 2025-08-28T07:50:55Z

I have labelled this awaiting-author to address the last PR feedback. Please click resolve on any review comment you have addressed, and remove the awaiting-author label once you have addressed all review comments. (You can do so by commenting just the word -awaiting-author in a comment.)

robertmaxton42 · 2025-09-02T01:59:32Z

Mathlib/Data/ULift.lean

+  ext x; rfl
+
+lemma ext_heq {α β : Type u} (x : ULift.{u'} α) (y : ULift.{u'} β)
+    (h : HEq x.down y.down) : HEq x y := by


Suggested change

(h : HEq x.down y.down) : HEq x y := by

(h : x.down ≍ y.down) : x ≍ y := by

robertmaxton42 · 2025-09-02T01:59:56Z

Mathlib/Data/ULift.lean

+
+@[simp]
+lemma ext_heq_iff {α β : Type u} (h : α = β)
+    (x : ULift.{u'} α) (y : ULift.{u'} β) : HEq x y ↔ HEq x.down y.down := by


Suggested change

(x : ULift.{u'} α) (y : ULift.{u'} β) : HEq x y ↔ HEq x.down y.down := by

(x : ULift.{u'} α) (y : ULift.{u'} β) : x ≍ y ↔ x.down ≍ y.down := by

robertmaxton42 · 2025-09-02T02:04:06Z

@grunweg Unfortunately, I don't think I can address that last comment properly anymore; am I going to have to make a new PR for this to go through?

grunweg · 2025-09-08T16:09:37Z

@robertmaxton42 Indeed, it seems you need to migrate your PR to a fork now. (There's a migrate_to_fork.py script now; using the latest version on the master branch is recommended.)

feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas

33cb839

robertmaxton42 requested a review from eric-wieser May 2, 2025 00:53

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label May 2, 2025

eric-wieser reviewed May 2, 2025

View reviewed changes

Mathlib/Data/ULift.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label May 2, 2025

add suggestions from code review

ee60408

Co-authored-by: Eric Wieser <[email protected]>

eric-wieser reviewed May 2, 2025

View reviewed changes

apply suggestions from review

08bce6e

eric-wieser reviewed May 2, 2025

View reviewed changes

robertmaxton42 added 2 commits May 1, 2025 22:10

naming suggestions from review

f2ae392

add doc comment to conj

0d63fa4

robertmaxton42 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 2, 2025

robertmaxton42 requested a review from eric-wieser May 18, 2025 09:19

leanprover-community-bot-assistant assigned ericrbg Aug 13, 2025

eric-wieser reviewed Aug 28, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 28, 2025

grunweg unassigned ericrbg Aug 28, 2025

robertmaxton42 commented Sep 2, 2025

View reviewed changes

grunweg changed the title ~~feat (ULift): conjugation by ULift.up/down, misc cast/heq lemmas~~ feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas Nov 19, 2025

	(h : HEq x.down y.down) : HEq x y := by
	(h : x.down ≍ y.down) : x ≍ y := by

	(x : ULift.{u'} α) (y : ULift.{u'} β) : HEq x y ↔ HEq x.down y.down := by
	(x : ULift.{u'} α) (y : ULift.{u'} β) : x ≍ y ↔ x.down ≍ y.down := by

feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas #24533

Are you sure you want to change the base?

feat(ULift): conjugation by ULift.up/down, misc cast/heq lemmas #24533

Conversation

robertmaxton42 commented May 2, 2025

Uh oh!

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

Uh oh!

PR summary 0d63fa4ea4

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robertmaxton42 May 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg commented Aug 27, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented Aug 28, 2025

Uh oh!

robertmaxton42 commented Aug 28, 2025

Uh oh!

grunweg commented Aug 28, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robertmaxton42 commented Sep 2, 2025

Uh oh!

grunweg commented Sep 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented May 2, 2025 •

edited

Loading

robertmaxton42 May 2, 2025 •

edited

Loading