Algebra.norm for projective algebra extensions

Stream: mathlib4

[Richard Hill]

I suggest introducing a more general version of Algebra.norm. Currently, this definition requires an R-algebra S which is f.g. and free as an R-module, but one can define the norm when S is f.g. and projective, rather than free.

This would be useful for example in the following setup: L is a finite extension of a number field or function field K; R is a Dedekind domain with field of fractions K and S is the integral closure of R in L. We currently have no norm map from S to R apart from the special cases where S is a free R-module, but S is always projective over R.

I suggest something like this:

import Mathlib

section projective_determinant

variable (R : Type) [CommRing R] (M: Type) [AddCommGroup M] [Module R M] [Module.Finite R M] [hM : Module.Projective R M]

lemma Module.Projective.finite_split : ∃ n : ℕ, ∃ s : (Fin n → R) →ₗ[R] M, ∃ i : M →ₗ[R] (Fin n → R),
    s ∘ₗ i = LinearMap.id := by
  obtain ⟨n,s,hs⟩ := Module.Finite.exists_fin' R M
  obtain ⟨i,hi⟩ := Module.projective_lifting_property s LinearMap.id hs
  use n,s,i


variable {R M}

/--
The "determinant" of a linear map `φ : P →ₗ[R] P`, where `P` is a finitely generated
projective `R`-module.

This is defined as follows. There is a module `Q` such that
`P ⊕ Q` is isomorphic to the free module `F := (Fin n → R)`.
The determinant of `φ` is defined to be the
determinant `φ ⊕ id : F →ₗ[R] F`.
-/
noncomputable
def projectiveDet (φ : M →ₗ[R] M) : R := by
  have h₁ := Module.Projective.finite_split R M
  let n := h₁.choose
  have h₂ := h₁.choose_spec
  let s := h₂.choose
  have h₃ := h₂.choose_spec
  let i := h₃.choose
  let Φ : (Fin n → R) →ₗ[R] (Fin n → R) := 1 - i.comp s + i.comp (φ.comp s)
  exact LinearMap.det Φ


/-
# TODO :
1. this is well defined, i.e. doesn't depend on a choice of splitting `P ⊕ Q ≃ Free`.
2. this coincides with the usual determinant for free modules,
3. This is compatible with base change,
  i.e. the determinant of `φ ⊗ id : P ⊗ S →ₗ[S] P ⊗ S` is `algebaMap R S` of the determinant of `φ`.
4. `projectiveDet (φ ∘ₗ ψ) = ...`
5. `projectiveDet 0 = 0` if `P` is nontrivial.
6. `projectiveDet LinearMap.id = 1`
-/

end projective_determinant

section projective_norm

variable (R S : Type) [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S]

noncomputable
def Algebra.norm' : S →*₀ R where
  toFun s := projectiveDet (Algebra.lmul R S s)
  map_zero' := sorry
  map_one' := sorry
  map_mul' := sorry


end projective_norm

Is this something which is worth pursuing?

[Kevin Buzzard]

We have the norm from L to K right? Is it not hard to prove that the norm of something in the integral closure of S is still integral over S and hence presumably in the integral closure of R in K?

On the other hand, what you're doing is strictly more general, and I've used your definition in the past (for characteristic power series of projective Banach modules). NB the proof that it's independent of Q is by considering P+Q+P+Q' and the fact that phi+1+1+1 and 1+1+phi+1 are conjugate so have the same char poly. If you're sticking to the f.g. projective case you could even define char poly this way (that way you get trace and norm).

[Richard Hill]

Thanks for your comments.

Yes, the norm from L to K is in Mathlib because K is a field, so L is free over K. One could simply prove that this norm maps S to R. This is often done prime-by-prime, using the fact that locally S is locally free over R. But that would mean that L and K come into the definition of the norm from S to R, which could make the notation more awkward.

Another way of defining the norm from S to R would be (up to a sign) a power of the constant term in the minimal polynomial. This is the most direct method, but it seems like an odd way to define the norm.

The definition which I sketched out is more general, as it does not require R and S to be Dedekind rings, and it does not mention K or L.

I'm a bit confused by your comment on char polys. The char poly does depend on the splitting, since its degree depends on the rank of $P \oplus Q$. If one wanted to define the trace by the same trick, then I guess one should take the trace of \phi \oplus (0 : Q \to Q) instead of \phi \oplus id.

[Kevin Buzzard]

The char power series (starts 1+aX+... instead of X^n+aX^(n-1)+...) is independent of splitting. I agree that there should be a definition independent of L and K and mathematically your plan sounds fine to me.

[Andrew Yang]

We have docs#Algebra.intNorm that came from flt-regular as it is more easily defined that way. But I agree this definition is better.

[Richard Hill]

@Kevin Buzzard ok, thanks for clarifying; I thought you were talking about charpoly. I assume the characteristic power series is something like $\det (1 + x \smul \phi)$, although I'm not familiar with the definition. If one defined the determinant to be the leading coefficient, would this be compatible with usual determinants (in the case that the usual determinant is 0)?

@Andrew Yang Thanks for pointing that out. I have some slight issues with Algebra.intNorm. First, it assumes separability, which isn't needed. More importantly, it is not general enough to be used in the definition of Ideal.spanNorm. Because of this, it is not used in Ideal.relNorm. Consequently, Ideal.relNorm is only defined when S is a free R-module (where R \to S is an extension of Dedekind domains). It would be nice to use Ideal.relNorm in more general situations (eg. to state the theorems of class field theory).

[Andrew Yang]

The reason it assumes separability is that mathlib does not know (or at least did not know at the time) how norm behaves under purely inseparable extensions. Once we have the general version of docs#Algebra.norm_eq_prod_embeddings we can remove that easily.

As for ideal norms, In flt-regular, we had Ideal.spanIntNorm to deal with this exact situation. This approach works for arbitrary finite extension of integrally closed domains (which are not necessarily projective) but I'm not sure if we need this generality or not.

[Richard Hill]

Thank you, it looks like Ideal.spanIntNorm solves the problem. Will this replace Ideal.relNorm in Mathlib?

[Andrew Yang]

I don't think anyone has active plans for it. The thing is Algebra.norm (or the suggestion you raised) and Algebra.intNorm aren't strictly generalisations of each other and it is not clear to me if we should drop either of them.

[Richard Hill]

Yes I see that people might want to keep Ideal.spanNorm, but I can't see an argument for Ideal.relNorm. It only applies to Dedekind domains, so Ideal.spanIntNorm generalizes it (or at least this will be true when the separability condition is removed).