English
A certain family of algebra homomorphisms is linearly independent over B; more precisely, the map sending an algebra hom to its linearization is linear-independent.
Русский
Определенная семья алгебраических гомоморфизмов линейно независима над полем B; отображение к линейному отображению сохраняет линейную независимость.
LaTeX
$$$\\text{LinearIndependent } B (AlgHom.toLinearMap : (A \\to_A[R] B) \\to A \\to_L[R] B)$$$
Lean4
theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Algebra R A]
[CommRing B] [IsDomain B] [Algebra R B] : LinearIndependent B (AlgHom.toLinearMap : (A →ₐ[R] B) → A →ₗ[R] B) :=
have : LinearIndependent B (LinearMap.ltoFun R A B ∘ AlgHom.toLinearMap) :=
((linearIndependent_monoidHom A B).comp ((↑) : (A →ₐ[R] B) → A →* B) fun _ _ hfg =>
AlgHom.ext fun _ => DFunLike.ext_iff.1 hfg _ :
_)
this.of_comp _
