English
For a linear isomorphism e: M ≃ M, trace is invariant under conjugation: tr_N(e·f·e^{-1}) = tr_M(f).
Русский
Для линейного изоморфизма e: M ≃ M след сохраняется под конъюгацией: tr_N(e f e^{-1}) = tr_M(f).
LaTeX
$$$ \operatorname{trace}_R N (e \cdot f \cdot e^{-1}) = \operatorname{trace}_R M f. $$$
Lean4
@[simp]
theorem trace_conj' (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) : trace R N (e.conj f) = trace R M f := by
classical
by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)
· obtain ⟨s, ⟨b⟩⟩ := hM
haveI := Module.Finite.of_basis b
haveI := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
haveI := Module.Finite.of_basis (b.map e)
haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe, LinearEquiv.self_trans_symm,
LinearEquiv.refl_toLinearMap, id_comp]
· rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
rintro ⟨s, ⟨b⟩⟩
exact
hM
⟨s.image e.symm,
⟨(b.map e.symm).reindex ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩
