quotientKerAlgEquivOfRightInverse

English

If f: A → B has a right inverse g: B → A (i.e., f ∘ g = id_B), then A/(ker f) ≃ₐ B.

Русский

Если у гомоморфизма f: A → B есть правый обратный g: B → A (f ∘ g = id_B), то A/(ker f) ≃ₐ B.

LaTeX

$$$\exists\; g: B \to A\; (f \circ g = \mathrm{id}_B) \Rightarrow (A/\ker f) \cong_A B$$$

Lean4

/-- The **first isomorphism** theorem for algebras, computable version. -/
@[simps!]
def quotientKerAlgEquivOfRightInverse {f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g f) :
    (A ⧸ RingHom.ker f) ≃ₐ[R₁] B :=
  { RingHom.quotientKerEquivOfRightInverse hf, kerLiftAlg f with }

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