|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Andrew Yang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Andrew Yang |
| 5 | +-/ |
| 6 | +import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties |
| 7 | +import Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct |
| 8 | +import Mathlib.Topology.LocalAtTarget |
| 9 | + |
| 10 | +/-! |
| 11 | +# Morphisms surjective on stalks |
| 12 | +
|
| 13 | +We define the classe of morphisms between schemes that are surjective on stalks. |
| 14 | +We show that this class is stable under composition and base change. |
| 15 | +
|
| 16 | +We also show that (`AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback`) |
| 17 | +if `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of |
| 18 | +`X × Y` (cartesian product as topological spaces) with the induced topology. |
| 19 | +-/ |
| 20 | + |
| 21 | +open CategoryTheory CategoryTheory.Limits Topology |
| 22 | + |
| 23 | +namespace AlgebraicGeometry |
| 24 | + |
| 25 | +universe u |
| 26 | + |
| 27 | +variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) |
| 28 | + |
| 29 | +/-- The class of morphisms `f : X ⟶ Y` between schemes such that |
| 30 | +`𝒪_{Y, f x} ⟶ 𝒪_{X, x}` is surjective for all `x : X`. -/ |
| 31 | +@[mk_iff] |
| 32 | +class SurjectiveOnStalks : Prop where |
| 33 | + surj_on_stalks : ∀ x, Function.Surjective (f.stalkMap x) |
| 34 | + |
| 35 | +theorem Scheme.Hom.stalkMap_surjective (f : X.Hom Y) [SurjectiveOnStalks f] (x) : |
| 36 | + Function.Surjective (f.stalkMap x) := |
| 37 | + SurjectiveOnStalks.surj_on_stalks x |
| 38 | + |
| 39 | +namespace SurjectiveOnStalks |
| 40 | + |
| 41 | +instance (priority := 900) [IsOpenImmersion f] : SurjectiveOnStalks f := |
| 42 | + ⟨fun _ ↦ (ConcreteCategory.bijective_of_isIso _).2⟩ |
| 43 | + |
| 44 | +instance : MorphismProperty.IsMultiplicative @SurjectiveOnStalks where |
| 45 | + id_mem _ := inferInstance |
| 46 | + comp_mem {X Y Z} f g hf hg := by |
| 47 | + refine ⟨fun x ↦ ?_⟩ |
| 48 | + rw [Scheme.stalkMap_comp] |
| 49 | + exact (hf.surj_on_stalks x).comp (hg.surj_on_stalks (f.base x)) |
| 50 | + |
| 51 | +instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [SurjectiveOnStalks f] |
| 52 | + [SurjectiveOnStalks g] : SurjectiveOnStalks (f ≫ g) := |
| 53 | + MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance |
| 54 | + |
| 55 | +lemma eq_stalkwise : |
| 56 | + @SurjectiveOnStalks = stalkwise (Function.Surjective ·) := by |
| 57 | + ext; exact surjectiveOnStalks_iff _ |
| 58 | + |
| 59 | +instance : IsLocalAtTarget @SurjectiveOnStalks := |
| 60 | + eq_stalkwise ▸ stalkwiseIsLocalAtTarget_of_respectsIso RingHom.surjective_respectsIso |
| 61 | + |
| 62 | +instance : IsLocalAtSource @SurjectiveOnStalks := |
| 63 | + eq_stalkwise ▸ stalkwise_isLocalAtSource_of_respectsIso RingHom.surjective_respectsIso |
| 64 | + |
| 65 | +lemma Spec_iff {R S : CommRingCat.{u}} {φ : R ⟶ S} : |
| 66 | + SurjectiveOnStalks (Spec.map φ) ↔ RingHom.SurjectiveOnStalks φ := by |
| 67 | + rw [eq_stalkwise, stalkwise_Spec_map_iff RingHom.surjective_respectsIso, |
| 68 | + RingHom.SurjectiveOnStalks] |
| 69 | + |
| 70 | +instance : HasRingHomProperty @SurjectiveOnStalks RingHom.SurjectiveOnStalks := |
| 71 | + eq_stalkwise ▸ .stalkwise RingHom.surjective_respectsIso |
| 72 | + |
| 73 | +variable {f} in |
| 74 | +lemma iff_of_isAffine [IsAffine X] [IsAffine Y] : |
| 75 | + SurjectiveOnStalks f ↔ RingHom.SurjectiveOnStalks (f.app ⊤) := by |
| 76 | + rw [← Spec_iff, MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)] |
| 77 | + rfl |
| 78 | + |
| 79 | +theorem of_comp [SurjectiveOnStalks (f ≫ g)] : SurjectiveOnStalks f := by |
| 80 | + refine ⟨fun x ↦ ?_⟩ |
| 81 | + have := (f ≫ g).stalkMap_surjective x |
| 82 | + rw [Scheme.stalkMap_comp] at this |
| 83 | + exact Function.Surjective.of_comp this |
| 84 | + |
| 85 | +instance stableUnderBaseChange : |
| 86 | + MorphismProperty.IsStableUnderBaseChange @SurjectiveOnStalks := by |
| 87 | + apply HasRingHomProperty.isStableUnderBaseChange |
| 88 | + apply RingHom.IsStableUnderBaseChange.mk |
| 89 | + · exact (HasRingHomProperty.isLocal_ringHomProperty @SurjectiveOnStalks).respectsIso |
| 90 | + intros R S T _ _ _ _ _ H |
| 91 | + exact H.baseChange |
| 92 | + |
| 93 | +/-- If `Y ⟶ S` is surjective on stalks, then for every `X ⟶ S`, `X ×ₛ Y` is a subset of |
| 94 | +`X × Y` (cartesian product as topological spaces) with the induced topology. -/ |
| 95 | +lemma isEmbedding_pullback {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) [SurjectiveOnStalks g] : |
| 96 | + IsEmbedding (fun x ↦ ((pullback.fst f g).base x, (pullback.snd f g).base x)) := by |
| 97 | + let L := (fun x ↦ ((pullback.fst f g).base x, (pullback.snd f g).base x)) |
| 98 | + have H : ∀ R A B (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) |
| 99 | + (iY : Spec B ⟶ Y) (iS : Spec R ⟶ S) (e₁ e₂), IsOpenImmersion iX → IsOpenImmersion iY → |
| 100 | + IsOpenImmersion iS → IsEmbedding (L ∘ (pullback.map f' g' f g iX iY iS e₁ e₂).base) := by |
| 101 | + intro R A B f' g' iX iY iS e₁ e₂ _ _ _ |
| 102 | + have H : SurjectiveOnStalks g' := |
| 103 | + have : SurjectiveOnStalks (g' ≫ iS) := e₂ ▸ inferInstance |
| 104 | + .of_comp _ iS |
| 105 | + obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f' := ⟨_, Spec.map_preimage _⟩ |
| 106 | + obtain ⟨ψ, rfl⟩ : ∃ ψ, Spec.map ψ = g' := ⟨_, Spec.map_preimage _⟩ |
| 107 | + letI := φ.toAlgebra |
| 108 | + letI := ψ.toAlgebra |
| 109 | + rw [HasRingHomProperty.Spec_iff (P := @SurjectiveOnStalks)] at H |
| 110 | + convert ((iX.isOpenEmbedding.prodMap iY.isOpenEmbedding).isEmbedding.comp |
| 111 | + (PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks R A B H)).comp |
| 112 | + (Scheme.homeoOfIso (pullbackSpecIso R A B)).isEmbedding |
| 113 | + ext1 x |
| 114 | + obtain ⟨x, rfl⟩ := (Scheme.homeoOfIso (pullbackSpecIso R A B).symm).surjective x |
| 115 | + simp only [Scheme.homeoOfIso_apply, Function.comp_apply] |
| 116 | + ext |
| 117 | + · simp only [← Scheme.comp_base_apply, pullback.lift_fst, Iso.symm_hom, Iso.inv_hom_id] |
| 118 | + erw [← Scheme.comp_base_apply, pullbackSpecIso_inv_fst_assoc] |
| 119 | + rfl |
| 120 | + · simp only [← Scheme.comp_base_apply, pullback.lift_snd, Iso.symm_hom, Iso.inv_hom_id] |
| 121 | + erw [← Scheme.comp_base_apply, pullbackSpecIso_inv_snd_assoc] |
| 122 | + rfl |
| 123 | + let 𝒰 := S.affineOpenCover.openCover |
| 124 | + let 𝒱 (i) := ((𝒰.pullbackCover f).obj i).affineOpenCover.openCover |
| 125 | + let 𝒲 (i) := ((𝒰.pullbackCover g).obj i).affineOpenCover.openCover |
| 126 | + let U (ijk : Σ i, (𝒱 i).J × (𝒲 i).J) : TopologicalSpace.Opens (X.carrier × Y) := |
| 127 | + ⟨{ P | P.1 ∈ ((𝒱 ijk.1).map ijk.2.1 ≫ (𝒰.pullbackCover f).map ijk.1).opensRange ∧ |
| 128 | + P.2 ∈ ((𝒲 ijk.1).map ijk.2.2 ≫ (𝒰.pullbackCover g).map ijk.1).opensRange }, |
| 129 | + (continuous_fst.1 _ ((𝒱 ijk.1).map ijk.2.1 ≫ |
| 130 | + (𝒰.pullbackCover f).map ijk.1).opensRange.2).inter (continuous_snd.1 _ |
| 131 | + ((𝒲 ijk.1).map ijk.2.2 ≫ (𝒰.pullbackCover g).map ijk.1).opensRange.2)⟩ |
| 132 | + have : Set.range L ⊆ (iSup U : _) := by |
| 133 | + simp only [Scheme.Cover.pullbackCover_J, Scheme.Cover.pullbackCover_obj, Set.range_subset_iff] |
| 134 | + intro z |
| 135 | + simp only [SetLike.mem_coe, TopologicalSpace.Opens.mem_iSup, Sigma.exists, Prod.exists] |
| 136 | + obtain ⟨is, s, hsx⟩ := 𝒰.exists_eq (f.base ((pullback.fst f g).base z)) |
| 137 | + have hsy : (𝒰.map is).base s = g.base ((pullback.snd f g).base z) := by |
| 138 | + rwa [← Scheme.comp_base_apply, ← pullback.condition, Scheme.comp_base_apply] |
| 139 | + obtain ⟨x : (𝒰.pullbackCover f).obj is, hx⟩ := |
| 140 | + Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop |
| 141 | + (P := @IsOpenImmersion) inferInstance _ _ hsx.symm |
| 142 | + obtain ⟨y : (𝒰.pullbackCover g).obj is, hy⟩ := |
| 143 | + Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop |
| 144 | + (P := @IsOpenImmersion) inferInstance _ _ hsy.symm |
| 145 | + obtain ⟨ix, x, rfl⟩ := (𝒱 is).exists_eq x |
| 146 | + obtain ⟨iy, y, rfl⟩ := (𝒲 is).exists_eq y |
| 147 | + refine ⟨is, ix, iy, ⟨x, hx⟩, ⟨y, hy⟩⟩ |
| 148 | + let 𝓤 := (Scheme.Pullback.openCoverOfBase 𝒰 f g).bind |
| 149 | + (fun i ↦ Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) _ _) |
| 150 | + refine isEmbedding_of_iSup_eq_top_of_preimage_subset_range _ ?_ U this _ (fun i ↦ (𝓤.map i).base) |
| 151 | + (fun i ↦ (𝓤.map i).continuous) ?_ ?_ |
| 152 | + · fun_prop |
| 153 | + · rintro i x ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩ |
| 154 | + obtain ⟨x₁', hx₁'⟩ := |
| 155 | + Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop |
| 156 | + (P := @IsOpenImmersion) inferInstance _ _ hx₁.symm |
| 157 | + obtain ⟨x₂', hx₂'⟩ := |
| 158 | + Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop |
| 159 | + (P := @IsOpenImmersion) inferInstance _ _ hx₂.symm |
| 160 | + obtain ⟨z, hz⟩ := |
| 161 | + Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop |
| 162 | + (P := @IsOpenImmersion) inferInstance _ _ (hx₁'.trans hx₂'.symm) |
| 163 | + refine ⟨(pullbackFstFstIso _ _ _ _ _ _ (𝒰.map i.1) ?_ ?_).hom.base z, ?_⟩ |
| 164 | + · simp [pullback.condition] |
| 165 | + · simp [pullback.condition] |
| 166 | + · dsimp only |
| 167 | + rw [← hx₁', ← hz, ← Scheme.comp_base_apply] |
| 168 | + erw [← Scheme.comp_base_apply] |
| 169 | + congr 4 |
| 170 | + apply pullback.hom_ext <;> simp [𝓤, ← pullback.condition, ← pullback.condition_assoc] |
| 171 | + · intro i |
| 172 | + have := H (S.affineOpenCover.obj i.1) (((𝒰.pullbackCover f).obj i.1).affineOpenCover.obj i.2.1) |
| 173 | + (((𝒰.pullbackCover g).obj i.1).affineOpenCover.obj i.2.2) |
| 174 | + ((𝒱 i.1).map i.2.1 ≫ 𝒰.pullbackHom f i.1) |
| 175 | + ((𝒲 i.1).map i.2.2 ≫ 𝒰.pullbackHom g i.1) |
| 176 | + ((𝒱 i.1).map i.2.1 ≫ (𝒰.pullbackCover f).map i.1) |
| 177 | + ((𝒲 i.1).map i.2.2 ≫ (𝒰.pullbackCover g).map i.1) |
| 178 | + (𝒰.map i.1) (by simp [pullback.condition]) (by simp [pullback.condition]) |
| 179 | + inferInstance inferInstance inferInstance |
| 180 | + convert this using 6 |
| 181 | + apply pullback.hom_ext <;> |
| 182 | + simp [𝓤, ← pullback.condition, ← pullback.condition_assoc, Scheme.Cover.pullbackHom] |
| 183 | + |
| 184 | +end SurjectiveOnStalks |
| 185 | + |
| 186 | +end AlgebraicGeometry |
0 commit comments