English
If e is a ring equivalence compatible with algebra maps, then trace_A C x equals trace_B C x after transporting via e.
Русский
Если e — кольцевое эквивалентство совместимо с алгебраическими отображениями, тогда след A C x равен следу B C x после переноса через e.
LaTeX
$$$\\operatorname{trace}_{A,C}(x) = \\operatorname{trace}_{B,C}(e x)$ under compatibility$$
Lean4
theorem trace_eq_of_ringEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C] [Algebra A C] [Algebra B C]
(e : A ≃+* B) (he : (algebraMap B C).comp e = algebraMap A C) (x) : e (Algebra.trace A C x) = Algebra.trace B C x :=
by
classical
by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
· obtain ⟨s, ⟨b⟩⟩ := h
letI : Algebra A B := RingHom.toAlgebra e
letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
rw [Algebra.trace_eq_matrix_trace b,
Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
rw [AddMonoidHom.map_trace]
congr
ext i j
simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply,
LinearMap.zero_apply, map_zero]
intro ⟨s, ⟨b⟩⟩
exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩
