botEquivOfInjective — Mathlib

English

If the algebra map algebraMap R A is injective, then the bottom subalgebra is algebraically equivalent to R.

Русский

Если алгебра_map R A инъективен, то нижняя подалгебра изоморфна R как R-алгебра.

LaTeX

$$$ \\mathrm{botEquivOfInjective} (h) : (\\bot : \\mathrm{Subalgebra} R A) \\simeq_{\\! R} R $$$

Lean4

/-- The bottom subalgebra is isomorphic to the base ring. -/
noncomputable def botEquivOfInjective (h : Function.Injective (algebraMap R A)) : (⊥ : Subalgebra R A) ≃ₐ[R] R :=
  AlgEquiv.symm <|
    AlgEquiv.ofBijective (Algebra.ofId R _)
      ⟨fun _x _y hxy => h (congr_arg Subtype.val hxy :), fun ⟨_y, x, hx⟩ => ⟨x, Subtype.eq hx⟩⟩

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