Conjugation typeclass

Stream: Is there code for X?

[Robert Maxton]

Is there any general way to represent adjunction-like types or families of types that have a meaningful "conjugation" operation $y^{-1}xy$? docs#CategoryTheory.Adjunction itself sort of counts, but universe levels in the category theory library are generally stricter than we'd like for something like this I think.

We have docs#Equiv.conj, but that's restricted to a) Equivs and b) single types that are c) inverse 'on the nose'.

If not, is this something we want in Mathlib?

[Edward van de Meent]

in what kind of generality are you thinking? are you thinking of something like docs#MulAction?

[Robert Maxton]

Extreme generality, one step up from a notational typeclass. Ideally it'd be something that lets the definition of 'inverse' and 'identity' be type-dependent, but I'd settle for just being built off of (families of) EquivLike(s).

[Robert Maxton]

MulAction is definitely too narrow; at the least I'd like to be able to tag ULift and Shrink, for example, as well as any other similar "morally a natural transformation between families of types" structures.

[Aaron Liu]

Are ULift and Shrink conjugations?

[Aaron Liu]

what are they conjugating?

[Edward van de Meent]

exactly... i feel like i'm missing the common pattern?

[Robert Maxton]

they aren't conjugations, but you can define conjugations on them and they're frequently used -- Equiv.ulift (f (Equiv.ulift.symm ...)

[Aaron Liu]

Can you define what a conjugation is?

[Aaron Liu]

are you looking for a functor?

[Robert Maxton]

Not quite... I think in categorical terms, the thing I'm looking for is basically a pseudonatural equivalence?
... Yeah, the general version is a pseudonatural equivalence, and the more specific version that does things up to strict equality is just a natural isomorphism

[Robert Maxton]

e.g. the only thing stopping us from defining a natural isomorphism between the (_root_.) Functors ULift and 𝟭 Type is universe levels

[Aaron Liu]

actually I think the problem is your functors have different targets

[Robert Maxton]

In what sense?

[Aaron Liu]

well I guess if it's ULift.{u, u} then they have the same target and you can define a natural isomorphism (which is docs#CategoryTheory.uliftFunctorTrivial)

[Robert Maxton]

oh, well, yeah, but that's the universe level thing I'm talking about

[Aaron Liu]

oh ok

[Kyle Miller]

docs#Quandle might be unfamiliar, but it's an algebraic structure encoding conjugation-like operations.

docs#Quandle.Conj is a group as a quandle, where the action is conjugation (docs#Quandle.conj_act_eq_conj)

Quandles (more generally racks) have enveloping groups (defined in that file), and it satisfies the adjunction (R →◃ Quandle.Conj G) ≃ (EnvelGroup R →* G), and so there's a universal property that rack homomorphisms to the conjugation quandle of a group factors through the enveloping group of the rack.

I don't remember what conditions you need for the homomorphism from a rack to the conjugation quandle of its enveloping group to be injective. But at least this all suggests that this is a generalization of conjugation. Maybe not the generalization you want, but it could be worth a look.

[Edward van de Meent]

Kyle Miller said:

docs#Quandle might be unfamiliar, but it's an algebraic structure encoding conjugation-like operations.

now you're just making up words

it does seem important to note that this encodes an action by some type on the same type

[Kevin Buzzard]

I believe it's Conway who was having fun making up words here

[Kyle Miller]

"Quandle" is due to David Joyce. Conway was involved in the study a couple decades before, but used the word "wrack".

[Kyle Miller]

Edward van de Meent said:

on the same type

Yes, a quandle itself is a type acting on itself, but there's a more general structure (augmented quandles) where you have a group G acting on a set Q, with a function Q -> G such that Q acting on itself via this function is a quandle. For example, if Q is a normal subgroup of G, G acts on Q by conjugation, and Q -> G is the inclusion map, you've got an augmented quandle.

Anyway, this is unlikely to help with Robert's question, even if there were some categorification of quandles that helps organize it. Re-reading the thread more carefully, I see the more general question might be 'how can we organize universe lifting/unlifting arguments better'.

[Robert Maxton]

At least partially, yes. I mean, I also want to have a nice interface for e.g. conjugating a functor by a family of categorical equivalences, but I don't mind if that turns out to be best handled separately.