English
If e1:A1≃A2 and e2:B1≃B2 satisfy a compatibility with the base maps, then trace_A1 B1 x equals e1^{-1}(trace_A2 B2 (e2 x)).
Русский
Если e1: A1≃A2 и e2: B1≃B2 удовлетворяют совместимости с базовыми отображениями, то след A1 B1 x равен e1^{-1}( trace A2 B2 (e2 x) ).
LaTeX
$$$\\operatorname{trace}_{A1,B1}(x) = e1^{-1}(\\operatorname{trace}_{A2,B2}(e2 x))$ with compatibility$$
Lean4
theorem trace_eq_of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [CommRing B₁] [CommRing A₂] [CommRing B₂]
[Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
(he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) (x) :
Algebra.trace A₁ B₁ x = e₁.symm (Algebra.trace A₂ B₂ (e₂ x)) :=
by
letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra
let e' : B₁ ≃ₐ[A₁] B₂ := { e₂ with commutes' := fun _ ↦ rfl }
rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e', RingEquiv.symm_apply_apply]
rfl
