[Merged by Bors] - feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms

[YaelDillies]

Generalise ..._seminorm_class to arbitrary codomains (rather than just ℝ). Instantiate mul_ring_norm_class for absolute values.

---

Match leanprover-community/mathlib4#1238

[ADedecker]

If I understand correctly, you are generalizing the hom classes [*]_seminorm_class to take values in more general types, but the original bundled [*]_seminorm stay with real values, is that right? Is that simply for deduplication, or do you have a precise use case in mind? Could you add a comment explaining this "inconsistency" somewhere?

[YaelDillies]

Yes, precisely. The point is that absolute values are multiplicative ring norms, but not necessarily real-valued, while we don't care about the type of non-real-valued multiplicative ring norms.

[Vierkantor]

So just to be clear, this PR contains the following changes:

• move norm classes to algebra/order/hom/basic.lean
• generalize to arbitrary codomains
• instantiate mul_ring_norm_class (absolute_value R S)

It's very annoying to review a PR that moves and changes code at the same time. And I'm not convinced that this is the best strategy for dealing with the mathlib4 port. As far as I can tell, the consensus is that changes to ported files should have a simultaneous mathlib4 PR that is reviewed at the same time. I'll ask on Zulip what we should do.

[YaelDillies]

@semorrison explained in the last porting meeting on thursday that we were against

Instead, I will mark algebra.order.hom.basic as No: Partially ported on the porting status.

So I guess either:

• We move forward here and do it anyway. I think that's okay because all the new material is circumscribed to the second part of the file.
• We wait for the tide to reach algebra.group_power.order. This is going to take a while, but this PR is probably not very prone to rotting.

[YaelDillies]

Now that algebra.group_power.order is ported, I opened a matching PR.

[Vierkantor]

Could you explain what this means specifically? Do you have an example of this instance not applying when it should?

[YaelDillies]

If I do

@[priority 100] -- See note [lower instance priority]
instance ring_seminorm_class.to_nonneg_hom_class [non_unital_non_assoc_ring α]
  [linear_ordered_semiring β] [ring_seminorm_class F α β] : nonneg_hom_class F α β :=
infer_instance

typeclass search fails, even though ring_seminorm_class.to_add_group_seminorm_class and add_group_seminorm_class.to_nonneg_hom_class are both instances.

[Vierkantor]

Aha, this is because of diamond inheritance in instance parameters that depend on an out_param: add_group_seminorm_class.to_nonneg_hom_class requires a linear_ordered_add_comm_monoid instance, and ring_seminorm_class.to_add_group_seminorm_class requires a ordered_semiring instance. These have a common ancestor in ordered_add_comm_monoid so normally what happens is Lean wants to unify @linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid β ?inst1 =?= @ordered_semiring.to_ordered_add_comm_monoid β ?inst2, sees that it can unstuck by inferring instances for ?inst1 and ?inst2, unfolds those instances, compares equality field-wise, and succeeds.

Here, because β is an out_param of nonneg_hom_class, β becomes a metavariable that isn't solved until the ring_seminorm_class parameter is filled in. But we can't fill that in until we reach ring_seminorm_class from add_group_seminorm_class. And we can't check that these are defeq because it requires getting unstuck, and it can't unstuck because the instance is full of metavariables, so Lean gives up the equality check.

Hacking on mathlib4#888 has taught me the Lean 4 synthesis algorithm is even worse at instance params depending on outParams so I expect the conclusion would have to be that this instance is required to help Lean get unstuck.

[YaelDillies]

Oh dear 😦

Then I guess this PR is ready

[Vierkantor]

Let's add a comment:

Suggested change

	-- TODO: Somehow this does not get inferred.
	-- This instance is simply the composition of the instances
	-- `add_group_seminorm_class.to_nonneg_hom_class` and
	-- `ring_seminorm_class.to_add_group_seminorm_class`. However, it has to be
	-- declared explicitly due to hitting an edge case in the inference algorithm:
	-- those instances both depend on a different subclass of `ordered_add_monoid β`, but `β` is an
	-- `out_param` that cannot be inferred until both instances are applied.
	-- So we have to do it manually until Lean becomes smarter.
	-- Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Instance.20diamonds.20depending.20on.20.60outParam.60s

[Vierkantor]

I've edited the suggestion to add a pointer to a relevant Zulip thread. If we really want to get this working, I think the right solution is to forbid extending a class in conditions where this limitation applies, and instead use unbundled inheritance.

If you want to add a library note, I'd add it as a separate comment, specifying exactly what goes wrong and some options for dealing with it:

Diamond inheritance cannot depend on `out_param`s in the following circumstances:
 * there are three classes `top`, `middle`, `bottom`
 * all of these classes have a parameter `(α : out_param _)`
 * all of these classes have an instance parameter `[root α]` that depends on this `out_param`
 * the `root` class has two child classes: `left` and `right`, these are siblings in the hierarchy
 * the instance `bottom.to_middle` takes a `[left α]` parameter
 * the instance `middle.to_top` takes a `[right α]` parameter
 * there is a `leaf` class that inherits from both `left` and `right`.
In that case, given instances `bottom α` and `leaf α`, Lean cannot synthesize a `top α` instance, even though the hypotheses of the instances `bottom.to_middle` and `middle.to_top` are satisfied.

There are two workarounds:
 * You could replace the bundled inheritance implemented by the instance `middle.to_top` with unbundled inheritance implemented by adding a `[top α]` parameter to the `middle` class. This is the preferred option since it is also more compatible with Lean 4, at the cost of being more work to implement and more verbose to use.
 * You could weaken the `bottom.to_middle` instance by making it depend on a subclass of `middle.to_top`'s parameter, in this example replacing `[left α]` with `[leaf α]`.

[Vierkantor]

Other than that TODO remark, I'm happy with these changes.

[Vierkantor]

bors d+

[bors]

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

[YaelDillies]

Library note added and typeclass inference cursed. I think this is ready.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests