Should Rep R G be funlike?

Stream: mathlib4

[Kevin Buzzard]

Doing representation theory with Richard Hill using Rep k G I want things like map_add to work, and one way to make this happen would be something like

instance (A B : Rep R G) : FunLike (A ⟶ B) A.V B.V where -- or should it be A B not A.V B.V?
  coe f := (f : A.V → B.V)
  coe_injective' _ _ hfg := CategoryTheory.ConcreteCategory.hom_ext_iff.mpr (congrFun hfg)

instance (A B : Rep R G) : AddHomClass (A ⟶ B) A B where
  map_add f a₁ a₂ := by
    change f.hom _ = f.hom _ + f.hom _
    simp only [map_add]

But I'm now confused about whether we should be doing this. If we don't make (A ⟶ B) an AddHomClass then we end up with hom f.homs everywhere after the concrete category redesign (or ModuleCat.Hom.hom f's everywhere in ModuleCat). Sorry to be so confused about what should be happening here -- what are we supposed to be doing?

[Kevin Buzzard]

Is the issue that Rep R G can't currently be a concrete category because we haven't decided what the best way to do non-category-theory rep theory is, so we don't know what to put for the hom sets??

[Eric Wieser]

What's hom f.hom in this context? Are the two homs different?

[Eric Wieser]

ModuleCat.Hom.hom f seems ok to me if we can make it use dot notation

[Kevin Buzzard]

import Mathlib

variable (R G : Type) [CommRing R] [Group G]

open CategoryTheory ConcreteCategory

instance (A B : Rep R G) (f : A ⟶ B) :
    f.hom 0 = 0 := by
  -- ⊢ (hom f.hom) 0 = 0
  sorry

[Kevin Buzzard]

I think the issue is that Rep R G is no longer a concrete category because we don't know what the morphisms are, so to apply f we go through the module category (f.hom is a morphism in the module category) and then hom f.hom is coming from the concrete category. One fix is to make Rep R G FunLike and AddHomClass etc etc, and another fix would be to add some bundled structure for morphisms of representations and make Rep R G concrete.

[Edison Xie]

Kevin Buzzard said:

make Rep R G FunLike

Rep R G now is a R-module V and a ringhom fromG to CategoryTheory.End V right?

[Aaron Liu]

I have

import Mathlib

variable (R G : Type) [CommRing R] [Group G]

open CategoryTheory

#synth ConcreteCategory (Rep R G) (Action.HomSubtype (ModuleCat R) G)

[Kevin Buzzard]

This is something else which is confusing me:

#synth ConcreteCategory (ModuleCat R) (fun A B ↦ A →ₗ[R] B) -- works

instance (A B : ModuleCat R) : FunLike (A ⟶ B) A B := inferInstance -- fails

[Aaron Liu]

Now it's confusing me too

[Kevin Buzzard]

Aaron Liu said:

I have

import Mathlib

variable (R G : Type) [CommRing R] [Group G]

open CategoryTheory

#synth ConcreteCategory (Rep R G) (Action.HomSubtype (ModuleCat R) G)

This is going to make the infoview even worse, I should think!

[Edison Xie]

are these two instance the same on ModuleCat: Action.instConcreteCategoryHomSubtypeV andModuleCat.instConcreteCategoryLinearMapIdCarrier R?

[Aaron Liu]

Do you mean

import Mathlib

variable (R G : Type) [CommRing R] [Group G]

open CategoryTheory

instance (A B : Rep R G) (f : A ⟶ B) :
    ⇑(ConcreteCategory.hom f.hom) = ⇑(ConcreteCategory.hom f) := rfl