feat(AlgebraicGeometry): dominant morphisms of schemes (#17961)

Co-authored-by: Andrew Yang <[email protected]>

Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

@@ -222,21 +222,35 @@ 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) :
     IsLocalAtTarget (topologically P) := by
   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`. -/

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

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