Skip to content

Commit 3773dce

Browse files
erdOnepre-commit-ci-lite[bot]chrisflav
committed
feat(AlgebraicGeometry): abelian varieties are abelian (#35354)
We show that proper geometrically-integral group schemes over fields are commutative. Co-authored-by: Christian Merten Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Christian Merten <christian@merten.dev>
1 parent 194a1d4 commit 3773dce

File tree

10 files changed

+270
-2
lines changed

10 files changed

+270
-2
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1302,6 +1302,7 @@ public import Mathlib.AlgebraicGeometry.Geometrically.Irreducible
13021302
public import Mathlib.AlgebraicGeometry.Geometrically.Reduced
13031303
public import Mathlib.AlgebraicGeometry.Gluing
13041304
public import Mathlib.AlgebraicGeometry.GluingOneHypercover
1305+
public import Mathlib.AlgebraicGeometry.Group.Abelian
13051306
public import Mathlib.AlgebraicGeometry.Group.Smooth
13061307
public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic
13071308
public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

‎Mathlib/AlgebraicGeometry/AlgClosed/Basic.lean‎

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ namespace AlgebraicGeometry
2525

2626
universe u
2727

28-
variable {X : Scheme.{u}} {K : Type u} [Field K] [IsAlgClosed K]
28+
variable {X Y : Scheme.{u}} {K : Type u} [Field K] [IsAlgClosed K]
2929
(f : X ⟶ Spec (.of K)) [LocallyOfFiniteType f] (x : X) (hx : IsClosed {x})
3030

3131
/-- If `X` is a locally of finite type `k`-scheme and `k` is algebraically closed, then
@@ -84,4 +84,29 @@ def pointEquivClosedPoint :
8484
rw [reassoc_of% Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, p.2]
8585
right_inv x := by simp
8686

87+
lemma ext_of_apply_closedPoint_eq
88+
{f g : Spec (.of K) ⟶ X} (h : X ⟶ Spec (.of K))
89+
[LocallyOfFiniteType h]
90+
(hf : f ≫ h = 𝟙 _) (hg : g ≫ h = 𝟙 _)
91+
(H : f (IsLocalRing.closedPoint K) = g (IsLocalRing.closedPoint K)) : f = g :=
92+
congr($((pointEquivClosedPoint h).injective (a₁ := ⟨f, hf⟩) (a₂ := ⟨g, hg⟩) (Subtype.ext H)).1)
93+
94+
/-- Let `X` and `Y` be locally of finite type `K`-schemes with `K` algebraically closed and `Y`
95+
separated over `K`. Suppose `X` is reduced, then two `K`-morphisms `f g : X ⟶ Y` are equal if
96+
they are equal on the closed points of a dense locally closed subset of `X`. -/
97+
lemma ext_of_apply_eq {f g : X ⟶ Y} (i : Y ⟶ Spec (.of K)) [IsSeparated i] [LocallyOfFiniteType i]
98+
[IsReduced X] [LocallyOfFiniteType (f ≫ i)]
99+
(S : Set X) (hS : IsLocallyClosed S) (hS' : Dense S)
100+
(H : ∀ x ∈ S, IsClosed {x} → f x = g x)
101+
(H' : f ≫ i = g ≫ i) : f = g := by
102+
have : JacobsonSpace ↥X := LocallyOfFiniteType.jacobsonSpace (f ≫ i)
103+
refine ext_of_fromSpecResidueField_eq f g i (S ∩ closedPoints X) ?_ ?_ H'
104+
· rwa [dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
105+
← dense_iff_closure_eq]
106+
· intro x ⟨hxS, hx⟩
107+
rw [← cancel_epi (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom)]
108+
refine ext_of_apply_closedPoint_eq i ?_ ?_ (by simpa using H x hxS hx) <;>
109+
simp only [Category.assoc, ← SpecMap_residueFieldIsoBase_inv (f ≫ i) x hx, ← Spec.map_comp,
110+
Iso.inv_hom_id, Spec.map_id, ← H']
111+
87112
end AlgebraicGeometry

‎Mathlib/AlgebraicGeometry/Group/Abelian.lean‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
/-
2+
Copyright (c) 2026 Andrew Yang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Andrew Yang, Christian Merten
5+
-/
6+
module
7+
8+
public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
9+
public import Mathlib.AlgebraicGeometry.Geometrically.Integral
10+
public import Mathlib.AlgebraicGeometry.ZariskisMainTheorem
11+
public import Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_
12+
13+
/-!
14+
# Abelian varieties
15+
16+
## Main results
17+
- `AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral`:
18+
A proper geometrically integral group scheme over a field is commutative.
19+
20+
-/
21+
22+
@[expose] public section
23+
24+
open CategoryTheory Limits
25+
26+
namespace AlgebraicGeometry
27+
28+
universe u
29+
30+
variable {K : Type u} [Field K] {X : Scheme.{u}}
31+
32+
open MonoidalCategory CartesianMonoidalCategory MonObj
33+
34+
instance (G : Over (Spec (.of K))) [GrpObj G] : IsClosedImmersion η[G].left :=
35+
isClosedImmersion_of_comp_eq_id (Y := Spec (.of K)) G.hom η[G].left (by simp)
36+
37+
theorem isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed [IsAlgClosed K]
38+
(G : Over (Spec (.of K))) [IsProper G.hom] [IsIntegral (G ⊗ G).left] [GrpObj G] :
39+
IsCommMonObj G := by
40+
let S := Spec (.of K)
41+
let point : S := IsLocalRing.closedPoint K
42+
have hpoint : IsClosed {point} := isClosed_discrete _
43+
have : Nonempty G.left := ⟨η[G].left point⟩
44+
have : IsProper (G ⊗ G).hom := by dsimp; infer_instance
45+
have : JacobsonSpace (G ⊗ G).left := LocallyOfFiniteType.jacobsonSpace (Y := Spec _) (G ⊗ G).hom
46+
have : Surjective G.hom := ⟨Function.surjective_to_subsingleton (α := G.left) (β := Spec _) _⟩
47+
have : IsProper (fst G G).left := by dsimp; infer_instance
48+
have : Surjective (fst G G).left := by dsimp; infer_instance
49+
have : IsProper ((GrpObj.commutator G).left ≫ G.hom) := by rw [Over.w]; infer_instance
50+
have : IsClosedImmersion ((lift η[G] η[G]).left ≫ (fst G G).left) := by
51+
simpa using inferInstanceAs (IsClosedImmersion η[G].left)
52+
have : IsClosedImmersion (lift η[G] η[G]).left := .of_comp _ (g := (fst G G).left)
53+
let γ : G ⊗ G ⟶ G ⊗ G := lift (fst _ _) (GrpObj.commutator _)
54+
have : IsProper (γ.left ≫ (fst G G).left) := by simpa [γ]
55+
have : IsProper γ.left := .of_comp _ (fst G G).left
56+
-- It suffices to check that `γ : (x, y) ↦ x * y * x⁻¹ * y⁻¹` is constantly `1`.
57+
rw [isCommMonObj_iff_commutator_eq_toUnit_η]
58+
ext1
59+
have H : γ.left '' ((fst G G).left ⁻¹' {η[G].left point}) ⊆ {(lift η[G] η[G]).left point} := by
60+
rw [Set.image_subset_iff, ← Set.diff_eq_empty, ← Set.not_nonempty_iff_eq_empty]
61+
intro H
62+
obtain ⟨c₀, ⟨hc₁, hc₂⟩, hc₃⟩ := nonempty_inter_closedPoints H <| by
63+
rw [Set.diff_eq_compl_inter, ← Set.image_singleton, ← Set.image_singleton];
64+
refine (IsOpen.isLocallyClosed ?_).inter (IsClosed.isLocallyClosed ?_)
65+
· exact (((lift η[G] η[G]).left.isClosedMap _ hpoint).preimage γ.left.continuous).isOpen_compl
66+
· exact (η[G].left.isClosedMap _ hpoint).preimage (fst G G).left.continuous
67+
obtain ⟨⟨c, hc⟩, e⟩ := (pointEquivClosedPoint (G ⊗ G).hom).surjective ⟨c₀, hc₃⟩
68+
obtain rfl : c point = c₀ := congr(($e).1)
69+
let fc : 𝟙_ (Over S) ⟶ 𝟙_ (Over S) ⊗ G := lift (𝟙 _) (Over.homMk c hc ≫ snd G G)
70+
have : c ≫ pullback.fst G.hom G.hom = η[G].left :=
71+
ext_of_apply_closedPoint_eq G.hom (by simpa) (by simp) (by simpa)
72+
have H₁ : c = fc.left ≫ (η[G] ▷ G).left := by dsimp; ext <;> simp [fc, S, this]
73+
have H₂ : fc ≫ η ▷ G ≫ γ = lift η η := by ext1 <;> simp [fc, γ, S]
74+
exact hc₂ <| by simp [H₁, H₂, ← Scheme.Hom.comp_apply, Category.assoc, ← Over.comp_left]
75+
-- Since the image of `y ↦ γ(e, y)` is finite, by Zariski Main, there exists an open
76+
-- `1 ∈ U ⊆ G` such that `γ ∣_ U` factors through a finite scheme over `U`.
77+
obtain ⟨U, hηU, H⟩ := exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage
78+
γ.left (fst G G).left (η[G].left point) (by
79+
dsimp [-Scheme.Hom.comp_base, γ]
80+
simp only [pullback.lift_fst]
81+
exact (Set.finite_singleton _).subset H)
82+
have H (x : U) : ((pullback.fst G.hom G.hom) ⁻¹' {x.1} ∩ Set.range ⇑γ.left).Finite := by
83+
refine ((((γ.left.imageι ≫ (fst G G).left) ∣_ U).finite_preimage_singleton x).image
84+
(Scheme.Opens.ι _ ≫ γ.left.imageι)).subset ?_
85+
have : U.ι ⁻¹' {x.1} = {x} := by ext; simp
86+
rw [← this, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
87+
morphismRestrict_ι, ← Category.assoc, Scheme.Hom.comp_base (_ ≫ _) (fst G G).left,
88+
TopCat.coe_comp, Set.preimage_comp, Set.image_preimage_eq_inter_range]
89+
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι]
90+
dsimp
91+
rw [Set.image_preimage_eq_inter_range, Scheme.IdealSheafData.range_subschemeι,
92+
Scheme.Hom.support_ker, ← Set.inter_assoc, ← Set.preimage_inter,
93+
Set.singleton_inter_of_mem x.2, IsClosed.closure_eq
94+
(by exact γ.left.isClosedMap.isClosed_range)]
95+
-- It suffices to check set-theoretic equality on closed points of `U ×[k] G`.
96+
refine ext_of_apply_eq G.hom _
97+
((fst G G).left ⁻¹ᵁ U).isOpen.isLocallyClosed
98+
(((fst G G).left ⁻¹ᵁ U).isOpen.dense ?_) ?_ ?_
99+
· exact .preimage ⟨_, hηU⟩ (fst G G).left.surjective
100+
· intro y hyU hy
101+
have hx : IsClosed {(fst G G).left y} := by simpa using (fst G G).left.isClosedMap _ hy
102+
let x : 𝟙_ _ ⟶ G := Over.homMk (pointOfClosedPoint G.hom _ hx) (by simp)
103+
let xe : (G ⊗ G).left := (fst G G ≫ (ρ_ _).inv ≫ G ◁ η[G]).left y
104+
have : γ.left y = xe := by
105+
-- By the choice of `U`, the set `γ({y} ×[k] G)` is finite and hence, by irreducibility,
106+
-- a singleton.
107+
refine subsingleton_image_closure_of_finite_of_isPreirreducible
108+
(hx.preimage (fst G G).left.continuous).isLocallyClosed ?_ γ.left.continuous
109+
γ.left.isClosedMap ((H ⟨_, hyU⟩).subset (Set.image_subset_iff.mpr fun _ ↦ by
110+
simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base, γ])) ?_ ?_
111+
· let α : G ⊗ G ⟶ G ⊗ G := toUnit _ ≫ x ⊗ₘ 𝟙 _
112+
convert ((IrreducibleSpace.isIrreducible_univ _).image α.left
113+
α.left.continuous.continuousOn).isPreirreducible
114+
rw [Over.tensorHom_left]
115+
simp [Set.range_comp, Scheme.Pullback.range_map, x]
116+
· exact ⟨y, subset_closure (by simp), rfl⟩
117+
· refine ⟨xe, subset_closure ?_, ?_⟩
118+
· simp [xe, ← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]
119+
· simp only [xe, γ, ← Scheme.Hom.comp_apply, ← Over.comp_left]
120+
congr 6; ext <;> simp
121+
convert congr((snd G G).left $this) using 1
122+
· simp [γ, ← Scheme.Hom.comp_apply]
123+
· simp [xe, ← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]
124+
· simp
125+
126+
/-- A proper geometrically integral group scheme over a field is commutative. -/
127+
@[stacks 0BFD]
128+
theorem isCommMonObj_of_isProper_of_geometricallyIntegral
129+
(G : Over (Spec (.of K))) [IsProper G.hom] [GeometricallyIntegral G.hom] [GrpObj G] :
130+
IsCommMonObj G := by
131+
let f := Spec.map (CommRingCat.ofHom <| algebraMap K (AlgebraicClosure K))
132+
let G' := (Over.pullback f).obj G
133+
have : IsProper G'.hom := by dsimp [G']; infer_instance
134+
have : IsIntegral (G' ⊗ G').left := by dsimp [G']; infer_instance
135+
let : GrpObj G' := Functor.grpObjObj
136+
have := isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed G'
137+
rw [isCommMonObj_iff_commutator_eq_toUnit_η] at this ⊢
138+
apply (Over.pullback f).map_injective
139+
rw [← cancel_epi (Functor.Monoidal.μIso (Over.pullback f) G G).hom]
140+
dsimp [GrpObj.commutator] at this ⊢
141+
simpa only [Functor.map_mul, one_eq_one, comp_one, Functor.map_one, Functor.map_inv',
142+
comp_mul, GrpObj.comp_inv, Functor.Monoidal.μ_fst, Functor.Monoidal.μ_snd]
143+
144+
end AlgebraicGeometry

‎Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -168,4 +168,16 @@ instance (P : MorphismProperty Scheme) [P.DescendsAlong (@Surjective ⊓ @Flat
168168
· dsimp [MorphismProperty.isomorphisms] at H ⊢
169169
exact IsZariskiLocalAtTarget.of_isPullback (.flip <| .of_hasPullback _ _) H
170170

171+
instance {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [QuasiCompact f] :
172+
(Over.pullback f).Faithful :=
173+
MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
174+
(P := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
175+
⟨⟨inferInstance, inferInstance⟩, inferInstance⟩
176+
177+
instance {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [Flat f] [LocallyOfFinitePresentation f] :
178+
(Over.pullback f).Faithful :=
179+
MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
180+
(P := @Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)
181+
⟨⟨inferInstance, inferInstance⟩, inferInstance⟩
182+
171183
end AlgebraicGeometry

‎Mathlib/AlgebraicGeometry/Morphisms/Separated.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -297,6 +297,15 @@ lemma ext_of_isDominant_of_isSeparated [IsReduced X] {f g : X ⟶ Y}
297297
rw [← cancel_epi (equalizer.ι f' g').left]
298298
exact congr($(equalizer.condition f' g').left)
299299

300+
lemma ext_of_fromSpecResidueField_eq (f g : X ⟶ Y) (i : Y ⟶ Z) [IsSeparated i] [IsReduced X]
301+
(S : Set X) (hS' : Dense S)
302+
(H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g)
303+
(H' : f ≫ i = g ≫ i) : f = g := by
304+
suffices IsDominant (equalizer.ι f g) from
305+
ext_of_isDominant_of_isSeparated i H' (equalizer.ι f g) (equalizer.condition _ _)
306+
refine ⟨.mono (fun x hx ↦ ⟨equalizer.lift _ (H _ hx) default, ?_⟩) hS'⟩
307+
rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]
308+
300309
variable (S) in
301310
/--
302311
Suppose `X` is a reduced `S`-scheme and `Y` is a separated `S`-scheme.

‎Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,9 @@ instance [Surjective f] [Surjective g] : Surjective (f ≫ g) := ⟨g.surjective
7373
lemma Surjective.of_comp [Surjective (f ≫ g)] : Surjective g where
7474
surj := Function.Surjective.of_comp (g := f) (f ≫ g).surjective
7575

76+
instance (priority := low) [Nonempty X] [Subsingleton Y] (f : X ⟶ Y) :
77+
Surjective f := ⟨Function.surjective_to_subsingleton _⟩
78+
7679
lemma Surjective.comp_iff [Surjective f] : Surjective (f ≫ g) ↔ Surjective g :=
7780
⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩
7881

‎Mathlib/AlgebraicGeometry/Noetherian.lean‎

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Geno Racklin Asher
66
module
77

88
public import Mathlib.AlgebraicGeometry.Morphisms.Immersion
9-
public import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
9+
public import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
1010
public import Mathlib.RingTheory.Localization.Submodule
1111
public import Mathlib.RingTheory.Spectrum.Prime.Noetherian
1212

@@ -250,6 +250,28 @@ theorem LocallyOfFiniteType.isLocallyNoetherian
250250
algebraize [φ.hom]
251251
simp_all [Algebra.FiniteType.isNoetherianRing R]
252252

253+
instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S)
254+
[IsLocallyNoetherian Y] [LocallyOfFiniteType f] :
255+
IsLocallyNoetherian (Limits.pullback f g) :=
256+
LocallyOfFiniteType.isLocallyNoetherian (Limits.pullback.snd _ _)
257+
258+
instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S)
259+
[IsLocallyNoetherian X] [LocallyOfFiniteType g] :
260+
IsLocallyNoetherian (Limits.pullback f g) :=
261+
LocallyOfFiniteType.isLocallyNoetherian (Limits.pullback.fst _ _)
262+
263+
instance (priority := low) {X Y : Scheme} (f : X ⟶ Y)
264+
[IsLocallyNoetherian Y] [LocallyOfFiniteType f] :
265+
LocallyOfFinitePresentation f := by
266+
refine ⟨fun {U hU V hV} hUV ↦ ?_⟩
267+
let := (f.appLE U V hUV).hom.toAlgebra
268+
have : IsNoetherianRing Γ(Y, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
269+
exact Algebra.FinitePresentation.of_finiteType.mp (f.finiteType_appLE hU hV hUV)
270+
271+
lemma LocallyOfFinitePresentation.iff_locallyOfFiniteType {X Y : Scheme} {f : X ⟶ Y}
272+
[IsLocallyNoetherian Y] : LocallyOfFinitePresentation f ↔ LocallyOfFiniteType f :=
273+
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
274+
253275
/-- A scheme `X` is Noetherian if it is locally Noetherian and compact. -/
254276
@[mk_iff]
255277
class IsNoetherian (X : Scheme) : Prop extends IsLocallyNoetherian X, CompactSpace X

‎Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,14 @@ lemma GrpObj.inv_eq_inv : ι = (𝟙 G)⁻¹ := by simp [Hom.inv_def]
182182
@[reassoc (attr := simp)]
183183
lemma GrpObj.one_inv : η[G] ≫ ι = η := by simp [GrpObj.inv_eq_inv, GrpObj.comp_inv, one_eq_one]
184184

185+
open scoped _root_.CategoryTheory.Obj in
186+
/-- If `G` is a group object and `F` is monoidal,
187+
then `Hom(X, G) → Hom(F X, F G)` preserves inverses. -/
188+
@[simp] lemma Functor.map_inv' {D : Type*} [Category* D] [CartesianMonoidalCategory D] (F : C ⥤ D)
189+
[F.Monoidal] {X G : C} (f : X ⟶ G) [GrpObj G] :
190+
F.map (f⁻¹) = (F.map f)⁻¹ := by
191+
rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]
192+
185193
@[deprecated (since := "2025-09-13")] alias Grp_Class.inv_eq_inv := GrpObj.inv_eq_inv
186194

187195
/-- The commutator of `G` as a morphism. This is the map `(x, y) ↦ x * y * x⁻¹ * y⁻¹`,

‎Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,12 @@ lemma tensorUnit_hom : (𝟙_ (Over X)).hom = 𝟙 X := rfl
7171
lemma lift_left {R S T : Over X} (f : R ⟶ S) (g : R ⟶ T) :
7272
(lift f g).left = pullback.lift f.left g.left (f.w.trans g.w.symm) := rfl
7373

74+
@[simp]
75+
lemma fst_left {R S : Over X} : (fst R S).left = pullback.fst _ _ := rfl
76+
77+
@[simp]
78+
lemma snd_left {R S : Over X} : (snd R S).left = pullback.snd _ _ := rfl
79+
7480
@[simp]
7581
lemma toUnit_left {R : Over X} : (toUnit R).left = R.hom := rfl
7682

‎Mathlib/Topology/JacobsonSpace.lean‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,12 @@ lemma closedPoints_eq_univ [T1Space X] :
5858
closedPoints X = Set.univ :=
5959
Set.eq_univ_iff_forall.mpr fun _ ↦ isClosed_singleton
6060

61+
lemma Set.Finite.isDiscrete_of_subset_closedPoints
62+
{s : Set X} (hs : s.Finite) (hs' : s ⊆ closedPoints X) : IsDiscrete s := by
63+
have : T1Space s := ⟨fun x ↦ by convert (hs' x.2).preimage continuous_subtype_val; aesop⟩
64+
have : Finite s := hs
65+
exact ⟨inferInstance⟩
66+
6167
end closedPoints
6268

6369
/-- The class of Jacobson spaces, i.e.
@@ -102,6 +108,16 @@ lemma nonempty_inter_closedPoints [JacobsonSpace X] {Z : Set X}
102108
(hZ : Z.Nonempty) (hZ' : IsLocallyClosed Z) : (Z ∩ closedPoints X).Nonempty :=
103109
jacobsonSpace_iff_locallyClosed.mp inferInstance Z hZ hZ'
104110

111+
theorem JacobsonSpace.closure_inter_closedPoints_eq_closure [JacobsonSpace X]
112+
{S : Set X} (hS : IsLocallyClosed S) : closure (S ∩ closedPoints X) = closure S := by
113+
refine (closure_mono (Set.inter_subset_left)).antisymm ?_
114+
rw [IsClosed.closure_subset_iff isClosed_closure]
115+
intro x hx
116+
by_contra H
117+
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := nonempty_inter_closedPoints (Z := S \ closure (S ∩ closedPoints X))
118+
⟨x, hx, H⟩ (.inter hS isClosed_closure.isOpen_compl.isLocallyClosed)
119+
exact hy₂ (subset_closure ⟨hy₁, hy₃⟩)
120+
105121
lemma isClosed_singleton_of_isLocallyClosed_singleton [JacobsonSpace X] {x : X}
106122
(hx : IsLocallyClosed {x}) : IsClosed {x} := by
107123
obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
@@ -175,3 +191,25 @@ lemma TopologicalSpace.IsOpenCover.jacobsonSpace_iff {ι : Type*} {U : ι → Op
175191
rw [Set.eq_empty_iff_forall_notMem]
176192
intro z (hz : z.1 = y.1)
177193
exact h (hz ▸ z.2)
194+
195+
theorem subsingleton_image_closure_of_finite_of_isPreirreducible [JacobsonSpace X]
196+
{S : Set X} (hS : IsLocallyClosed S) (hS' : IsPreirreducible S)
197+
(hf₁ : Continuous f) (hf₂ : IsClosedMap f) (hfS : (f '' S).Finite) :
198+
(f '' closure S).Subsingleton := by
199+
obtain rfl | hS'' := S.eq_empty_or_nonempty
200+
· simp
201+
replace hS' : IsIrreducible S := ⟨hS'', hS'⟩
202+
have H₁ : IsIrreducible (S ∩ closedPoints X) := by
203+
rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
204+
isIrreducible_iff_closure] at hS'
205+
have H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y := by
206+
rintro _ ⟨x, hx, rfl⟩; simpa using hf₂ _ hx.2
207+
have H₃ := ((hfS.subset (Set.image_mono Set.inter_subset_left)).isDiscrete_of_subset_closedPoints
208+
H₂).subsingleton_of_isPreirreducible (H₁.image _ hf₁.continuousOn).isPreirreducible
209+
have H₄ : IsClosed (f '' (S ∩ closedPoints X)) := by
210+
obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
211+
· simp [h]
212+
· rw [H₃.eq_singleton_of_mem hx]; exact H₂ hx
213+
have := image_closure_subset_closure_image (s := S ∩ closedPoints X) hf₁
214+
rw [JacobsonSpace.closure_inter_closedPoints_eq_closure hS, H₄.closure_eq] at this
215+
exact H₃.anti this

0 commit comments

Comments
 (0)
⚡