Theorems · Theorem · ring theory

bijective_algebraMap_of_linearMap

∀ {F : Type u_1} {E : Type u_2} [inst : CommSemiring F] [inst_1 : Semiring E] [inst_2 : Algebra F E] (b : F →ₗ[F] E),
  Function.Bijective ⇑b → Function.Bijective ⇑(algebraMap F E)

If E is an F-algebra, and there exists a bijective F-linear map from F to E, then the algebra map from F to E is also bijective. NOTE: The same result can also be obtained if there are two F-linear maps from F to E, one is injective, the other one is surjective. In this case, use injective_algebraMap_of_linearMap and surjective_algebraMap_of_linearMap separately.

Defined in

Mathlib.Algebra.Algebra.Basic

Cited by

1 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra