English
Theorem map: If A is linearly disjoint from the subobject represented by B, then the image under any algebra homomorphism preserves disjointness with the image of B.
Русский
Теорема map: если A линейно неразделимо от подобъекта B, то образ A под алгебраическим гомоморфизмом сохраняет неразделимость с образом B.
LaTeX
$$$\\forall f, (A LinearDisjoint B) \\Rightarrow ((A.map f) LinearDisjoint (B.map f)).$$$
Lean4
/-- Linear disjointness of an intermediate field with a tower of field embeddings is preserved by
algebra homomorphisms. -/
theorem map' (H : A.LinearDisjoint L) (K : Type*) [Field K] [Algebra F K] [Algebra L K] [IsScalarTower F L K]
[Algebra E K] [IsScalarTower F E K] [IsScalarTower L E K] :
(A.map (IsScalarTower.toAlgHom F E K)).LinearDisjoint L :=
by
rw [linearDisjoint_iff] at H ⊢
have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
rw [← AlgHom.range_comp] at this
convert this
ext; exact IsScalarTower.algebraMap_apply L E K _
