!4#5041 RepresentationTheory.Rep

Stream: PR reviews

[Amelia Livingston]

Take 2 of porting this file now that I've refactored some of the mathlib3 version. The port now has no errors and is ready for review. Some proofs had to be changed quite a bit because of simp behaving differently.

Also, some imported files have definitions for which @[simps] generates lemmas that unfold the types of certain terms. This means the linter complains that the LHS of some of my lemmas simplify to [something syntactically equal to the LHS] because the @[simps] lemmas just simplify some types in the LHS. I've added nolint simpNF when this is the case. I can't get simp to use some of my nolint simpNF lemmas anyway, though.

[Scott Morrison]

I recommend trying modifying those @[simps] attributes, tell it to only write simp lemmas for the non-type fields. It seems simp lemmas for type fields in category theory are often unhelpful.

[Amelia Livingston]

thank you! I will do that.

[Amelia Livingston]

Unfortunately removing simp lemmas for type fields is causing Category.comp_id, Category.id_comp rewrites to fail :(

[Scott Morrison]

@Amelia Livingston I can have a look at this. If you have hints about which @[simps] attributes I should be looking at that would be helpful.

[Amelia Livingston]

thank you! The ones firing a lot for me come from

• CategoryTheory.Monoidal.transport in CategoryTheory.Monoidal.Transport
• Action.functorCategoryEquivalence, Action.FunctorCategoryEquivalence.functor and Action.FunctorCategoryEquivalence.inverse in RepresentationTheory.Action
• CategoryTheory.Equivalence.symm in CategoryTheory.Equivalence
• Also the lemma CategoryTheory.Monoidal.tensorObj_obj in CategoryTheory.Monoidal.FunctorCategory which doesn't come from a @[simps]

[Amelia Livingston]

Alternatively, I don't actually need the lemmas I've added nolint simpNFto to be simp lemmas

(they're MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, Rep.homEquiv_apply_hom and Rep.homEquiv_symm_apply_hom, all in RepresentationTheory.Rep, fwiw)

so for the purposes of this PR I could just remove the simp attribute. But I'm interested to know the solution to this in general