Skip to content

Commit c68aa10

Browse files
chrisflavchrisflav
committed
feat(AlgebraicGeometry/Morphisms): affine + ring hom property (#18356)
We add a constructor for properties of affine morphisms of schemes satisfying a given property of ring homomorphisms on sections.
1 parent c817ca4 commit c68aa10

File tree

5 files changed

+261
-3
lines changed

5 files changed

+261
-3
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -893,6 +893,7 @@ import Mathlib.AlgebraicGeometry.Modules.Presheaf
893893
import Mathlib.AlgebraicGeometry.Modules.Sheaf
894894
import Mathlib.AlgebraicGeometry.Modules.Tilde
895895
import Mathlib.AlgebraicGeometry.Morphisms.Affine
896+
import Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
896897
import Mathlib.AlgebraicGeometry.Morphisms.Basic
897898
import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
898899
import Mathlib.AlgebraicGeometry.Morphisms.Constructors

‎Mathlib/AlgebraicGeometry/AffineScheme.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -574,6 +574,35 @@ lemma appLE_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (hU : IsA
574574
RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra, ← CommRingCat.comp_eq_ring_hom_comp,
575575
Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]
576576

577+
lemma app_basicOpen_eq_away_map {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens}
578+
(hU : IsAffineOpen U) (h : IsAffineOpen (f ⁻¹ᵁ U)) (r : Γ(Y, U)) :
579+
haveI := hU.isLocalization_basicOpen r
580+
haveI := h.isLocalization_basicOpen (f.app U r)
581+
f.app (Y.basicOpen r) =
582+
IsLocalization.Away.map Γ(Y, Y.basicOpen r) Γ(X, X.basicOpen (f.app U r)) (f.app U) r ≫
583+
X.presheaf.map (eqToHom (by simp)).op := by
584+
haveI := hU.isLocalization_basicOpen r
585+
haveI := h.isLocalization_basicOpen (f.app U r)
586+
apply IsLocalization.ringHom_ext (.powers r)
587+
rw [← CommRingCat.comp_eq_ring_hom_comp, ← CommRingCat.comp_eq_ring_hom_comp,
588+
IsLocalization.Away.map, ← Category.assoc]
589+
nth_rw 3 [CommRingCat.comp_eq_ring_hom_comp]
590+
rw [IsLocalization.map_comp, RingHom.algebraMap_toAlgebra, ← CommRingCat.comp_eq_ring_hom_comp,
591+
RingHom.algebraMap_toAlgebra, Category.assoc, ← X.presheaf.map_comp]
592+
simp
593+
594+
/-- `f.app (Y.basicOpen r)` is isomorphic to map induced on localizations
595+
`Γ(Y, Y.basicOpen r) ⟶ Γ(X, X.basicOpen (f.app U r))` -/
596+
def appBasicOpenIsoAwayMap {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens}
597+
(hU : IsAffineOpen U) (h : IsAffineOpen (f ⁻¹ᵁ U)) (r : Γ(Y, U)) :
598+
haveI := hU.isLocalization_basicOpen r
599+
haveI := h.isLocalization_basicOpen (f.app U r)
600+
Arrow.mk (f.app (Y.basicOpen r)) ≅
601+
Arrow.mk (IsLocalization.Away.map Γ(Y, Y.basicOpen r)
602+
Γ(X, X.basicOpen (f.app U r)) (f.app U) r) :=
603+
Arrow.isoMk (Iso.refl _) (X.presheaf.mapIso (eqToIso (by simp)).op) <| by
604+
simp [hU.app_basicOpen_eq_away_map f h]
605+
577606
include hU in
578607
theorem isLocalization_of_eq_basicOpen {V : X.Opens} (i : V ⟶ U) (e : V = X.basicOpen f) :
579608
@IsLocalization.Away _ _ f Γ(X, V) _ (X.presheaf.map i.op).toAlgebra := by

‎Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
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.Affine
7+
import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
8+
9+
/-!
10+
# Affine morphisms with additional ring hom property
11+
12+
In this file we define a constructor `affineAnd Q` for affine target morphism properties of schemes
13+
from a property of ring homomorphisms `Q`: A morphism `f : X ⟶ Y` with affine target satisfies
14+
`affineAnd Q` if it is an affine morphim (i.e. `X` is affine) and the induced ring map on global
15+
sections satisfies `Q`.
16+
17+
`affineAnd Q` inherits most stability properties of `Q` and is local at the target if `Q` is local
18+
at the (algebraic) source.
19+
20+
Typical examples of this are affine morphisms (where `Q` is trivial), finite morphisms
21+
(where `Q` is module finite) or closed immersions (where `Q` is being surjective).
22+
23+
-/
24+
25+
universe v u
26+
27+
open CategoryTheory TopologicalSpace Opposite MorphismProperty
28+
29+
namespace AlgebraicGeometry
30+
31+
section
32+
33+
variable (Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)
34+
35+
/-- This is the affine target morphism property where the source is affine and
36+
the induced map of rings on global sections satisfies `P`. -/
37+
def affineAnd : AffineTargetMorphismProperty :=
38+
fun X _ f ↦ IsAffine X ∧ Q (f.app ⊤)
39+
40+
@[simp]
41+
lemma affineAnd_apply {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] :
42+
affineAnd Q f ↔ IsAffine X ∧ Q (f.app ⊤) :=
43+
Iff.rfl
44+
45+
attribute [local simp] AffineTargetMorphismProperty.toProperty_apply
46+
47+
variable {Q}
48+
49+
/-- If `P` respects isos, also `affineAnd P` respects isomorphisms. -/
50+
lemma affineAnd_respectsIso (hP : RingHom.RespectsIso Q) :
51+
(affineAnd Q).toProperty.RespectsIso := by
52+
refine RespectsIso.mk _ ?_ ?_
53+
· intro X Y Z e f ⟨hZ, ⟨hY, hf⟩⟩
54+
simpa [hP.cancel_right_isIso, isAffine_of_isIso e.hom]
55+
· intro X Y Z e f ⟨hZ, hf⟩
56+
simpa [AffineTargetMorphismProperty.toProperty, isAffine_of_isIso e.inv, hP.cancel_left_isIso]
57+
58+
/-- `affineAnd P` is local if `P` is local on the (algebraic) source. -/
59+
lemma affineAnd_isLocal (hPi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationPreserves Q)
60+
(hQs : RingHom.OfLocalizationSpan Q) : (affineAnd Q).IsLocal where
61+
respectsIso := affineAnd_respectsIso hPi
62+
to_basicOpen {X Y _} f r := fun ⟨hX, hf⟩ ↦ by
63+
simp only [Opens.map_top] at hf
64+
constructor
65+
· simp only [Scheme.preimage_basicOpen, Opens.map_top]
66+
exact (isAffineOpen_top X).basicOpen _
67+
· dsimp only [Opens.map_top]
68+
rw [morphismRestrict_app, hPi.cancel_right_isIso, Scheme.Opens.ι_image_top]
69+
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
70+
hPi.cancel_right_isIso]
71+
haveI := (isAffineOpen_top X).isLocalization_basicOpen (f.app ⊤ r)
72+
apply hQl
73+
exact hf
74+
of_basicOpenCover {X Y _} f s hs hf := by
75+
dsimp [affineAnd] at hf
76+
haveI : IsAffine X := by
77+
apply isAffine_of_isAffineOpen_basicOpen (f.app ⊤ '' s)
78+
· apply_fun Ideal.map (f.app ⊤) at hs
79+
rwa [Ideal.map_span, Ideal.map_top] at hs
80+
· rintro - ⟨r, hr, rfl⟩
81+
simp_rw [Scheme.preimage_basicOpen] at hf
82+
exact (hf ⟨r, hr⟩).left
83+
refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.app ⊤) s hs fun a ↦ ?_⟩
84+
refine ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.app ⊤ a.val)), inferInstance,
85+
inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩
86+
· exact (isAffineOpen_top X).isLocalization_basicOpen (f.app ⊤ a.val)
87+
· obtain ⟨_, hf⟩ := hf a
88+
rw [morphismRestrict_app, hPi.cancel_right_isIso, Scheme.Opens.ι_image_top] at hf
89+
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map _ (isAffineOpen_top X)] at hf
90+
rwa [hPi.cancel_right_isIso] at hf
91+
92+
/-- If `P` is stable under base change, so is `affineAnd P`. -/
93+
lemma affineAnd_stableUnderBaseChange (hQi : RingHom.RespectsIso Q)
94+
(hQb : RingHom.StableUnderBaseChange Q) :
95+
(affineAnd Q).StableUnderBaseChange := by
96+
haveI : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi
97+
apply AffineTargetMorphismProperty.StableUnderBaseChange.mk
98+
intro X Y S _ _ f g ⟨hY, hg⟩
99+
exact ⟨inferInstance, hQb.pullback_fst_app_top _ hQi f _ hg⟩
100+
101+
lemma targetAffineLocally_affineAnd_iff (hQi : RingHom.RespectsIso Q)
102+
{X Y : Scheme.{u}} (f : X ⟶ Y) :
103+
targetAffineLocally (affineAnd Q) f ↔ ∀ U : Y.Opens, IsAffineOpen U →
104+
IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (f.app U) := by
105+
simp only [targetAffineLocally, affineAnd_apply, morphismRestrict_app, hQi.cancel_right_isIso]
106+
refine ⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩
107+
· obtain ⟨hfU, hf⟩ := hf ⟨U, hU⟩
108+
exact ⟨hfU, by rwa [Scheme.Opens.ι_image_top] at hf⟩
109+
· refine ⟨(h U U.2).1, ?_⟩
110+
rw [Scheme.Opens.ι_image_top]
111+
exact (h U U.2).2
112+
113+
end
114+
115+
section
116+
117+
variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
118+
119+
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
120+
composition if `Q` is. -/
121+
lemma HasAffineProperty.affineAnd_isStableUnderComposition {P : MorphismProperty Scheme.{u}}
122+
(hA : HasAffineProperty P (affineAnd Q)) (hQ : RingHom.StableUnderComposition Q) :
123+
P.IsStableUnderComposition where
124+
comp_mem {X Y Z} f g hf hg := by
125+
haveI := hA
126+
wlog hZ : IsAffine Z
127+
· rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
128+
intro U
129+
rw [morphismRestrict_comp]
130+
exact this hA hQ _ _ (IsLocalAtTarget.restrict hf _) (IsLocalAtTarget.restrict hg _) hA U.2
131+
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg
132+
obtain ⟨hY, hg⟩ := hg
133+
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
134+
obtain ⟨hX, hf⟩ := hf
135+
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]
136+
exact ⟨hX, hQ _ _ hg hf⟩
137+
138+
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
139+
base change if `Q` is. -/
140+
lemma HasAffineProperty.affineAnd_stableUnderBaseChange {P : MorphismProperty Scheme.{u}}
141+
(_ : HasAffineProperty P (affineAnd Q)) (hQi : RingHom.RespectsIso Q)
142+
(hQb : RingHom.StableUnderBaseChange Q) :
143+
P.StableUnderBaseChange :=
144+
HasAffineProperty.stableUnderBaseChange
145+
(AlgebraicGeometry.affineAnd_stableUnderBaseChange hQi hQb)
146+
147+
/-- If `Q` contains identities and respects isomorphisms (i.e. is satisfied by isomorphisms),
148+
and `P` is affine locally defined by `affineAnd Q`, then `P` contains identities. -/
149+
lemma HasAffineProperty.affineAnd_containsIdentities {P : MorphismProperty Scheme.{u}}
150+
(hA : HasAffineProperty P (affineAnd Q)) (hQi : RingHom.RespectsIso Q)
151+
(hQ : RingHom.ContainsIdentities Q) :
152+
P.ContainsIdentities where
153+
id_mem X := by
154+
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
155+
intro U hU
156+
exact ⟨hU, hQ _⟩
157+
158+
/-- A convenience constructor for `HasAffineProperty P (affineAnd Q)`. The `IsAffineHom` is bundled,
159+
since this goes well with defining morphism properties via `extends IsAffineHom`. -/
160+
lemma HasAffineProperty.affineAnd_iff (P : MorphismProperty Scheme.{u})
161+
(hQi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationPreserves Q)
162+
(hQs : RingHom.OfLocalizationSpan Q) :
163+
HasAffineProperty P (affineAnd Q) ↔
164+
∀ {X Y : Scheme.{u}} (f : X ⟶ Y), P f ↔
165+
(IsAffineHom f ∧ ∀ U : Y.Opens, IsAffineOpen U → Q (f.app U)) := by
166+
simp_rw [isAffineHom_iff]
167+
refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩
168+
· rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]
169+
aesop
170+
· ext X Y f
171+
rw [targetAffineLocally_affineAnd_iff hQi, h f]
172+
aesop
173+
174+
lemma HasAffineProperty.affineAnd_le_isAffineHom (P : MorphismProperty Scheme.{u})
175+
(hA : HasAffineProperty P (affineAnd Q)) : P ≤ @IsAffineHom := by
176+
intro X Y f hf
177+
wlog hY : IsAffine Y
178+
· rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (iSup_affineOpens_eq_top _)]
179+
intro U
180+
exact this P hA _ (IsLocalAtTarget.restrict hf _) U.2
181+
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf
182+
rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]
183+
exact hf.1
184+
185+
end
186+
187+
end AlgebraicGeometry

‎Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,15 +16,15 @@ of ring homs. For `P` a property of ring homs, we have two ways of defining a pr
1616
morphisms:
1717
1818
Let `f : X ⟶ Y`,
19-
- `targetAffineLocally (affine_and P)`: the preimage of an affine open `U = Spec A` is affine
20-
(`= Spec B`) and `A ⟶ B` satisfies `P`. (TODO)
19+
- `targetAffineLocally (affineAnd P)`: the preimage of an affine open `U = Spec A` is affine
20+
(`= Spec B`) and `A ⟶ B` satisfies `P`. (in `Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean`)
2121
- `affineLocally P`: For each pair of affine open `U = Spec A ⊆ X` and `V = Spec B ⊆ f ⁻¹' U`,
2222
the ring hom `A ⟶ B` satisfies `P`.
2323
2424
For these notions to be well defined, we require `P` be a sufficient local property. For the former,
2525
`P` should be local on the source (`RingHom.RespectsIso P`, `RingHom.LocalizationPreserves P`,
2626
`RingHom.OfLocalizationSpan`), and `targetAffineLocally (affine_and P)` will be local on
27-
the target. (TODO)
27+
the target.
2828
2929
For the latter `P` should be local on the target (`RingHom.PropertyIsLocal P`), and
3030
`affineLocally P` will be local on both the source and the target.

‎Mathlib/RingTheory/LocalProperties/Basic.lean‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,47 @@ theorem RingHom.PropertyIsLocal.ofLocalizationSpan (hP : RingHom.PropertyIsLocal
248248
· apply hP.StableUnderCompositionWithLocalizationAway.right _ r
249249
exact hs' ⟨r, hr⟩
250250

251+
lemma RingHom.OfLocalizationSpan.ofIsLocalization
252+
(hP : RingHom.OfLocalizationSpan P) (hPi : RingHom.RespectsIso P)
253+
{R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤)
254+
(hT : ∀ r : s, ∃ (Rᵣ Sᵣ : Type u) (_ : CommRing Rᵣ) (_ : CommRing Sᵣ)
255+
(_ : Algebra R Rᵣ) (_ : Algebra S Sᵣ) (_ : IsLocalization.Away r.val Rᵣ)
256+
(_ : IsLocalization.Away (f r.val) Sᵣ) (fᵣ : Rᵣ →+* Sᵣ)
257+
(_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f),
258+
P fᵣ) : P f := by
259+
apply hP _ s hs
260+
intro r
261+
obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, fᵣ, hfᵣ, hf⟩ := hT r
262+
let e₁ := (Localization.algEquiv (.powers r.val) Rᵣ).toRingEquiv
263+
let e₂ := (IsLocalization.algEquiv (.powers (f r.val))
264+
(Localization (.powers (f r.val))) Sᵣ).symm.toRingEquiv
265+
have : Localization.awayMap f r.val =
266+
(e₂.toRingHom.comp fᵣ).comp e₁.toRingHom := by
267+
apply IsLocalization.ringHom_ext (.powers r.val)
268+
ext x
269+
have : fᵣ ((algebraMap R Rᵣ) x) = algebraMap S Sᵣ (f x) := by
270+
rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]
271+
simp [-AlgEquiv.symm_toRingEquiv, e₂, e₁, Localization.awayMap, IsLocalization.Away.map, this]
272+
rw [this]
273+
apply hPi.right
274+
apply hPi.left
275+
exact hf
276+
277+
/-- Variant of `RingHom.OfLocalizationSpan.ofIsLocalization` where
278+
`fᵣ = IsLocalization.Away.map`. -/
279+
lemma RingHom.OfLocalizationSpan.ofIsLocalization'
280+
(hP : RingHom.OfLocalizationSpan P) (hPi : RingHom.RespectsIso P)
281+
{R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set R) (hs : Ideal.span s = ⊤)
282+
(hT : ∀ r : s, ∃ (Rᵣ Sᵣ : Type u) (_ : CommRing Rᵣ) (_ : CommRing Sᵣ)
283+
(_ : Algebra R Rᵣ) (_ : Algebra S Sᵣ) (_ : IsLocalization.Away r.val Rᵣ)
284+
(_ : IsLocalization.Away (f r.val) Sᵣ),
285+
P (IsLocalization.Away.map Rᵣ Sᵣ f r)) : P f := by
286+
apply hP.ofIsLocalization hPi _ s hs
287+
intro r
288+
obtain ⟨Rᵣ, Sᵣ, _, _, _, _, _, _, hf⟩ := hT r
289+
exact ⟨Rᵣ, Sᵣ, inferInstance, inferInstance, inferInstance, inferInstance,
290+
inferInstance, inferInstance, IsLocalization.Away.map Rᵣ Sᵣ f r, IsLocalization.map_comp _, hf⟩
291+
251292
lemma RingHom.OfLocalizationSpanTarget.ofIsLocalization
252293
(hP : RingHom.OfLocalizationSpanTarget P) (hP' : RingHom.RespectsIso P)
253294
{R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤)

0 commit comments

Comments
 (0)