PatchingCarriers.lean

1 import PaperXII.HeckeCarriers
2 import PaperXII.OrdinaryCompletion
3 import PaperXII.DerivedPatching
4 
5 /-!
6 # Actual ordinary and derived patched carriers
7 
8 The ordinary branch retains the coefficient quotient and module control
9 isomorphism. The derived branch retains an actual isomorphism in the derived
10 category. Full support is assumed only for the patched object and is proved
11 for the finite-level carrier.
12 -/
13 
14 set_option autoImplicit false
15 
16 noncomputable section
17 
18 open CategoryTheory
19 
20 universe u
21 
22 attribute [local instance] HasDerivedCategory.standard
23 
24 namespace PaperXII.PatchingCarriers
25 
26 open HeckeCarriers
27 
28 variable {A R T : Type u} [CommRing A] [CommRing R] [CommRing T]
29 
30 /-- The ordinary patching input uses the actual coefficient quotient and
31 the actual module quotient. Finite generation at finite level is not assumed. -/
32 structure OrdinaryDatum (A R : Type u) [CommRing A] [CommRing R] [Algebra A R] where
33   noetherian : IsNoetherianRing A
34   ideal : Ideal A
35   coefficient : (A ⧸ ideal) ≃ₐ[A] R
36   patched : FiniteModule A
37   finiteLevel : ModuleCat.{u} R
38   comparison : (patched.object ⧸ (ideal • ⊤ : Submodule A patched.object)) ≃ₗ[A]
39     (ModuleCat.restrictScalars (algebraMap A R)).obj finiteLevel
40   patchedSupport : ModuleSupport.FullSupport A patched.object
41 
42 variable [Algebra A R]
43 
44 /-- The finite-level object with its specified coefficient action restricted to A. -/
45 abbrev OrdinaryDatum.restricted (D : OrdinaryDatum A R) : ModuleCat.{u} A :=
46   (ModuleCat.restrictScalars (algebraMap A R)).obj D.finiteLevel
47 
48 /-- This scalar tower is induced by the actual coefficient algebra map. -/
49 instance OrdinaryDatum.restricted_scalarTower (D : OrdinaryDatum A R) :
50     IsScalarTower A R D.restricted where
51   smul_assoc a r m := by
52     change (a • r) • m = algebraMap A R a • (r • m)
53     rw [Algebra.smul_def, mul_smul]
54 
55 /-- Finite generation is descended through the supplied module control map. -/
56 theorem OrdinaryDatum.finite_level_finite (D : OrdinaryDatum A R) :
57     Module.Finite R D.finiteLevel := by
58   change Module.Finite R D.restricted
59   exact OrdinaryCompletion.finite_level_finite (R := R) (H := D.restricted)
60     D.ideal D.comparison
61 
62 /-- The finite-level ordinary carrier has the literal supplied module. -/
63 def OrdinaryDatum.finiteModule (D : OrdinaryDatum A R) : FiniteModule R where
64   object := D.finiteLevel
65   finite := D.finite_level_finite
66 
67 /-- Quotient support descent proves finite-level full support. -/
68 theorem OrdinaryDatum.fullSupport (D : OrdinaryDatum A R) :
69     FullSupport (.inl D.finiteModule) := by
70   let : IsNoetherianRing A := D.noetherian
71   change ModuleSupport.FullSupport R D.restricted
72   exact OrdinaryCompletion.finite_level_fullSupport (H := D.restricted)
73     D.ideal D.coefficient D.comparison D.patchedSupport
74 
75 /-- The derived patching input retains the actual derived comparison and full
76 support of the patched complex. -/
77 structure DerivedDatum (A R : Type u) [CommRing A] [CommRing R] where
78   datum : DerivedPatching.Datum A R
79   patchedSupport : PerfectDerivedSupport.FullSupport datum.patched
80 
81 omit [Algebra A R] in
82 /-- Derived quotient support descent proves finite-level full support. -/
83 theorem DerivedDatum.fullSupport (D : DerivedDatum A R) :
84     FullSupport (.inr D.datum.finitePerfect) :=
85   DerivedPatching.fullSupport_descends D.datum D.patchedSupport
86 
87 /-- A patched carrier consists of one of the two actual patching constructions. -/
88 def PatchedCarrier (A R : Type u) [CommRing A] [CommRing R] [Algebra A R] :=
89   OrdinaryDatum A R ⊕ DerivedDatum A R
90 
91 /-- Recover the finite-level ordinary or perfect derived carrier. -/
92 def PatchedCarrier.finiteCarrier : PatchedCarrier A R → Carrier R
93   | .inl D => .inl D.finiteModule
94   | .inr D => .inr D.datum.finitePerfect
95 
96 /-- Both branches derive the same precise finite-level support conclusion. -/
97 theorem PatchedCarrier.fullSupport (D : PatchedCarrier A R) :
98     FullSupport D.finiteCarrier := by
99   cases D with
100   | inl D => exact D.fullSupport
101   | inr D => exact D.fullSupport
102 
103 /-- An actual support comparison carries the descended support to a Hecke carrier. -/
104 theorem PatchedCarrier.comparison_fullSupport (D : PatchedCarrier A R)
105     (f : R →+* T) (H : Carrier T)
106     (comparison : SupportComparison f D.finiteCarrier H) : FullSupport H :=
107   supportComparison_fullSupport f D.finiteCarrier H comparison D.fullSupport
108 
109 end PaperXII.PatchingCarriers

Back to source controls