English
Preservation under maps with field-range adjustments: if H holds, then a further map yields linear disjointness with L'.
Русский
Сохранение линейной независимости при дальнейшем отображении с изменением диапазона полей.
LaTeX
$$$H \\rightarrow \\text{(IsScalarTower...).fieldRange.LinearDisjoint L'}$$$
Lean4
/-- Linear disjointness is preserved by algebra homomorphism. -/
theorem map'' {L' : Type*} [Field L'] [Algebra F L'] [Algebra L' E] [IsScalarTower F L' E]
(H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L') (K : Type*) [Field K] [Algebra F K] [Algebra L K]
[IsScalarTower F L K] [Algebra L' K] [IsScalarTower F L' K] [Algebra E K] [IsScalarTower F E K]
[IsScalarTower L E K] [IsScalarTower L' E K] : (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L' :=
by
rw [linearDisjoint_iff] at H ⊢
have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this
rw [AlgHom.fieldRange_toSubalgebra]
convert this <;> (ext; exact IsScalarTower.algebraMap_apply _ E K _)
