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))