Scaled/absolute trace from algebraic closure

Stream: Is there code for X?

[Michał Staromiejski]

In characteristic 0, the map $\bar K \to K$ defined by $x \mapsto \frac{1}{[K(x) : K]} \mathop{Tr}^{K(x)}_K (x)$ is linear and I use it in some of my results. Does it have a name? There are some papers naming it "absolute trace" but usually absolute trace is a trace to the prime field. Do we have it defined in Mathlib (I could not find anything)?

[Johan Commelin]

I don't think we have something like that.

[Michał Staromiejski]

I could add it then, the question is how to name it? I would go with absoluteTrace: even if the name is sometimes used in different context, there are still a lot of publications naming it like this, for example here.
But I'm open for other suggestions especially if someone encountered this map already with another name.

[Xavier Roblot]

What about something like normalized trace ?

[Michał Staromiejski]

Sounds also good: normalizedTrace?

[Kevin Buzzard]

That sounds good to me. I remember that Tate used this trace to great effect in his $p$-divisible groups paper but I've just got around to seeing what he calls it and he just calls it $t$ :-)

[Ruben Van de Velde]

$t$ for "T"ate?

[Michał Staromiejski]

Tate's_t then? :zany_face:

[Michał Staromiejski]

@Kevin Buzzard, just out of curiosity, could you refer me to the Tate paper, please? What I could find online defines the trace scaled by the degree of the extension, not for the individual element... Anyway, I'll use normalizedTrace even if it would not match exactly.

BTW, my definition follows more or less this pattern:

variable (F K : Type*) [Field F] [Field K] [Algebra F K]

/- define raw function by some formula -/
def myMap' (a : K) : F := ...

/- facts about `myMap'` -/
theorem myMap'_fact1 : ... := ...
theorem myMap'_fact2 : ... := ...

/- add a structure to `myMap'` -/
def myMap : K →ₗ[F] F where
  toFun := myMap'
  map_add' := ... /- here use the facts above, often multiple times -/
  map_smul' := ... /- here use the facts above, often multiple times -/

/- here go facts about linear map `myMap` -/

/- Should `myMap'_fact<n>`'s be repeated here just for `myMap`? -/

The question is in the last comment. Didn't find anything analogous, maybe someone could refer or in general what are guidelines here?

[Junyan Xu]

Maybe your myMap'(_fact<n>) could be private?

[Kevin Buzzard]

Michal it sounds like you've found the right paper, it's his paper on p-divisible groups from the 60s or 70s. I don't understand what you're claiming the difference is between what you're doing and what Tate was doing. Making the field bigger doesn't change the normalised trace.

[Michał Staromiejski]

Yup, found also this with some references. Thanks for hints, I was just curious, never saw this map before (but also I'm not doing crazy research in algebraic NT :smile:).

[Michał Staromiejski]

Junyan Xu said:

Maybe your myMap'(_fact<n>) could be private?

Do we have similar patterns in mathlib?

[Junyan Xu]

Maybe docs#LinearMap.detAux / traceAux is somewhat similar (they're not private though)

[Michał Staromiejski]

Thanks. Created PR #21571 with auxiliary results having normalizedTrace' in the names, but I can also name the raw function normalizedTraceAux and the results accordingly, WDYT?

[Junyan Xu]

Aux is more indicative IMO.

[Jz Pan]

Michał Staromiejski said:

Tate's_t then? :zany_face:

TateT in Mathematica's convention, just like WeierstrassP :joy:

Oh, but TateT could also be Tate's module $T$