Determinant under restriction of scalars

Stream: Is there code for X?

[Yaël Dillies]

Do we know that docs#LinearMap.det and docs#LinearMap commute?

import Mathlib.LinearAlgebra.Determinant

namespace LinearMap
variable {M A B : Type*} [CommRing A] [CommRing B] [AddCommGroup M] [Algebra A B] [Module A M]
  [Module B M] [IsScalarTower A B M]

lemma det_restrictScalars (f : M →ₗ[B] M) : algebraMap A B (f.restrictScalars A).det = f.det := sorry

[Yaël Dillies]

This result isn't in mathlib, but I suspect it will be immediate from some very general result about mapping det under ring homs

[Adam Topaz]

don't you need some finiteness assumptions for this to be true? (given that det is a junk value when there is no finite basis)

[Yaël Dillies]

Sure yes, can assume that (in my case, A = ℝ, B = M = ℂ)

[Andrew Yang]

docs#RingHom.map_det ?

[Yaël Dillies]

Thanks! I should be able to take it from there

[Junyan Xu]

Yury G. Kudryashov said:

So, the goal should be LinearMap.det (f.restrictScalars R) = Algebra.norm R (LinearMap.det f) which isn't in the library yet.

[Junyan Xu]

The matrices of f over A and B are not of the same dimension ...

[Kevin Buzzard]

Is this even true? If A = ℝ and B = ℂ but M=ℂ^n then multiplication by $r\in\R$ has got determinant $r^n$ but its restriction of scalars is $\R^{2n}\to\R^{2n}$ so has det $r^{2n}$.

[Junyan Xu]

You're replying to Yaël's original post, not to me (or Yury), right?

[Yaël Dillies]

Updated statement:

import Mathlib.RingTheory.Norm.Defs

namespace LinearMap
variable {M A B : Type*} [CommRing A] [CommRing B] [AddCommGroup M] [Algebra A B] [Module A M]
  [Module B M] [IsScalarTower A B M] [Module.Finite A B] [Module.Finite B M]

lemma det_restrictScalars (f : M →ₗ[B] M) : (f.restrictScalars A).det = Algebra.norm A f.det := by
  sorry

[Junyan Xu]

A lot better now that the dot notation works for LinearMap.det ...

[Kevin Buzzard]

What does Algebra.norm mean if we're not free? If it's a junk value then this may again be wrong. I would believe something like this under the extra hypotheses that M is projective (eg free) over B and B is projective over A (eg if A and B were both fields)

[Kevin Buzzard]

docs#Algebra.norm

[Kevin Buzzard]

So that definition returns junk unless $B$ is f.g. free over $A$, which is quite unlike mathlib: the correct generality is that $B$ is a f.g. projective $A$-module, and it works like this: one definition of projective is "direct summand of free" so writte $B\oplus C=A^n$ and now given an $A$-linear endomorphism of $B$ (e.g. multiplication by an element of $B$), extend to an endomorphism of $B\oplus C$ by using the identity on $C$, and now you have an endomorphism of $A^n$ so just take its determinant. This is independent of choice of $C$ because on $(B\oplus C)\oplus(B\oplus C')$ the endomorphisms $(\phi\oplus 1)\oplus(1\oplus 1)$ and $(1\oplus 1)\oplus(\phi\oplus 1)$ are conjugate and hence have the same determinant.

[Kevin Buzzard]

But the bottom line is that right now with current definitions you're also going to need freeness hypotheses before the theorem is provable.

[Andrew Yang]

Also see #mathlib4 > Algebra.norm for projective algebra extensions

[Junyan Xu]

Yeah, Algebra.norm has junk value 1 when the module is not free. And it would be an interesting project to generalize it to finite projective modules. I think traces work for arbitrary finite projective modules, but norms only work for those with constant rank. The way traces work is $\mathrm{End}_R(P)\simeq P^\vee\otimes_R P\to R$, and the way norms work is $\mathrm{End}_R(P)\to\mathrm{End}_R(\wedge^d_R P)\simeq\mathrm{End}_R(R)\simeq R$ where $d$ is the constant rank of $P$ and $\wedge^d_R$ denotes the $d$ th exterior power over $R$.

This definition of norm seems to give an accessible proof to the desired result (Edit: after reviewing the other thread, I think @Antoine Chambert-Loir's suggestion to formalize Determinants of block matrices is still the simplest and the way to move forward; once that's done we can easily generalize to projective modules by considering localizations at primes): consider the isomorphisms $B\otimes_A(\wedge^{dn}_A P)\simeq\wedge^{dn}_B(B\otimes_A P)\simeq\wedge^{dn}_B(P^n)\simeq(\wedge^d_B P)^{\otimes n}$ where $n=[B:A]$ and $d=[P:B]$. (The last isomorphism is by repeated application of this.) These are free $B$-modules of rank 1, so any B-endomorphism is scalar multiplication by some $b\in B$. Consider the endomorphisms induced by f, a B-endomorphism of P: on the LHS, restrict scalars to A and take the determinant, we get Algebra.norm b = (f.restrictScalars A).det ^ n. On the RHS, we simply get b = f.det ^ n. Combining both we get the desired result up to taking the $n$ th root. To get rid of $n$ I think you might reduce to some universal case with polynomial rings over Z, embed into some algebraically closed field where matrices have Jordan normal form, and also reduce to local rings where projective modules are flat. Haven't worked out all details though.

[Junyan Xu]

norms only work for those with constant rank

Hmm I think I'm wrong. Kevin's construction does work in the nonconstant rank case.

[Antoine Chambert-Loir]

Two remarks, I'm not sure I understand all of the above.

1. In nonconstant rank, one has to decide about what the norm should be. Presumably, the geometric vision of schemes calls for something local, and the only bizarre thing that will happen is that the norm will be locally polynomial, homogeneous, of some degree, but that degree is not a given integer.
2. For transitivity of norms, I don't understand how the issue of an additional $n$-th power shows up. I have written a proof of transitivity of norms in notes for students, there are probably mistakes in it, but that problem didn't appear. I presume that you try to do two things at once.

[Junyan Xu]

I've proven det_restrictScalars (and Algebra.norm_norm) for finite free modules in 230 lines by formalizing Silvester's paper; hopefully I'll open a PR soon. Instead of working in a commutative Subring of the matrix ring, I work with a RingHom from a commutative ring to the matrix ring . It's a bit annoying that there seems to be a DecidableEq diamond issue when Subtype and Prod interact, and as a result I have to use some convert. One symptom is that map_one doesn't work (generates a OneHomClass goal) probably because 1 : Matrix m m S is defined using DecidableEq m. Zulip thinks my proof is 1000+ characters too long so I'll just post a web editor link.

[Junyan Xu]

Re @Antoine Chambert-Loir's comments:

1. it's just a bit disappointing that we can define the trace for a f.g. proj. module without realizing it as a direct summand of a f.g. free module, but can't do the same for the norm.
2. I've tried to directly construct an isomorphism $\wedge^{dn}_A P\simeq\wedge^n_A(\wedge^d_B P)$ that is equivariant w.r.t. the action of some B-linear endomorphism of P, which would give the det_restrictScalars result without the n-th power. Given that $n=[B:A]$ and $d=[P:B]$, both sides are free A-modules of rank 1, but I don't even know a way to construct an isomorphism when n=d=2 that always works. Since the isomorphism is required to be equivariant, a natural attempt is to use multilinear maps of the form $(p_1,p_2,p_3,p_4)\mapsto(p_1\wedge p_2)\wedge(p_3\wedge p_4)$. However, this map isn't alternating: if we choose a basis $\{e_1,e_2\}$ of P over B and assume there's a basis $\{1,b\}$ of B over A, then $(e_1,e_2,be_1,e_2)$ should map to 0 due to repeated $e_2$, but is mapped to $e\wedge be$, where $e:=e_1\wedge e_2$; since $\{e\}$ is an B-basis of $\wedge^d_B P$, $\{e,be\}$ is an A-basis, so $\{e\wedge be\}$ is an A-basis of $\wedge^n(\wedge^d_B P)$ and so $e\wedge be\ne 0$. Therefore, we have to combine several permuted version of this map to produce an alternating map, and even then it's not clear it would map a generator to a generator. Given that Silvester's result is also more general (since there are $\lfloor n^2/4\rfloor+1 \gg n$ -dimensional commutative subalgebras in the nxn matrix algebra), I didn't pursue this approach further.

[Junyan Xu]

#19978

[Johan Commelin]

I had one question: https://github.com/leanprover-community/mathlib4/pull/19978#discussion_r1886340006
But it shouldn't block this PR

[Antoine Chambert-Loir]

I don't think the answer is positive. With a 2x2 matrix with complex entries viewed as 2x2 real matrices, that would say $|ad-bc|^2 = |a|^2|d|^2-|b|^2|c|^2$.

[Johan Commelin]

Hah! Thanks for putting me straight!

[Junyan Xu]

Today I realized that if $M$ is a module over a commutative semiring $R$, then $M^\vee\otimes_R M\to\mathrm{Hom}_R(M,M)$ is surjective iff $M$ is a finite projective $R$-module, and in this case the map is bijective. (I suppose this map isn't always injective but an example eludes me at the moment.) Therefore, finite projective modules are indeed the natural class of modules for the trace.

[Johan Commelin]

Cool! Did you already formalize it?

[Junyan Xu]

The "only if" part can be made quite short (under 10 lines); it also provides a nice refactorization of the proof that an invertible module is finite projective. The proof actually only requires that LinearMap.id lies in the range; to demystify it, notice that M being finite projective is equivalent to the existence of a surjective map Rⁿ → M with a splitting M → Rⁿ. If you write a preimage of LinearMap.id as ∑ i, f i ⊗ m i, then the m i provides the first map and the f i provides the second.

The "if" direction is lTensorHomEquivHomLTensor for finite free modules. It's interesting that this generalizes in various ways: $M^\vee\otimes_R N\to\text{Hom}_R(M,N)$ is an isomorphism if $M$ is finite projective, or if $N$ is projective and either $M$ or $N$ is finite.

I also found yesterday that the observation has been made before.

[Dean Young]

(deleted)

[Dean Young]

At first I suggested something to do with effective descent, but I notice using @Junyan Xu's comment that there is another convenient feature of projective modules that is probably better:

For a smooth Lie group G with tangent space 𝖌, Ω¹(G) is is a projective module with linear dual 𝔤.

Ω¹(G,𝔤) is contractible onto the Maurer-Cartan form, which I don't fully understand. But in any case, Ω¹(G,𝔤) is also the internal hom of 𝔤 with itself because of the projective property, and one obtains elements of it, dμₓ, from d applied to the action of G on Ω⁰(G).

A resulting action of G on Ω¹(G,𝖌) is A to the sum of xAx⁻¹ and xdx⁻¹. If it's contractinle, then it is an EG and it bears a closer relationship with G-principal bundles than the typical functorial construction of EG because it classifies bundles with connection (it is also homotopic to the usual EG in a spaces over BG).

This is something that uses the theorem above about projective modules and the projective assumption, and which is maybe also related to the characteristic polynomial of a connection (t ↦ det(I + tA) as a function on [0,1] (edit: it's rather the characteristic polynomial of the curvature form.

[Dean Young]

I think a lot of this theory works for the setting of algebraic groups with a projective module as their tangent space. Iwould be keen to hear about how the power of t in the characteristic polynomial interacts with the grade of the lie algebra valued differential forms in that setting.

[Dean Young]

Evidently it's the characteristic polynomial of the curvature form that is more commonly considered, in Chern-Weil theory. It is an image of the Chern classes chₙ : [BGLᵣ(ℂ),Bⁿℤ] ≅ { ℤ if n is even, 0 otherwise, so that the integral cohomology of BGLᵣ(ℂ) ≃ Grass(∞,r) is ℤ[[x]] (or ℤ[x], but then one can't have it as [BGLᵣ(ℂ),ΠₙBⁿℤ]). This has an image in [BGLₙ(ℂ),Bᵈℂ] which can be expressed as the characteristic polynomial of the curvature form Dω where ω is the Maurer-Cartan form or more generally the Ehresman connection 1-form.

[Dean Young]

Note that there is such thing as a topological connection which is simply enough to do parallell transport using an internal universe.

I think I must have made many errors here but the main thing is that the characteristic polynomial of the curvature. It's possible one of my mistakes is that the Maurer-Cartan form is flat as far as I know, in which case one might try a connection 1-form on a G-principal bundle instead.