English
If X is subsingleton and reduced and Y is Jacobson, then IsFinite f iff LocallyOfFiniteType f.
Русский
Если X одноточечен, сведён и Y — Jacobson, то IsFinite f эквивалентно LocallyOfFiniteType f.
LaTeX
$$$\mathrm{IsFinite}(f) \iff \mathrm{LocallyOfFiniteType}(f)$ under the given hypotheses.$$
Lean4
/-- If `X` is a Jacobson scheme and `k` is a field,
`Spec(k) ⟶ X` is finite iff it is (locally) of finite type.
(The statement is more general to allow the empty scheme as well) -/
theorem isFinite_iff_locallyOfFiniteType_of_jacobsonSpace {X Y : Scheme.{u}} {f : X ⟶ Y} [Subsingleton X] [IsReduced X]
[JacobsonSpace Y] : IsFinite f ↔ LocallyOfFiniteType f :=
by
wlog hY : ∃ S, Y = Spec S generalizing X Y
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
have inst (i) := ((Y.affineCover.pullback₁ f).f i).isOpenEmbedding.injective.subsingleton
have inst (i) := isReduced_of_isOpenImmersion ((Y.affineCover.pullback₁ f).f i)
have inst (i) := JacobsonSpace.of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding
exact forall_congr' fun i ↦ this ⟨_, rfl⟩
obtain ⟨S, rfl⟩ := hY
wlog hX : ∃ R, X = Spec R generalizing X
· rw [← MorphismProperty.cancel_left_of_respectsIso (P := @IsFinite) X.isoSpec.inv, ←
MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType) X.isoSpec.inv]
have inst := X.isoSpec.inv.isOpenEmbedding.injective.subsingleton
refine this ⟨_, rfl⟩
cases isEmpty_or_nonempty X
· exact ⟨inferInstance, inferInstance⟩
have : IrreducibleSpace X := ⟨‹_›⟩
obtain ⟨R, rfl⟩ := hX
have : IsDomain R := (affine_isIntegral_iff R).mp (isIntegral_of_irreducibleSpace_of_isReduced _)
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [IsFinite.SpecMap_iff, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
have := (PrimeSpectrum.t1Space_iff_isField (R := R)).mp (show T1Space (Spec R) by infer_instance)
letI := this.toField
letI := φ.hom.toAlgebra
have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›
change Module.Finite _ _ ↔ Algebra.FiniteType _ _
exact ⟨fun _ ↦ inferInstance, fun _ ↦ finite_of_finite_type_of_isJacobsonRing _ _⟩
