algebra_iso_of_iso — Mathlib

English

If an algebra morphism f has its carrier part f.f an isomorphism, then f is an isomorphism of algebras.

Русский

Если морфизм алгебр f имеет носительную часть f.f — изоморфизм, то сам f является изоморфизмом алгебр.

LaTeX

$$$$\\forall f:\\,A \\to B,\\ [IsIso(f.f)] \\Rightarrow IsIso(f).$$$$

Lean4

/-- Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.
-/
theorem algebra_iso_of_iso {A B : Algebra T} (f : A ⟶ B) [IsIso f.f] : IsIso f :=
  ⟨⟨{ f := inv f.f, h := by simp }, by cat_disch⟩⟩

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