AdicLocalConditions.lean

1 import PaperXII.LocalQuotients
2 import PaperXII.ClassSpines
3 import Mathlib.Algebra.MvPolynomial.Eval
4 
5 /-! Effectivity for declared polynomial quotient conditions on actual matrix
6 entries. Every positive precision detects the same ideal. Arbitrary arithmetic
7 conditions are not identified with such an ideal without a separate argument. -/
8 set_option autoImplicit false
9 namespace PaperXII.AdicLocalConditions
10 
11 open ContinuousMonoidHom Matrix
12 open AdicMatrixGroups AdicCompanions ClassCompanions ContinuousClasses LocalQuotients
13 
14 variable {R S : Type} [CommRing R] [CommRing S] (I : Ideal R)
15 
16 /-- Vanishing on an ideal is detected at every positive adic precision. -/
17 theorem ideal_killed_iff_positive [IsHausdorff I R] (J : Ideal S) (f : S →+* R) :
18     J ≤ RingHom.ker f ↔ ∀ n, 0 < n → J ≤ RingHom.ker ((quotientMap I n).comp f) := by
19   constructor
20   · intro h n _ a ha
21     change quotientMap I n (f a) = 0
22     rw [show f a = 0 from h ha, map_zero]
23   · intro h a ha
24     change f a = 0
25     apply PaperX.RepresentationLimits.scalar_ext I
26     intro n
27     cases n with
28     | zero =>
29       have : Subsingleton (R ⧸ I ^ 0) := coeff_zero_subsingleton I
30       exact Subsingleton.elim _ _
31     | succ n =>
32       have hn := h (n + 1) (Nat.succ_pos n) ha
33       change (Ideal.Quotient.mk (I ^ (n + 1))) (f a) = 0 at hn
34       simpa only [map_zero] using hn
35 
36 /-- Actual quotient factorization is detected by all positive finite reductions. -/
37 theorem factors_iff_positive [IsHausdorff I R] (J : Ideal S) (f : S →+* R) :
38     Factors J f ↔ ∀ n, 0 < n → Factors J ((quotientMap I n).comp f) := by
39   simp only [factors_iff, ideal_killed_iff_positive I]
40 
41 variable {Γ ι : Type} [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
42 
43 /-- Coordinates are the actual matrix entries at specified group elements. -/
44 abbrev Coordinates := Γ × ι × ι
45 
46 /-- Evaluate the coordinate polynomial ring on the actual continuous adic representation. -/
47 def point (ρ : AdicRep (Γ := Γ) (ι := ι) I) : MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R →+* R :=
48   MvPolynomial.eval₂Hom (RingHom.id R) (fun x ↦ (ρ x.1).val x.2.1 x.2.2)
49 
50 /-- Finite evaluation uses the same polynomial coefficients reduced modulo I^n. -/
51 def finitePoint (n : ℕ) (σ : Γ →ₜ* GL ι (Coeff I n)) :
52     MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R →+* Coeff I n :=
53   MvPolynomial.eval₂Hom (quotientMap I n) (fun x ↦ (σ x.1).val x.2.1 x.2.2)
54 
55 /-- Evaluation commutes with the actual reduction of continuous representations. -/
56 theorem point_reduces (ρ : AdicRep (Γ := Γ) (ι := ι) I) (n : ℕ) :
57     (quotientMap I n).comp (point I ρ) = finitePoint I n (reduceRep I n ρ) := by
58   rw [point, MvPolynomial.comp_eval₂Hom]
59   rfl
60 
61 /-- Every relation in a declared coordinate ideal holds integrally if it holds at all positive levels. -/
62 theorem ideal_effective [IsHausdorff I R]
63     (J : Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R))
64     (ρ : AdicRep (Γ := Γ) (ι := ι) I)
65     (h : ∀ n, 0 < n → J ≤ RingHom.ker (finitePoint I n (reduceRep I n ρ))) :
66     J ≤ RingHom.ker (point I ρ) := by
67   apply (ideal_killed_iff_positive I J (point I ρ)).mpr
68   intro n hn
69   rw [point_reduces]
70   exact h n hn
71 
72 /-- The original evaluation point has a unique map from the actual condition quotient. -/
73 theorem exists_unique_condition_factor [IsHausdorff I R]
74     (J : Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R))
75     (ρ : AdicRep (Γ := Γ) (ι := ι) I)
76     (h : ∀ n, 0 < n → J ≤ RingHom.ker (finitePoint I n (reduceRep I n ρ))) :
77     ∃! g : (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R) ⧸ J →+* R,
78       g.comp (Ideal.Quotient.mk J) = point I ρ := by
79   obtain ⟨g, hg⟩ := (factors_iff J (point I ρ)).mpr (ideal_effective I J ρ h)
80   exact ⟨g, hg, fun k hk ↦ factor_unique J (point I ρ) k g hk hg⟩
81 
82 /-- Class completion preserves the actual quotient condition when every allowed frame satisfies it. -/
83 theorem class_condition_preserved [IsHausdorff I R]
84     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
85     (J : Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R))
86     (ρ : AdicRealization I (Framed I C))
87     (h : ∀ n, 0 < n → ∀ σ, Framed I C n σ → J ≤ RingHom.ker (finitePoint I n σ)) :
88     Factors J (point I ρ.val) := by
89   apply (factors_iff J _).mpr
90   apply ideal_effective I J ρ.val
91   intro n hn
92   exact h n hn (reduceRep I n ρ.val) (ρ.property n)
93 
94 /-- A whole indexed family of declared local ideals survives the same completion. -/
95 theorem all_class_conditions_preserved [IsHausdorff I R] {V : Type}
96     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
97     (J : V → Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R))
98     (ρ : AdicRealization I (Framed I C))
99     (h : ∀ v n, 0 < n → ∀ σ, Framed I C n σ → J v ≤ RingHom.ker (finitePoint I n σ)) :
100     ∀ v, Factors (J v) (point I ρ.val) := fun v ↦ class_condition_preserved I C (J v) ρ (h v)
101 
102 /-- Actual continuous class realizations exist with all specified polynomial quotient conditions. -/
103 theorem exists_class_realization_with_conditions [IsAdicComplete I R]
104     (hI : I.FG) [Finite (R ⧸ I)]
105     (C : ∀ n, LevelClass (Γ := Γ) (ι := ι) I n → Prop)
106     (hC : ∀ n c, C (n + 1) c → C n (classStep I n c))
107     (finiteC : ∀ n, 0 < n → Finite {c // C n c})
108     (hc : ∀ n, 0 < n → ∀ c, C n c → PaperX.ClassInvariants.ClassContinuous c)
109     (hne : ∀ n, 0 < n → ∃ c, C n c)
110     {V : Type} (J : V → Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) R))
111     (h : ∀ v n, 0 < n → ∀ σ, Framed I C n σ → J v ≤ RingHom.ker (finitePoint I n σ)) :
112     ∃ ρ : AdicRealization I (Framed I C), ∀ v, Factors (J v) (point I ρ.val) := by
113   obtain ⟨ρ⟩ := exists_class_realization_positive I hI C hC finiteC hc hne
114   exact ⟨ρ, all_class_conditions_preserved I C J ρ h⟩
115 
116 end PaperXII.AdicLocalConditions

Back to source controls