instIsStableUnderBaseChangeScheme

English

If f: X → Y is an integral morphism, then for any base change X ×_Y Y' → Y' the induced morphism remains integral.

Русский

Если f: X → Y интегрально, то при любом базисном изменении X ×_Y Y' → Y' полученное отображение остаётся интегральным.

LaTeX

$$IsStableUnderBaseChange IsIntegralHom$$

Lean4

instance : IsStableUnderBaseChange @IsIntegralHom :=
  HasAffineProperty.affineAnd_isStableUnderBaseChange (Q := RingHom.IsIntegral) hasAffineProperty
    RingHom.isIntegral_respectsIso RingHom.isIntegral_isStableUnderBaseChange

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