English
For X, f: X → Spec R, IsClosedImmersion f iff there exists an ideal I ⊆ R and an isomorphism X ≅ Spec(R/I) with f factoring through Spec.map (R → R/I).
Русский
Для X, f: X → Spec R: замкнутое вложение f эквивалентно существованию идеала I ⊆ R и изоморфизму X ≅ Spec(R/I) так, что f факторизуется через Spec.map (R → R/I).
LaTeX
$$$IsClosedImmersion(f) \\iff \\exists I, e:\\ X \\cong Spec(R/I), f = e.hom \\circ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))$$$
Lean4
theorem Spec_iff {R : CommRingCat} {f : X ⟶ Spec R} :
IsClosedImmersion f ↔
∃ I : Ideal R, ∃ e : X ≅ Spec (.of <| R ⧸ I), f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) :=
by
constructor
· intro H
obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f
let φ := (Scheme.ΓSpecIso R).inv ≫ f.appTop
refine
⟨RingHom.ker φ.1,
Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩
·
exact
⟨φ.1.kerLift_injective,
Ideal.Quotient.lift_surjective_of_surjective _ _
(h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩
· simp only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map, Quiver.Hom.unop_op, Category.assoc,
← Spec.map_comp]
change f = X.isoSpec.hom ≫ Spec.map φ
simp only [Scheme.isoSpec, asIso_hom, Spec.map_comp, ← Scheme.toSpecΓ_naturality_assoc, ← SpecMap_ΓSpecIso_hom, φ]
simp only [← Spec.map_comp, Iso.inv_hom_id, Spec.map_id, Category.comp_id]
· rintro ⟨I, e, rfl⟩
infer_instance