map — Mathlib

English

Another preservation result: the linear disjointness of A with L transfers through a chain of algebra homomorphisms.

Русский

Еще одно сохранение: линейная независимость A и L переносится через цепочку алгебраических гомоморфизмов.

LaTeX

$$$\\text{map'''} : A.LinearDisjoint L \\rightarrow (A.map f).LinearDisjoint L$$$

Lean4

/-- Linear disjointness of intermediate fields is preserved by algebra homomorphisms. -/
theorem map (H : A.LinearDisjoint B) {K : Type*} [Field K] [Algebra F K] (f : E →ₐ[F] K) :
    (A.map f).LinearDisjoint (B.map f) :=
  linearDisjoint_iff'.2 ((linearDisjoint_iff'.1 H).map f f.injective)

Похожие утверждения