Add opposite

Stream: maths

[Yury G. Kudryashov]

Related to this thread, I want to have an additive version of docs#has_mul.to_has_opposite_scalar

[Yury G. Kudryashov]

To do this, I need to define add_opposite.

[Yury G. Kudryashov]

Of course, I can do it but may be it's a good reason to think about opposite API. I have a few questions:

1. Why do we want opposite to be irreducible (unlike order_dual etc)?
2. Should I separate opposite (category theory) from opposite (multiplicative opposite)?
3. If we want it to stay irreducible, should I turn it into a one-field structure?

[Yakov Pechersky]

For 1, is it because multiplication is a binary operation that returns data while le is a binary relation that returns a Prop?

[Yury G. Kudryashov]

My guess is that people who wrote opposite and order_dual had different applications in mind.

[Johan Commelin]

Regarding 2: since preorders and categories are quite related, I guess it almost makes more sense to unify "opposite category" (currently opposite) and "opposite order" (currently order_dual), and have a different type alias for "opposite algebra" (currently opposite)

[Johan Commelin]

My understanding is that opposite was made irreducible because the category library got mightily confused otherwise. @Scott Morrison Can you confirm? Or was there another reason?

[Yury G. Kudryashov]

I don't want order_dual to be irreducible!

[Yury G. Kudryashov]

If we split two meanings of opposite, which one inherits the notation? What notation should we use for the other one?

[Johan Commelin]

Sure, I understand. So maybe Scott will save my idea by telling us that opposite doesn't need to be irreducible for categories after all...

[Johan Commelin]

But maybe it's as Yakov says: order_dual flips Proppy things around, whereas opposite flips data things around.

[Yury G. Kudryashov]

If we flip ≤ and ≥, then we flip min and max, and this is data.

[Johan Commelin]

That's right, and inf and sup as well, of course.

[Yury G. Kudryashov]

@Scott Morrison could you please have a look at this thread?

[Scott Morrison]

I don't think it needs to be irreducible, but having opposite irreducible removed an easy source of confusion.

[Scott Morrison]

It would be equally good as a structure.

[Scott Morrison]

I guess I don't understand in this discussion why we might want to make to semireducible again.

[Yury G. Kudryashov]

To be able to use it for "dual" proofs like we do with order_dual?

[Yury G. Kudryashov]

And the main question is whether we should use different opposite for "multiplicative opposite" and "category theory opposite".

[Yury G. Kudryashov]

Since the "multiplicative opposite" is going to get an additive version.

[Yury G. Kudryashov]

And what should we do with notation if we split to opposites.

[Scott Morrison]

I don't object to splitting opposites. The category theory one is a common generalisation of the multiplicative opposite and the order dual, and I can't think of any particular reason it is "closer" to one or the other.

[Yury G. Kudryashov]

What do you think about notation?

[Scott Morrison]

If we can't use \op for both, that seems a good reason not to split them to me. :-)

[Reid Barton]

Scott Morrison said:

It would be equally good as a structure.

Equally good from the standpoint of avoiding confusion, but actually making it a structure would be pretty rough for the opposite category, I found.

[Reid Barton]

Logically, opposite corresponds to order_dual because opposite is something we apply to the objects of a category, not the morphisms. (The thing corresponding to the multiplicative opposite would be the construction that reverses the order of $\otimes$ in a monoidal category.)

[Reid Barton]

However, the practical difference between opposite for categories and order_dual is that it seems like order_dual is almost exclusively used in "dual proofs", while the opposite of a category is something we're actually interested in. I'm not sure exactly why this should be (it seems like the uses of opposite categories in category theory should also correspond to uses of the opposite orders in order theory, maybe order theory is just simpler so we can just unfold the definition where it would otherwise arise, and/or we have less order theory).

[Reid Barton]

I would assume that is why the fact that order_dual is a plain def hasn't led to any confusion about what a <= b means yet.

[Reid Barton]

On the other hand, I am not sure if we have any good solution for opposite in Lean 4 yet.

[Yury G. Kudryashov]

Good reason to split: we want to_additive to send opposite Monoid to opposite AddMonoid, not add_opposite AddMonoid.

[Yury G. Kudryashov]

What about Xᵒᵖ (category theory), Xᵐᵒᵖ (multiplicative), Xᵃᵒᵖ (additive)?

[Eric Wieser]

Or maybe put the notation behind a locale?

[Eric Wieser]

And use X⁺ᵒᵖ and Xᵒᵖ for the algebra versions, and Xᵒᵖ for category theory, but in different locales

[Scott Morrison]

We in fact already have ᵐᵒᵖ, in src#category_theory.monoidal.opposite, although as Reid points out above this matches up well with the multiplicative opposite anyway. In any case, the monoidal opposite is sufficiently specialized that it can of course disappear into a locale if it is ever problematic.

[Yury G. Kudryashov]

One more possibility: Xˣᵒᵖ and X⁺ᵒᵖ for multiplicative and additive opposites.

[Yury G. Kudryashov]

There is also Xᕯᵒᵖ

[Yury G. Kudryashov]

(two stars, one symbol)

[Yury G. Kudryashov]

I'm trying to separate category theory opposite from multiplicative opposite. Which one should I use for docs#rack?

[Yury G. Kudryashov]

@Kyle Miller :up:

[Kyle Miller]

Let's call this a multiplicative opposite, since x ◃ y is is generalizing x * y * x⁻¹

[Eric Wieser]

I wonder how much overlap shelf and docs#mul_distrib_mul_action have

[Kyle Miller]

I'm trying to remember why I didn't use has_scalar (and introduce a has_inv_scalar) instead of using the quandle-traditional triangle. I think there might have been two reasons: (1) some quandles have a scalar structure already, like $\mathbb{Z}[t,t^{-1}]$, and (2) it's a self-action, and homomorphisms of self-actions transform both arguments of the operation.

[Eric Wieser]

Regarding 2, I guess we don't have docs#mul_distrib_mul_action_hom to sit between docs#mul_action_hom and docs#mul_semiring_action_hom