Paper XII · Lean source
CorrectedOccupancy.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/CorrectedOccupancy.lean24 lines
Original source path
core/publication/source/lean_guide/formal_release/lean/PaperXII/CorrectedOccupancy.leanSkip declarations and read code
1 import PaperXII.OrdinaryPatching
2 import Mathlib.RingTheory.Spectrum.Prime.Topology
3
4 /-! Amended Paper XII 6.12: each component is contained in the support.
5 The original reversed containment is not claimed as proved. -/
6 set_option autoImplicit false
7 namespace PaperXII.CorrectedOccupancy
8 open ModuleSupport
9
10 /-- Full support after patching contains every entire irreducible component. -/
11 theorem componentwise_occupancy
12 {A R P M : Type*} [CommRing A] [CommRing R] [Algebra A R]
13 [AddCommGroup P] [Module A P] [Module.Finite A P]
14 [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower A R M]
15 (I : Ideal A) (hf : Function.Surjective (algebraMap A R))
16 (hker : RingHom.ker (algebraMap A R) = I)
17 (e : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] M) (h : FullSupport A P) :
18 ∀ Z ∈ irreducibleComponents (PrimeSpectrum R), Z ⊆ Module.support R M := by
19 have hs := OrdinaryPatching.fullSupport_descends I hf hker e h
20 intro Z _
21 rw [show Module.support R M = Set.univ from hs]
22 exact Set.subset_univ Z
23
24 end PaperXII.CorrectedOccupancy
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: efbbb72e4f864a073569846e95a9a25470d45c95c9b3d7ed3bd84a6d9125dd93
Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion