English
If f: S →+* Matrix(n,n,R) and f.det denotes determinant in S-linear context, then the determinant after restricting scalars equals the norm of that determinant.
Русский
Пусть f: S →+* Mat_n(R). Детеминант после ограничения скалярности равен норме детерминанта в контексте расширения.
LaTeX
$$$\\det_R(f|_R) = \\mathrm{Norm}_{R}^{S}(\\det_S f).$$$
Lean4
theorem det_restrictScalars [AddCommGroup A] [Module R A] [Module S A] [IsScalarTower R S A] [Module.Free S A]
{f : A →ₗ[S] A} : (f.restrictScalars R).det = Algebra.norm R f.det := by
classical
nontriviality R
nontriviality A
have := Module.nontrivial S A
let ⟨ιS, bS⟩ := Module.Free.exists_basis (R := R) (M := S)
let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)
have := bS.index_nonempty
have := bA.index_nonempty
cases fintypeOrInfinite ιS; swap
·
rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
cases fintypeOrInfinite ιA; swap
·
rw [det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA), map_one,
det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
rw [Algebra.norm_eq_matrix_det bS, ← AlgHom.coe_toRingHom, ← det_toMatrix bA, det_det, ←
det_toMatrix (bS.smulTower' bA), restrictScalars_toMatrix, RingHom.coe_coe]
