OrdinaryPatching.lean

1 import PaperXII.QuotientSupport
2 import Mathlib.RingTheory.Noetherian.Basic
3 
4 /-! Paper XII, Theorem 6.11. Only actual algebra and module identifications are inputs. -/
5 namespace PaperXII.OrdinaryPatching
6 
7 open ModuleSupport QuotientSupport
8 
9 variable {A R P M : Type*} [CommRing A] [CommRing R]
10     [AddCommGroup P] [Module A P] [Module.Finite A P]
11 
12 /-- Full support descends to the actual augmentation quotient. -/
13 theorem quotient_fullSupport (I : Ideal A) (h : FullSupport A P) :
14     FullSupport (A ⧸ I) (P ⧸ (I • ⊤ : Submodule A P)) := by
15   apply (fullSupport_iff_localizations _ _).mpr
16   intro q
17   apply (support_quotient_iff I q).mpr
18   exact (fullSupport_iff_localizations A P).mp h _
19 
20 /-- A concrete presentation of the ordinary patching identifications:
21 A → R is surjective with kernel I, and P/IP ≃ M as A-modules.
22 There is no support or occupancy conclusion in these inputs. -/
23 theorem fullSupport_descends [Algebra A R] [AddCommGroup M] [Module A M]
24     [Module R M] [IsScalarTower A R M]
25     (I : Ideal A) (hf : Function.Surjective (algebraMap A R))
26     (hker : RingHom.ker (algebraMap A R) = I)
27     (e : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] M)
28     (h : FullSupport A P) : FullSupport R M := by
29   let : Module.Finite A M := Module.Finite.equiv e
30   apply (fullSupport_iff_localizations R M).mpr
31   intro q
32   apply (mem_support_restrictScalars_iff hf q).mp
33   rw [← e.support_eq, Module.support_quotient]
34   refine ⟨(fullSupport_iff_localizations A P).mp h _, ?_⟩
35   change I ≤ Ideal.comap (algebraMap A R) q.asIdeal
36   rw [← hker]
37   exact Ideal.ker_le_comap _
38 
39 /-- The near-faithfulness conclusion of 6.11, including transported patching data. -/
40 theorem nearlyFaithful_descends [IsNoetherianRing A]
41     [Algebra A R] [AddCommGroup M] [Module A M]
42     [Module R M] [IsScalarTower A R M]
43     (I : Ideal A) (hf : Function.Surjective (algebraMap A R))
44     (hker : RingHom.ker (algebraMap A R) = I)
45     (e : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] M)
46     (h : NearlyFaithful A P) : NearlyFaithful R M := by
47   let : IsNoetherianRing R := isNoetherianRing_of_surjective A R (algebraMap A R) hf
48   let : Module.Finite A M := Module.Finite.equiv e
49   let : Module.Finite R M := Module.Finite.of_restrictScalars_finite A R M
50   exact (nearlyFaithful_iff_fullSupport R M).mpr
51     (fullSupport_descends I hf hker e ((nearlyFaithful_iff_fullSupport A P).mp h))
52 
53 /-- The reduced-ring faithfulness conclusion of 6.11. -/
54 theorem faithful_descends_of_reduced [IsNoetherianRing A] [IsReduced R]
55     [Algebra A R] [AddCommGroup M] [Module A M]
56     [Module R M] [IsScalarTower A R M]
57     (I : Ideal A) (hf : Function.Surjective (algebraMap A R))
58     (hker : RingHom.ker (algebraMap A R) = I)
59     (e : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] M)
60     (h : NearlyFaithful A P) : FaithfulSMul R M := by
61   let : IsNoetherianRing R := isNoetherianRing_of_surjective A R (algebraMap A R) hf
62   exact (nearlyFaithful_iff_faithful_of_reduced R M).mp
63     (nearlyFaithful_descends I hf hker e h)
64 
65 /-- All conclusions of 6.11 from the actual ring and module quotient identifications. -/
66 theorem conclusions_of_quotient_identifications [IsNoetherianRing A]
67     [Algebra A R] [AddCommGroup M] [Module A M]
68     [Module R M] [IsScalarTower A R M]
69     (I : Ideal A) (eR : (A ⧸ I) ≃ₐ[A] R)
70     (eM : (P ⧸ (I • ⊤ : Submodule A P)) ≃ₗ[A] M)
71     (h : FullSupport A P) :
72     FullSupport R M ∧ NearlyFaithful R M ∧ (IsReduced R → FaithfulSMul R M) := by
73   have hmap : algebraMap A R = eR.toRingHom.comp (Ideal.Quotient.mk I) := by
74     ext a
75     exact (eR.commutes a).symm
76   have hf : Function.Surjective (algebraMap A R) := by
77     rw [hmap]
78     exact eR.surjective.comp Ideal.Quotient.mk_surjective
79   have hker : RingHom.ker (algebraMap A R) = I := by
80     ext a
81     change algebraMap A R a = 0 ↔ a ∈ I
82     rw [hmap]
83     change eR (Ideal.Quotient.mk I a) = 0 ↔ a ∈ I
84     constructor
85     · intro hz
86       apply Ideal.Quotient.eq_zero_iff_mem.mp
87       apply eR.injective
88       exact hz.trans (map_zero eR).symm
89     · intro ha
90       rw [Ideal.Quotient.eq_zero_iff_mem.mpr ha, map_zero]
91   have hn := (nearlyFaithful_iff_fullSupport A P).mpr h
92   refine ⟨fullSupport_descends I hf hker eM h,
93     nearlyFaithful_descends I hf hker eM hn, ?_⟩
94   intro hred
95   let : IsReduced R := hred
96   exact faithful_descends_of_reduced I hf hker eM hn
97 
98 end PaperXII.OrdinaryPatching

Back to source controls