determinant of "restrict scalars" map

[kbuzzard]

If A,B are commutative rings, B is a finite free A-algebra and M is a finite free B-module (think A=reals, B=complexes, M=f.d. complex vector space), and if phi:M->M is B-linear, then it's also A-linear (think: a C-linear map C^n -> C^n is also R-linear as a map R^{2n} -> R^{2n}). So it makes sense to talk about det_B(phi) and det_A(phi), and if you think about the case where phi is just scalar multiplication by a real number r then you see that these numbers are different: one is r^n and the other is r^{2n}. In general what's true is that det_A(phi) is the norm from B to A of det_B(phi), where "norm b" here means "consider multiplication by b as an A-linear map B -> B and take its determinant".

One proof of this claim is: choose an A-basis for B, choose a B-basis for M, construct an A-basis for M by multiplying them together, and reduce to a calculation about the det of block diagonal matrices being the product of the dets of the blocks.

This is the sorry in FLT.Mathlib.RingTheory.Norm.Defs.

[YaelDillies]

See https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Determinant.20under.20restriction.20of.20scalars and https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/LinearMap.2Edet.20and.20restrictScalars