instMap — Mathlib

English

IsSeparated holds for Spec.map f for ring hom f: R→S (dup).

Русский

IsSeparated справедливо для Spec.map f при гомоморфизме f:R→S (дубликат).

LaTeX

$$$\forall R,S,f:\text{CommRingCat}.(R\to S),\; \text{IsSeparated}(\text{Spec.map } f).$$$

Lean4

instance (R S : CommRingCat.{u}) (f : R ⟶ S) : IsSeparated (Spec.map f) :=
  by
  constructor
  letI := f.hom.toAlgebra
  change IsClosedImmersion (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))
  rw [diagonal_Spec_map, MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion]
  exact
    .spec_of_surjective _ fun x ↦
      ⟨.tmul R 1 x, (Algebra.TensorProduct.lmul'_apply_tmul (R := R) (S := S) 1 x).trans (one_mul x)⟩

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