instIsClosedImmersionLiftSchemeId

English

If f is an affine morphism (IsAffineHom) then f is IsSeparated.

Русский

Если f есть аффинное отображение (IsAffineHom), то оно разделено.

LaTeX

$$$[\text{IsAffineHom } f] \Rightarrow IsSeparated(f).$$$

Lean4

/-- Given `f : X ⟶ Y` and `g : Y ⟶ Z` such that `g` is separated, the induced map
`X ⟶ X ×[Z] Y` is a closed immersion. -/
instance [IsSeparated g] : IsClosedImmersion (pullback.lift (𝟙 _) f (Category.id_comp (f ≫ g))) :=
  by
  rw [← MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (pullback.fst f (𝟙 Y))]
  rw [←
    MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (pullback.congrHom rfl (Category.id_comp g)).inv]
  convert (inferInstanceAs <| IsClosedImmersion (pullback.mapDesc f (𝟙 _) g)) using 1
  ext : 1 <;> simp [pullback.condition]

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