Zulip Chat Archive

Stream: maths

Topic: Rep k G is closed


Winston Yin (Jul 16 2022 at 01:24):

@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 (Jul 16 2022 at 01:50):

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

Antoine Labelle (Jul 16 2022 at 02:05):

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 (Jul 16 2022 at 02:07):

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

Antoine Labelle (Jul 16 2022 at 02:14):

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 (Jul 16 2022 at 02:16):

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 (Jul 16 2022 at 02:19):

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

Antoine Labelle (Jul 16 2022 at 02:24):

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 (Jul 16 2022 at 02:25):

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 (Jul 16 2022 at 02:27):

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

Antoine Labelle (Jul 16 2022 at 02:28):

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 (Jul 16 2022 at 02:30):

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 (Jul 16 2022 at 02:30):

I'll take another shot at it

Antoine Labelle (Jul 16 2022 at 02:31):

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 (Jul 16 2022 at 04:42):

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

Winston Yin (Jul 16 2022 at 08:39):

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

Antoine Labelle (Jul 16 2022 at 14:06):

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

Winston Yin (Jul 18 2022 at 02:31):

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 (Jul 18 2022 at 02:45):

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 (Jul 18 2022 at 03:41):

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

Antoine Labelle (Jul 18 2022 at 12:33):

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

Winston Yin (Jul 19 2022 at 02:25):

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 (Jul 19 2022 at 02:36):

φ : 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 (Jul 19 2022 at 02:41):

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

Winston Yin (Jul 20 2022 at 23:32):

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.


Last updated: Dec 20 2023 at 11:08 UTC