|
| 1 | +/- |
| 2 | +Copyright (c) 2022 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.Topology.LocalAtTarget |
| 7 | +import Mathlib.AlgebraicGeometry.Morphisms.Constructors |
| 8 | + |
| 9 | +/-! |
| 10 | +
|
| 11 | +## Properties on the underlying functions of morphisms of schemes. |
| 12 | +
|
| 13 | +This file includes various results on properties of morphisms of schemes that come from properties |
| 14 | +of the underlying map of topological spaces, including |
| 15 | +
|
| 16 | +- `Injective` |
| 17 | +- `Surjective` |
| 18 | +- `IsOpenMap` |
| 19 | +- `IsClosedMap` |
| 20 | +- `Embedding` |
| 21 | +- `OpenEmbedding` |
| 22 | +- `ClosedEmbedding` |
| 23 | +
|
| 24 | +-/ |
| 25 | + |
| 26 | +open CategoryTheory |
| 27 | + |
| 28 | +namespace AlgebraicGeometry |
| 29 | + |
| 30 | +universe u |
| 31 | + |
| 32 | +section Injective |
| 33 | + |
| 34 | +variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) |
| 35 | + |
| 36 | +instance : MorphismProperty.RespectsIso (topologically Function.Injective) := |
| 37 | + topologically_respectsIso _ (fun e ↦ e.injective) (fun _ _ hf hg ↦ hg.comp hf) |
| 38 | + |
| 39 | +instance injective_isLocalAtTarget : IsLocalAtTarget (topologically Function.Injective) := by |
| 40 | + refine topologically_isLocalAtTarget _ (fun _ s h ↦ h.restrictPreimage s) |
| 41 | + fun f ι U H _ hf x₁ x₂ e ↦ ?_ |
| 42 | + obtain ⟨i, hxi⟩ : ∃ i, f x₁ ∈ U i := by simpa using congr(f x₁ ∈ $H) |
| 43 | + exact congr(($(@hf i ⟨x₁, hxi⟩ ⟨x₂, show f x₂ ∈ U i from e ▸ hxi⟩ (Subtype.ext e))).1) |
| 44 | + |
| 45 | +end Injective |
| 46 | + |
| 47 | +section Surjective |
| 48 | + |
| 49 | +variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) |
| 50 | + |
| 51 | +/-- A morphism of schemes is surjective if the underlying map is. -/ |
| 52 | +@[mk_iff] |
| 53 | +class Surjective : Prop where |
| 54 | + surj : Function.Surjective f.1.base |
| 55 | + |
| 56 | +lemma surjective_eq_topologically : |
| 57 | + @Surjective = topologically Function.Surjective := by ext; exact surjective_iff _ |
| 58 | + |
| 59 | +lemma Scheme.Hom.surjective (f : X.Hom Y) [Surjective f] : Function.Surjective f.1.base := |
| 60 | + Surjective.surj |
| 61 | + |
| 62 | +instance (priority := 100) [IsIso f] : Surjective f := ⟨f.homeomorph.surjective⟩ |
| 63 | + |
| 64 | +instance [Surjective f] [Surjective g] : Surjective (f ≫ g) := ⟨g.surjective.comp f.surjective⟩ |
| 65 | + |
| 66 | +lemma Surjective.of_comp [Surjective (f ≫ g)] : Surjective g where |
| 67 | + surj := Function.Surjective.of_comp (g := f.1.base) (f ≫ g).surjective |
| 68 | + |
| 69 | +lemma Surjective.comp_iff [Surjective f] : Surjective (f ≫ g) ↔ Surjective g := |
| 70 | + ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩ |
| 71 | + |
| 72 | +instance : MorphismProperty.RespectsIso @Surjective := |
| 73 | + surjective_eq_topologically ▸ topologically_respectsIso _ (fun e ↦ e.surjective) |
| 74 | + (fun _ _ hf hg ↦ hg.comp hf) |
| 75 | + |
| 76 | +instance surjective_isLocalAtTarget : IsLocalAtTarget @Surjective := by |
| 77 | + have : MorphismProperty.RespectsIso @Surjective := inferInstance |
| 78 | + rw [surjective_eq_topologically] at this ⊢ |
| 79 | + refine topologically_isLocalAtTarget _ (fun _ s h ↦ h.restrictPreimage s) fun f ι U H _ hf x ↦ ?_ |
| 80 | + obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H) |
| 81 | + obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩ |
| 82 | + exact ⟨y, congr(($hy).1)⟩ |
| 83 | + |
| 84 | +end Surjective |
| 85 | + |
| 86 | +section IsOpenMap |
| 87 | + |
| 88 | +instance : (topologically IsOpenMap).RespectsIso := |
| 89 | + topologically_respectsIso _ (fun e ↦ e.isOpenMap) (fun _ _ hf hg ↦ hg.comp hf) |
| 90 | + |
| 91 | +instance isOpenMap_isLocalAtTarget : IsLocalAtTarget (topologically IsOpenMap) := |
| 92 | + topologically_isLocalAtTarget _ |
| 93 | + (fun _ s hf ↦ hf.restrictPreimage s) |
| 94 | + (fun _ _ _ hU _ hf ↦ (isOpenMap_iff_isOpenMap_of_iSup_eq_top hU).mpr hf) |
| 95 | + |
| 96 | +end IsOpenMap |
| 97 | + |
| 98 | +section IsClosedMap |
| 99 | + |
| 100 | +instance : (topologically IsClosedMap).RespectsIso := |
| 101 | + topologically_respectsIso _ (fun e ↦ e.isClosedMap) (fun _ _ hf hg ↦ hg.comp hf) |
| 102 | + |
| 103 | +instance isClosedMap_isLocalAtTarget : IsLocalAtTarget (topologically IsClosedMap) := |
| 104 | + topologically_isLocalAtTarget _ |
| 105 | + (fun _ s hf ↦ hf.restrictPreimage s) |
| 106 | + (fun _ _ _ hU _ hf ↦ (isClosedMap_iff_isClosedMap_of_iSup_eq_top hU).mpr hf) |
| 107 | + |
| 108 | +end IsClosedMap |
| 109 | + |
| 110 | +section Embedding |
| 111 | + |
| 112 | +instance : (topologically Embedding).RespectsIso := |
| 113 | + topologically_respectsIso _ (fun e ↦ e.embedding) (fun _ _ hf hg ↦ hg.comp hf) |
| 114 | + |
| 115 | +instance embedding_isLocalAtTarget : IsLocalAtTarget (topologically Embedding) := |
| 116 | + topologically_isLocalAtTarget _ |
| 117 | + (fun _ s hf ↦ hf.restrictPreimage s) |
| 118 | + (fun _ _ _ hU hfcont hf ↦ (embedding_iff_embedding_of_iSup_eq_top hU hfcont).mpr hf) |
| 119 | + |
| 120 | +end Embedding |
| 121 | + |
| 122 | +section OpenEmbedding |
| 123 | + |
| 124 | +instance : (topologically OpenEmbedding).RespectsIso := |
| 125 | + topologically_respectsIso _ (fun e ↦ e.openEmbedding) (fun _ _ hf hg ↦ hg.comp hf) |
| 126 | + |
| 127 | +instance openEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically OpenEmbedding) := |
| 128 | + topologically_isLocalAtTarget _ |
| 129 | + (fun _ s hf ↦ hf.restrictPreimage s) |
| 130 | + (fun _ _ _ hU hfcont hf ↦ (openEmbedding_iff_openEmbedding_of_iSup_eq_top hU hfcont).mpr hf) |
| 131 | + |
| 132 | +end OpenEmbedding |
| 133 | + |
| 134 | +section ClosedEmbedding |
| 135 | + |
| 136 | +instance : (topologically ClosedEmbedding).RespectsIso := |
| 137 | + topologically_respectsIso _ (fun e ↦ e.closedEmbedding) (fun _ _ hf hg ↦ hg.comp hf) |
| 138 | + |
| 139 | +instance closedEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically ClosedEmbedding) := |
| 140 | + topologically_isLocalAtTarget _ |
| 141 | + (fun _ s hf ↦ hf.restrictPreimage s) |
| 142 | + (fun _ _ _ hU hfcont hf ↦ (closedEmbedding_iff_closedEmbedding_of_iSup_eq_top hU hfcont).mpr hf) |
| 143 | + |
| 144 | +end ClosedEmbedding |
| 145 | + |
| 146 | +end AlgebraicGeometry |
0 commit comments