Paper XII · Lean source
ComponentSupport.lean
Inherited / related evidence Coverage and evidence
The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
PaperXII/ComponentSupport.lean21 lines
Original source path
core/publication/source/lean_guide/formal_release/lean/PaperXII/ComponentSupport.leanSkip declarations and read code
1 import PaperXII.ModuleSupport
2 import Mathlib.RingTheory.Spectrum.Prime.Topology
3
4 /-! Paper XII, Corollary 6.8, including actual irreducible components and generic points. -/
5 namespace PaperXII.ComponentSupport
6
7 open ModuleSupport
8
9 /-- Every irreducible component has a generic point with nonzero localized module. -/
10 theorem exists_genericPoint_nontrivial_localization
11 {R M : Type*} [CommRing R] [IsNoetherianRing R]
12 [AddCommGroup M] [Module R M] [Module.Finite R M]
13 (h : NearlyFaithful R M) (Z : Set (PrimeSpectrum R))
14 (hZ : Z ∈ irreducibleComponents (PrimeSpectrum R)) :
15 ∃ p : PrimeSpectrum R, IsGenericPoint p Z ∧
16 Nontrivial (LocalizedModule p.asIdeal.primeCompl M) := by
17 obtain ⟨p, hp⟩ := QuasiSober.sober hZ.1
18 (isClosed_of_mem_irreducibleComponents Z hZ)
19 exact ⟨p, hp, nontrivial_localization_of_nearlyFaithful R M h p⟩
20
21 end PaperXII.ComponentSupport
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: d6a2a42f8834ba233d1126093c3074975ff638db33d3c2a2d8c6f237b420d9df
Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion