isLocalHom_of_isIso — Mathlib

English

If f: R → S is an isomorphism in CommRingCat (i.e., an isomorphism in the category of commutative rings), then f.hom is a local homomorphism.

Русский

Если f: R → S является изоморфизмом в CommRingCat, то f.hom — локальный гомоморфизм.

LaTeX

$$$\text{IsLocalHom} f.hom$ for any isomorphism $f$.$$

Lean4

@[instance 100]
theorem isLocalHom_of_isIso {R S : CommRingCat} (f : R ⟶ S) [IsIso f] : IsLocalHom f.hom :=
  isLocalHom_of_iso (asIso f)

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