English
If H = M.LinearDisjoint N and f is an injective algebra homomorphism, then the images (M.map f) and (N.map f) are linearly disjoint in the target.
Русский
Если H = M.LinearDisjoint N и f — инъективный алгебраический гомоморфизм, тогда образы (M.map f) и (N.map f) линейно несовместны в целевом поле/алгебре.
LaTeX
$$If H: M.LinearDisjoint N and hf: Function.Injective f, then (M.map f).LinearDisjoint (N.map f).$$
Lean4
/-- Linear disjointness is preserved by injective algebra homomorphisms. -/
theorem map (H : M.LinearDisjoint N) {T : Type w} [Semiring T] [Algebra R T] {F : Type*} [FunLike F S T]
[AlgHomClass F R S T] (f : F) (hf : Function.Injective f) : (M.map f).LinearDisjoint (N.map f) :=
by
rw [linearDisjoint_iff] at H ⊢
have : _ ∘ₗ (TensorProduct.congr (M.equivMapOfInjective f hf) (N.equivMapOfInjective f hf)).toLinearMap = _ :=
M.mulMap_map_comp_eq N f
replace H : Function.Injective ((f : S →ₗ[R] T) ∘ₗ mulMap M N) := hf.comp H
simpa only [← this, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] using H
