Rep k G is closed

Stream: maths

[Winston Yin]

@Antoine Labelle Just for practice I decided to take a crack at showing monoidal_closed (Rep k G) by following docs#Module.category_theory.monoidal_closed. I got as far as constructing rep_coyoneda (...) : (Rep k G)ᵒᵖ ⥤ (Rep k G) ⥤ Rep k G, similar to docs#category_theory.linear_coyoneda, but I'm getting a bit stuck at proving the equivalent of docs#Module.monoidal_closed_hom_equiv. Specifically, the Module version uses linear_map.compr₂, which we don't have for representation hom. Is there any category theory gadgetry that'll help bridge this final step?

[Antoine Labelle]

That's great! How did you define rep_coyoneda exactly?

[Antoine Labelle]

By the way, it's fine if you want to stick to Rep k G but I think the way I would approach this is to prove that more generally that Action G C is monoidal closed whenever the category C is monoidal closed (or maybe even the functor category D ⥤ C?), which shouldn't really be harder.

[Winston Yin]

I was just sticking to Rep k G for practice. Happy to generalise once I get the hang of it

[Antoine Labelle]

For Action G C, I think the internal hom between objects (V, ρ) and (V', ρ') in Action G C would be ihom V V' with the action given by g ↦ (ρ' g) ∘ - ∘ (ρ g), where the composition here should be understood in the sense of docs#category_theory.monoidal_closed.pre. Now I realize that we don't seem to have a post-compostion version of category_theory.monoidal_closed.pre, so we would need that first.

[Winston Yin]

For rep_coyoneda, the objects are mapped by (Rep k G)ᵒᵖ → (Rep k G) → Rep k G := λ Y X, Rep.of (representation.lin_hom (unop Y).ρ X.ρ). Then the functors are constructed using linear.right_comp and linear.left_comp

[Winston Yin]

Perhaps it's not ideal that it uses lin_hom here?

[Antoine Labelle]

I see. I guess that can work for Rep k G, but the point of the category theory approach is to avoid using things like representation.lin_hom. My feeling for working with the category library so far is that we want to avoid as much as possible the mix of categorical and noncategorical definitions, since it is quite annoying to translate between the two.

[Winston Yin]

I agree. Still trying to gain some intuition about this approach. I found that Lean really struggles to type check when we liberally go back and forth between ⟶ and the particular implementation such as →ₗ[k]

[Antoine Labelle]

Yes, it's best this avoid this back and forth as much as possible I'd say.

[Antoine Labelle]

And if you stick to using just the categorical language (so no →ₗ[k]) then it shouldn't be harder to do it for Action V C than Rep k G, the proof should basically be the same.

[Winston Yin]

Yep. The category theory stuff for Module currently relies on →ₗ[k] a lot, so maybe that's not the best place to learn

[Winston Yin]

I'll take another shot at it

[Antoine Labelle]

Unfortunately there's not a lot of other instances of monoidal_closed which you can take inspiration from, but feel free to ask more questions.

[Antoine Labelle]

Actually I realized we do have postcomposition by external morphisms on ihom: it is simply internal_hom.flip.map.

[Winston Yin]

internal_hom needs limits.has_finite_products. Is that necessary for post composition?

[Antoine Labelle]

Oh sorry, I'm talking about docs#category_theory.monoidal_closed.internal_hom, not docs#category_theory.internal_hom.

[Winston Yin]

For Action G C, I think the internal hom between objects (V, ρ) and (V', ρ') in Action G C would be ihom V V' with the action given by g ↦ (ρ' g) ∘ - ∘ (ρ g)

How do I reconcile this with the fact that when G is a group, the action is given by g ↦ (ρ' g) ∘ - ∘ (ρ g⁻¹)? I managed to built pre- and post-composition using docs#monoidal_closed.internal_hom, together with nice composition properties. It remains to construct the part - ∘ (ρ g⁻¹) to compose oppositely to the multiplication on G

[Antoine Labelle]

Oh sorry I did mean rho of g inverse and not rho of g on the right. Is that what your question is about?

[Winston Yin]

Yes that clears it up. Then G has to be a group. I guess that’s no surprise

[Antoine Labelle]

Yes it only works for groups (or more generally for functors from a groupoid to a monoidal closed category).

[Winston Yin]

So far I've managed to define (Action V G)ᵒᵖ ⥤ Action V G ⥤ Action V G using g ↦ (ρ' g) ∘ - ∘ (ρ g⁻¹). Now I'd like to construct the equiv between (X ⊗ Y) ⟶ Z and Y ⟶ [X, Z], which should be provided by curry/uncurry in V. The issue I'm getting stuck on is showing that the (un)curried V-homs commute with the G-action on Y and [X, Z]. The G-action on [X, Z] refers to g⁻¹, while the action on X ⊗ Y doesn't. It's not totally clear to me how to show this even on paper yet

[Junyan Xu]

φ : Y ⟶ [X, Z] commuting with G-action is equivalent to φ (g • y) x = g • φ y (g⁻¹ • x) for all x : X, g : G, which is equivalent to φ (g • y) (g • x) = g • φ y x for all x : X, g : G, because λ x, g⁻¹ • x is bijective.

[Winston Yin]

Ah thanks. I reckon docs#Action.ρ_Aut, etc should come in handy

[Winston Yin]

I've completed the construction of the monoidal_closed (Action V G) instance in PR #15579. The proof is complete and sorry-free, but some parts are quite long, and some stylistic improvements are probably a good idea.