From 0cb54c9f7ec15f9e156f7a3d9ffe4ace90e41f86 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Mon, 21 Oct 2024 15:44:23 +0000 Subject: [PATCH] feat(AlgebraicGeometry): dominant morphisms of schemes (#17961) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- .../Morphisms/Constructors.lean | 20 +++++- .../Morphisms/UnderlyingMap.lean | 69 ++++++++++++++----- Mathlib/Topology/LocalAtTarget.lean | 12 ++++ 3 files changed, 81 insertions(+), 20 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean b/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean index 6cfb3141006be..bb4b68e99832c 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean @@ -222,8 +222,8 @@ lemma topologically_respectsIso we may check the corresponding properties on topological spaces. -/ lemma topologically_isLocalAtTarget [(topologically P).RespectsIso] - (hP₂ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set β), - P f → P (s.restrictPreimage f)) + (hP₂ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set β) + (_ : Continuous f) (_ : IsOpen s), P f → P (s.restrictPreimage f)) (hP₃ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → TopologicalSpace.Opens β) (_ : iSup U = ⊤) (_ : Continuous f), (∀ i, P ((U i).carrier.restrictPreimage f)) → P f) : @@ -231,12 +231,26 @@ lemma topologically_isLocalAtTarget apply IsLocalAtTarget.mk' · intro X Y f U hf simp_rw [topologically, morphismRestrict_base] - exact hP₂ f.base U.carrier hf + exact hP₂ f.base U.carrier f.base.2 U.2 hf · intro X Y f ι U hU hf apply hP₃ f.base U hU f.base.continuous fun i ↦ ?_ rw [← morphismRestrict_base] exact hf i +/-- A variant of `topologically_isLocalAtTarget` +that takes one iff statement instead of two implications. -/ +lemma topologically_isLocalAtTarget' + [(topologically P).RespectsIso] + (hP : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u} + (U : ι → TopologicalSpace.Opens β) (_ : iSup U = ⊤) (_ : Continuous f), + P f ↔ (∀ i, P ((U i).carrier.restrictPreimage f))) : + IsLocalAtTarget (topologically P) := by + refine topologically_isLocalAtTarget P ?_ (fun f _ U hU hU' ↦ (hP f U hU hU').mpr) + introv hf hs H + refine by simpa using (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩ + rw [← top_le_iff] + exact le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩ + end Topologically /-- `stalkwise P` holds for a morphism if all stalks satisfy `P`. -/ diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean index ed2f3268b2efc..3d31004a41fb1 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean @@ -20,6 +20,7 @@ of the underlying map of topological spaces, including - `Embedding` - `IsOpenEmbedding` - `IsClosedEmbedding` +- `DenseRange` (`IsDominant`) -/ @@ -37,7 +38,7 @@ instance : MorphismProperty.RespectsIso (topologically Function.Injective) := topologically_respectsIso _ (fun e ↦ e.injective) (fun _ _ hf hg ↦ hg.comp hf) instance injective_isLocalAtTarget : IsLocalAtTarget (topologically Function.Injective) := by - refine topologically_isLocalAtTarget _ (fun _ s h ↦ h.restrictPreimage s) + refine topologically_isLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) fun f ι U H _ hf x₁ x₂ e ↦ ?_ obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H) exact congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1) @@ -76,7 +77,8 @@ instance : MorphismProperty.RespectsIso @Surjective := instance surjective_isLocalAtTarget : IsLocalAtTarget @Surjective := by have : MorphismProperty.RespectsIso @Surjective := inferInstance rw [surjective_eq_topologically] at this ⊢ - refine topologically_isLocalAtTarget _ (fun _ s h ↦ h.restrictPreimage s) fun f ι U H _ hf x ↦ ?_ + refine topologically_isLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_ + intro α β _ _ f ι U H _ hf x obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H) obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩ exact ⟨y, congr(($hy).1)⟩ @@ -89,9 +91,7 @@ instance : (topologically IsOpenMap).RespectsIso := topologically_respectsIso _ (fun e ↦ e.isOpenMap) (fun _ _ hf hg ↦ hg.comp hf) instance isOpenMap_isLocalAtTarget : IsLocalAtTarget (topologically IsOpenMap) := - topologically_isLocalAtTarget _ - (fun _ s hf ↦ hf.restrictPreimage s) - (fun _ _ _ hU _ hf ↦ (isOpenMap_iff_isOpenMap_of_iSup_eq_top hU).mpr hf) + topologically_isLocalAtTarget' _ fun _ _ _ hU _ ↦ isOpenMap_iff_isOpenMap_of_iSup_eq_top hU end IsOpenMap @@ -101,9 +101,7 @@ instance : (topologically IsClosedMap).RespectsIso := topologically_respectsIso _ (fun e ↦ e.isClosedMap) (fun _ _ hf hg ↦ hg.comp hf) instance isClosedMap_isLocalAtTarget : IsLocalAtTarget (topologically IsClosedMap) := - topologically_isLocalAtTarget _ - (fun _ s hf ↦ hf.restrictPreimage s) - (fun _ _ _ hU _ hf ↦ (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr hf) + topologically_isLocalAtTarget' _ fun _ _ _ hU _ ↦ isClosedMap_iff_isClosedMap_of_iSup_eq_top hU end IsClosedMap @@ -113,9 +111,7 @@ instance : (topologically Embedding).RespectsIso := topologically_respectsIso _ (fun e ↦ e.embedding) (fun _ _ hf hg ↦ hg.comp hf) instance embedding_isLocalAtTarget : IsLocalAtTarget (topologically Embedding) := - topologically_isLocalAtTarget _ - (fun _ s hf ↦ hf.restrictPreimage s) - (fun _ _ _ hU hfcont hf ↦ (embedding_iff_embedding_of_iSup_eq_top hU hfcont).mpr hf) + topologically_isLocalAtTarget' _ fun _ _ _ ↦ embedding_iff_embedding_of_iSup_eq_top end Embedding @@ -125,9 +121,7 @@ instance : (topologically IsOpenEmbedding).RespectsIso := topologically_respectsIso _ (fun e ↦ e.isOpenEmbedding) (fun _ _ hf hg ↦ hg.comp hf) instance isOpenEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically IsOpenEmbedding) := - topologically_isLocalAtTarget _ - (fun _ s hf ↦ hf.restrictPreimage s) - (fun _ _ _ hU hfcont hf ↦ (isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top hU hfcont).mpr hf) + topologically_isLocalAtTarget' _ fun _ _ _ ↦ isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top end IsOpenEmbedding @@ -137,10 +131,51 @@ instance : (topologically IsClosedEmbedding).RespectsIso := topologically_respectsIso _ (fun e ↦ e.isClosedEmbedding) (fun _ _ hf hg ↦ hg.comp hf) instance isClosedEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically IsClosedEmbedding) := - topologically_isLocalAtTarget _ - (fun _ s hf ↦ hf.restrictPreimage s) - (fun _ _ _ hU hfcont ↦ (isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top hU hfcont).mpr) + topologically_isLocalAtTarget' _ + fun _ _ _ ↦ isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top end IsClosedEmbedding +section IsDominant + +variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) + +/-- A morphism of schemes is dominant if the underlying map has dense range. -/ +@[mk_iff] +class IsDominant : Prop where + denseRange : DenseRange f.base + +lemma dominant_eq_topologically : + @IsDominant = topologically DenseRange := by ext; exact isDominant_iff _ + +lemma Scheme.Hom.denseRange (f : X.Hom Y) [IsDominant f] : DenseRange f.base := + IsDominant.denseRange + +instance (priority := 100) [Surjective f] : IsDominant f := ⟨f.surjective.denseRange⟩ + +instance [IsDominant f] [IsDominant g] : IsDominant (f ≫ g) := + ⟨g.denseRange.comp f.denseRange g.base.2⟩ + +instance : MorphismProperty.IsMultiplicative @IsDominant where + id_mem := fun _ ↦ inferInstance + comp_mem := fun _ _ _ _ ↦ inferInstance + +lemma IsDominant.of_comp [H : IsDominant (f ≫ g)] : IsDominant g := by + rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢ + exact H.trans (closure_mono (Set.range_comp_subset_range f.base g.base)) + +lemma IsDominant.comp_iff [IsDominant f] : IsDominant (f ≫ g) ↔ IsDominant g := + ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩ + +instance IsDominant.respectsIso : MorphismProperty.RespectsIso @IsDominant := + MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ f (_ : IsIso f) ↦ inferInstance + +instance IsDominant.isLocalAtTarget : IsLocalAtTarget @IsDominant := + have : MorphismProperty.RespectsIso (topologically DenseRange) := + dominant_eq_topologically ▸ IsDominant.respectsIso + dominant_eq_topologically ▸ topologically_isLocalAtTarget' DenseRange + fun _ _ _ hU _ ↦ denseRange_iff_denseRange_of_iSup_eq_top hU + +end IsDominant + end AlgebraicGeometry diff --git a/Mathlib/Topology/LocalAtTarget.lean b/Mathlib/Topology/LocalAtTarget.lean index c1e9f1b8153f2..73a4072157b9c 100644 --- a/Mathlib/Topology/LocalAtTarget.lean +++ b/Mathlib/Topology/LocalAtTarget.lean @@ -199,6 +199,18 @@ theorem isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top (h : Continuous f · simp_rw [Set.range_restrictPreimage] apply isClosed_iff_coe_preimage_of_iSup_eq_top hU +omit [TopologicalSpace α] in +theorem denseRange_iff_denseRange_of_iSup_eq_top : + DenseRange f ↔ ∀ i, DenseRange ((U i).1.restrictPreimage f) := by + simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage, + ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage + continuous_subtype_val] + simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff, + Subtype.range_coe_subtype, SetLike.mem_coe] + rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq] + congr 1 + simpa using congr(($hU).1).symm + @[deprecated (since := "2024-10-20")] alias closedEmbedding_iff_closedEmbedding_of_iSup_eq_top := isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top