English
If A,B are flat R-algebras and A ⊗_R B is a domain, there exists a field K and injective R-algebra maps from A and B into K with linearly disjoint images.
Русский
Если A и B плоские над R и A ⊗_R B — область, существует поле K и инъективные R-алгебр-мappings fa: A→K, fb: B→K с линейно раздельными образами.
LaTeX
$$$\\exists K\\; \\exists fa: A \\to_R K\\; \\exists fb: B \\to_R K\\; (fa \\text{ инъективно}) \\land (fb \\text{ инъективно}) \\land (fa(A) \\perp_L fb(B))$$$
Lean4
/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then `trace` and `algebraMap` commutes.
-/
theorem trace_algebraMap (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R B] [Module.Finite R B] (x : B) :
Algebra.trace A S (algebraMap B S x) = algebraMap R A (Algebra.trace R B x) := by
simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)), Matrix.trace, map_sum,
leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply, Matrix.diag_apply, Matrix.map_apply]
