of_valuativeCriterion — Mathlib

English

If f is quasi-separated and satisfies ValuativeCriterion.Uniqueness, then f is separated.

Русский

Если f является квазосепарабельным и удовлетворяет ValuativeCriterion.Uniqueness, тогда f является отделимым.

LaTeX

$$$\text{QuasiSeparated}(f) \wedge \mathrm{ValuativeCriterion.Uniqueness}(f) \Rightarrow \mathrm{IsSeparated}(f)$$$

Lean4

/-- The **valuative criterion** for separated morphisms. -/
@[stacks 01L0]
theorem of_valuativeCriterion [QuasiSeparated f] (hf : ValuativeCriterion.Uniqueness f) : IsSeparated f where
  diagonal_isClosedImmersion :=
    by
    suffices h : ValuativeCriterion.Existence (pullback.diagonal f)
      by
      have : QuasiCompact (pullback.diagonal f) := AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact
      apply IsClosedImmersion.of_isPreimmersion
      apply IsClosedMap.isClosed_range
      apply (topologically @IsClosedMap).universally_le
      exact (UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h).out
    intro S
    have hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f) :=
      ⟨by simp [← S.commSq.w_assoc]⟩
    let S' : ValuativeCommSq f := ⟨S.R, S.K, S.i₁, S.i₂ ≫ pullback.fst f f ≫ f, hc⟩
    have : Subsingleton S'.commSq.LiftStruct := hf S'
    let S'l₁ : S'.commSq.LiftStruct := ⟨S.i₂ ≫ pullback.fst f f, by simp [S', ← S.commSq.w_assoc], by simp [S']⟩
    let S'l₂ : S'.commSq.LiftStruct :=
      ⟨S.i₂ ≫ pullback.snd f f, by simp [S', ← S.commSq.w_assoc], by simp [S', pullback.condition]⟩
    have h₁₂ : S'l₁ = S'l₂ := Subsingleton.elim _ _
    constructor
    constructor
    refine ⟨S.i₂ ≫ pullback.fst _ _, ?_, ?_⟩
    · simp [← S.commSq.w_assoc]
    · simp only [Category.assoc]
      apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
      · simp
      · simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
        exact congrArg CommSq.LiftStruct.l h₁₂

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