isLocalHom_of_iso — Mathlib

English

If f: R → S is an isomorphism of commutative rings, then f.hom is a local homomorphism.

Русский

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

LaTeX

$$$\text{IsLocalHom}(f.hom)$ whenever $f$ is an isomorphism.$$

Lean4

theorem isLocalHom_of_iso {R S : CommRingCat} (f : R ≅ S) : IsLocalHom f.hom.hom :=
  {
    map_nonunit := fun a ha => by
      convert f.inv.hom.isUnit_map ha
      simp }
    -- see Note [lower instance priority]

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