overEquivIdealSheafData — Mathlib

English

There is a contravariant equivalence between the category of closed subschemes over X and the lattice of ideal sheaves on X.

Русский

Существует контравариантная эквивалентность между категорией замкнутых подсхем над X и решёткой идеал-шаров на X.

LaTeX

$$$Over^{\\mathrm{op}}(IsClosedImmersion\\;\\top X) \\simeq X. IdealSheafData$$$

Lean4

/-- The category of closed subschemes is contravariantly equivalent
to the lattice of ideal sheaves. -/
noncomputable def overEquivIdealSheafData (X : Scheme.{u}) :
    (MorphismProperty.Over @IsClosedImmersion ⊤ X)ᵒᵖ ≌ X.IdealSheafData
    where
  functor := (MorphismProperty.Over.forget _ _ _).op ⋙ X.kerFunctor
  inverse :=
    { obj I := .op <| .mk _ I.subschemeι inferInstance
      map {I J} h := (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion h.le)).op
      map_comp f g := Quiver.Hom.unop_inj (by ext1; simp) }
  unitIso :=
    NatIso.ofComponents
      (fun Y ↦
        letI : IsClosedImmersion Y.unop.hom := Y.unop.prop
        ((MorphismProperty.Over.isoMk (asIso Y.unop.hom.toImage).symm).op))
      fun {X Y} f ↦ by
      apply Quiver.Hom.unop_inj
      ext1
      dsimp
      rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, ← cancel_mono (Scheme.IdealSheafData.subschemeι _)]
      simp
  counitIso := NatIso.ofComponents (fun I ↦ eqToIso (by simp))

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