Documentation of character.v

There are several definitions in character.v which are not documented:

• trow and trowb,tprod : tensor (also called) Kronecker product of matrices
• grepr0 and dadd_grepr : nul and direct sum of representations
• muln_grepr : direct multiple of a representation
• prod_repr : tensor product of representations
• standard_irr, standard_socle, standard_irr_coef, standard_grepr

Though, the latter might be considered as internal and kept undocumented, I feel that the first four above items deserve to be exposed.

Also, it seems that prod_repr should be prod_grepr for consistency.

I'm ok to help here, I'm asking if it is left undocumented on purpose.

Indeed, it needs documentation.

I agree character is clearly undocumented Please do the PR!

There is also the question of naming convention: I thing that prod_repr should be prod_grepr for consistency with muln_grepr, dadd_grepr , prod_repr... Any agreement on that ?

you can put it in the PR too or make a separate one as you prefer

These definitions were left undocumented because they are all considered to be internal:

• grepr0, dadd_grepr, muln_grepr are essentially only used to construct standard_grepr
• Indeed the representation type which they operate on is also undocumented, for the same reason (it is used in the statement of the cfreprP reflection lemma, but usually one destructs the extracted representation to expose the underlying mx_representationinstance. So if anything, it's the representation type and its rdegree projector that could be documented.
• The representation type just bundles the representation degree with the matrix representation, while mx_representation exposes it; this bundling is a technical necessity to be able to use the bigop library, but is not otherwise needed when using characters, hence the type is considered internal.
• While representation coerces to mx_representation, the Representationconstructor could be made into the converse coercion, which would further blur the distinction between the two types, but I refrained from doing so as I was wary of how Coq behaves with circular coercions, and representation is only used internally in the formalisation of characters.
• The _grepr suffix indicates operations on the representation type, as opposed to the _repr suffix which indicates operations on the mx_representation type (and is used throughout mxrepresentation.v). Thus, the naming of prod_repr, which does operate on mx_representation, is not an oversight. It is only used to prove that characters are closed under product, so was left undocumented (but it could be mentioned).
• While tensor product of matrices is certainly generally useful, character.v is not the right place to provide it, and indeed the formalisation here is quite incomplete - it is, again, just an internal construction needed to get products of characters. If at some point a proper formalisation of tensor products is added to the matrix/algebra library (I believe @CohenCyril had worked on one at some point) then obviously it should be used in character.vinstead of the current tprod bespoke definition.

@ggonthier : Thanks for your detailed answer. I was suspecting that you didn't want to expose those construction, because while general, then were not sufficiently developed to be exposed. That's why I created this issue instead of throwing a pull request.

Now the question is : what should we do ?

• Should this issue be closed as wontfix ?
• Should we create an other issue about the implementation of tensor product of matrices ?