English
If there exists a surjective F-linear map b : F → E, then the algebra map algebraMap F E is surjective.
Русский
Если существует сюръективное F-линейное отображение b: F → E, то алгебраMap F E сюръективен.
LaTeX
$$$\\text{If } b\\text{ is surjective, then } algebraMap F E\\;: F \\to E\\text{ is surjective}.$$$
Lean4
/-- If `E` is an `F`-algebra, and there exists a surjective `F`-linear map from `F` to `E`,
then the algebra map from `F` to `E` is also surjective. -/
theorem surjective_algebraMap_of_linearMap (hb : Surjective b) : Surjective (algebraMap F E) := fun x ↦
by
obtain ⟨x, rfl⟩ := hb x
obtain ⟨y, hy⟩ := hb (b 1 * b 1)
refine ⟨x * y, ?_⟩
obtain ⟨z, hz⟩ := hb 1
apply_fun (x • z • ·) at hy
rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one, ← smul_eq_mul,
map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul, ← Algebra.algebraMap_eq_smul_one] at hy
