bijective_algebraMap_iff — Mathlib

English

In the setting where R is a field, the algebra map algebraMap R A is bijective if and only if the top subalgebra equals the bottom one.

Русский

При условии, что R является полем, алгебраическое отображение algebraMap R A биективно тогда и только тогда, когда верхняя подалгебра равна нижней.

LaTeX

$$$ \\text{bijective_algebraMap_iff} : \\mathrm{Function.Bijective} (\\mathrm{algebraMap} R A) \\;\\iff\\; (\\top : \\mathrm{Subalgebra} R A) = \\bot $$$

Lean4

theorem bijective_algebraMap_iff {R A : Type*} [Field R] [Semiring A] [Nontrivial A] [Algebra R A] :
    Function.Bijective (algebraMap R A) ↔ (⊤ : Subalgebra R A) = ⊥ :=
  ⟨fun h => surjective_algebraMap_iff.1 h.2, fun h => ⟨(algebraMap R A).injective, surjective_algebraMap_iff.2 h⟩⟩

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