isStableUnderBaseChange — Mathlib

English

Closed immersions are stable under base change.

Русский

Замкнутые вложения сохраняются при базовой смене.

LaTeX

$$$IsStableUnderBaseChange(IsClosedImmersion)$$$

Lean4

/-- Being a closed immersion is stable under base change. -/
instance isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsClosedImmersion :=
  by
  apply HasAffineProperty.isStableUnderBaseChange
  haveI := HasAffineProperty.isLocal_affineProperty @IsClosedImmersion
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g ⟨ha, hsurj⟩
  exact
    ⟨inferInstance,
      RingHom.surjective_isStableUnderBaseChange.pullback_fst_appTop _ RingHom.surjective_respectsIso f _ hsurj⟩

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