finitePresentation_respectsIso — Mathlib

English

Finitely presented property is preserved under ring isomorphisms: if two rings are isomorphic, one is finitely presented over a base iff the other is.

Русский

Свойство конечного презентирования сохраняется под изоморфизмами колец: если кольца изоморфны, то одно имеет конечное презентирование над основанием тогда и другое имеет.

LaTeX

$$$\text{RingIsomorphisms preserve }\operatorname{FinitePresentation}.$$$

Lean4

/-- Being finitely-presented respects isomorphisms. -/
theorem finitePresentation_respectsIso : RingHom.RespectsIso @RingHom.FinitePresentation :=
  finitePresentation_stableUnderComposition.respectsIso fun e ↦
    .of_surjective _ e.surjective <| by simpa using Submodule.fg_bot

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