hasAffineProperty — Mathlib

English

Let R → S be a ring hom. The morphism between spectra, Spec.map φ, is integral if and only if φ is an integral ring hom.

Русский

Пусть R → S — гомоморфизм колец. Отображение спектра Spec.map φ интегрально тогда и только тогда, когда φ сам по себе интегрален как гомоморфизм колец.

LaTeX

$$$IsIntegralHom(\mathrm{Spec\ map}\ φ) \iff φ.hom.IsIntegral$$$

Lean4

instance hasAffineProperty :
    HasAffineProperty @IsIntegralHom fun X _ f _ ↦ IsAffine X ∧ RingHom.IsIntegral (f.app ⊤).hom :=
  by
  change HasAffineProperty @IsIntegralHom (affineAnd RingHom.IsIntegral)
  rw [HasAffineProperty.affineAnd_iff _ RingHom.isIntegral_respectsIso
      RingHom.isIntegral_isStableUnderBaseChange.localizationPreserves.away RingHom.isIntegral_ofLocalizationSpan]
  simp [isIntegralHom_iff]

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