diff --git a/Mathlib.lean b/Mathlib.lean index 4308c4d1d9eeb9..db532ad88374ec 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -193,6 +193,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward public import Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify +public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Subobject public import Mathlib.Algebra.Category.ModuleCat.Products public import Mathlib.Algebra.Category.ModuleCat.Projective public import Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension @@ -200,13 +201,16 @@ public import Mathlib.Algebra.Category.ModuleCat.Pseudofunctor public import Mathlib.Algebra.Category.ModuleCat.Semi public import Mathlib.Algebra.Category.ModuleCat.Sheaf public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Annihilator public import Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Free public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.IdealSheaf public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization public import Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallySurjective public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous @@ -215,8 +219,11 @@ public import Mathlib.Algebra.Category.ModuleCat.Simple public import Mathlib.Algebra.Category.ModuleCat.Stalk public import Mathlib.Algebra.Category.ModuleCat.Subobject public import Mathlib.Algebra.Category.ModuleCat.Tannaka +public import Mathlib.Algebra.Category.ModuleCat.Topology.AnnihilatorStalk +public import Mathlib.Algebra.Category.ModuleCat.Topology.AnnihilatorStalkFiniteType public import Mathlib.Algebra.Category.ModuleCat.Topology.Basic public import Mathlib.Algebra.Category.ModuleCat.Topology.Homology +public import Mathlib.Algebra.Category.ModuleCat.Topology.SheafifyInstances public import Mathlib.Algebra.Category.ModuleCat.Ulift public import Mathlib.Algebra.Category.MonCat.Adjunctions public import Mathlib.Algebra.Category.MonCat.Basic @@ -1393,6 +1400,7 @@ public import Mathlib.AlgebraicGeometry.Group.Smooth public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial public import Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent +public import Mathlib.AlgebraicGeometry.IdealSheaf.Quasicoherent public import Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme public import Mathlib.AlgebraicGeometry.Limits public import Mathlib.AlgebraicGeometry.LimitsOver diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Subobject.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Subobject.lean new file mode 100644 index 00000000000000..6a45f1dc8cc003 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Subobject.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono + +/-! +# Subobjects of presheaves of modules from a family of submodules + +Given a presheaf of modules `M` over a presheaf of rings `R` and a family of +submodules `N X ≤ M.obj X` that is stable under the restriction maps of `M`, +we construct the corresponding subobject of `M` in the category +`PresheafOfModules R`, together with its inclusion monomorphism. + +## Main definitions + +* `PresheafOfModules.Submodule M`: a family of submodules of `M`, stable + under restriction. +* `PresheafOfModules.Submodule.toPresheafOfModules`: the associated + presheaf of modules. +* `PresheafOfModules.Submodule.ι`: the inclusion into `M`, a monomorphism. + +-/ + +@[expose] public section + +universe v v₁ u₁ u + +open CategoryTheory + +namespace PresheafOfModules + +variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ RingCat.{u}} + +/-- A family of submodules `N X ≤ M.obj X` of a presheaf of modules `M`, stable +under the restriction maps of `M`. This is the data needed to cut out a +subobject of `M` in `PresheafOfModules R`. -/ +structure Submodule (M : PresheafOfModules.{v} R) where + /-- the submodule of `M.obj X` -/ + toSubmodule (X : Cᵒᵖ) : _root_.Submodule (R.obj X) (M.obj X) + /-- the family is stable under restriction -/ + map_mem ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) ⦃m : M.obj X⦄ (hm : m ∈ toSubmodule X) : + M.map f m ∈ toSubmodule Y + +namespace Submodule + +variable {M : PresheafOfModules.{v} R} (N : M.Submodule) + +@[ext] +lemma ext {N₁ N₂ : M.Submodule} (h : ∀ X, N₁.toSubmodule X = N₂.toSubmodule X) : + N₁ = N₂ := by + cases N₁; cases N₂; congr 1; ext X : 1; exact h X + +set_option backward.isDefEq.respectTransparency false in +/-- The subobject of `M` cut out by the family of submodules `N`, as a presheaf of modules: over +`X` it is the submodule `N.toSubmodule X`, with restriction maps induced by those of `M`. -/ +noncomputable def toPresheafOfModules : PresheafOfModules.{v} R where + obj X := ModuleCat.of (R.obj X) (N.toSubmodule X) + map {X Y} f := ModuleCat.ofHom + (Y := (ModuleCat.restrictScalars (R.map f).hom).obj (ModuleCat.of (R.obj Y) (N.toSubmodule Y))) + { toFun := fun m ↦ ⟨M.map f m.val, N.map_mem f m.property⟩ + map_add' := fun a b ↦ Subtype.ext (map_add (M.map f).hom a.val b.val) + map_smul' := fun r m ↦ Subtype.ext (M.map_smul f r m.val) } + +@[simp] +lemma toPresheafOfModules_obj (X : Cᵒᵖ) : + (N.toPresheafOfModules).obj X = ModuleCat.of _ (N.toSubmodule X) := rfl + +@[simp] +lemma toPresheafOfModules_map_apply {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : N.toSubmodule X) : + ((N.toPresheafOfModules).map f m).val = M.map f m.val := rfl + +/-- The inclusion of the subobject cut out by `N` into `M`. -/ +noncomputable def ι : N.toPresheafOfModules ⟶ M := + homMk { app := fun X ↦ AddCommGrpCat.ofHom (N.toSubmodule X).subtype.toAddMonoidHom + naturality := fun {X Y} f ↦ by ext m; rfl } + (fun X r m ↦ rfl) + +@[simp] +lemma ι_app_apply (X : Cᵒᵖ) (m : N.toSubmodule X) : (N.ι).app X m = m.val := rfl + +lemma ι_app_injective (X : Cᵒᵖ) : Function.Injective ((N.ι).app X) := + Subtype.val_injective + +instance : Mono N.ι := mono_of_injective N.ι_app_injective + +lemma mem_iff {X : Cᵒᵖ} (m : M.obj X) : + (∃ n : N.toSubmodule X, (N.ι).app X n = m) ↔ m ∈ N.toSubmodule X := + ⟨fun ⟨n, hn⟩ ↦ hn ▸ n.property, fun hm ↦ ⟨⟨m, hm⟩, rfl⟩⟩ + +end Submodule + +end PresheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean new file mode 100644 index 00000000000000..1ffed2f2d5a575 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Sheaf/Annihilator.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.Grp.ForgetCorepresentable +public import Mathlib.Algebra.Category.ModuleCat.Presheaf.Subobject +public import Mathlib.Algebra.Category.ModuleCat.Sheaf +public import Mathlib.CategoryTheory.Sites.Subsheaf +public import Mathlib.RingTheory.Ideal.Maps + +/-! +# The annihilator ideal (pre)sheaf of a (pre)sheaf of modules + +Given a presheaf of modules `M` over a presheaf of rings `R`, we define the +annihilator `PresheafOfModules.annihilator M`, a sub-presheaf of modules of the +unit `unit R` (i.e. `R` viewed as a module over itself). Its sections over `X` +are the sections `r` of `R` whose restriction along every `f : X ⟶ Y` +annihilates `M.obj Y`. Equivalently, this is the kernel of the action of `R` +on `M` computed in the internal hom; phrasing it via restrictions avoids relying +on an internal hom for sheaves of modules. + +When `R` is a sheaf of rings and `M` a sheaf of modules, the annihilator is a +sheaf, giving `SheafOfModules.annihilator M` together with its inclusion +monomorphism into `unit R`. + +-/ + +@[expose] public section + +universe v v₁ u₁ u w + +open CategoryTheory Opposite + +namespace PresheafOfModules + +variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ RingCat.{u}} (M : PresheafOfModules.{v} R) + +/-- The annihilator ideal of `M` at `X`: those sections `r` of `R` over `X` +whose restriction along every `f : X ⟶ Y` annihilates `M.obj Y`. -/ +def annihilatorIdeal (X : Cᵒᵖ) : Ideal (R.obj X) where + carrier := { r | ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (m : M.obj Y), R.map f r • m = 0 } + zero_mem' Y f m := by rw [map_zero, zero_smul] + add_mem' {a b} ha hb Y f m := by rw [map_add, add_smul, ha f m, hb f m, add_zero] + smul_mem' c r hr Y f m := by rw [smul_eq_mul, map_mul, mul_smul, hr f m, smul_zero] + +variable {M} + +@[simp] +lemma mem_annihilatorIdeal {X : Cᵒᵖ} (r : R.obj X) : + r ∈ M.annihilatorIdeal X ↔ + ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (m : M.obj Y), R.map f r • m = 0 := + Iff.rfl + +variable (M) + +/-- The annihilator of `M`, as a family of submodules of `unit R` stable under +restriction. -/ +noncomputable def annihilatorSystem : (unit R).Submodule where + toSubmodule X := M.annihilatorIdeal X + map_mem {X Y} f r hr := by + refine (mem_annihilatorIdeal _).mpr fun Z g m ↦ ?_ + have h := (mem_annihilatorIdeal _).mp hr (f ≫ g) m + rwa [R.map_comp, RingCat.comp_apply] at h + +/-- The annihilator of a presheaf of modules `M`, a sub-presheaf of modules of +`unit R`. -/ +noncomputable def annihilator : PresheafOfModules.{u} R := + M.annihilatorSystem.toPresheafOfModules + +/-- The inclusion of the annihilator of `M` into `unit R`. -/ +noncomputable def annihilatorι : M.annihilator ⟶ unit R := + M.annihilatorSystem.ι + +instance : Mono M.annihilatorι := + inferInstanceAs (Mono M.annihilatorSystem.ι) + +variable {M} + +@[simp] +lemma annihilatorι_app_apply (X : Cᵒᵖ) (r : (M.annihilatorSystem.toSubmodule X)) : + M.annihilatorι.app X r = r.val := rfl + +/-- The annihilator is antitone with respect to morphisms that are surjective on sections: +if `f : M ⟶ N` is componentwise surjective, then everything annihilating `M` annihilates `N`. -/ +lemma annihilatorIdeal_le_of_surjective {M N : PresheafOfModules.{v} R} (f : M ⟶ N) + (hf : ∀ Y, Function.Surjective (f.app Y)) (X : Cᵒᵖ) : + M.annihilatorIdeal X ≤ N.annihilatorIdeal X := by + intro r hr + refine (mem_annihilatorIdeal r).mpr fun Y g n ↦ ?_ + obtain ⟨m, rfl⟩ := hf Y n + have hlin : f.app Y (R.map g r • m) = R.map g r • f.app Y m := (f.app Y).hom.map_smul _ _ + rw [← hlin, (mem_annihilatorIdeal r).mp hr g m] + exact (f.app Y).hom.map_zero + +end PresheafOfModules + +namespace SheafOfModules + +open PresheafOfModules + +variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C} + +/-- The underlying type-valued presheaf of an `AddCommGrpCat`-valued sheaf is a sheaf of types. +This holds at any universe `w`, since the forgetful functor of `AddCommGrpCat.{w}` is +corepresentable (by `ULift.{w} ℤ`); in particular it does not require `w = max v₁ u₁`. -/ +private lemma presieveIsSheaf_comp_forget {A : Cᵒᵖ ⥤ AddCommGrpCat.{w}} + (h : Presheaf.IsSheaf J A) : + Presieve.IsSheaf J (A ⋙ CategoryTheory.forget AddCommGrpCat.{w}) := + Presieve.isSheaf_iso J (Functor.isoWhiskerLeft A AddCommGrpCat.coyonedaObjIsoForget) + (h (AddCommGrpCat.of (ULift.{w} ℤ))) + +variable + [J.HasSheafCompose (forget₂ RingCat.{max v₁ u₁} AddCommGrpCat.{max v₁ u₁})] + {R : Sheaf J RingCat.{max v₁ u₁}} (M : SheafOfModules.{v} R) + +/-- The annihilator of a sheaf of modules `M`, as a sheaf of modules: a subobject of +`unit R` whose sections over `X` are those `r : R.obj X` annihilating `M` locally. -/ +noncomputable def annihilator : SheafOfModules.{max v₁ u₁} R where + val := M.val.annihilator + isSheaf := by + -- The underlying type-valued presheaf of `unit R`, which is a sheaf. + let F : Cᵒᵖ ⥤ Type (max v₁ u₁) := + (PresheafOfModules.unit R.obj).presheaf ⋙ CategoryTheory.forget AddCommGrpCat.{max v₁ u₁} + have hF : Presieve.IsSheaf J F := + presieveIsSheaf_comp_forget (SheafOfModules.unit R).isSheaf + -- The annihilator as a subfunctor of `F`. + let G : Subfunctor F := + { obj := fun X ↦ { r : R.obj.obj X | r ∈ M.val.annihilatorIdeal X } + map := fun {U V} i r hr ↦ M.val.annihilatorSystem.map_mem i hr } + -- `M.val` is separated, as the underlying type-valued presheaf of a sheaf. + have hsep : Presieve.IsSheaf J (M.val.presheaf ⋙ CategoryTheory.forget AddCommGrpCat.{v}) := + presieveIsSheaf_comp_forget M.isSheaf + -- The annihilator subfunctor is a sheaf: it is closed under the topology. + have hG : Presieve.IsSheaf J G.toFunctor := by + rw [G.isSheaf_iff hF] + intro U s hs + change ∀ ⦃Y : Cᵒᵖ⦄ (f : U ⟶ Y) (m : M.val.obj Y), R.obj.map f s • m = 0 + intro W φ m + -- Pull back the covering sieve along the morphism underlying `φ`. + have hpb : Sieve.pullback φ.unop (G.sieveOfSection s) ∈ J W.unop := + J.pullback_stable φ.unop hs + -- It suffices, by separatedness, that every restriction of `R.map φ s • m` vanishes. + apply (hsep _ hpb).isSeparatedFor.ext + intro Y f hf + -- On the pulled-back sieve, the relevant section lies in the annihilator ideal. + have hcomp : (f ≫ φ.unop).op = φ ≫ f.op := by rw [op_comp, Quiver.Hom.op_unop] + have key : R.obj.map (φ ≫ f.op) s ∈ M.val.annihilatorIdeal (op Y) := by + rw [← hcomp]; exact hf + -- Hence it annihilates the restriction of `m`. + have h0 : R.obj.map (φ ≫ f.op) s • M.val.map f.op m = 0 := by + have h := (mem_annihilatorIdeal _).mp key (𝟙 (op Y)) + (M.val.map f.op m : M.val.obj (op Y)) + rwa [R.obj.map_id, RingCat.id_apply] at h + change M.val.map f.op (R.obj.map φ s • m) = M.val.map f.op 0 + rw [map_zero, M.val.map_smul, ← RingCat.comp_apply, ← R.obj.map_comp, h0] + -- Transfer the sheaf condition back to `M.val.annihilator.presheaf`. + rw [Presheaf.isSheaf_iff_isSheaf_forget (J := J) + (s := CategoryTheory.forget AddCommGrpCat.{max v₁ u₁}), + isSheaf_iff_isSheaf_of_type] + exact Presieve.isSheaf_iso J (NatIso.ofComponents (fun _ ↦ Iso.refl _) (by intros; rfl)) hG + +/-- The inclusion of the annihilator of `M` into `unit R`. -/ +noncomputable def annihilatorι : M.annihilator ⟶ unit R := + ⟨M.val.annihilatorι⟩ + +end SheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/IdealSheaf.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/IdealSheaf.lean new file mode 100644 index 00000000000000..164bb7620ffb42 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Sheaf/IdealSheaf.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Annihilator + +/-! +# Ideal sheaves over a sheaf of rings + +We define an ideal sheaf over a sheaf of rings `R` on a site as a sub-sheaf of modules of the +unit `unit R` (i.e. `R` viewed as a module over itself), given concretely by a restriction-stable +family of ideals whose associated presheaf of modules is a sheaf. + +This is the general notion behind the scheme-theoretic `AlgebraicGeometry.Scheme.IdealSheafData`, +which is currently a placeholder for "actual subsheaves of `𝒪ₓ`": for a scheme `X`, an +`IdealSheaf X.ringCatSheaf` is precisely such a subsheaf of the structure sheaf, and +`IdealSheaf.ideal` reads off the ideal of sections over every open (not only the affine ones). + +## Main definitions + +* `SheafOfModules.IdealSheaf R`: an ideal sheaf over `R`. +* `SheafOfModules.IdealSheaf.ideal`: the ideal of sections over each object. +* `SheafOfModules.IdealSheaf.toSheafOfModules`/`ι`: the underlying sheaf of modules and its + inclusion monomorphism into `unit R`. +* `SheafOfModules.annihilatorIdealSheaf M`: the annihilator of `M` as an ideal sheaf. + +## Relation to `Scheme.IdealSheafData` + +For a scheme `X` (with structure sheaf `R = X.ringCatSheaf`), evaluating `IdealSheaf.ideal` on +affine opens produces a family of ideals of `Γ(X, U)`. Conversely, `Scheme.IdealSheafData` +records such a family on affine opens together with the localization compatibility +`map_ideal_basicOpen`. Translating between the two is a *quasi-coherence* statement: a general +`IdealSheaf` need not be quasi-coherent (its restriction maps need not be localizations), and an +`IdealSheafData` only constrains affine opens. Building the order isomorphism between +quasi-coherent ideal sheaves and `IdealSheafData` is the refactor envisaged in +`AlgebraicGeometry/IdealSheaf/Basic.lean` and is left for future work; this file provides the +target notion of "actual subsheaf of `𝒪ₓ`" that such a refactor requires. + +-/ + +@[expose] public section + +universe v v₁ u₁ u + +open CategoryTheory + +namespace SheafOfModules + +variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C} (R : Sheaf J RingCat.{u}) + +/-- An ideal sheaf over a sheaf of rings `R` is a restriction-stable family of ideals of `R` +whose associated presheaf of modules (a sub-presheaf of `unit R`) is a sheaf. It is the +sheaf-of-modules incarnation of a sheaf of ideals. -/ +structure IdealSheaf where + /-- the underlying restriction-stable family of ideals -/ + toSubmodule : (PresheafOfModules.unit R.obj).Submodule + /-- the associated presheaf of modules is a sheaf -/ + isSheaf : Presheaf.IsSheaf J toSubmodule.toPresheafOfModules.presheaf + +namespace IdealSheaf + +variable {R} + +/-- The ideal of sections of an ideal sheaf over `X`. -/ +def ideal (I : IdealSheaf R) (X : Cᵒᵖ) : Ideal (R.obj.obj X) := + I.toSubmodule.toSubmodule X + +@[ext] +lemma ext {I J : IdealSheaf R} (h : ∀ X, I.ideal X = J.ideal X) : I = J := by + obtain ⟨I, _⟩ := I + obtain ⟨J, _⟩ := J + congr 1 + exact PresheafOfModules.Submodule.ext h + +instance : PartialOrder (IdealSheaf R) := + PartialOrder.lift ideal (fun _ _ h ↦ ext (congrFun h)) + +lemma le_def {I J : IdealSheaf R} : I ≤ J ↔ ∀ X, I.ideal X ≤ J.ideal X := Iff.rfl + +/-- The underlying sheaf of modules of an ideal sheaf. -/ +noncomputable def toSheafOfModules (I : IdealSheaf R) : SheafOfModules.{u} R where + val := I.toSubmodule.toPresheafOfModules + isSheaf := I.isSheaf + +variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})] + +/-- The inclusion of an ideal sheaf into the unit `unit R`. -/ +noncomputable def ι (I : IdealSheaf R) : I.toSheafOfModules ⟶ unit R := + ⟨I.toSubmodule.ι⟩ + +instance (I : IdealSheaf R) : Mono I.ι.val := + inferInstanceAs (Mono I.toSubmodule.ι) + +end IdealSheaf + +variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})] + +/-- The annihilator of a sheaf of modules `M`, packaged as an ideal sheaf over `R`. -/ +noncomputable def annihilatorIdealSheaf {R : Sheaf J RingCat.{max v₁ u₁}} + [J.HasSheafCompose (forget₂ RingCat.{max v₁ u₁} AddCommGrpCat.{max v₁ u₁})] + (M : SheafOfModules.{v} R) : IdealSheaf R where + toSubmodule := M.val.annihilatorSystem + isSheaf := M.annihilator.isSheaf + +end SheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Sheaf/LocallySurjective.lean b/Mathlib/Algebra/Category/ModuleCat/Sheaf/LocallySurjective.lean new file mode 100644 index 00000000000000..042060df46872a --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Sheaf/LocallySurjective.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.Grp.Abelian +public import Mathlib.Algebra.Category.Grp.EpiMono +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian +public import Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits +public import Mathlib.CategoryTheory.Sites.Abelian +public import Mathlib.CategoryTheory.Sites.EpiMono + +/-! +# Epimorphisms of sheaves of modules are locally surjective + +In this file, we show that an epimorphism `f : M ⟶ N` of sheaves of modules over a sheaf +of rings `R` is locally surjective on underlying sections, i.e. the underlying morphism of +presheaves of abelian groups `(PresheafOfModules.toPresheaf R.obj).map f.val` is +`Presheaf.IsLocallySurjective`. + +## Main results + +* `SheafOfModules.toSheaf_preservesEpimorphisms`: the functor `SheafOfModules.toSheaf R` + preserves epimorphisms. +* `SheafOfModules.isLocallySurjective_of_epi`: an epimorphism of sheaves of modules is + locally surjective. + +-/ + +@[expose] public section + +universe v v' u u' + +open CategoryTheory Limits + +variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C} + +namespace SheafOfModules + +variable {R : Sheaf J RingCat.{u}} [HasSheafify J AddCommGrpCat.{v}] + [J.WEqualsLocallyBijective AddCommGrpCat.{v}] + +variable (J) in +/-- A morphism `f` of sheaves of modules is locally surjective if the underlying morphism +of presheaves of abelian groups is locally surjective. -/ +abbrev IsLocallySurjective {M N : SheafOfModules.{v} R} (f : M ⟶ N) : Prop := + PresheafOfModules.IsLocallySurjective J f.val + +/-- The composition `PresheafOfModules.sheafification (𝟙 R.obj) ⋙ SheafOfModules.toSheaf R` +preserves finite colimits: indeed, it is naturally isomorphic to +`PresheafOfModules.toPresheaf R.obj ⋙ presheafToSheaf J AddCommGrpCat`, both factors of +which preserve finite colimits. -/ +noncomputable instance : + PreservesFiniteColimits + (PresheafOfModules.sheafification (𝟙 R.obj) ⋙ toSheaf.{v} R) := + preservesFiniteColimits_of_natIso + (PresheafOfModules.sheafificationCompToSheaf (𝟙 R.obj)).symm + +/-- The functor `SheafOfModules.toSheaf R : SheafOfModules R ⥤ Sheaf J AddCommGrpCat` +preserves epimorphisms. + +Since `SheafOfModules R` is the reflective localization of `PresheafOfModules R.obj` along the +sheafification functor `L := PresheafOfModules.sheafification (𝟙 R.obj)`, with fully faithful +right adjoint, a functor out of `SheafOfModules R` preserves colimits of a given shape as soon +as its precomposition with `L` does (`Adjunction.preservesColimitsOfShape_iff`). +Applied with the shape `WalkingSpan` (pushouts), this gives preservation of epimorphisms. -/ +noncomputable instance toSheaf_preservesEpimorphisms : + (toSheaf.{v} R).PreservesEpimorphisms := by + have adj := PresheafOfModules.sheafificationAdjunction (𝟙 R.obj) + have : PreservesColimitsOfShape WalkingSpan (toSheaf.{v} R) := + (adj.preservesColimitsOfShape_iff (toSheaf R) WalkingSpan).mpr inferInstance + infer_instance + +variable (J) in +/-- An epimorphism of sheaves of modules is locally surjective on underlying sections. -/ +theorem isLocallySurjective_of_epi {M N : SheafOfModules.{v} R} (f : M ⟶ N) [Epi f] : + IsLocallySurjective J f := + (Sheaf.isLocallySurjective_iff_epi' (φ := (toSheaf R).map f)).mpr inferInstance + +variable (J) in +/-- A morphism of sheaves of modules is an epimorphism if and only if it is locally surjective +on underlying sections. -/ +theorem epi_iff_isLocallySurjective {M N : SheafOfModules.{v} R} (f : M ⟶ N) : + Epi f ↔ IsLocallySurjective J f := by + refine ⟨fun _ ↦ isLocallySurjective_of_epi J f, fun hf ↦ ?_⟩ + have hf' : Sheaf.IsLocallySurjective ((toSheaf R).map f) := hf + have : Epi ((toSheaf R).map f) := + (Sheaf.isLocallySurjective_iff_epi' (φ := (toSheaf R).map f)).mp hf' + exact (toSheaf R).epi_of_epi_map this + +end SheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalk.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalk.lean new file mode 100644 index 00000000000000..eaf8ab2faa8e2c --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalk.lean @@ -0,0 +1,153 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Stalk +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Annihilator + +/-! +# Stalks of the annihilator ideal sheaf + +For a presheaf of modules `M` over a presheaf of rings `R` on a topological space `X`, we +compare the stalk of the annihilator ideal (pre)sheaf at a point `x` with the module-theoretic +annihilator `Module.annihilator (R.stalk x) (M.presheaf.stalk x)`. + +The germ of any section of the annihilator ideal lands in `Module.annihilator` of the stalks +(`PresheafOfModules.germ_mem_annihilator_stalk`); equality of the two requires a finiteness +hypothesis on `M`. + +-/ + +@[expose] public section + +universe u + +open CategoryTheory TopologicalSpace Opposite TopCat.Presheaf + +namespace PresheafOfModules + +variable {X : TopCat.{u}} {R : X.Presheaf RingCat.{u}} (M : PresheafOfModules.{u} R) {x : X} + +/-- The germ at `x` of a section `r` of `R` that annihilates `M` locally annihilates the stalk +`M.presheaf.stalk x`. This is the "easy" containment that holds with no finiteness hypothesis. -/ +theorem germ_mem_annihilator_stalk {U : Opens X} (hx : x ∈ U) (r : R.obj (op U)) + (hr : r ∈ M.annihilatorIdeal (op U)) : + R.germ U x hx r ∈ Module.annihilator (R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x) := by + rw [Module.mem_annihilator] + intro mx + obtain ⟨V, hxV, m, rfl⟩ := exists_germ_eq M.presheaf mx + have hxW : x ∈ U ⊓ V := ⟨hx, hxV⟩ + rw [← germ_res_apply R (homOfLE inf_le_left) x hxW r, + ← germ_res_apply M.presheaf (homOfLE inf_le_right) x hxW m, + ← M.germ_ringCat_smul x (U ⊓ V) hxW, + (mem_annihilatorIdeal r).mp hr (homOfLE (inf_le_left : U ⊓ V ≤ U)).op + (M.presheaf.map (homOfLE inf_le_right).op m)] + exact map_zero _ + +/-- **Stalk of the annihilator ideal sheaf.** +Under a finite *local generation* hypothesis, the stalk of the annihilator ideal (pre)sheaf at `x` +recovers the module-theoretic annihilator `Module.annihilator (R.stalk x) (M.presheaf.stalk x)`: +an element `ρ` of the ring stalk annihilates the module stalk if and only if it is the germ of a +section of the annihilator ideal. + +The `←` direction is the easy `germ_mem_annihilator_stalk`. The `→` direction is the substantial +one; it uses that `M` is locally generated near `x` by the finite family `t`. Concretely, `hgen` +says that every section over `V ≤ U₀` is, locally around each of its points, an `R`-linear +combination of the (restrictions of the) generators `t i`. + +The commutativity hypothesis `hRcomm` is needed because, for a *left* module, the implication +"`r` annihilates the generators ⟹ `r` annihilates the module" requires moving `r` past the +coefficients of a linear combination. -/ +theorem mem_annihilator_stalk_iff + (hM : TopCat.Presheaf.IsSheaf M.presheaf) + (hRcomm : ∀ (U : (Opens X)ᵒᵖ) (a b : R.obj U), a * b = b * a) + {ι : Type u} [Fintype ι] {U₀ : Opens X} (hx₀ : x ∈ U₀) (t : ι → M.obj (op U₀)) + (hgen : ∀ ⦃V : Opens X⦄ (hVU₀ : V ≤ U₀) (m : M.obj (op V)) ⦃y : X⦄ (_ : y ∈ V), + ∃ (W : Opens X) (hWV : W ≤ V) (_ : y ∈ W) (a : ι → R.obj (op W)), + M.presheaf.map (homOfLE hWV).op m = + ∑ i, a i • M.presheaf.map (homOfLE (le_trans hWV hVU₀)).op (t i)) + (ρ : R.stalk x) : + ρ ∈ Module.annihilator (R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x) ↔ + ∃ (U : Opens X) (hx : x ∈ U) (r : R.obj (op U)), + r ∈ M.annihilatorIdeal (op U) ∧ R.germ U x hx r = ρ := by + -- The action commutes with restriction of sections. + have hsmul_res : ∀ ⦃U V : (Opens X)ᵒᵖ⦄ (g : U ⟶ V) (r : R.obj U) (m : M.obj U), + M.presheaf.map g (r • m) = R.map g r • M.presheaf.map g m := + fun U V g r m => M.map_smul g r m + constructor + · intro hρ + rw [Module.mem_annihilator] at hρ + -- Choose a representative `r₀` of `ρ` over some `U_r ≤ U₀`. + obtain ⟨U_r, hUr, hxUr, r₀, hr₀⟩ := exists_le_germ_eq R ρ hx₀ + -- Each generator is annihilated by `r₀` at the stalk, hence on a neighborhood `W i` of `x`. + have hg : ∀ i, germ M.presheaf U_r x hxUr (r₀ • M.presheaf.map (homOfLE hUr).op (t i)) = + germ M.presheaf U_r x hxUr 0 := by + intro i + rw [map_zero] + erw [M.germ_ringCat_smul] + rw [hr₀] + exact hρ _ + choose W hxW iU iV he using + fun i => germ_eq M.presheaf x hxUr hxUr + (r₀ • M.presheaf.map (homOfLE hUr).op (t i)) 0 (hg i) + have he' : ∀ i, M.presheaf.map (iU i).op + (r₀ • M.presheaf.map (homOfLE hUr).op (t i)) = 0 := + fun i => (he i).trans (map_zero _) + -- The common neighborhood on which `r₀` annihilates all generators. + set U' : Opens X := U_r ⊓ ⨅ i, W i with hU'def + have hU'Ur : U' ≤ U_r := by rw [hU'def]; exact inf_le_left + have hU'Wi : ∀ i, U' ≤ W i := fun i => by + rw [hU'def]; exact le_trans inf_le_right (iInf_le _ i) + have hxU' : x ∈ U' := by + rw [hU'def] + refine ⟨hxUr, ?_⟩ + rw [Opens.coe_iInf] + exact Set.mem_iInter.mpr fun i => hxW i + refine ⟨U', hxU', R.map (homOfLE hU'Ur).op r₀, ?_, ?_⟩ + · -- `r₀|_{U'}` lies in the annihilator ideal over `U'`. + refine (mem_annihilatorIdeal _).mpr ?_ + intro Y f m + obtain ⟨V, rfl⟩ : ∃ V, Y = op V := ⟨Y.unop, rfl⟩ + have hVU' : V ≤ U' := f.unop.le + have hVU₀ : V ≤ U₀ := le_trans hVU' (le_trans hU'Ur hUr) + -- It suffices, by separatedness, to check the equality locally around each point of `V`. + refine hM.section_ext ?_ + intro y hy + obtain ⟨Wy, hWyV, hyWy, a, ha⟩ := hgen hVU₀ m hy + have h1 : Wy ≤ U_r := le_trans hWyV (le_trans hVU' hU'Ur) + have h2 : Wy ≤ U₀ := le_trans hWyV hVU₀ + have hWyWi : ∀ i, Wy ≤ W i := fun i => le_trans hWyV (le_trans hVU' (hU'Wi i)) + -- `r₀` annihilates each generator already on `Wy`. + have key : ∀ i, R.map (homOfLE h1).op r₀ • + M.presheaf.map (homOfLE h2).op (t i) = 0 := by + intro i + have hsz : M.presheaf.map (homOfLE h1).op + (r₀ • M.presheaf.map (homOfLE hUr).op (t i)) = 0 := by + have hm : (homOfLE h1).op = (iU i).op ≫ (homOfLE (hWyWi i)).op := Subsingleton.elim _ _ + rw [hm, Functor.map_comp, ConcreteCategory.comp_apply, he' i, map_zero] + erw [hsmul_res] at hsz + have hm2 : (homOfLE h2).op = (homOfLE hUr).op ≫ (homOfLE h1).op := Subsingleton.elim _ _ + rw [hm2, Functor.map_comp, ConcreteCategory.comp_apply] + exact hsz + -- Express `r₀|_V • m` locally as a combination of annihilated generators. + refine ⟨Wy, hWyV, hyWy, ?_⟩ + have hA : R.map (homOfLE hWyV).op (R.map f (R.map (homOfLE hU'Ur).op r₀)) = + R.map (homOfLE h1).op r₀ := by + have hm : (homOfLE h1).op = (homOfLE hU'Ur).op ≫ f ≫ (homOfLE hWyV).op := + Subsingleton.elim _ _ + rw [hm] + simp only [Functor.map_comp, ConcreteCategory.comp_apply] + erw [hsmul_res] + rw [hA, ha, Finset.smul_sum] + refine (Finset.sum_eq_zero fun i _ => ?_).trans (map_zero _).symm + rw [← mul_smul, hRcomm, mul_smul, key i, smul_zero] + · -- The germ of `r₀|_{U'}` is `ρ`. + rw [germ_res_apply] + exact hr₀ + · rintro ⟨U, hx, r, hr, rfl⟩ + exact germ_mem_annihilator_stalk M hx r hr + +end PresheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalkFiniteType.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalkFiniteType.lean new file mode 100644 index 00000000000000..9fbab41fc13f04 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Topology/AnnihilatorStalkFiniteType.lean @@ -0,0 +1,195 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Topology.AnnihilatorStalk +public import Mathlib.Algebra.Category.ModuleCat.Topology.SheafifyInstances +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallySurjective + +/-! +# Stalk of the annihilator ideal sheaf of a finite-type sheaf of modules + +For a sheaf of modules `M` of finite type over a (commutative) sheaf of rings `R` on a topological +space `X`, the stalk of the annihilator ideal sheaf at a point `x` recovers the module-theoretic +annihilator `Module.annihilator (R.stalk x) (Mₓ)`. + +This upgrades `PresheafOfModules.mem_annihilator_stalk_iff`, replacing its explicit local-generation +hypothesis by `[M.IsFiniteType]`. The slice-site sheafification instances needed to even state +`M.IsFiniteType` over the topological site are provided in +`Mathlib.Algebra.Category.ModuleCat.Topology.SheafifyInstances`. +-/ + +@[expose] public section + +universe u + +open CategoryTheory TopologicalSpace Opposite TopCat.Presheaf + +namespace SheafOfModules + +section FreeDecomposition + +open CategoryTheory Limits + +variable {C : Type u} [Category.{u} C] {J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}} + [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}] + [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})] + +/-- A section of the free sheaf of modules `free ι` (for a finite index type `ι`) over an object +`B` is a finite combination `∑ i, (ιFree i)_B (c i)` of the values of the standard basis sections, +with coefficients `c i` sections of `unit R` over `B`. -/ +lemma exists_val_obj_eq_sum_ιFree {ι : Type u} [Fintype ι] (B : Cᵒᵖ) + (b : (free (R := R) ι).val.obj B) : + ∃ c : ι → R.obj.obj B, + b = (∑ i, (ιFree i).val.app B (c i) : (free (R := R) ι).val.obj B) := by + classical + let f : ι → SheafOfModules.{u} R := fun _ ↦ unit R + haveI : HasFiniteBiproducts (SheafOfModules.{u} R) := Abelian.hasFiniteBiproducts + haveI : HasBiproduct f := inferInstance + let Φ := SheafOfModules.evaluation (R := R) B + haveI : Φ.Additive := + inferInstanceAs (Functor.Additive (forget R ⋙ PresheafOfModules.evaluation R.obj B)) + let e := biproduct.isoCoproduct f + have hιe : ∀ i, biproduct.ι f i ≫ e.hom = Sigma.ι f i := fun i ↦ by + rw [biproduct.isoCoproduct_hom, biproduct.ι_desc] + have key : 𝟙 (⨁ f) = ∑ i, biproduct.π f i ≫ biproduct.ι f i := + (IsBilimit.total (biproduct.isBilimit f)).symm + have hid : 𝟙 (∐ f) = ∑ i, (e.inv ≫ biproduct.π f i) ≫ Sigma.ι f i := by + have h0 : 𝟙 (∐ f) = e.inv ≫ (𝟙 (⨁ f)) ≫ e.hom := by + rw [Category.id_comp, e.inv_hom_id] + rw [h0, key, Preadditive.sum_comp, Preadditive.comp_sum] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + simp only [Category.assoc, hιe i] + refine ⟨fun i ↦ Φ.map (e.inv ≫ biproduct.π f i) b, ?_⟩ + have hΦ := congr(Φ.map $hid) + rw [Φ.map_id, Φ.map_sum] at hΦ + have hb : b = (∑ i, Φ.map ((e.inv ≫ biproduct.π f i) ≫ Sigma.ι f i)).hom b := by + rw [← hΦ]; rfl + conv_lhs => rw [hb] + rw [ModuleCat.hom_sum, LinearMap.sum_apply] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + rw [Φ.map_comp] + rfl + +/-- The image under a morphism `φ : free ι ⟶ N` of a section `b` of `free ι` over an object `Z` +is the finite `R(Z)`-linear combination `∑ i, c i • (φ ∘ freeSectionᵢ)(Z)` of the images of the +standard basis sections, for suitable coefficients `c i`. -/ +lemma exists_app_eq_sum_smul {ι : Type u} [Fintype ι] {N : SheafOfModules.{u} R} + (φ : free (R := R) ι ⟶ N) (Z : Cᵒᵖ) (b : (free (R := R) ι).val.obj Z) : + ∃ c : ι → R.obj.obj Z, + φ.val.app Z b = ∑ i, c i • (sectionsMap φ (freeSection i)).eval Z := by + obtain ⟨c, hc⟩ := exists_val_obj_eq_sum_ιFree Z b + refine ⟨c, ?_⟩ + rw [hc, map_sum] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + have h1 : (ιFree i).val.app Z (c i) = c i • (ιFree i).val.app Z (1 : R.obj.obj Z) := by + rw [← map_smul] + congr 1 + exact (mul_one (c i)).symm + rw [h1, map_smul] + rfl + +end FreeDecomposition + +variable {X : TopCat.{u}} {R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}} + (M : SheafOfModules.{u} R) + +set_option backward.isDefEq.respectTransparency false in +open Limits in +/-- The local-generation bridge: if `π : free ι ⟶ M.over U₀` is an epimorphism of sheaves of +modules over the slice site, then every section `m` of `M` over `V ≤ U₀` is, locally around each +of its points, an `R`-linear combination of (the restrictions of) the sections +`(sectionsMap π (freeSectionᵢ))` over `U₀`. -/ +lemma exists_localGeneration_of_epi {ι : Type u} [Fintype ι] {U₀ : Opens X} + (π : free (R := R.over U₀) ι ⟶ M.over U₀) [Epi π] ⦃V : Opens X⦄ (hVU₀ : V ≤ U₀) + (m : M.val.obj (op V)) ⦃y : X⦄ (hyV : y ∈ V) : + ∃ (W : Opens X) (hWV : W ≤ V) (_ : y ∈ W) (a : ι → R.obj.obj (op W)), + M.val.presheaf.map (homOfLE hWV).op m = + ∑ i, a i • M.val.presheaf.map (homOfLE (le_trans hWV hVU₀)).op + ((sectionsMap π (freeSection (R := R.over U₀) i)).eval (op (Over.mk (𝟙 U₀)))) := by + -- `π` is locally surjective on sections over the slice site `J.over U₀`. + haveI hLS : Presheaf.IsLocallySurjective ((Opens.grothendieckTopology X).over U₀) + ((PresheafOfModules.toPresheaf (R.over U₀).obj).map π.val) := + isLocallySurjective_of_epi _ π + set g := (PresheafOfModules.toPresheaf (R.over U₀).obj).map π.val with hg + set A : Over U₀ := Over.mk (homOfLE hVU₀) with hA + -- `m` is a section of `(M.over U₀).val` (a sheaf on the slice site) over the object `A`. + let m' : ToType (((PresheafOfModules.toPresheaf (R.over U₀).obj).obj + (M.over U₀).val).obj (op A)) := m + have hcov : Presheaf.imageSieve g m' ∈ ((Opens.grothendieckTopology X).over U₀) A := + Presheaf.imageSieve_mem _ g _ + rw [GrothendieckTopology.mem_over_iff, Opens.mem_grothendieckTopology] at hcov + obtain ⟨W, fWV, hSf, hyW⟩ := hcov y hyV + have hWV : W ≤ V := leOfHom fWV + rw [show fWV = homOfLE hWV from Subsingleton.elim _ _, Sieve.overEquiv_iff] at hSf + set B : Over U₀ := Over.mk (homOfLE hWV ≫ A.hom) with hB + set bhom : B ⟶ A := Over.homMk (homOfLE hWV) with hbhom + obtain ⟨b, hb⟩ := hSf + obtain ⟨c, hc⟩ := exists_app_eq_sum_smul π (op B) b + refine ⟨W, hWV, hyW, c, ?_⟩ + have e1 : π.val.app (op B) b = M.val.presheaf.map (homOfLE hWV).op m := by + have hL : (g.app (op B)) b = π.val.app (op B) b := rfl + have hR : (((PresheafOfModules.toPresheaf (R.over U₀).obj).obj (M.over U₀).val).map bhom.op) m' + = M.val.presheaf.map (homOfLE hWV).op m := rfl + rw [← hL, ← hR]; exact hb + rw [← e1, hc] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + congr 1 + exact ((sectionsMap π (freeSection (R := R.over U₀) i)).property + (Over.homMk (homOfLE (le_trans hWV hVU₀)) : B ⟶ Over.mk (𝟙 U₀)).op).symm + +set_option backward.isDefEq.respectTransparency false in +set_option maxHeartbeats 1000000 in +-- Unifying the slice-site data of `exists_localGeneration_of_epi` against the chart `σ.X i₀` +-- forces some costly unfolding of the `over`/pushforward construction. +/-- A finite-type sheaf of modules over a topological space is, near any point `x`, generated by +a finite family of sections `t` over a neighborhood `U₀` of `x`: every section over `V ≤ U₀` is, +locally around each of its points, an `R`-linear combination of the `t i`. -/ +theorem exists_localGeneration_of_isFiniteType [M.IsFiniteType] (x : X) : + ∃ (ι : Type u) (_ : Fintype ι) (U₀ : Opens X) (_ : x ∈ U₀) (t : ι → M.val.obj (op U₀)), + ∀ ⦃V : Opens X⦄ (hVU₀ : V ≤ U₀) (m : M.val.obj (op V)) ⦃y : X⦄ (_ : y ∈ V), + ∃ (W : Opens X) (hWV : W ≤ V) (_ : y ∈ W) (a : ι → R.obj.obj (op W)), + M.val.presheaf.map (homOfLE hWV).op m = + ∑ i, a i • M.val.presheaf.map (homOfLE (le_trans hWV hVU₀)).op (t i) := by + -- Step 1: extract a finite local generation datum and a chart `U₀ = σ.X i₀ ∋ x`. + obtain ⟨σ, hσ⟩ := IsFiniteType.exists_localGeneratorsData (M := M) + obtain ⟨i₀, hxi₀⟩ := ((Opens.coversTop_iff (U := σ.X)).mp σ.coversTop).exists_mem x + letI : (σ.generators i₀).IsFiniteType := hσ.isFiniteType i₀ + haveI : Finite (σ.generators i₀).I := inferInstance + haveI : Fintype (σ.generators i₀).I := Fintype.ofFinite _ + -- Step 2: turn the generating sections of `M.over (σ.X i₀)` into honest sections over `U₀`. + refine ⟨(σ.generators i₀).I, inferInstance, σ.X i₀, hxi₀, + fun i => ((σ.generators i₀).s i).eval (Opposite.op (Over.mk (𝟙 (σ.X i₀)))), ?_⟩ + -- Step 3: the local-generation bridge, applied to the epimorphism `(σ.generators i₀).π`. + set G := σ.generators i₀ with hG + intro V hVU₀ m y hyV + -- `sectionsMap G.π (freeSection i) = G.s i`, so the generators match the chosen sections `t`. + have hsπ : ∀ i, sectionsMap G.π (freeSection (R := R.over (σ.X i₀)) i) = G.s i := fun i ↦ + sectionsMap_freeHomEquiv_symm_freeSection G.s i + obtain ⟨W, hWV, hyW, a, ha⟩ := M.exists_localGeneration_of_epi G.π hVU₀ m hyV + refine ⟨W, hWV, hyW, a, ?_⟩ + rw [ha] + refine Finset.sum_congr (Finset.ext fun i ↦ by simp) fun i _ ↦ ?_ + rw [hsπ i] + +/-- **Stalk of the annihilator ideal sheaf of a finite-type module.** +For a finite-type sheaf of modules `M` over a commutative sheaf of rings `R` on a topological +space, an element `ρ` of the ring stalk at `x` annihilates the module stalk `Mₓ` if and only if it +is the germ of a section of the annihilator ideal sheaf. -/ +theorem mem_annihilator_stalk_iff_of_isFiniteType [M.IsFiniteType] {x : X} + (hRcomm : ∀ (U : (Opens X)ᵒᵖ) (a b : R.obj.obj U), a * b = b * a) + (ρ : TopCat.Presheaf.stalk (C := RingCat.{u}) (X := X) R.obj x) : + ρ ∈ Module.annihilator (TopCat.Presheaf.stalk (C := RingCat.{u}) (X := X) R.obj x) + ↑(TopCat.Presheaf.stalk M.val.presheaf x) ↔ + ∃ (U : Opens X) (hx : x ∈ U) (r : R.obj.obj (op U)), + r ∈ M.val.annihilatorIdeal (op U) ∧ + TopCat.Presheaf.germ (C := RingCat.{u}) (X := X) R.obj U x hx r = ρ := by + obtain ⟨ι, hfin, U₀, hx₀, t, hgen⟩ := M.exists_localGeneration_of_isFiniteType x + letI := hfin + exact M.val.mem_annihilator_stalk_iff M.isSheaf hRcomm hx₀ t hgen ρ + +end SheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/SheafifyInstances.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/SheafifyInstances.lean new file mode 100644 index 00000000000000..ee60cac0530d90 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Topology/SheafifyInstances.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.CategoryTheory.Sites.Equivalence +public import Mathlib.CategoryTheory.Sites.Over +public import Mathlib.CategoryTheory.Sites.Whiskering +public import Mathlib.Algebra.Category.Grp.Abelian +public import Mathlib.Algebra.Category.Grp.FilteredColimits +public import Mathlib.Algebra.Category.Ring.Limits +public import Mathlib.Algebra.Category.ModuleCat.Sheaf +public import Mathlib.Topology.Sheaves.Sheaf + +/-! +# Sheafification instances for the site of opens of a topological space + +The category of opens `Opens X` of a topological space `X` (with the Grothendieck topology +`Opens.grothendieckTopology X`) is essentially small, so the abstract essentially-small-site +machinery provides sheafification of `AddCommGrpCat`-valued presheaves, both on the site itself +and on every slice. These instances make the sheaf-of-modules finite-type API (which is stated for +a general site under such hypotheses) applicable over a topological space. +-/ + +@[expose] public section + +universe u + +open CategoryTheory TopologicalSpace + +variable (X : TopCat.{u}) + +noncomputable instance : + HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{u} := + hasSheafifyEssentiallySmallSite _ _ + +instance : + (Opens.grothendieckTopology X).WEqualsLocallyBijective AddCommGrpCat.{u} := + .ofEssentiallySmall _ + +noncomputable instance (U : Opens X) : + HasSheafify ((Opens.grothendieckTopology X).over U) AddCommGrpCat.{u} := + hasSheafifyEssentiallySmallSite _ _ + +instance (U : Opens X) : + ((Opens.grothendieckTopology X).over U).WEqualsLocallyBijective AddCommGrpCat.{u} := + .ofEssentiallySmall _ + +set_option synthInstance.maxHeartbeats 100000 in +-- Synthesizing `HasSheafCompose` searches for limit preservation of +-- `forget₂ RingCat AddCommGrpCat` through several `forget₂` layers, needing a larger budget. +instance : + (Opens.grothendieckTopology X).HasSheafCompose + (forget₂ RingCat.{u} AddCommGrpCat.{u}) := + inferInstance + +set_option synthInstance.maxHeartbeats 100000 in +-- See the comment on the base-site instance above. +instance (U : Opens X) : + ((Opens.grothendieckTopology X).over U).HasSheafCompose + (forget₂ RingCat.{u} AddCommGrpCat.{u}) := + inferInstance diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf/Quasicoherent.lean b/Mathlib/AlgebraicGeometry/IdealSheaf/Quasicoherent.lean new file mode 100644 index 00000000000000..cf8a1778ff26f0 --- /dev/null +++ b/Mathlib/AlgebraicGeometry/IdealSheaf/Quasicoherent.lean @@ -0,0 +1,649 @@ +/- +Copyright (c) 2026 Christian Merten. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Merten +-/ +module + +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.IdealSheaf +public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent +public import Mathlib.Algebra.Category.ModuleCat.Topology.SheafifyInstances +public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic +public import Mathlib.AlgebraicGeometry.Modules.Presheaf +public import Mathlib.AlgebraicGeometry.Modules.Tilde +public import Mathlib.CategoryTheory.Sites.Spaces +public import Mathlib.RingTheory.LocalProperties.Basic + +/-! +# Ideal sheaves from `IdealSheafData` + +For a scheme `X`, the structure `AlgebraicGeometry.Scheme.IdealSheafData X` records the data of an +ideal sheaf via its ideals on affine opens. In this file we build the correspondence between +`IdealSheafData X` and quasi-coherent ideal sheaves of the structure sheaf. To a datum `D` we +associate an honest subsheaf of modules `D.toIdealSheaf` of `𝒪ₓ`, given by the family of ideals + +`r ∈ (D.toIdealSheaf).ideal U ↔ ∀ (V : X.affineOpens) (h : V.1 ≤ U), r|_V ∈ D.ideal V`, + +and conversely, to a quasi-coherent ideal sheaf `I` we associate the datum `I.toIdealSheafData` of +its sections on affine opens. + +## Main definitions + +* `SheafOfModules.IdealSheaf.IsQuasicoherent`: a thin wrapper saying that the underlying sheaf of + modules of an ideal sheaf is quasi-coherent. +* `AlgebraicGeometry.Scheme.IdealSheafData.toIdealSheaf`: the ideal subsheaf of `𝒪ₓ` determined by + an `IdealSheafData`. +* `SheafOfModules.IdealSheaf.toIdealSheafData`: the `IdealSheafData` of sections of a quasi-coherent + ideal sheaf. + +## Main results + +* `AlgebraicGeometry.Scheme.IdealSheafData.toIdealSheaf_ideal`: on affine opens, `toIdealSheaf` + recovers the given ideals. +* `AlgebraicGeometry.Scheme.IdealSheafData.toIdealSheaf_mono`: `toIdealSheaf` is monotone. +* `AlgebraicGeometry.Scheme.IdealSheafData.toIdealSheaf_isQuasicoherent`: `toIdealSheaf` is + quasi-coherent. +* `SheafOfModules.IdealSheaf.over_isQuasicoherent_iff`: the affine-local criterion (the *engine* of + the correspondence) characterising quasi-coherence over an affine open by the basic-open + localization condition on sections. + +The resulting order isomorphism is left for future work. +-/ + +@[expose] public section + +universe v₁ u₁ u + +open CategoryTheory Opposite TopologicalSpace + +namespace SheafOfModules.IdealSheaf + +variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C} + {R : Sheaf J RingCat.{u}} + [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})] + [∀ X, HasWeakSheafify (J.over X) AddCommGrpCat.{u}] + [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}] + +/-- An ideal sheaf is quasi-coherent if its underlying sheaf of modules is. -/ +def IsQuasicoherent (I : IdealSheaf R) : Prop := + I.toSheafOfModules.IsQuasicoherent + +end SheafOfModules.IdealSheaf + +namespace AlgebraicGeometry.Scheme.IdealSheafData + +variable {X : Scheme.{u}} + +/-- The underlying type-valued presheaf of an `AddCommGrpCat`-valued sheaf is a sheaf of types. +A local copy of the (private) lemma of the same name in `Sheaf/Annihilator.lean`. -/ +private lemma presieveIsSheaf_comp_forget {C : Type u₁} [Category.{v₁} C] + {J : GrothendieckTopology C} {A : Cᵒᵖ ⥤ AddCommGrpCat.{u}} (h : Presheaf.IsSheaf J A) : + Presieve.IsSheaf J (A ⋙ CategoryTheory.forget AddCommGrpCat.{u}) := + Presieve.isSheaf_iso J (Functor.isoWhiskerLeft A AddCommGrpCat.coyonedaObjIsoForget) + (h (AddCommGrpCat.of (ULift.{u} ℤ))) + +/-- An element of `Γ(X, W)` (with `W` affine) lies in `D.ideal W` as soon as, locally on a cover of +`W` by basic opens, its restriction lies in the corresponding ideal of the datum. -/ +private lemma mem_ideal_of_basicOpen_cover (D : X.IdealSheafData) {W : X.affineOpens} + {s : Γ(X, W.1)} + (H : ∀ x : W.1, ∃ g : Γ(X, W.1), (x : X) ∈ X.basicOpen g ∧ + (X.ringCatSheaf.obj.map (homOfLE (X.basicOpen_le g)).op).hom s ∈ + D.ideal (X.affineBasicOpen g)) : + s ∈ D.ideal W := by + choose g hxg hg using H + have hspan : Ideal.span (Set.range g) = ⊤ := by + rw [← W.2.self_le_iSup_basicOpen_iff] + intro x hx + exact TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨g ⟨x, hx⟩, ⟨x, hx⟩, rfl⟩, hxg ⟨x, hx⟩⟩ + have inst := W.2.isLocalization_basicOpen + refine Submodule.mem_of_isLocalized_span (Set.range g) hspan + (fun i ↦ Γ(X, X.basicOpen i.1)) (fun i ↦ Algebra.linearMap Γ(X, W.1) Γ(X, X.basicOpen i.1)) ?_ + rintro ⟨_, j, rfl⟩ + rw [Ideal.localized₀_eq_restrictScalars_map, Submodule.restrictScalars_mem, + show algebraMap Γ(X, W.1) Γ(X, X.basicOpen (g j)) = + (X.presheaf.map (homOfLE (X.basicOpen_le (g j))).op).hom from rfl, + D.map_ideal_basicOpen W (g j)] + exact hg j + +variable (D : X.IdealSheafData) + +set_option backward.isDefEq.respectTransparency false in +/-- The submodule system on `unit 𝒪ₓ` cut out by an `IdealSheafData`: over an open `V`, the sections +`r` whose restriction to every affine open `W ≤ V` lies in `D.ideal W`. -/ +noncomputable def toSubmodule : + (PresheafOfModules.unit X.ringCatSheaf.obj).Submodule := + let R : Sheaf _ RingCat.{u} := X.ringCatSheaf + { toSubmodule := fun V ↦ + { carrier := { r | ∀ (W : X.affineOpens) (i : V ⟶ op W.1), + (R.obj.map i).hom r ∈ D.ideal W } + add_mem' := fun ha hb W i ↦ by rw [map_add]; exact add_mem (ha W i) (hb W i) + zero_mem' := fun W i ↦ by rw [map_zero]; exact zero_mem _ + smul_mem' := fun c r hr W i ↦ by + rw [smul_eq_mul, map_mul]; exact Ideal.mul_mem_left _ _ (hr W i) } + map_mem := @fun U V f m hm W i ↦ by + have comp : (R.obj.map i).hom ((R.obj.map f).hom m) = (R.obj.map (f ≫ i)).hom m := by + rw [R.obj.map_comp, RingCat.hom_comp, RingHom.comp_apply] + rw [show (PresheafOfModules.unit R.obj).map f m = (R.obj.map f).hom m from rfl, comp] + exact hm W (f ≫ i) } + +set_option backward.isDefEq.respectTransparency false in +/-- The ideal subsheaf of `𝒪ₓ` determined by an `IdealSheafData`. -/ +noncomputable def toIdealSheaf : SheafOfModules.IdealSheaf X.ringCatSheaf where + toSubmodule := D.toSubmodule + isSheaf := by + let R : Sheaf _ RingCat.{u} := X.ringCatSheaf + have comp : ∀ {A B E : (Opens X)ᵒᵖ} (p : A ⟶ B) (q : B ⟶ E) (t : R.obj.obj A), + (R.obj.map (p ≫ q)).hom t = (R.obj.map q).hom ((R.obj.map p).hom t) := + fun p q t ↦ by rw [R.obj.map_comp, RingCat.hom_comp, RingHom.comp_apply] + let F : (Opens X)ᵒᵖ ⥤ Type u := + (PresheafOfModules.unit R.obj).presheaf ⋙ CategoryTheory.forget AddCommGrpCat.{u} + have hF : Presieve.IsSheaf (Opens.grothendieckTopology X) F := + presieveIsSheaf_comp_forget (SheafOfModules.unit R).isSheaf + let G : Subfunctor F := + { obj := fun V ↦ { r : R.obj.obj V | ∀ (W : X.affineOpens) (i : V ⟶ op W.1), + (R.obj.map i).hom r ∈ D.ideal W } + map := @fun U V f m hm ↦ D.toSubmodule.map_mem f hm } + have hG : Presieve.IsSheaf (Opens.grothendieckTopology X) G.toFunctor := by + rw [G.isSheaf_iff hF] + intro U s hs W i + apply D.mem_ideal_of_basicOpen_cover + intro x + have hW : W.1 ≤ U.unop := leOfHom i.unop + rw [Opens.mem_grothendieckTopology] at hs + obtain ⟨V, f, hVf, hxV⟩ := hs x.1 (hW x.2) + obtain ⟨g, hgV, hxg⟩ := W.2.exists_basicOpen_le (V := V) ⟨x.1, hxV⟩ x.2 + refine ⟨g, hxg, ?_⟩ + have hmem := hVf (X.affineBasicOpen g) (homOfLE hgV).op + -- `hmem : (R.obj.map (homOfLE hgV).op).hom (F.map f.op s) ∈ D.ideal (X.affineBasicOpen g)` + rw [show F.map f.op s = (R.obj.map f.op).hom s from rfl, ← comp] at hmem + change (R.obj.map (homOfLE (X.basicOpen_le g)).op).hom ((R.obj.map i).hom s) ∈ _ + rw [← comp, Subsingleton.elim (i ≫ (homOfLE (X.basicOpen_le g)).op) + (f.op ≫ (homOfLE hgV).op)] + exact hmem + rw [Presheaf.isSheaf_iff_isSheaf_forget (J := Opens.grothendieckTopology X) + (s := CategoryTheory.forget AddCommGrpCat.{u}), isSheaf_iff_isSheaf_of_type] + exact Presieve.isSheaf_iso (Opens.grothendieckTopology X) + (NatIso.ofComponents (fun _ ↦ Iso.refl _) (by intros; rfl)) hG + +set_option backward.isDefEq.respectTransparency false in +lemma toIdealSheaf_ideal (V : X.affineOpens) : + (D.toIdealSheaf).ideal (op V.1) = D.ideal V := by + ext r + constructor + · intro hr + have h1 := hr V (𝟙 (op V.1)) + rwa [CategoryTheory.Functor.map_id, RingCat.hom_id, RingHom.id_apply] at h1 + · intro hr W i + have h : W.1 ≤ V.1 := leOfHom i.unop + rw [show i = (homOfLE h).op from Subsingleton.elim _ _, ← D.map_ideal h] + exact Ideal.mem_map_of_mem _ hr + +lemma toIdealSheaf_mono : Monotone (toIdealSheaf (X := X)) := by + intro D D' hD U r hr W i + exact hD W (hr W i) + +end AlgebraicGeometry.Scheme.IdealSheafData + +namespace SheafOfModules.IdealSheaf + +open AlgebraicGeometry + +variable {X : Scheme.{u}} + +section Engine + +open AlgebraicGeometry.Scheme.Modules CategoryTheory.Limits Submodule IsLocalizedModule + +/-- The corestriction `J ⟶ Ideal.map (algebraMap A B) J` of the algebra map exhibits the extended +ideal as a localization away from `f`, whenever `B` is the localization of `A` away from `f`. -/ +theorem isLocalizedModule_idealMap {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] (f : A) + [IsLocalization.Away f B] (J : Ideal A) : + IsLocalizedModule (.powers f) (Algebra.idealMap B J) := by + rw [Algebra.idealMap_eq_ofEq_comp_toLocalized₀ B (.powers f) J] + exact IsLocalizedModule.of_linearEquiv _ _ _ + +/-- **Algebraic bridge.** For a localization `B` of `A` away from `f`, the corestriction `c` of the +algebra map to ideals `J ⟶ J'` exhibits `J'` as a localization of `J` away from `f` if and only if +`J'` is the extension of scalars `J.map (algebraMap A B)`. -/ +theorem isLocalizedModule_corestrict_iff {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] + (f : A) [IsLocalization.Away f B] (J : Ideal A) (J' : Ideal B) + (c : J →ₗ[A] J'.restrictScalars A) (hc : ∀ x : J, ((c x : B)) = algebraMap A B (x : A)) : + IsLocalizedModule (.powers f) c ↔ Ideal.map (algebraMap A B) J = J' := by + constructor + · intro hloc + apply le_antisymm + · rw [Ideal.map_le_iff_le_comap] + intro x hx + rw [Ideal.mem_comap, ← hc ⟨x, hx⟩] + exact (c ⟨x, hx⟩).2 + · intro y hy + obtain ⟨⟨m, s⟩, hms⟩ := IsLocalizedModule.surj (.powers f) c ⟨y, hy⟩ + have hval : algebraMap A B (s : A) * y = algebraMap A B (m : A) := by + have h2 := congr(Subtype.val $hms) + simp only [SetLike.val_smul, Submonoid.smul_def] at h2 + rw [hc m] at h2 + simpa [Algebra.smul_def] using h2 + have hunit : IsUnit (algebraMap A B (s : A)) := by + obtain ⟨n, hn⟩ := s.2 + rw [← hn, map_pow] + exact (IsLocalization.Away.algebraMap_isUnit f).pow n + obtain ⟨u, hu⟩ := hunit + have : y = (↑u⁻¹ : B) * algebraMap A B (m : A) := by + rw [← hval, ← hu, ← mul_assoc, Units.inv_mul, one_mul] + rw [this] + exact Ideal.mul_mem_left _ _ (Ideal.mem_map_of_mem _ m.2) + · intro hJ + subst hJ + have hce : c = Algebra.idealMap B J := by ext x; exact hc x + rw [hce] + exact isLocalizedModule_idealMap f J + +/-- Quasi-coherence is preserved by the equivalence `Scheme.Modules.overEquiv` (which identifies +sheaves of `𝒪_X`-modules over the slice site over `U` with sheaves of `𝒪_U`-modules). -/ +private lemma isQuasicoherent_overEquiv_functor {U : X.Opens} + (K : SheafOfModules (X.ringCatSheaf.over U)) [K.IsQuasicoherent] : + ((overEquiv U).functor.obj K).IsQuasicoherent := by + change ((Opens.sheafOfModulesEquivOver U X.ringCatSheaf).functor.obj K).IsQuasicoherent + unfold Opens.sheafOfModulesEquivOver + apply +allowSynthFailures SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint + · exact Opens.sheafOfModulesEquivOverUnit U X.ringCatSheaf + · intro Y + set G := (Opens.overEquivalence U).symm.functor + have hG : G.IsContinuous (Opens.grothendieckTopology ↥U) + ((Opens.grothendieckTopology ↥X).over U) := + inferInstanceAs <| U.overEquivalence.inverse.IsContinuous _ _ + have : RepresentablyFlat (Over.post (X := Y) G) := RepresentablyFlat.of_isRightAdjoint _ + exact Functor.isContinuous_of_coverPreserving + (compatiblePreservingOfFlat _ (Over.post (X := Y) G)) + ((CoverPreserving.of_isContinuous (F := G) _ _).overPost Y) + +private lemma isQuasicoherent_overEquiv_inverse {U : X.Opens} (N : (U : Scheme.{u}).Modules) + [N.IsQuasicoherent] : + ((overEquiv U).inverse.obj N).IsQuasicoherent := by + change ((Opens.sheafOfModulesEquivOver U X.ringCatSheaf).inverse.obj N).IsQuasicoherent + unfold Opens.sheafOfModulesEquivOver + apply +allowSynthFailures SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint + · exact Opens.sheafOfModulesEquivOverInverseUnit U X.ringCatSheaf + · intro Y + set G := (Opens.overEquivalence U).symm.inverse + have hG : G.IsContinuous ((Opens.grothendieckTopology ↥X).over U) + (Opens.grothendieckTopology ↥U) := + inferInstanceAs <| U.overEquivalence.functor.IsContinuous _ _ + have : RepresentablyFlat (Over.post (X := Y) G) := RepresentablyFlat.of_isRightAdjoint _ + exact Functor.isContinuous_of_coverPreserving + (compatiblePreservingOfFlat _ (Over.post (X := Y) G)) + ((CoverPreserving.of_isContinuous (F := G) _ _).overPost Y) + · exact ‹N.IsQuasicoherent› + +/-- Over an open `U`, the slice-site restriction `M.over U` is quasi-coherent iff its transport +`M.restrict U.ι` to `𝒪_U`-modules is. -/ +private lemma over_isQuasicoherent_iff_restrict (M : SheafOfModules X.ringCatSheaf) (U : X.Opens) : + (M.over U).IsQuasicoherent ↔ ((restrictFunctor U.ι).obj M).IsQuasicoherent := by + constructor + · intro h + haveI := isQuasicoherent_overEquiv_functor (M.over U) + exact (SheafOfModules.isQuasicoherent (U : Scheme.{u}).ringCatSheaf).prop_of_iso + ((overFunctorEquiv U).app M) ‹_› + · intro h + haveI : ((overEquiv U).functor.obj (M.over U)).IsQuasicoherent := + (SheafOfModules.isQuasicoherent (U : Scheme.{u}).ringCatSheaf).prop_of_iso + ((overFunctorEquiv U).app M).symm h + haveI := isQuasicoherent_overEquiv_inverse ((overEquiv U).functor.obj (M.over U)) + exact (SheafOfModules.isQuasicoherent (X.ringCatSheaf.over U)).prop_of_iso + ((overEquiv U).unitIso.app (M.over U)).symm ‹_› + +/-- Restriction along an isomorphism of schemes neither creates nor destroys quasi-coherence. -/ +private lemma restrictFunctor_isQuasicoherent_iff_of_isIso {Y Z : Scheme.{u}} (g : Y ⟶ Z) + [IsIso g] (K : Z.Modules) : + ((restrictFunctor g).obj K).IsQuasicoherent ↔ K.IsQuasicoherent := by + constructor + · intro h + haveI : ((restrictFunctor g).obj K).IsQuasicoherent := h + haveI := Scheme.Modules.isQuasicoherent_restrictFunctor (inv g) ((restrictFunctor g).obj K) + have iso : (restrictFunctor g ⋙ restrictFunctor (inv g)).obj K ≅ K := + ((restrictFunctorComp (inv g) g).app K).symm ≪≫ + (restrictFunctorCongr (show inv g ≫ g = 𝟙 Z by simp)).app K ≪≫ + (restrictFunctorId).app K + exact (SheafOfModules.isQuasicoherent Z.ringCatSheaf).prop_of_iso iso ‹_› + · intro h + haveI : K.IsQuasicoherent := h + infer_instance + +/-- For an affine open `V`, transporting `M` to `Spec Γ(X, V)` along `IsAffineOpen.fromSpec` +preserves and reflects quasi-coherence. -/ +private lemma restrict_isQuasicoherent_iff_fromSpec (V : X.affineOpens) + (M : SheafOfModules X.ringCatSheaf) : + ((restrictFunctor V.1.ι).obj M).IsQuasicoherent ↔ + ((restrictFunctor V.2.fromSpec).obj M).IsQuasicoherent := by + have iso : (restrictFunctor V.2.fromSpec).obj M ≅ + (restrictFunctor V.2.isoSpec.inv).obj ((restrictFunctor V.1.ι).obj M) := + (restrictFunctorCongr (show V.2.fromSpec = V.2.isoSpec.inv ≫ V.1.ι from + (V.2.isoSpec_inv_ι).symm)).app M ≪≫ + (restrictFunctorComp V.2.isoSpec.inv V.1.ι).app M + constructor + · intro hN + haveI : ((restrictFunctor V.2.isoSpec.inv).obj + ((restrictFunctor V.1.ι).obj M)).IsQuasicoherent := + (restrictFunctor_isQuasicoherent_iff_of_isIso V.2.isoSpec.inv _).mpr hN + exact (SheafOfModules.isQuasicoherent (Spec Γ(X, V.1)).ringCatSheaf).prop_of_iso iso.symm ‹_› + · intro hP + haveI : ((restrictFunctor V.2.isoSpec.inv).obj + ((restrictFunctor V.1.ι).obj M)).IsQuasicoherent := + (SheafOfModules.isQuasicoherent (Spec Γ(X, V.1)).ringCatSheaf).prop_of_iso iso hP + exact (restrictFunctor_isQuasicoherent_iff_of_isIso V.2.isoSpec.inv _).mp ‹_› + +/-- Quasi-coherence of `M.over V` for an affine open `V` is equivalent to the `tilde`-localizing +condition on `Spec Γ(X, V)`: the basic-open restriction maps of the transported sheaf are +localizations. This is the categorical core of `over_isQuasicoherent_iff`. -/ +lemma over_isQuasicoherent_iff_isLocalizing (V : X.affineOpens) + (M : SheafOfModules X.ringCatSheaf) : + (M.over V.1).IsQuasicoherent ↔ + IsLocalizing (modulesSpecToSheaf.obj ((restrictFunctor V.2.fromSpec).obj M)) := by + rw [over_isQuasicoherent_iff_restrict, restrict_isQuasicoherent_iff_fromSpec, + AlgebraicGeometry.isQuasicoherent_iff_isIso_fromTildeΓ, + AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing] + +end Engine + +set_option backward.isDefEq.respectTransparency false in +/-- **Affine-local engine of the `IdealSheafData ↔ quasi-coherent ideal sheaf` correspondence.** + +Over an affine open `V`, the restriction of an ideal subsheaf `I` of `𝒪ₓ` is quasi-coherent if and +only if its sections satisfy the basic-open localization condition: for every `f : Γ(X, V)`, the +ideal on the basic open `D(f)` is obtained from the ideal on `V` by extension of scalars along the +localization map `Γ(X, V) → Γ(X, D(f))`. + +This is the affine-local heart of the correspondence between `Scheme.IdealSheafData` and +quasi-coherent ideal sheaves. Both directions reduce, via the equivalence between sheaves of modules +on `𝒪_X` restricted to `V` and sheaves of `𝒪_V`-modules (`Scheme.Modules.overFunctorEquiv`, +`Scheme.Modules.overEquiv`) and the identification `V ≅ Spec Γ(X, V)` (`IsAffineOpen.isoSpec`), to +the `tilde`-equivalence on the affine scheme `Spec Γ(X, V)`: a module on `Spec R` is quasi-coherent +iff its restriction maps to basic opens are localizations +(`AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing`, +`AlgebraicGeometry.isQuasicoherent_iff_isIso_fromTildeΓ`), and for the structure sheaf the localized +sections of an ideal subsheaf are precisely the extension of scalars +(`Submodule.localized₀`, `IsAffineOpen.isLocalization_basicOpen`). -/ +lemma over_isQuasicoherent_iff (I : SheafOfModules.IdealSheaf X.ringCatSheaf) (V : X.affineOpens) : + (I.toSheafOfModules.over V.1).IsQuasicoherent ↔ + ∀ f : Γ(X, V.1), + (I.ideal (op V.1)).map (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = + I.ideal (op (X.basicOpen f)) := by + rw [over_isQuasicoherent_iff_isLocalizing V I.toSheafOfModules] + refine forall_congr' fun f => ?_ + haveI := V.2.isLocalization_basicOpen f + -- The basic-open restriction map of the transported ideal sheaf on `Spec Γ(X, V)`, identified + -- via `Scheme.Modules.restrictAppIso` and `IsAffineOpen.fromSpec_image_basicOpen` with the + -- corestriction of the localization map `Γ(X, V) → Γ(X, D(f))` to the ideals, is a localization + -- away from `f` if and only if `Ideal.map` recovers the ideal on `D(f)` + -- (`isLocalizedModule_corestrict_iff`). The remaining step is the `Γ(X, V)`-linear identification + -- of the section modules `Γ(_, ⊤)` and `Γ(_, D(f))` of the transported sheaf with the ideal + -- sections of `I`, compatibly with the restriction map. + set N := (Scheme.Modules.restrictFunctor V.2.fromSpec).obj I.toSheafOfModules with hN + have e1 : V.2.fromSpec ''ᵁ (⊤ : (Spec Γ(X, V.1)).Opens) = V.1 := by + rw [Scheme.Hom.image_top_eq_opensRange]; exact V.2.opensRange_fromSpec + have hW1 : (op V.1 : (Opens X)ᵒᵖ) = op (V.2.fromSpec ''ᵁ ⊤) := congrArg op e1.symm + have key : (V.2.fromSpec.appIso ⊤).inv ≫ X.presheaf.map (eqToHom hW1.symm) = + (Scheme.ΓSpecIso Γ(X, V.1)).hom := by + rw [Iso.inv_comp_eq, Scheme.Hom.appIso_hom, V.2.fromSpec_app_of_le _ e1.ge] + simp only [Category.assoc] + rw [← Functor.map_comp_assoc, Subsingleton.elim ((homOfLE le_top).op ≫ _) + (𝟙 (op (⊤ : (Spec Γ(X, V.1)).Opens))), + CategoryTheory.Functor.map_id, Category.id_comp, Iso.inv_hom_id, Category.comp_id] + congr 1 + have key' : (Scheme.ΓSpecIso Γ(X, V.1)).inv ≫ (V.2.fromSpec.appIso ⊤).inv = + X.presheaf.map (eqToHom hW1) := by + rw [Iso.inv_comp_eq, ← key] + simp only [Category.assoc, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, + CategoryTheory.Functor.map_id, Category.comp_id] + have gkey : ∀ (U : (Spec Γ(X, V.1)).Opens) (hW : V.2.fromSpec ''ᵁ U ≤ V.1), + (Scheme.ΓSpecIso Γ(X, V.1)).inv ≫ (Spec Γ(X, V.1)).presheaf.map U.leTop.op ≫ + (V.2.fromSpec.appIso U).inv = X.presheaf.map (homOfLE hW).op := by + intro U hW + rw [Scheme.Hom.appIso_inv_naturality] + calc (Scheme.ΓSpecIso Γ(X, V.1)).inv ≫ (V.2.fromSpec.appIso ⊤).inv ≫ + X.presheaf.map ((Scheme.Hom.opensFunctor V.2.fromSpec).op.map U.leTop.op) + = ((Scheme.ΓSpecIso Γ(X, V.1)).inv ≫ (V.2.fromSpec.appIso ⊤).inv) ≫ + X.presheaf.map ((Scheme.Hom.opensFunctor V.2.fromSpec).op.map U.leTop.op) := by + rw [Category.assoc] + _ = X.presheaf.map (eqToHom hW1) ≫ + X.presheaf.map ((Scheme.Hom.opensFunctor V.2.fromSpec).op.map U.leTop.op) := by + rw [key'] + _ = X.presheaf.map (homOfLE hW).op := by rw [← Functor.map_comp]; congr 1 + have hact : ∀ (U : (Spec Γ(X, V.1)).Opens) (W' : X.Opens) (hUW : V.2.fromSpec ''ᵁ U = W') + (hle : W' ≤ V.1) (r : Γ(X, V.1)) + (x : ((modulesSpecToSheaf.obj N).obj.obj (op U))), + (I.toSheafOfModules.val.map (eqToHom (congrArg op hUW))).hom (r • x) = + (X.presheaf.map (homOfLE hle).op).hom r • + (I.toSheafOfModules.val.map (eqToHom (congrArg op hUW))).hom x := by + intro U W' hUW hle r x + have hW : V.2.fromSpec ''ᵁ U ≤ V.1 := hUW ▸ hle + rw [Scheme.Modules.smul_Spec_def (M := N) (U := U), ← Scheme.Modules.smul_apply] + have h := Scheme.Modules.smul_restrictAppIso_hom (f := V.2.fromSpec) I.toSheafOfModules U + (((Spec Γ(X, V.1)).presheaf.map U.leTop.op) ((Scheme.ΓSpecIso Γ(X, V.1)).inv r)) + simp only [Scheme.Modules.restrictAppIso, Iso.refl_hom, Category.comp_id, Category.id_comp] at h + rw [h] + erw [Scheme.Modules.smul_apply, PresheafOfModules.map_smul] + congr 1 + have hg := ConcreteCategory.congr_hom (gkey U hW) r + simp only [CommRingCat.comp_apply] at hg + rw [show (X.ringCatSheaf.obj.map (eqToHom (congrArg op hUW))).hom + ((V.2.fromSpec.appIso U).inv (((Spec Γ(X, V.1)).presheaf.map U.leTop.op) + ((Scheme.ΓSpecIso Γ(X, V.1)).inv r))) + = (X.ringCatSheaf.obj.map (eqToHom (congrArg op hUW))).hom + ((X.presheaf.map (homOfLE hW).op).hom r) from by rw [← hg]] + rw [show (X.ringCatSheaf.obj.map (eqToHom (congrArg op hUW))).hom + ((X.presheaf.map (homOfLE hW).op).hom r) + = (X.presheaf.map (eqToHom (congrArg op hUW))).hom + ((X.presheaf.map (homOfLE hW).op).hom r) from rfl] + rw [← CommRingCat.comp_apply, ← Functor.map_comp] + congr 2 + -- basic opens facts + have e2 : V.2.fromSpec ''ᵁ (PrimeSpectrum.basicOpen f) = X.basicOpen f := + V.2.fromSpec_image_basicOpen f + -- e₁ : M⊤ ≃ₗ[A] ↥(I.ideal (op V.1)) + let e₁ : ((modulesSpecToSheaf.obj N).obj.obj (op ⊤)) ≃ₗ[Γ(X, V.1)] ↥(I.ideal (op V.1)) := + { toFun := fun x => (I.toSheafOfModules.val.map (eqToHom (congrArg op e1))).hom x + invFun := fun y => (I.toSheafOfModules.val.map (eqToHom (congrArg op e1.symm))).hom y + map_add' := fun a b => by rw [map_add] + map_smul' := fun r x => by + simp only [RingHom.id_apply] + rw [hact ⊤ V.1 e1 le_rfl r x] + congr 1 + rw [Subsingleton.elim (homOfLE (le_refl V.1)).op (𝟙 (op V.1)), + CategoryTheory.Functor.map_id]; rfl + left_inv := fun x => Subtype.ext (by + change (X.ringCatSheaf.obj.map (eqToHom (congrArg op e1.symm))).hom + ((X.ringCatSheaf.obj.map (eqToHom (congrArg op e1))).hom x.1) = x.1 + rw [← RingCat.comp_apply, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, + CategoryTheory.Functor.map_id, RingCat.id_apply]) + right_inv := fun y => Subtype.ext (by + change (X.ringCatSheaf.obj.map (eqToHom (congrArg op e1))).hom + ((X.ringCatSheaf.obj.map (eqToHom (congrArg op e1.symm))).hom y.1) = y.1 + rw [← RingCat.comp_apply, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, + CategoryTheory.Functor.map_id, RingCat.id_apply]) } + letI : Algebra Γ(X, V.1) ↑(X.ringCatSheaf.obj.obj (op (X.basicOpen f))) := + (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom.toAlgebra + let e₂ : ((modulesSpecToSheaf.obj N).obj.obj (op (PrimeSpectrum.basicOpen f))) ≃ₗ[Γ(X, V.1)] + ↥((I.ideal (op (X.basicOpen f))).restrictScalars Γ(X, V.1)) := + { toFun := fun x => (I.toSheafOfModules.val.map (eqToHom (congrArg op e2))).hom x + invFun := fun y => (I.toSheafOfModules.val.map (eqToHom (congrArg op e2.symm))).hom y + map_add' := fun a b => by rw [map_add] + map_smul' := fun r x => by + simp only [RingHom.id_apply] + rw [hact (PrimeSpectrum.basicOpen f) (X.basicOpen f) e2 (X.basicOpen_le f) r x] + exact algebraMap_smul Γ(X, X.basicOpen f) r _ + left_inv := fun x => Subtype.ext (by + change (X.ringCatSheaf.obj.map (eqToHom (congrArg op e2.symm))).hom + ((X.ringCatSheaf.obj.map (eqToHom (congrArg op e2))).hom x.1) = x.1 + rw [← RingCat.comp_apply, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, + CategoryTheory.Functor.map_id, RingCat.id_apply]) + right_inv := fun y => Subtype.ext (by + change (X.ringCatSheaf.obj.map (eqToHom (congrArg op e2))).hom + ((X.ringCatSheaf.obj.map (eqToHom (congrArg op e2.symm))).hom y.1) = y.1 + rw [← RingCat.comp_apply, ← Functor.map_comp, eqToHom_trans, eqToHom_refl, + CategoryTheory.Functor.map_id, RingCat.id_apply]) } + set ψ := ((modulesSpecToSheaf.obj N).obj.map (PrimeSpectrum.basicOpen f).leTop.op).hom with hψ + let c := e₂.toLinearMap ∘ₗ ψ ∘ₗ e₁.symm.toLinearMap + have hc : ∀ x : I.ideal (op V.1), + ((c x).val : Γ(X, X.basicOpen f)) + = algebraMap Γ(X, V.1) Γ(X, X.basicOpen f) x.1 := by + intro x + change (X.ringCatSheaf.obj.map (eqToHom (congrArg op e2))) + ((X.ringCatSheaf.obj.map ((Scheme.Hom.opensFunctor V.2.fromSpec).op.map + (PrimeSpectrum.basicOpen f).leTop.op)) + ((X.ringCatSheaf.obj.map (eqToHom (congrArg op e1.symm))) x.1)) + = algebraMap Γ(X, V.1) Γ(X, X.basicOpen f) x.1 + have hcomp : X.ringCatSheaf.obj.map (eqToHom (congrArg op e1.symm)) ≫ + X.ringCatSheaf.obj.map ((Scheme.Hom.opensFunctor V.2.fromSpec).op.map + (PrimeSpectrum.basicOpen f).leTop.op) ≫ + X.ringCatSheaf.obj.map (eqToHom (congrArg op e2)) + = X.ringCatSheaf.obj.map (homOfLE (X.basicOpen_le f)).op := by + rw [← Functor.map_comp, ← Functor.map_comp]; congr 1 + have hap := ConcreteCategory.congr_hom hcomp x.1 + simp only [RingCat.comp_apply] at hap + exact hap + have main := isLocalizedModule_corestrict_iff (A := Γ(X, V.1)) (B := Γ(X, X.basicOpen f)) f + (I.ideal (op V.1)) (I.ideal (op (X.basicOpen f))) c hc + have hiff : IsLocalizedModule (.powers f) c ↔ IsLocalizedModule (.powers f) ψ := by + rw [show c = e₂.toLinearMap ∘ₗ (ψ ∘ₗ e₁.symm.toLinearMap) from rfl] + rw [IsLocalizedModule.comp_iff_of_bijective_left (Submonoid.powers f) e₂.toLinearMap + e₂.bijective] + rw [IsLocalizedModule.comp_iff_of_bijective_right (Submonoid.powers f) e₁.symm.toLinearMap + e₁.symm.bijective] + exact hiff.symm.trans main + +set_option backward.isDefEq.respectTransparency false in +/-- The forward direction of `over_isQuasicoherent_iff`. -/ +lemma map_ideal_eq_of_isQuasicoherent + (I : SheafOfModules.IdealSheaf X.ringCatSheaf) (hI : I.IsQuasicoherent) + (V : X.affineOpens) (f : Γ(X, V.1)) : + (I.ideal (op V.1)).map (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = + I.ideal (op (X.basicOpen f)) := by + haveI : I.toSheafOfModules.IsQuasicoherent := hI + exact (I.over_isQuasicoherent_iff V).mp (isQuasicoherent_over I.toSheafOfModules V.1) f + +end SheafOfModules.IdealSheaf + +namespace AlgebraicGeometry.Scheme.IdealSheafData + +variable {X : Scheme.{u}} + +set_option backward.isDefEq.respectTransparency false in +/-- The quasi-coherent ideal sheaf `D.toIdealSheaf` associated to an `IdealSheafData` is indeed +quasi-coherent. -/ +theorem toIdealSheaf_isQuasicoherent (D : X.IdealSheafData) : + (D.toIdealSheaf).IsQuasicoherent := by + haveI : ∀ V : X.affineOpens, + (D.toIdealSheaf.toSheafOfModules.over ((fun V : X.affineOpens ↦ V.1) V)).IsQuasicoherent := by + intro V + rw [D.toIdealSheaf.over_isQuasicoherent_iff V] + intro f + rw [D.toIdealSheaf_ideal V, D.map_ideal_basicOpen V f] + exact (D.toIdealSheaf_ideal (X.affineBasicOpen f)).symm + exact SheafOfModules.IsQuasicoherent.of_coversTop D.toIdealSheaf.toSheafOfModules + (fun V : X.affineOpens ↦ V.1) + ((Opens.coversTop_iff _ (fun V : X.affineOpens ↦ V.1)).mpr (iSup_affineOpens_eq_top X)) + +end AlgebraicGeometry.Scheme.IdealSheafData + +namespace SheafOfModules.IdealSheaf + +open AlgebraicGeometry + +variable {X : Scheme.{u}} + +set_option backward.isDefEq.respectTransparency false in +/-- The `IdealSheafData` associated to a quasi-coherent ideal sheaf of `𝒪ₓ`. On an affine open `V` +its ideal is the sections `I(V)`; the compatibility with basic opens is exactly the quasi-coherence +of `I` (`SheafOfModules.IdealSheaf.map_ideal_eq_of_isQuasicoherent`). -/ +noncomputable def toIdealSheafData (I : SheafOfModules.IdealSheaf X.ringCatSheaf) + (hI : I.IsQuasicoherent) : X.IdealSheafData where + ideal V := I.ideal (op V.1) + map_ideal_basicOpen U f := I.map_ideal_eq_of_isQuasicoherent hI U f + +set_option backward.isDefEq.respectTransparency false in +@[simp] +lemma toIdealSheafData_ideal (I : SheafOfModules.IdealSheaf X.ringCatSheaf) + (hI : I.IsQuasicoherent) (V : X.affineOpens) : + (I.toIdealSheafData hI).ideal V = I.ideal (op V.1) := + rfl + +set_option backward.isDefEq.respectTransparency false in +lemma toIdealSheafData_mono {I J : SheafOfModules.IdealSheaf X.ringCatSheaf} + (hI : I.IsQuasicoherent) (hJ : J.IsQuasicoherent) (hIJ : I ≤ J) : + I.toIdealSheafData hI ≤ J.toIdealSheafData hJ := by + rw [AlgebraicGeometry.Scheme.IdealSheafData.le_def] + intro V + exact (SheafOfModules.IdealSheaf.le_def.mp hIJ) (op V.1) + +set_option backward.isDefEq.respectTransparency false in +/-- The `IdealSheafData` associated to a quasi-coherent ideal sheaf `I` recovers `I`: +`(I.toIdealSheafData hI).toIdealSheaf = I`. The nontrivial inclusion says that a section which is +affine-locally in `I` lies in `I`, and is proved by gluing via `I.isSheaf` (the sieve of affine +opens contained in the given open is covering, since affine opens form a basis). -/ +lemma toIdealSheafData_toIdealSheaf (I : SheafOfModules.IdealSheaf X.ringCatSheaf) + (hI : I.IsQuasicoherent) : + (I.toIdealSheafData hI).toIdealSheaf = I := by + letI R : Sheaf _ RingCat.{u} := X.ringCatSheaf + refine IdealSheaf.ext fun U => le_antisymm ?_ ?_ + · -- nontrivial inclusion: affine-local membership implies membership + intro r hr + let F : (Opens X)ᵒᵖ ⥤ Type u := + (PresheafOfModules.unit R.obj).presheaf ⋙ CategoryTheory.forget AddCommGrpCat.{u} + have hF : Presieve.IsSheaf (Opens.grothendieckTopology X) F := + AlgebraicGeometry.Scheme.IdealSheafData.presieveIsSheaf_comp_forget + (SheafOfModules.unit R).isSheaf + let GI : Subfunctor F := + { obj := fun V ↦ { r : R.obj.obj V | r ∈ I.ideal V } + map := @fun A B f m hm ↦ I.toSubmodule.map_mem f hm } + have hGI : Presieve.IsSheaf (Opens.grothendieckTopology X) GI.toFunctor := by + have hI' : Presieve.IsSheaf (Opens.grothendieckTopology X) + (I.toSubmodule.toPresheafOfModules.presheaf ⋙ + CategoryTheory.forget AddCommGrpCat.{u}) := + AlgebraicGeometry.Scheme.IdealSheafData.presieveIsSheaf_comp_forget I.isSheaf + exact Presieve.isSheaf_iso _ + (NatIso.ofComponents (fun _ ↦ Iso.refl _) (by intros; rfl)) hI' + refine (GI.isSheaf_iff hF).mp hGI U r ?_ + rw [Opens.mem_grothendieckTopology] + intro x hx + obtain ⟨W, hWaff, hxW, hWU⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens hx + refine ⟨W, homOfLE hWU, ?_, hxW⟩ + change (R.obj.map (homOfLE hWU).op).hom r ∈ I.ideal (op W) + exact hr ⟨W, hWaff⟩ (homOfLE hWU).op + · -- trivial inclusion: `I` is restriction-stable + intro r hr W i + have hmem := I.toSubmodule.map_mem i hr + rwa [show (PresheafOfModules.unit R.obj).map i r = (R.obj.map i).hom r from rfl] at hmem + +end SheafOfModules.IdealSheaf + +namespace AlgebraicGeometry.Scheme.IdealSheafData + +variable {X : Scheme.{u}} + +set_option backward.isDefEq.respectTransparency false in +/-- **The order isomorphism realizing the equivalence between `Scheme.IdealSheafData X` and +quasi-coherent ideal sheaves of `𝒪ₓ`.** A datum `D` is sent to the quasi-coherent ideal subsheaf +`D.toIdealSheaf`, and a quasi-coherent ideal sheaf `I` to its `IdealSheafData` of affine sections +`I.toIdealSheafData`. -/ +noncomputable def orderIsoQuasicoherentIdealSheaf : + X.IdealSheafData ≃o + { I : SheafOfModules.IdealSheaf X.ringCatSheaf // I.IsQuasicoherent } where + toFun D := ⟨D.toIdealSheaf, D.toIdealSheaf_isQuasicoherent⟩ + invFun I := I.1.toIdealSheafData I.2 + left_inv D := + AlgebraicGeometry.Scheme.IdealSheafData.ext <| funext fun V => by + rw [SheafOfModules.IdealSheaf.toIdealSheafData_ideal, D.toIdealSheaf_ideal V] + right_inv I := Subtype.ext (I.1.toIdealSheafData_toIdealSheaf I.2) + map_rel_iff' {D D'} := by + constructor + · intro h + rw [AlgebraicGeometry.Scheme.IdealSheafData.le_def] + intro V + have hle : D.toIdealSheaf ≤ D'.toIdealSheaf := h + rw [← D.toIdealSheaf_ideal V, ← D'.toIdealSheaf_ideal V] + exact SheafOfModules.IdealSheaf.le_def.mp hle (op V.1) + · intro h + exact toIdealSheaf_mono h + +end AlgebraicGeometry.Scheme.IdealSheafData