English
In a commutative ring, A.LinearDisjoint B ↔ B.LinearDisjoint A.
Русский
В коммутативном кольце A.LinearDisjoint B ⇔ B.LinearDisjoint A.
LaTeX
$$$A.LinearDisjoint B \iff B.LinearDisjoint A$$$
Lean4
/-- Images of two `R`-algebras `A` and `B` in `A ⊗[R] B` are linearly disjoint. -/
theorem include_range (A : Type v) [Semiring A] (B : Type w) [Semiring B] [Algebra R A] [Algebra R B] :
(Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B).range.LinearDisjoint
(Algebra.TensorProduct.includeRight : B →ₐ[R] A ⊗[R] B).range :=
by
rw [Subalgebra.LinearDisjoint, Submodule.linearDisjoint_iff]
change
Function.Injective <|
Submodule.mulMap (LinearMap.range Algebra.TensorProduct.includeLeft)
(LinearMap.range Algebra.TensorProduct.includeRight)
rw [← Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap]
exact LinearEquiv.injective _
