isSeparated — Mathlib

English

The projective spectrum Proj 𝒜 is a separated scheme; equivalently, the diagonal morphism is a closed immersion, witnessed via an open cover and pullbacks of affine morphisms.

Русский

Проективный спектр Proj 𝒜 является отделимым схемой; эквивалентно — диагональный морфизм является камерной иммерсией, доказуемый с помощью открытой обложки и линейных отображений.

LaTeX

$$$\mathrm{Proj}(\mathcal A)\ \text{is separated}$$$

Lean4

instance isSeparated : IsSeparated (toSpecZero 𝒜) :=
  by
  refine
    ⟨IsZariskiLocalAtTarget.of_openCover
        (Pullback.openCoverOfLeftRight (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover _ _) ?_⟩
  intro ⟨i, j⟩
  dsimp [Scheme, Cover.pullbackHom]
  refine
    (MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion) (f := (pullbackDiagonalMapIdIso ..).inv)
          _).mp
      ?_
  let e₁ :
    pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
      Spec (.of <| TensorProduct (𝒜 0) (Away 𝒜 i.2) (Away 𝒜 j.2)) :=
    by
    refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 i.2) (Away 𝒜 j.2)
    · simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]; rfl
    · simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]; rfl
  let e₂ : pullback ((affineOpenCover 𝒜).f i) ((affineOpenCover 𝒜).f j) ≅ Spec (.of <| Away 𝒜 (i.2 * j.2)) :=
    pullbackAwayιIso 𝒜 _ _ _ _ rfl
  rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsClosedImmersion) _ e₁.hom, ←
    MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion) e₂.inv]
  let F : Away 𝒜 i.2.1 ⊗[𝒜 0] Away 𝒜 j.2.1 →+* Away 𝒜 (i.2.1 * j.2.1) :=
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _)) (fun _ _ ↦ .all _ _)).toRingHom
  have : Function.Surjective F := lift_awayMapₐ_awayMapₐ_surjective 𝒜 i.2.2 j.2.2 rfl i.1.2
  convert IsClosedImmersion.spec_of_surjective (CommRingCat.ofHom (R := Away 𝒜 i.2.1 ⊗[𝒜 0] Away 𝒜 j.2.1) F) this using
    1
  rw [← cancel_mono (pullbackSpecIso ..).inv]
  apply pullback.hom_ext
  · simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id, limit.lift_π,
      PullbackCone.mk_pt, PullbackCone.mk_π_app, e₂, e₁, pullbackDiagonalMapIdIso_inv_snd_fst, pullbackSpecIso_inv_fst,
      ← Spec.map_comp]
    erw [pullbackAwayιIso_inv_fst]
    congr 1
    ext x : 2
    exact
      DFunLike.congr_fun
        (Algebra.TensorProduct.lift_comp_includeLeft (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _))
            (fun _ _ ↦ .all _ _)).symm
        x
  · simp only [Iso.trans_hom, congrHom_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id, limit.lift_π,
      PullbackCone.mk_pt, PullbackCone.mk_π_app, pullbackDiagonalMapIdIso_inv_snd_snd, pullbackSpecIso_inv_snd,
      ← Spec.map_comp, e₂, e₁]
    erw [pullbackAwayιIso_inv_snd]
    congr 1
    ext x : 2
    exact
      DFunLike.congr_fun
        (Algebra.TensorProduct.lift_comp_includeRight (awayMapₐ 𝒜 j.2.2 rfl) (awayMapₐ 𝒜 i.2.2 (mul_comm _ _))
            (fun _ _ ↦ .all _ _)).symm
        x

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