LinearMap.det and restrictScalars

Stream: maths

[Yury G. Kudryashov]

Do we have a proof of LinearMap.det (f.restrictScalars R) = LinearMap.det (LinearMap.mul R A (LinearMap.det f))? [I hope, I've got the formula right]. I can't find it using loogle, so probably not. How do I prove it in the right generality? The proof that first comes to my mind is to use uniqueness of det, but probably this puts too many requirements on R and/or A.

[Yury G. Kudryashov]

Also, do we/should we have a name for LinearMap.det (LinearMap.mul R A x)?

[Antoine Chambert-Loir]

It would be a nice result to add, as a particular case that the determinant of a block matrix with commuting blocks can be computed as the determinant of the determinant.
https://doi.org/10.2307/3620776

[Junyan Xu]

LinearMap.det (LinearMap.mul R A x) is Algebra.norm R x (docs#Algebra.norm).

[Antoine Chambert-Loir]

Yes, but does mathlib have transitivity of norm?

[Riccardo Brasca]

Not in general

[Riccardo Brasca]

Well, maybe yes https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Norm/Basic.html#Algebra.norm_norm

[Antoine Chambert-Loir]

(That's only for field extensions.)

[Yury G. Kudryashov]

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

[Antoine Chambert-Loir]

Indeed, and that's the main application I know of the paper linked into my earlier answer. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/LinearMap.2Edet.20and.20restrictScalars/near/467036489

[Yury G. Kudryashov]

I downloaded the paper but I won't have time to formalize it at least until the next weekend.

[Yury G. Kudryashov]

I want to have it to show that any complex vector space has a natural orientation.

[Yury G. Kudryashov]

Of course, I can prove it for Complex and Real, but this isn't the way.

[Junyan Xu]

I have a formalization of Silvester's paper now: #Is there code for X? > Determinant under restriction of scalars @ 💬

[Yury G. Kudryashov]

Thank you!