groupCohomology namespace

Stream: mathlib4

[Violeta Hernández]

We have a groupCohomology namespace used for theorems such as Hilbert 90 (docs#groupCohomology.exists_mul_galRestrict_of_norm_eq_one). This smells quite fishy to me, don't we generally make namespaces UpperCamelCase?

[Joël Riou]

No. The reason the name is not capitalized is that this lemma is related to group cohomology (which corrresponds to the definition groupCohomology, which is not a type). We have a bunch of other examples, like kernel.lift, etc, for definitions that are related to kernel in category theory.

[Violeta Hernández]

Sure, but the lemma I mentioned doesn't even mention groupCohomology. So it's not enabling any sort of dot notation, and it feels more like just a bare namespace.

[Joël Riou]

Even though there is no groupCohomology, this is a standard group cohomology result...

[Violeta Hernández]

We don't generally preface theorems on field theory with a FieldTheory namespace, or theorems on topology with a Topology namespace.

[Rémy Degenne]

But we do preface results in measure theory with MeasureTheory, and similarly for ProbabilityTheory.

[Violeta Hernández]

Huh. Is there a general rule for this?

[Edward van de Meent]

i have to say i agree with Violeta here that it should be capitalised, as the theorem is not about the declaration docs#groupCohomology but about the field of Group Cohomology.

[Edward van de Meent]

also, one might argue that, since groupCohomology gives an element of ModuleCat k, it actually is a type and therefore should be capitalised?

[Edward van de Meent]

that interpretation might not be consistent with the rest of mathlib though, i haven't checked.

[Joël Riou]

I do not think we want to revert https://github.com/leanprover-community/mathlib4/pull/6029

[Yury G. Kudryashov]

Edward van de Meent said:

also, one might argue that, since groupCohomology gives an element of ModuleCat k, it actually is a type and therefore should be capitalised?

No, ModuleCat is not a Sort*; it's a bundled object.

[Edward van de Meent]

i know it's a bundled object, but one can treat it as a Sort because the coercion exists