jacobsonSpace — Mathlib

English

If X → Y is LocallyOfFiniteType and Y is Jacobson, then X is Jacobson.

Русский

Если локально конечен тип X → Y, и Y имеет пространство Джейкобсона, то X тоже имеет пространство Джейкобсона.

LaTeX

$$$\\text{LocallyOfFiniteType}(f) \\land \\text{JacobsonSpace}(Y) \\Rightarrow \\text{JacobsonSpace}(X)$$$

Lean4

nonrec theorem jacobsonSpace (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace Y] : JacobsonSpace X :=
  by
  wlog hY : ∃ S, Y = Spec S
  · rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]
    intro i
    have inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) := MorphismProperty.pullback_snd _ _ inferInstance
    have inst : JacobsonSpace Y :=
      ‹_› -- TC gets stuck on the WLOG hypothesis without it.

    have inst : JacobsonSpace (Y.affineCover.X i) := .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
    let e := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.isEmbedding.toHomeomorph
    have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have inst : JacobsonSpace (Spec R) :=
      ‹_› -- TC gets stuck on the WLOG hypothesis without it.

    rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]
    intro i
    have := this _ (X.affineCover.f i ≫ f) ⟨_, rfl⟩
    let e := (X.affineCover.f i).isOpenEmbedding.isEmbedding.toHomeomorph
    exact .of_isClosedEmbedding e.symm.isClosedEmbedding
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f
  have : RingHom.FiniteType φ.hom := HasRingHomProperty.Spec_iff.mp ‹_›
  algebraize [φ.hom]
  have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
  exact PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

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