From c156373e5610e25498e305f5b0ee8b3adb4c1aec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 3 Jul 2023 16:14:58 +0000 Subject: [PATCH] feat: port AlgebraicGeometry.Morphisms.QuasiCompact (#5642) Co-authored-by: Jujian Zhang --- Mathlib.lean | 1 + Mathlib/AlgebraicGeometry/Limits.lean | 4 +- .../Morphisms/QuasiCompact.lean | 351 ++++++++++++++++++ Mathlib/AlgebraicGeometry/Scheme.lean | 13 + 4 files changed, 366 insertions(+), 3 deletions(-) create mode 100644 Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean diff --git a/Mathlib.lean b/Mathlib.lean index f6d2accf97848..731cb5abf0584 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -427,6 +427,7 @@ import Mathlib.AlgebraicGeometry.LocallyRingedSpace import Mathlib.AlgebraicGeometry.LocallyRingedSpace.HasColimits import Mathlib.AlgebraicGeometry.Morphisms.Basic import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion +import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact import Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed import Mathlib.AlgebraicGeometry.OpenImmersion.Basic import Mathlib.AlgebraicGeometry.OpenImmersion.Scheme diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean index 24ce2b808389b..2329c2d84f1df 100644 --- a/Mathlib/AlgebraicGeometry/Limits.lean +++ b/Mathlib/AlgebraicGeometry/Limits.lean @@ -95,9 +95,7 @@ instance (priority := 100) isOpenImmersion_of_isEmpty {X Y : Scheme} (f : X ⟶ [IsEmpty X.carrier] : IsOpenImmersion f := by apply (config := { allowSynthFailures := true }) IsOpenImmersion.of_stalk_iso · apply openEmbedding_of_continuous_injective_open - -- Porting note : `continuity` failed - -- see https://github.com/leanprover-community/mathlib4/issues/5030 - · exact f.1.base.2 + · continuity · rintro (i : X.carrier); exact isEmptyElim i · intro U _; convert isOpen_empty (α := Y); ext; rw [Set.mem_empty_iff_false, iff_false_iff] exact fun x => isEmptyElim (show X.carrier from x.choose) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean new file mode 100644 index 0000000000000..1ae1b4e2b4850 --- /dev/null +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang + +! This file was ported from Lean 3 source module algebraic_geometry.morphisms.quasi_compact +! leanprover-community/mathlib commit 13361559d66b84f80b6d5a1c4a26aa5054766725 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.AlgebraicGeometry.Morphisms.Basic +import Mathlib.Topology.Spectral.Hom +import Mathlib.AlgebraicGeometry.Limits + +/-! +# Quasi-compact morphisms + +A morphism of schemes is quasi-compact if the preimages of quasi-compact open sets are +quasi-compact. + +It suffices to check that preimages of affine open sets are compact +(`quasiCompact_iff_forall_affine`). + +-/ + + +noncomputable section + +open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace + +universe u + +open scoped AlgebraicGeometry + +namespace AlgebraicGeometry + +variable {X Y : Scheme.{u}} (f : X ⟶ Y) + +/-- +A morphism is `quasi-compact` if the underlying map of topological spaces is, i.e. if the preimages +of quasi-compact open sets are quasi-compact. +-/ +@[mk_iff] +class QuasiCompact (f : X ⟶ Y) : Prop where + /-- Preimage of compact open set under a quasi-compact morphism between schemes is compact. -/ + isCompact_preimage : ∀ U : Set Y.carrier, IsOpen U → IsCompact U → IsCompact (f.1.base ⁻¹' U) +#align algebraic_geometry.quasi_compact AlgebraicGeometry.QuasiCompact + +theorem quasiCompact_iff_spectral : QuasiCompact f ↔ IsSpectralMap f.1.base := + ⟨fun ⟨h⟩ => ⟨by continuity, h⟩, fun h => ⟨h.2⟩⟩ +#align algebraic_geometry.quasi_compact_iff_spectral AlgebraicGeometry.quasiCompact_iff_spectral + +/-- The `affine_target_morphism_property` corresponding to `quasi_compact`, asserting that the +domain is a quasi-compact scheme. -/ +def QuasiCompact.affineProperty : AffineTargetMorphismProperty := fun X _ _ _ => + CompactSpace X.carrier +#align algebraic_geometry.quasi_compact.affine_property AlgebraicGeometry.QuasiCompact.affineProperty + +instance (priority := 900) quasiCompactOfIsIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : + QuasiCompact f := by + constructor + intro U _ hU' + convert hU'.image (inv f.1.base).continuous_toFun using 1 + rw [Set.image_eq_preimage_of_inverse] + delta Function.LeftInverse + exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base] +#align algebraic_geometry.quasi_compact_of_is_iso AlgebraicGeometry.quasiCompactOfIsIso + +instance quasiCompactComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact f] + [QuasiCompact g] : QuasiCompact (f ≫ g) := by + constructor + intro U hU hU' + rw [Scheme.comp_val_base, coe_comp, Set.preimage_comp] + apply QuasiCompact.isCompact_preimage + · exact Continuous.isOpen_preimage (by + -- porting note: `continuity` failed + -- see https://github.com/leanprover-community/mathlib4/issues/5030 + exact Scheme.Hom.continuous g) _ hU + apply QuasiCompact.isCompact_preimage <;> assumption +#align algebraic_geometry.quasi_compact_comp AlgebraicGeometry.quasiCompactComp + +theorem isCompact_open_iff_eq_finset_affine_union {X : Scheme} (U : Set X.carrier) : + IsCompact U ∧ IsOpen U ↔ + ∃ s : Set X.affineOpens, s.Finite ∧ U = ⋃ (i : X.affineOpens) (_ : i ∈ s), i := by + apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion + (fun (U : X.affineOpens) => (U : Opens X.carrier)) + · rw [Subtype.range_coe]; exact isBasis_affine_open X + · exact fun i => i.2.isCompact +#align algebraic_geometry.is_compact_open_iff_eq_finset_affine_union AlgebraicGeometry.isCompact_open_iff_eq_finset_affine_union + +theorem isCompact_open_iff_eq_basicOpen_union {X : Scheme} [IsAffine X] (U : Set X.carrier) : + IsCompact U ∧ IsOpen U ↔ + ∃ s : Set (X.presheaf.obj (op ⊤)), + s.Finite ∧ U = ⋃ (i : X.presheaf.obj (op ⊤)) (_ : i ∈ s), X.basicOpen i := + (isBasis_basicOpen X).isCompact_open_iff_eq_finite_iUnion _ + (fun _ => ((topIsAffineOpen _).basicOpenIsAffine _).isCompact) _ +#align algebraic_geometry.is_compact_open_iff_eq_basic_open_union AlgebraicGeometry.isCompact_open_iff_eq_basicOpen_union + +theorem quasiCompact_iff_forall_affine : + QuasiCompact f ↔ + ∀ U : Opens Y.carrier, IsAffineOpen U → IsCompact (f.1.base ⁻¹' (U : Set Y.carrier)) := by + rw [QuasiCompact_iff] + refine' ⟨fun H U hU => H U U.isOpen hU.isCompact, _⟩ + intro H U hU hU' + obtain ⟨S, hS, rfl⟩ := (isCompact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩ + simp only [Set.preimage_iUnion] + exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop) +#align algebraic_geometry.quasi_compact_iff_forall_affine AlgebraicGeometry.quasiCompact_iff_forall_affine + +@[simp] +theorem QuasiCompact.affineProperty_toProperty {X Y : Scheme} (f : X ⟶ Y) : + (QuasiCompact.affineProperty : _).toProperty f ↔ IsAffine Y ∧ CompactSpace X.carrier := by + delta AffineTargetMorphismProperty.toProperty QuasiCompact.affineProperty; simp +#align algebraic_geometry.quasi_compact.affine_property_to_property AlgebraicGeometry.QuasiCompact.affineProperty_toProperty + +theorem quasiCompact_iff_affineProperty : + QuasiCompact f ↔ targetAffineLocally QuasiCompact.affineProperty f := by + rw [quasiCompact_iff_forall_affine] + trans ∀ U : Y.affineOpens, IsCompact (f.1.base ⁻¹' (U : Set Y.carrier)) + · exact ⟨fun h U => h U U.prop, fun h U hU => h ⟨U, hU⟩⟩ + apply forall_congr' + exact fun _ => isCompact_iff_compactSpace +#align algebraic_geometry.quasi_compact_iff_affine_property AlgebraicGeometry.quasiCompact_iff_affineProperty + +theorem quasiCompact_eq_affineProperty : + @QuasiCompact = targetAffineLocally QuasiCompact.affineProperty := by + ext + exact quasiCompact_iff_affineProperty _ +#align algebraic_geometry.quasi_compact_eq_affine_property AlgebraicGeometry.quasiCompact_eq_affineProperty + +theorem isCompact_basicOpen (X : Scheme) {U : Opens X.carrier} (hU : IsCompact (U : Set X.carrier)) + (f : X.presheaf.obj (op U)) : IsCompact (X.basicOpen f : Set X.carrier) := by + classical + refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1 + obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩ + let g : s → X.affineOpens := by + intro V + use V.1 ⊓ X.basicOpen f + have : V.1.1 ⟶ U := by + apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e] + convert @Set.subset_iUnion₂ _ _ _ + (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1 + erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op] + exact IsAffineOpen.basicOpenIsAffine V.1.prop _ + haveI : Finite s := hs.to_subtype + refine' ⟨Set.range g, Set.finite_range g, _⟩ + refine' (Set.inter_eq_right_iff_subset.mpr + (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans _ + rw [e, Set.iUnion₂_inter] + apply le_antisymm <;> apply Set.iUnion₂_subset + · intro i hi + -- porting note: had to make explicit the first given parameter to `Set.subset_iUnion₂` + exact Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩) + (@Set.subset_iUnion₂ _ _ _ + (fun (i : Scheme.affineOpens X) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace)) _ + (Set.mem_range_self ⟨i, hi⟩)) + · rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩ + rw [← hj'] + refine' Set.Subset.trans _ (Set.subset_iUnion₂ j hj) + exact Set.Subset.rfl +#align algebraic_geometry.is_compact_basic_open AlgebraicGeometry.isCompact_basicOpen + +theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _).IsLocal := by + constructor + · apply AffineTargetMorphismProperty.respectsIso_mk <;> rintro X Y Z e _ _ H + exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.1.base)), H] + · introv H + dsimp [affineProperty] at H ⊢ + change CompactSpace ((Opens.map f.val.base).obj (Y.basicOpen r)) + rw [Scheme.preimage_basicOpen f r] + erw [← isCompact_iff_compactSpace] + rw [← isCompact_univ_iff] at H + apply isCompact_basicOpen + exact H + · rintro X Y H f S hS hS' + rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS + delta QuasiCompact.affineProperty + rw [← isCompact_univ_iff] + change IsCompact ((Opens.map f.val.base).obj ⊤).1 + rw [← hS] + dsimp [Opens.map] + simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion] + exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i), + topIsAffineOpen _] +#align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal + +theorem QuasiCompact.affine_openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) : + List.TFAE + [QuasiCompact f, + ∃ (𝒰 : Scheme.OpenCover.{u} Y) (_ : ∀ i, IsAffine (𝒰.obj i)), + ∀ i : 𝒰.J, CompactSpace (pullback f (𝒰.map i)).carrier, + ∀ (𝒰 : Scheme.OpenCover.{u} Y) [∀ i, IsAffine (𝒰.obj i)] (i : 𝒰.J), + CompactSpace (pullback f (𝒰.map i)).carrier, + ∀ {U : Scheme} (g : U ⟶ Y) [IsAffine U] [IsOpenImmersion g], + CompactSpace (pullback f g).carrier, + ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤) (_ : ∀ i, IsAffineOpen (U i)), + ∀ i, CompactSpace (f.1.base ⁻¹' (U i).1)] := + quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_openCover_TFAE f +#align algebraic_geometry.quasi_compact.affine_open_cover_tfae AlgebraicGeometry.QuasiCompact.affine_openCover_tFAE + +theorem QuasiCompact.is_local_at_target : PropertyIsLocalAtTarget @QuasiCompact := + quasiCompact_eq_affineProperty.symm ▸ + QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal +#align algebraic_geometry.quasi_compact.is_local_at_target AlgebraicGeometry.QuasiCompact.is_local_at_target + +theorem QuasiCompact.openCover_tFAE {X Y : Scheme.{u}} (f : X ⟶ Y) : + List.TFAE + [QuasiCompact f, + ∃ 𝒰 : Scheme.OpenCover.{u} Y, + ∀ i : 𝒰.J, QuasiCompact (pullback.snd : (𝒰.pullbackCover f).obj i ⟶ 𝒰.obj i), + ∀ (𝒰 : Scheme.OpenCover.{u} Y) (i : 𝒰.J), + QuasiCompact (pullback.snd : (𝒰.pullbackCover f).obj i ⟶ 𝒰.obj i), + ∀ U : Opens Y.carrier, QuasiCompact (f ∣_ U), + ∀ {U : Scheme} (g : U ⟶ Y) [IsOpenImmersion g], + QuasiCompact (pullback.snd : pullback f g ⟶ _), + ∃ (ι : Type u) (U : ι → Opens Y.carrier) (_ : iSup U = ⊤), ∀ i, QuasiCompact (f ∣_ U i)] := + quasiCompact_eq_affineProperty.symm ▸ + QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal.openCover_TFAE f +#align algebraic_geometry.quasi_compact.open_cover_tfae AlgebraicGeometry.QuasiCompact.openCover_tFAE + +theorem quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] : + QuasiCompact f ↔ CompactSpace X.carrier := + quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_target_iff f +#align algebraic_geometry.quasi_compact_over_affine_iff AlgebraicGeometry.quasiCompact_over_affine_iff + +theorem compactSpace_iff_quasiCompact (X : Scheme) : + CompactSpace X.carrier ↔ QuasiCompact (terminal.from X) := + (quasiCompact_over_affine_iff _).symm +#align algebraic_geometry.compact_space_iff_quasi_compact AlgebraicGeometry.compactSpace_iff_quasiCompact + +theorem QuasiCompact.affine_openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y) + [∀ i, IsAffine (𝒰.obj i)] (f : X ⟶ Y) : + QuasiCompact f ↔ ∀ i, CompactSpace (pullback f (𝒰.map i)).carrier := + quasiCompact_eq_affineProperty.symm ▸ QuasiCompact.affineProperty_isLocal.affine_openCover_iff f 𝒰 +#align algebraic_geometry.quasi_compact.affine_open_cover_iff AlgebraicGeometry.QuasiCompact.affine_openCover_iff + +theorem QuasiCompact.openCover_iff {X Y : Scheme.{u}} (𝒰 : Scheme.OpenCover.{u} Y) (f : X ⟶ Y) : + QuasiCompact f ↔ ∀ i, QuasiCompact (pullback.snd : pullback f (𝒰.map i) ⟶ _) := + quasiCompact_eq_affineProperty.symm ▸ + QuasiCompact.affineProperty_isLocal.targetAffineLocallyIsLocal.openCover_iff f 𝒰 +#align algebraic_geometry.quasi_compact.open_cover_iff AlgebraicGeometry.QuasiCompact.openCover_iff + +theorem quasiCompact_respectsIso : MorphismProperty.RespectsIso @QuasiCompact := + quasiCompact_eq_affineProperty.symm ▸ + targetAffineLocally_respectsIso QuasiCompact.affineProperty_isLocal.1 +#align algebraic_geometry.quasi_compact_respects_iso AlgebraicGeometry.quasiCompact_respectsIso + +theorem quasiCompact_stableUnderComposition : + MorphismProperty.StableUnderComposition @QuasiCompact := fun _ _ _ _ _ _ _ => inferInstance +#align algebraic_geometry.quasi_compact_stable_under_composition AlgebraicGeometry.quasiCompact_stableUnderComposition + +theorem QuasiCompact.affineProperty_stableUnderBaseChange : + QuasiCompact.affineProperty.StableUnderBaseChange := by + intro X Y S _ _ f g h + rw [QuasiCompact.affineProperty] at h ⊢ + skip + let 𝒰 := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g + have : Finite 𝒰.J := by dsimp; infer_instance + have : ∀ i, CompactSpace (𝒰.obj i).carrier := by intro i; dsimp; infer_instance + exact 𝒰.compactSpace +#align algebraic_geometry.quasi_compact.affine_property_stable_under_base_change AlgebraicGeometry.QuasiCompact.affineProperty_stableUnderBaseChange + +theorem quasiCompact_stableUnderBaseChange : MorphismProperty.StableUnderBaseChange @QuasiCompact := + quasiCompact_eq_affineProperty.symm ▸ + QuasiCompact.affineProperty_isLocal.stableUnderBaseChange + QuasiCompact.affineProperty_stableUnderBaseChange +#align algebraic_geometry.quasi_compact_stable_under_base_change AlgebraicGeometry.quasiCompact_stableUnderBaseChange + +variable {Z : Scheme.{u}} + +instance (f : X ⟶ Z) (g : Y ⟶ Z) [QuasiCompact g] : + QuasiCompact (pullback.fst : pullback f g ⟶ X) := + quasiCompact_stableUnderBaseChange.fst f g inferInstance + +instance (f : X ⟶ Z) (g : Y ⟶ Z) [QuasiCompact f] : + QuasiCompact (pullback.snd : pullback f g ⟶ Y) := + quasiCompact_stableUnderBaseChange.snd f g inferInstance + +@[elab_as_elim] +theorem compact_open_induction_on {P : Opens X.carrier → Prop} (S : Opens X.carrier) + (hS : IsCompact S.1) (h₁ : P ⊥) + (h₂ : ∀ (S : Opens X.carrier) (_ : IsCompact S.1) (U : X.affineOpens), P S → P (S ⊔ U)) : + P S := by + classical + obtain ⟨s, hs, hs'⟩ := (isCompact_open_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩ + replace hs' : S = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs' + subst hs' + apply @Set.Finite.induction_on _ _ _ hs + · convert h₁; rw [iSup_eq_bot]; rintro ⟨_, h⟩; exact h.elim + · intro x s _ hs h₄ + have : IsCompact (⨆ i : s, (i : Opens X.carrier)).1 := by + refine' ((isCompact_open_iff_eq_finset_affine_union _).mpr _).1; exact ⟨s, hs, by simp⟩ + convert h₂ _ this x h₄ + rw [iSup_subtype, sup_comm] + conv_rhs => rw [iSup_subtype] + exact iSup_insert +#align algebraic_geometry.compact_open_induction_on AlgebraicGeometry.compact_open_induction_on + +theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : Scheme) + {U : Opens X} (hU : IsAffineOpen U) (x f : X.presheaf.obj (op U)) + (H : x |_ X.basicOpen f = 0) : ∃ n : ℕ, f ^ n * x = 0 := by + rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op)] at H + obtain ⟨⟨_, n, rfl⟩, e⟩ := (isLocalization_basicOpen hU f).eq_iff_exists'.mp H + exact ⟨n, by simpa [mul_comm x] using e⟩ +#align algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_affine_open AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen + +/-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then +`f ^ n * x = 0` for some `n`. -/ +theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme.{u}) + {U : Opens X.carrier} (hU : IsCompact U.1) (x f : X.presheaf.obj (op U)) + (H : x |_ X.basicOpen f = 0) : ∃ n : ℕ, f ^ n * x = 0 := by + obtain ⟨s, hs, e⟩ := (isCompact_open_iff_eq_finset_affine_union U.1).mp ⟨hU, U.2⟩ + replace e : U = iSup fun i : s => (i : Opens X.carrier) + · ext1; simpa using e + have h₁ : ∀ i : s, i.1.1 ≤ U := by + intro i + change (i : Opens X.carrier) ≤ U + rw [e] + -- porting note: `exact le_iSup _ _` no longer works + exact le_iSup (fun (i : s) => (i : Opens (X.toPresheafedSpace))) _ + have H' := fun i : s => + exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen X i.1.2 + (X.presheaf.map (homOfLE (h₁ i)).op x) (X.presheaf.map (homOfLE (h₁ i)).op f) ?_ + swap + · delta TopCat.Presheaf.restrictOpen TopCat.Presheaf.restrict at H ⊢ + convert congr_arg (X.presheaf.map (homOfLE _).op) H + · simp only [← comp_apply, ← Functor.map_comp] + rfl + . rw [map_zero] + simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right] + choose n hn using H' + haveI := hs.to_subtype + cases nonempty_fintype s + use Finset.univ.sup n + suffices ∀ i : s, X.presheaf.map (homOfLE (h₁ i)).op (f ^ Finset.univ.sup n * x) = 0 by + subst e + apply TopCat.Sheaf.eq_of_locally_eq.{u + 1, u} X.sheaf fun i : s => (i : Opens X.carrier) + intro i + rw [map_zero] + apply this + intro i + replace hn := + congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x) + (hn i) + dsimp at hn + simp only [← map_mul, ← map_pow] at hn + rwa [MulZeroClass.mul_zero, ← mul_assoc, ← pow_add, tsub_add_cancel_of_le] at hn + apply Finset.le_sup (Finset.mem_univ i) +#align algebraic_geometry.exists_pow_mul_eq_zero_of_res_basic_open_eq_zero_of_is_compact AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact + +end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean index a2e8ee1b7342c..fbf9064cafeb0 100644 --- a/Mathlib/AlgebraicGeometry/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/Scheme.lean @@ -62,6 +62,10 @@ def Hom (X Y : Scheme) : Type _ := instance : Category Scheme := { InducedCategory.category Scheme.toLocallyRingedSpace with Hom := Hom } +-- porting note: added to ease automation +@[continuity] +lemma Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous f.1.base := f.1.base.2 + /-- The structure sheaf of a scheme. -/ protected abbrev sheaf (X : Scheme) := X.toSheafedSpace.sheaf @@ -294,6 +298,15 @@ theorem mem_basicOpen (x : U) : ↑x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.ge RingedSpace.mem_basicOpen _ _ _ #align algebraic_geometry.Scheme.mem_basic_open AlgebraicGeometry.Scheme.mem_basicOpen +@[aesop norm simp (rule_sets [Restrict])] +theorem mem_basicOpen_top' {U : Opens X} (f : X.presheaf.obj (op U)) (x : X.carrier) : + x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit (X.presheaf.germ (⟨x, m⟩ : U) f) := by + fconstructor + . rintro ⟨y, hy1, rfl⟩ + exact ⟨y.2, hy1⟩ + . rintro ⟨m, hm⟩ + exact ⟨⟨x, m⟩, hm, rfl⟩ + @[simp] theorem mem_basicOpen_top (f : X.presheaf.obj (op ⊤)) (x : X.carrier) : x ∈ X.basicOpen f ↔ IsUnit (X.presheaf.germ (⟨x, trivial⟩ : (⊤ : Opens _)) f) :=