English
Over a reduced ring, if f and g commute and g − μ is nilpotent, then tr(fg) = μ tr(f).
Русский
Над редуцированным кольцом, если f и g коммутируют и g − μ является нильпотентом, то tr(fg) = μ tr(f).
LaTeX
$$$ [IsReduced\ R] \Rightarrow tr(f g) = \mu \; tr(f) \quad\text{если } [f,g]=0 \text{ и } (g-\mu I)^{n}=0. $$$
Lean4
theorem trace_comp_eq_mul_of_commute_of_isNilpotent [IsReduced R] {f g : Module.End R M} (μ : R) (h_comm : Commute f g)
(hg : IsNilpotent (g - algebraMap R _ μ)) : trace R M (f ∘ₗ g) = μ * trace R M f :=
by
set n := g - algebraMap R _ μ
replace hg : trace R M (f ∘ₗ n) = 0 :=
by
rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]
refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)
exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)
have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl
have : f ∘ₗ algebraMap R _ μ = μ • f := by ext;
simp -- TODO Surely exists?
rw [hμ, comp_add, map_add, hg, add_zero, this, LinearMap.map_smul, smul_eq_mul]
-- This result requires `Mathlib/RingTheory/TensorProduct/Free.lean`.
-- Maybe it should move elsewhere?
