English
Under a FractionRing-equivalence, traceDual commutes with the induced map; i.e., traceDual is preserved by the equivalence.
Русский
При эквивалентности дробной кольцевой теории дуальность по следу сохраняется под соответствующим отображением.
LaTeX
$$$\text{traceDual A (FractionRing A) I}.map(\FractionRing algEquiv B L) = \text{traceDual A K} (I.map(\FractionRing algEquiv B L)).$$$
Lean4
theorem map_equiv_traceDual [IsDomain A] [IsFractionRing B L] [IsDomain B] [FaithfulSMul A B]
(I : Submodule B (FractionRing B)) :
(traceDual A (FractionRing A) I).map (FractionRing.algEquiv B L) =
traceDual A K (I.map (FractionRing.algEquiv B L)) :=
by
change
Submodule.map (FractionRing.algEquiv B L).toLinearEquiv.toLinearMap _ =
traceDual A K (I.map (FractionRing.algEquiv B L).toLinearEquiv.toLinearMap)
rw [Submodule.map_equiv_eq_comap_symm, Submodule.map_equiv_eq_comap_symm]
ext x
simp only [traceDual, Submodule.mem_comap, Submodule.mem_mk]
apply (FractionRing.algEquiv B L).forall_congr
simp only [restrictScalars_mem, LinearEquiv.coe_coe, AlgEquiv.coe_symm_toLinearEquiv, traceForm_apply, mem_one,
AlgEquiv.toEquiv_eq_coe, EquivLike.coe_coe, mem_comap, AlgEquiv.symm_apply_apply]
refine fun {y} ↦ (forall_congr' fun hy ↦ ?_)
rw [Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv (FractionRing.algEquiv B L).toRingEquiv]
swap
· ext
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _
simp only [AlgEquiv.toRingEquiv_eq_coe, map_mul, AlgEquiv.coe_ringEquiv, AlgEquiv.apply_symm_apply,
← AlgEquiv.symm_toRingEquiv, AlgEquiv.algebraMap_eq_apply]
