linearIndependent_algHom_toLinearMap

English

Under suitable algebraic hypotheses, the map sending an algebra homomorphism to its linear map is linearly independent.

Русский

При соответствующих алгебраических условиях отображение гомоморфизма алгебры в линейный отображение линейно независимо.

LaTeX

$$$\\mathrm{LinearIndependent}_K(\\mathrm{AlgHom.toLinearMap})$$$

Lean4

@[stacks 0CKM]
theorem linearIndependent_algHom_toLinearMap (K M L) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L]
    [IsDomain L] [Algebra K L] : LinearIndependent L (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) :=
  by
  apply LinearIndependent.of_comp (LinearMap.ltoFun K M L)
  exact
    (linearIndependent_monoidHom M L).comp (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
      (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

Похожие утверждения