chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom by AntoineChambert-Loir · Pull Request #9564 · leanprover-community/mathlib4

AntoineChambert-Loir · 2024-01-08T21:08:46Z

I weaken a commutativity assumption for docs#AdjoinRoot.liftHom that the target algebra be commutative. It is only assumed to be a Semiring.
For that, I need to generalize docs#AdjoinRoot.lift which takes i : R ->+* S, a : S with f.eval₂ i a = 0 and defines AdjoinRoot f ->+* S that extends i and sends AdjoinRoot.root f to a.

The initial version of the PR was to define AdjoinRoot.lift' where S is only a Semiring, with the additional assumption hcomm : ∀ r, Commute (i r) a that the element a commutes with the image of i.

@jcommelin suggested to provide this argument as an autoParam, filled in by an ad hoc commutativity tactic. However, such an argument cannot be made implicit and a first version required to have this argument given each time, most of the time by _, even for all subsequent lemmas, AdjoinRoot.lift_mk, etc.

To avoid this, I tried to make this assumption a ⦃hcomm : ∀ r, Commute (i r) a⦄. This appears to have some side effects that proofs using an exact tactic or in term mode do not work well, but one can resort on by simp […]. Maybe @eric-wieser or @Vierkantor will have opinions on that. In some cases one can still give the argument as (hcomm := by commutativity).

(There are 3 options :

separate lemmas for the fully commutative case and for the case where a proof is needed
using the commutativity tactic, but with an argument _ sometimes
using the optional argument.)

jcommelin · 2024-01-09T10:41:26Z

+   -- It is a bit annoying that one be obliged to fill in this implicit hypothesis
+  AdjoinRoot.lift_root (hc := fun _ ↦ Commute.all _ _) (aeval_gen_minpoly F α)


I wonder whether it can maybe be supplied by a default argument/tactic. So that users in the commutative world never need to think about it.

@jcommelin I tried to think about this, but got confused by the syntax and could not make any progress (what I tried did not work at all). From the Zulip discussion, it seems that you had an idea of how that could be implemented… Could you please share some hint?

I pushed to jmc-AdjoinRoot. I'll let you decide which option you prefer.

(Note that I renamed lift' to lift, and there is now only one version.)

I just had a look! Wonderful!

…e ugly)

AntoineChambert-Loir · 2024-01-20T19:14:54Z

The AdjoinRoot.lift function now allows that target to be noncommutative, it only needs a proof that the element that AdjoinRoot.root f maps to commutes with the image of the ring.
Thanks to a tactic commutativity provided by @jcommelin , this argument can be filled automatically.
In all subsequent rewriting lemmas, I made it ⦃hcomm : ∀ r, Commute (i r) a⦄, but the defect is that I couldn't really use exact tactics, or term-mode proofs, so that the proofs are now a bit ugly, using a lot of by simp […].

This allows us to restore quite a few uses of `lift` to the original. The only drawback in the commutative case is we have to write `(lift i a h) x` instead of `lift i a h x` (since the autoparam comes after the `h`). Also, `simp` doesn't discharge autoparams automatically, so I added an extra set of lemmas that use implicits instead of autoparams, to be filled by unification.

Vierkantor · 2024-01-25T15:38:18Z

I pushed a commit which tags a few lemmas and replaces commutativity with a call to aesop. It's almost as good as original for the commutative case, if you ignore the parentheses :)

eric-wieser · 2024-01-27T08:35:10Z

-  apply Ideal.Quotient.lift _ (eval₂RingHom i x)
+It is currently only used in `AdjoinRoot.lift`. -/
+macro "commutativity" : tactic =>
+  `(tactic| first | aesop |


This should probably raise an error if there is no Commute in the goal

@eric-wieser Do you know how to check this? I don't...

Are Aesop rulesets a thing? If not, using guard_target would probably work.

guard_target isn't quite what we want here: for example, lift wants to use commutativity to solve ∀ r, Commute (i r) x.

WRT rulesets: do you mean we should set the commutativity tactic to use a commutativity ruleset exclusively? I feel like that's premature optimization.

Yes, I think we should do that because it matches the pattern set by measurability. I don't think that commutativity as a tactic should be solving everything that aesop can solve.

@eric-wieser @Vierkantor do you want me to try copying the measurability tactic file and build a commutativity tactic along its line?

Vierkantor · 2024-04-04T09:13:33Z

+/-
+Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Chambert-Lori (based on Measurability, by Miyahara Kō)


Typo? :)

Suggested change

Authors: Antoine Chambert-Lori (based on Measurability, by Miyahara Kō)

Authors: Antoine Chambert-Loir (based on Measurability, by Miyahara Kō)

joneugster · 2026-09-19T13:46:14Z

Mathlib has moved to PRs from forks. This PR is still from a branch of the main repository and will soon be closed! Please migrate the content to a fork and reopen a PR from there if you wish to do so. See Zulip topic for more instructions. Thank you for contributing to mathlib!

mathlib-bors · 2026-09-19T16:46:59Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

AntoineChambert-Loir · 2026-09-19T17:10:04Z

This PR has been migrated to a fork-based workflow: #43971

remove commutativity assumptions for AdjoinRoot

cd5ab01

AntoineChambert-Loir changed the title ~~remove commutativity assumptions for AdjoinRoot~~ remove commutativity assumptions for AdjoinRoot.lift Jan 8, 2024

AntoineChambert-Loir changed the title ~~remove commutativity assumptions for AdjoinRoot.lift~~ weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom Jan 8, 2024

Antoine Chambert-Loir added 3 commits January 8, 2024 22:10

lint100

fc1b4b4

cleanup docstring

0009115

explicitly add the theoretically implicit argument

e77dd6a

AntoineChambert-Loir added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels Jan 9, 2024

jcommelin reviewed Jan 9, 2024

View reviewed changes

eric-wieser reviewed Jan 9, 2024

View reviewed changes

Comment thread Mathlib/RingTheory/AdjoinRoot.lean Outdated

Antoine Chambert-Loir added 4 commits January 11, 2024 23:21

switch order of arguments, but do nothing (attempts failed)

06aae43

make the commutativity argument implicit whenever possible (proofs ar…

578890d

…e ugly)

adjust docstring and FieldTheory/Adjoin.lean

84790b9

linter 100

8da8342

Antoine Chambert-Loir and others added 3 commits January 20, 2024 20:16

adjust docstring in AdjoinRoot.lift

c219a55

Trying to make simpNF linter happy

de9d7fd

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 25, 2024

eric-wieser reviewed Jan 27, 2024

View reviewed changes

AntoineChambert-Loir added 2 commits April 1, 2024 17:54

Merge branch 'master' into ACL/AdjoinRoot

8c52a34

try to add commutativity tactic

fcbef43

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2024

AntoineChambert-Loir added 4 commits April 1, 2024 19:15

import commutativity

ea37e59

update Mathlib.lean

b93d422

make linter 100 happy

33817f9

update Tactic.lean

0ab20f0

AntoineChambert-Loir added WIP Work in progress and removed awaiting-review labels Apr 1, 2024

AntoineChambert-Loir added the awaiting-review label Apr 1, 2024

AntoineChambert-Loir added 2 commits April 1, 2024 22:48

try

d4bd005

try to extend commutativity

d6dbbf8

Vierkantor reviewed Apr 4, 2024

View reviewed changes

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 29, 2024

kim-em removed the awaiting-review label Jul 9, 2024

grunweg changed the title ~~weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom~~ chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom Nov 19, 2025

joneugster added the will-close-soon Unless something changes, we will close this PR soon label Sep 19, 2026

joneugster marked this pull request as draft September 19, 2026 16:46

AntoineChambert-Loir mentioned this pull request Sep 19, 2026

chore: weaken commutativity assumptions for AdjoinRoot.lift and AdjoinRoot.liftHom #43971

Draft

AntoineChambert-Loir added the migrated-to-fork label Sep 19, 2026

AntoineChambert-Loir closed this Sep 19, 2026

		-- It is a bit annoying that one be obliged to fill in this implicit hypothesis
		AdjoinRoot.lift_root (hc := fun _ ↦ Commute.all _ _) (aeval_gen_minpoly F α)

	Authors: Antoine Chambert-Lori (based on Measurability, by Miyahara Kō)
	Authors: Antoine Chambert-Loir (based on Measurability, by Miyahara Kō)

Conversation

AntoineChambert-Loir commented Jan 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Uh oh!

AntoineChambert-Loir commented Jan 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Vierkantor commented Jan 25, 2024

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!

joneugster commented Sep 19, 2026

Uh oh!

mathlib-bors Bot commented Sep 19, 2026

Uh oh!

AntoineChambert-Loir commented Sep 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

AntoineChambert-Loir commented Jan 8, 2024 •

edited

Loading

AntoineChambert-Loir commented Jan 20, 2024 •

edited

Loading