Spec_iff — Mathlib

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

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