SpecMap_iff — Mathlib

English

For a ring hom f, IsFinite Spec.map f is equivalent to f.hom.Finite.

Русский

Для гомоморфизма колец f, IsFinite Spec.map f эквивалентно f.hom.Finite.

LaTeX

$$$SpecMap_iff\\ (f : R\\to S) : IsFinite (Spec.map f) \\iff f.hom.Finite$$$

Lean4

theorem SpecMap_iff {R S : CommRingCat.{u}} (f : R ⟶ S) : IsFinite (Spec.map f) ↔ f.hom.Finite := by
  rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), and_iff_right (by infer_instance),
    RingHom.finite_respectsIso.arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f)]

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