|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Christian Merten. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Christian Merten |
| 5 | +-/ |
| 6 | +import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties |
| 7 | +import Mathlib.RingTheory.RingHom.StandardSmooth |
| 8 | + |
| 9 | +/-! |
| 10 | +
|
| 11 | +# Smooth morphisms |
| 12 | +
|
| 13 | +A morphism of schemes `f : X ⟶ Y` is smooth (of relative dimension `n`) if for each `x : X` there |
| 14 | +exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of |
| 15 | +`f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is |
| 16 | +standard smooth (of relative dimension `n`). |
| 17 | +
|
| 18 | +In other words, smooth (resp. smooth of relative dimension `n`) for scheme morphisms is associated |
| 19 | +to the property of ring homomorphisms `Locally IsStandardSmooth` |
| 20 | +(resp. `Locally (IsStandardSmoothOfRelativeDimension n)`). |
| 21 | +
|
| 22 | +## Implementation details |
| 23 | +
|
| 24 | +- Our definition is equivalent to defining `IsSmooth` as the associated scheme morphism property of |
| 25 | +the property of ring maps induced by `Algebra.Smooth`. The equivalence will follow from the |
| 26 | +equivalence of `Locally IsStandardSmooth` and `Algebra.IsSmooth`, but the latter is a (hard) TODO. |
| 27 | +
|
| 28 | +The reason why we choose the definition via `IsStandardSmooth`, is because verifying that |
| 29 | +`Algebra.IsSmooth` is local in the sense of `RingHom.PropertyIsLocal` is a (hard) TODO. |
| 30 | +
|
| 31 | +- The definition `RingHom.IsStandardSmooth` depends on universe levels for the generators and |
| 32 | +relations. For morphisms of schemes we set both to `0` to avoid unnecessary complications. |
| 33 | +
|
| 34 | +## Notes |
| 35 | +
|
| 36 | +This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in |
| 37 | +June 2024. |
| 38 | +
|
| 39 | +-/ |
| 40 | + |
| 41 | + |
| 42 | +noncomputable section |
| 43 | + |
| 44 | +open CategoryTheory |
| 45 | + |
| 46 | +universe t w v u |
| 47 | + |
| 48 | +namespace AlgebraicGeometry |
| 49 | + |
| 50 | +open RingHom |
| 51 | + |
| 52 | +variable (n m : ℕ) {X Y : Scheme.{u}} (f : X ⟶ Y) |
| 53 | + |
| 54 | +/-- |
| 55 | +A morphism of schemes `f : X ⟶ Y` is smooth if for each `x : X` there |
| 56 | +exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of |
| 57 | +`f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is |
| 58 | +standard smooth. |
| 59 | +-/ |
| 60 | +@[mk_iff] |
| 61 | +class IsSmooth : Prop where |
| 62 | + exists_isStandardSmooth : ∀ (x : X), ∃ (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) |
| 63 | + (e : V.1 ≤ f ⁻¹ᵁ U.1), IsStandardSmooth.{0, 0} (f.appLE U V e) |
| 64 | + |
| 65 | +/-- The property of scheme morphisms `IsSmooth` is associated with the ring |
| 66 | +homomorphism property `Locally IsStandardSmooth.{0, 0}`. -/ |
| 67 | +instance : HasRingHomProperty @IsSmooth (Locally IsStandardSmooth.{0, 0}) := by |
| 68 | + apply HasRingHomProperty.locally_of_iff |
| 69 | + · exact isStandardSmooth_localizationPreserves |
| 70 | + · exact isStandardSmooth_stableUnderCompositionWithLocalizationAway |
| 71 | + · intro X Y f |
| 72 | + rw [isSmooth_iff] |
| 73 | + |
| 74 | +/-- Being smooth is stable under composition. -/ |
| 75 | +instance : MorphismProperty.IsStableUnderComposition @IsSmooth := |
| 76 | + HasRingHomProperty.stableUnderComposition <| locally_stableUnderComposition |
| 77 | + isStandardSmooth_respectsIso isStandardSmooth_localizationPreserves |
| 78 | + isStandardSmooth_stableUnderComposition |
| 79 | + |
| 80 | +/-- The composition of smooth morphisms is smooth. -/ |
| 81 | +instance isSmooth_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmooth f] [IsSmooth g] : |
| 82 | + IsSmooth (f ≫ g) := |
| 83 | + MorphismProperty.comp_mem _ f g ‹IsSmooth f› ‹IsSmooth g› |
| 84 | + |
| 85 | +/-- Smooth of relative dimension `n` is stable under base change. -/ |
| 86 | +lemma isSmooth_stableUnderBaseChange : MorphismProperty.StableUnderBaseChange @IsSmooth := |
| 87 | + HasRingHomProperty.stableUnderBaseChange <| locally_stableUnderBaseChange |
| 88 | + isStandardSmooth_respectsIso isStandardSmooth_stableUnderBaseChange |
| 89 | + |
| 90 | +/-- |
| 91 | +A morphism of schemes `f : X ⟶ Y` is smooth of relative dimension `n` if for each `x : X` there |
| 92 | +exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of |
| 93 | +`f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is |
| 94 | +standard smooth of relative dimension `n`. |
| 95 | +-/ |
| 96 | +@[mk_iff] |
| 97 | +class IsSmoothOfRelativeDimension : Prop where |
| 98 | + exists_isStandardSmoothOfRelativeDimension : ∀ (x : X), ∃ (U : Y.affineOpens) |
| 99 | + (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1), |
| 100 | + IsStandardSmoothOfRelativeDimension.{0, 0} n (f.appLE U V e) |
| 101 | + |
| 102 | +/-- If `f` is smooth of any relative dimension, it is smooth. -/ |
| 103 | +lemma IsSmoothOfRelativeDimension.isSmooth [IsSmoothOfRelativeDimension n f] : IsSmooth f where |
| 104 | + exists_isStandardSmooth x := by |
| 105 | + obtain ⟨U, V, hx, e, hf⟩ := exists_isStandardSmoothOfRelativeDimension (n := n) (f := f) x |
| 106 | + exact ⟨U, V, hx, e, hf.isStandardSmooth⟩ |
| 107 | + |
| 108 | +/-- The property of scheme morphisms `IsSmoothOfRelativeDimension n` is associated with the ring |
| 109 | +homomorphism property `Locally (IsStandardSmoothOfRelativeDimension.{0, 0} n)`. -/ |
| 110 | +instance : HasRingHomProperty (@IsSmoothOfRelativeDimension n) |
| 111 | + (Locally (IsStandardSmoothOfRelativeDimension.{0, 0} n)) := by |
| 112 | + apply HasRingHomProperty.locally_of_iff |
| 113 | + · exact isStandardSmoothOfRelativeDimension_localizationPreserves n |
| 114 | + · exact isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n |
| 115 | + · intro X Y f |
| 116 | + rw [isSmoothOfRelativeDimension_iff] |
| 117 | + |
| 118 | +/-- Smooth of relative dimension `n` is stable under base change. -/ |
| 119 | +lemma isSmoothOfRelativeDimension_stableUnderBaseChange : |
| 120 | + MorphismProperty.StableUnderBaseChange (@IsSmoothOfRelativeDimension n) := |
| 121 | + HasRingHomProperty.stableUnderBaseChange <| locally_stableUnderBaseChange |
| 122 | + isStandardSmoothOfRelativeDimension_respectsIso |
| 123 | + (isStandardSmoothOfRelativeDimension_stableUnderBaseChange n) |
| 124 | + |
| 125 | +/-- Open immersions are smooth of relative dimension `0`. -/ |
| 126 | +instance (priority := 900) [IsOpenImmersion f] : IsSmoothOfRelativeDimension 0 f := |
| 127 | + HasRingHomProperty.of_isOpenImmersion |
| 128 | + (locally_holdsForLocalizationAway <| |
| 129 | + isStandardSmoothOfRelativeDimension_holdsForLocalizationAway).containsIdentities |
| 130 | + |
| 131 | +/-- Open immersions are smooth. -/ |
| 132 | +instance (priority := 900) [IsOpenImmersion f] : IsSmooth f := |
| 133 | + IsSmoothOfRelativeDimension.isSmooth 0 f |
| 134 | + |
| 135 | +/-- If `f` is smooth of relative dimension `n` and `g` is smooth of relative dimension |
| 136 | +`m`, then `f ≫ g` is smooth of relative dimension `n + m`. -/ |
| 137 | +instance isSmoothOfRelativeDimension_comp {Z : Scheme.{u}} (g : Y ⟶ Z) |
| 138 | + [hf : IsSmoothOfRelativeDimension n f] [hg : IsSmoothOfRelativeDimension m g] : |
| 139 | + IsSmoothOfRelativeDimension (n + m) (f ≫ g) where |
| 140 | + exists_isStandardSmoothOfRelativeDimension x := by |
| 141 | + obtain ⟨U₂, V₂, hfx₂, e₂, hf₂⟩ := hg.exists_isStandardSmoothOfRelativeDimension (f.base x) |
| 142 | + obtain ⟨U₁', V₁', hx₁', e₁', hf₁'⟩ := hf.exists_isStandardSmoothOfRelativeDimension x |
| 143 | + obtain ⟨r, s, hx₁, e₁, hf₁⟩ := exists_basicOpen_le_appLE_of_appLE_of_isAffine |
| 144 | + (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n) |
| 145 | + (isStandardSmoothOfRelativeDimension_localizationPreserves n) |
| 146 | + x V₂ U₁' V₁' V₁' hx₁' hx₁' e₁' hf₁' hfx₂ |
| 147 | + have e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂ := |
| 148 | + le_trans e₁ <| f.preimage_le_preimage_of_le <| le_trans (Y.basicOpen_le r) e₂ |
| 149 | + have heq : (f ≫ g).appLE U₂ (X.basicOpen s) e = g.appLE U₂ V₂ e₂ ≫ |
| 150 | + algebraMap Γ(Y, V₂) Γ(Y, Y.basicOpen r) ≫ f.appLE (Y.basicOpen r) (X.basicOpen s) e₁ := by |
| 151 | + rw [RingHom.algebraMap_toAlgebra, g.appLE_map_assoc, Scheme.appLE_comp_appLE] |
| 152 | + refine ⟨U₂, ⟨X.basicOpen s, V₁'.2.basicOpen s⟩, hx₁, e, heq ▸ ?_⟩ |
| 153 | + apply IsStandardSmoothOfRelativeDimension.comp ?_ hf₂ |
| 154 | + haveI : IsLocalization.Away r Γ(Y, Y.basicOpen r) := V₂.2.isLocalization_basicOpen r |
| 155 | + exact (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).right |
| 156 | + _ r _ hf₁ |
| 157 | + |
| 158 | +instance {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmoothOfRelativeDimension 0 f] |
| 159 | + [IsSmoothOfRelativeDimension 0 g] : |
| 160 | + IsSmoothOfRelativeDimension 0 (f ≫ g) := |
| 161 | + inferInstanceAs <| IsSmoothOfRelativeDimension (0 + 0) (f ≫ g) |
| 162 | + |
| 163 | +/-- Smooth of relative dimension `0` is stable under composition. -/ |
| 164 | +instance : MorphismProperty.IsStableUnderComposition (@IsSmoothOfRelativeDimension 0) where |
| 165 | + comp_mem _ _ _ _ := inferInstance |
| 166 | + |
| 167 | +end AlgebraicGeometry |
0 commit comments