CompletionBoundaryChecks.lean

1 import PaperXII.CompletedPointCategory
2 
3 /-! Exact edge checks for the completed objects and their defining ideals. -/
4 noncomputable section
5 set_option autoImplicit false
6 namespace PaperXII.CompletionBoundaryChecks
7 
8 variable {O ι : Type*} [CommRing O] [Fintype ι] [DecidableEq ι]
9 variable (R : ι → Type*) [∀ i, CommRing (R i)] [∀ i, Algebra O (R i)]
10 variable (mO : Ideal O) (m : ∀ i, Ideal (R i))
11 
12 omit [Fintype ι] in
13 /-- An empty tensor family retains the base-adic topology. -/
14 theorem empty_definingIdeal [IsEmpty ι] :
15     FiniteTensor.definingIdeal R mO m = mO.map (algebraMap O (FiniteTensor.Raw (O := O) R)) := by
16   simp [FiniteTensor.definingIdeal, FiniteTensor.conditions]
17 
18 omit [Fintype ι] in
19 /-- Zero local conditions generate the zero closed ideal, not a larger residual ideal. -/
20 theorem zero_closedConditions :
21     FiniteTensor.closedConditions R mO m (fun _ ↦ ⊥) = ⊥ := by
22   rw [FiniteTensor.closedConditions_eq]
23   simp only [Ideal.map_bot, iSup_bot]
24   apply Ideal.closure_eq_of_isClosed
25   exact isClosed_singleton
26 
27 omit [Fintype ι] in
28 /-- An inconsistent local condition kills the actual complete tensor ring. -/
29 theorem top_closedCondition (I : ∀ i, Ideal (R i)) (i : ι) (hi : I i = ⊤) :
30     FiniteTensor.closedConditions R mO m I = ⊤ := by
31   rw [FiniteTensor.closedConditions_eq]
32   apply top_unique
33   have h : (I i).map (FiniteTensor.completedInclude R mO m i).toRingHom ≤
34       ⨆ j, (I j).map (FiniteTensor.completedInclude R mO m j).toRingHom := le_iSup (fun j ↦ (I j).map (FiniteTensor.completedInclude R mO m j).toRingHom) i
35   rw [hi, Ideal.map_top] at h
36   exact h.trans (show (⨆ j, (I j).map (FiniteTensor.completedInclude R mO m j).toRingHom) ≤
37     (⨆ j, (I j).map (FiniteTensor.completedInclude R mO m j).toRingHom).closure from subset_closure)
38 
39 /-- Completion imposes no nontriviality premise in the main quotient comparison. -/
40 theorem quotientComparison_top (I : ∀ i, Ideal (R i)) :
41     Continuous (FiniteTensor.completed_tensor_quotient R mO m I) ∧
42       Continuous (FiniteTensor.completed_tensor_quotient R mO m I).symm :=
43   FiniteTensor.completed_tensor_quotient_continuous R mO m I
44 
45 end PaperXII.CompletionBoundaryChecks

Back to source controls