FiniteFreeCompletion.lean

1 import PaperXI.ResidueExtensionRealization
2 import Mathlib.RingTheory.AdicCompletion.Basic
3 import Mathlib.RingTheory.AdicCompletion.Noetherian
4 
5 /-! Completeness is derived in finite free coordinates, not assumed of the
6 constructed root ring. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.FiniteFreeCompletion
10 open IsLocalRing Module
11 variable {R : Type*} [CommRing R] (I : Ideal R)
12 variable {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
13 
14 theorem linear_congruence (f : M →ₗ[R] N) {x y : M} {n : ℕ}
15     (h : x ≡ y [SMOD (I ^ n • ⊤ : Submodule R M)]) :
16     f x ≡ f y [SMOD (I ^ n • ⊤ : Submodule R N)] := by
17   apply (h.map f).mono
18   rw [Submodule.map_smul'']
19   gcongr
20   exact le_top
21 
22 variable {ι : Type*} [Fintype ι] (b : Basis ι R M)
23 include b
24 
25 theorem precomplete [IsPrecomplete I R] : IsPrecomplete I M := by
26   classical
27   constructor
28   intro a ha
29   have hc : ∀ i, ∃ L : R, ∀ n,
30       b.coord i (a n) ≡ L [SMOD (I ^ n • ⊤ : Submodule R R)] := by
31     intro i
32     exact IsPrecomplete.prec' (fun n => b.coord i (a n))
33       (fun h => linear_congruence I (b.coord i) (ha h))
34   choose L hL using hc
35   refine ⟨∑ i, L i • b i, ?_⟩
36   intro n
37   rw [← b.sum_repr (a n)]
38   apply SModEq.sum
39   intro i _
40   exact linear_congruence I (LinearMap.toSpanSingleton R M (b i)) (hL i n)
41 
42 theorem hausdorff [IsHausdorff I R] : IsHausdorff I M := by
43   constructor
44   intro x hx
45   have hc : ∀ i, b.coord i x = 0 := by
46     intro i
47     apply IsHausdorff.haus' (I := I)
48     intro n
49     simpa using linear_congruence I (b.coord i) (hx n)
50   rw [← b.sum_repr x]
51   simp only [← Basis.coord_apply, hc, zero_smul, Finset.sum_const_zero]
52 
53 theorem complete [IsAdicComplete I R] : IsAdicComplete I M :=
54   { precomplete I b, hausdorff I b with }
55 
56 end PaperXI.FiniteFreeCompletion
57 
58 namespace PaperXI.CompleteResidueRealization
59 open IsLocalRing Polynomial
60 variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
61 variable (s : Type*) [Field s] [Algebra (ResidueField R) s]
62 variable [FiniteDimensional (ResidueField R) s] [Algebra.IsSeparable (ResidueField R) s]
63 variable [IsAdicComplete (maximalIdeal R) R]
64 
65 theorem complete :
66     IsAdicComplete (maximalIdeal (ResidueExtensionRealization.ring R s))
67       (ResidueExtensionRealization.ring R s) := by
68   let b := AdjoinRoot.powerBasis'
69     (ResidueExtensionRealization.monic R s).out
70   have hc := FiniteFreeCompletion.complete (maximalIdeal R) b.basis
71   rw [MonicResidueAlgebra.maximalIdeal_eq, MonicResidueAlgebra.specialIdeal]
72   exact { IsPrecomplete.map_algebraMap_iff.mpr hc.toIsPrecomplete,
73           IsHausdorff.map_algebraMap_iff.mpr hc.toIsHausdorff with }
74 
75 end PaperXI.CompleteResidueRealization

Back to source controls