Adic congruences, adic cylinders and division charts

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Basic7import Mathlib.Topology.Algebra.MvPolynomial8 9/-!10# Adic congruences, adic cylinders and division charts11 12This file sets up the adic language used by the measure-theoretic part of the development.13For an ideal `I` of a ring `R` and an `R`-module `M`, `x ≡ y (mod I^j M)` is `adicCongr I j x y`;14the adic cylinders `{y | y ≡ x (mod I^j M)}` generate the σ-algebra `adicCylinderSpace I M`.15We then introduce the coordinates attached to a division chart (an `O`-linear equivalence16`R ≃ (Fin n → O) × R` inverse to `(z, v) ↦ ∑ zᵢ bᵢ + f v`), the curve ideals17`(f + π ∑ zᵢ bᵢ)` they parametrize, ideal atlases and their measures, and the power-basis18coordinates of an unramified extension `O[X]/(Φ)`.19 20## Main results21 22* `mvPolynomial_zero_null`: zero sets of nonzero multivariate polynomials are null for products23  of atomless finite measures.24* `child_volume_ratio`: the local volume recursion for the children of a tangent pattern.25* `colored_subset_count`: the multinomial count of partially coloured maps `Fin Q → Option (Fin r)`.26* `division_linear_equivalence`: a lifted basis of `R/(f)` yields a division equivalence.27* `division_chart_rank_eq_of_residue_ideal_eq`: division charts with the same residue ideal28  have the same rank.29* `finite_coordinate_cylinder_basis`, `finite_coordinate_borel_cylinders`: on `O^n` with the30  `I`-adic topology, adic cylinders form a basis and generate the Borel σ-algebra.31 32Provenance: `Def_SurfaceBlowupV2_{AdicDigits, CylinderFamily, IdealCoordinates, Normalizer,33IdealAtlas, IdealChartSigma, UnramifiedMeasure}`, `Thm_Gen_PolyZeroNull`, `Thm_SurfaceBlowupV2_*`:34`algebra_product_congruence`, `child_volume_ratio`, `colored_subset_count`,35`common_vertical_exponent`, `congruence_bijection_measurable`, `coordinate_constraint_count`,36`coordinate_ideal_in_residue_cell`, `coordinate_module_pi_quotient_length`,37`coordinate_remainder_raises_order`, `division_chart_rank_eq_of_residue_ideal_eq`,38`division_coordinates_{injective, surjective}`, `division_{data, chart}_same_cell_recenter`,39`division_linear_equivalence`, `finite_coordinate_{adic_congruence, cylinder_basis,40borel_cylinders, linear_continuous}`.41-/42 43noncomputable section44 45open MeasureTheory46open scoped BigOperators ENNReal47 48namespace SurfaceBlowup49 50/-! ### Adic congruences and cylinders -/51 52section53 54variable {R M : Type} [CommRing R] [AddCommGroup M] [Module R M]55 56/-- `x ≡ y` modulo `I ^ j • M`. -/57def adicCongr (I : Ideal R) (j : ℕ) (x y : M) : Prop :=58  x - y ∈ (I ^ j • ⊤ : Submodule R M)59 60/-- A self-map `r` of `M` raises adic order: `x ≡ y (mod I^j)` implies `r x ≡ r y (mod I^(j+1))`. -/61def RaisesAdicOrder (I : Ideal R) (r : M → M) : Prop :=62  ∀ j x y, adicCongr I j x y → adicCongr I (j+1) (r x) (r y)63 64/-- The perturbation `x ↦ x + r x` of the identity by `r`. -/65def adicPerturb (r : M → M) (x : M) : M := x + r x66 67/-- The fixed-point iteration `x₀ = 0`, `x_{j+1} = y - r xⱼ` solving `x + r x = y`. -/68def digitIter (r : M → M) (y : M) : ℕ → M69  | 0 => 070  | j+1 => y - r (digitIter r y j)71 72/-- The quotient `M / I ^ j M`. -/73abbrev AdicQuotient (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M]74    (j : ℕ) := M ⧸ (I ^ j • ⊤ : Submodule R M)75 76/-- The reduction map `M → M / I ^ j M`. -/77def adicReduce (I : Ideal R) (j : ℕ) : M →ₗ[R] AdicQuotient I M j :=78  (I ^ j • ⊤ : Submodule R M).mkQ79 80/-- The adic cylinders of `M`: the empty set and the congruence classes modulo `I ^ j M`. -/81def adicCylinders (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M] : Set (Set M) :=82  {s | s = ∅ ∨ ∃ j x, s = {y | adicCongr I j y x}}83 84set_option warn.classDefReducibility false in85/-- The σ-algebra on `M` generated by the adic cylinders. -/86def adicCylinderSpace (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M] :87    MeasurableSpace M :=88  MeasurableSpace.generateFrom (adicCylinders I M)89 90end91 92/-! ### Division coordinates and curve ideals -/93 94section95 96variable {O R : Type} [CommRing O] [CommRing R] [Algebra O R]97 98/-- The lift `∑ i, zᵢ • bᵢ` of coordinates `z ∈ O^n` along representatives `b`. -/99def coordinateLift {n : ℕ} (b : Fin n → R) (z : Fin n → O) : R := ∑ i, z i • b i100 101/-- Scaling the coordinates by `a ∈ O` multiplies their lift by the image of `a`. -/102theorem coordinateLift_smul_eq_mul {n : ℕ} (b : Fin n → R) (a : O) (z : Fin n → O) :103    coordinateLift b (a • z) = algebraMap O R a * coordinateLift b z := by104  simp only [coordinateLift, Finset.mul_sum, Pi.smul_apply, smul_eq_mul, Algebra.smul_def, map_mul,105    mul_assoc]106 107/-- The division map `(z, v) ↦ ∑ zᵢ bᵢ + f v`. -/108def divisionMap {n : ℕ} (f : R) (b : Fin n → R) (s : (Fin n → O) × R) : R :=109  coordinateLift b s.1 + f * s.2110 111/-- The generator `f + ∑ zᵢ bᵢ`. -/112def normalizedGenerator {n : ℕ} (f : R) (b : Fin n → R) (z : Fin n → O) : R :=113  f + coordinateLift b z114 115/-- The remainder map `(z, v) ↦ π • E (v · ∑ zᵢ bᵢ)` of the normalization fixed-point problem. -/116def coordinateRemainder {n : ℕ} (pi : O) (b : Fin n → R)117    (E : R ≃ₗ[O] ((Fin n → O) × R)) (s : (Fin n → O) × R) : (Fin n → O) × R :=118  pi • E (s.2 * coordinateLift b s.1)119 120/-- The residue cell of `f`: principal ideals whose image modulo `π` is `(f mod π)`. -/121def residueIdealCell (pi f : R) : Set (Ideal R) :=122  {J | (∃ g : R, J = Ideal.span {g}) ∧123    Ideal.map (Ideal.Quotient.mk (Ideal.span {pi})) J =124      Ideal.span {Ideal.Quotient.mk (Ideal.span {pi}) f}}125 126/-- The principal ideal `(f + ∑ zᵢ bᵢ)`. -/127def normalizedIdeal {n : ℕ} (f : R) (b : Fin n → R) (z : Fin n → O) : Ideal R :=128  Ideal.span {normalizedGenerator f b z}129 130/-- The normal form of `h`: the solution `s` of `s + coordinateRemainder s = E h` (by choice). -/131def generatorNormalForm {n : ℕ} (pi : O) (b : Fin n → R)132    (E : R ≃ₗ[O] ((Fin n → O) × R)) (h : R) : (Fin n → O) × R :=133  Function.invFun (adicPerturb (coordinateRemainder pi b E)) (E h)134 135/-- The curve ideal `(f + π ∑ zᵢ bᵢ)` of the chart `(f, b)` at the coordinates `z`. -/136def coordinateIdeal {n : ℕ} (pi : O) (f : R) (b : Fin n → R) (z : Fin n → O) : Ideal R :=137  normalizedIdeal f b (pi • z)138 139/-- The transition map between two charts with the same residue cell. -/140def idealTransition {n : ℕ} (pi : O) (b c : Fin n → R)141    (F : R ≃ₗ[O] ((Fin n → O) × R)) (h0 : R) (z : Fin n → O) : Fin n → O :=142  (generatorNormalForm pi c F (h0 + coordinateLift b z)).1143 144end145 146/-! ### Ideal charts, atlases and their measures -/147 148section149 150variable (O R : Type) [CommRing O] [CommRing R] [Algebra O R]151 152/-- A division chart of rank `n`: a generator `f` regular modulo `π` with representatives `b`153and an `O`-linear equivalence `E` inverse to the division map. -/154structure IdealChart (pi : O) (n : ℕ) whereProposition 3.2155  /-- The centre generator. -/156  f : R157  /-- The coordinate representatives. -/158  b : Fin n → R159  /-- The division equivalence. -/160  E : R ≃ₗ[O] ((Fin n → O) × R)161  division : ∀ s, E.symm s = divisionMap f b s162  regular : Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>163    y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f)164 165/-- A finite atlas of `X` by charts of rank `n` whose residue cells partition `X`. -/166structure IdealAtlas (pi : O) (n : ℕ) (X : Set (Ideal R)) where167  /-- The chart index type. -/168  ι : Type169  [fin : Fintype ι]170  /-- The charts. -/171  chart : ι → IdealChart O R pi n172  cover : X = ⋃ i, residueIdealCell (algebraMap O R pi) (chart i).f173  disjoint : Pairwise fun i j =>174    Disjoint (residueIdealCell (algebraMap O R pi) (chart i).f)175      (residueIdealCell (algebraMap O R pi) (chart j).f)176 177attribute [instance] IdealAtlas.fin178 179/-- Division-chart data for the chart `z ↦ (f + pi·b(z))`: the representatives `b` carry an180`O`-linear division equivalence for `f` and `f` is regular modulo `pi`. -/181def IsDivisionChart (pi : O) {n : ℕ} (f : R) (b : Fin n → R) : Prop :=182  (∃ E : R ≃ₗ[O] ((Fin n → O) × R), ∀ s, E.symm s = divisionMap f b s) ∧183    Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>184      y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f)185 186variable {O R} in187/-- The centre and representatives of an ideal chart form a division chart. -/188theorem IdealChart.isDivisionChart {pi : O} {n : ℕ} (C : IdealChart O R pi n) :189    IsDivisionChart O R pi C.f C.b :=190  ⟨⟨C.E, C.division⟩, C.regular⟩191 192set_option warn.classDefReducibility false in193/-- The intrinsic σ-algebra on curve ideals: generated by the images of the Borel sets of `O^n`194under all division charts of all ranks `n`. -/195def idealChartSigma [MeasurableSpace O] (pi : O) : MeasurableSpace (Ideal R) :=Proposition 3.2196  MeasurableSpace.generateFrom197    {T : Set (Ideal R) | ∃ (n : ℕ) (f : R) (b : Fin n → R) (S : Set (Fin n → O)),198      IsDivisionChart O R pi f b ∧ MeasurableSet S ∧ T = coordinateIdeal pi f b '' S}199 200variable [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]201  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] [IsDomain O]202  [MeasurableSpace (Ideal R)]203 204/-- The pushforward of the coefficient measure of `O^n` along the chart's curve-ideal map. -/205noncomputable def chartMeasure (pi : O) (n : ℕ) (c : IdealChart O R pi n) : Measure (Ideal R) :=206  (coefficientMeasure O n).map (coordinateIdeal pi c.f c.b)207 208/-- The measure `q^(-n) ∑ᵢ chartMeasure (chart i)` of an atlas. -/209noncomputable def stateMeasure (pi : O) (n : ℕ) (q : ℕ) {X : Set (Ideal R)}210    (A : IdealAtlas O R pi n X) : Measure (Ideal R) :=211  ((q : ℝ≥0∞)⁻¹^n) • ∑ i : A.ι, chartMeasure O R pi n (A.chart i)212 213end214 215/-! ### Unramified extensions -/216 217section218 219variable (O : Type) [CommRing O] (Φ : Polynomial O) (hm : Φ.Monic)220 221/-- Coordinates of `O_δ = O[X]/(Φ)` in the power basis `1, θ, …, θ^(δ-1)` (`δ = natDegree Φ`). -/222noncomputable def powerCoordinates : AdjoinRoot Φ ≃ₗ[O] (Fin Φ.natDegree → O) :=223  (AdjoinRoot.powerBasis' hm).basis.equivFun224 225end226 227section228 229variable (O : Type) [CommRing O] [TopologicalSpace O] (Φ : Polynomial O) (hm : Φ.Monic)230 231set_option warn.classDefReducibility false in232/-- The topology of `O_δ` transported from the product topology of `O^δ` along the power basis. -/233noncomputable def unramifiedTopology : TopologicalSpace (AdjoinRoot Φ) :=234  TopologicalSpace.induced (powerCoordinates O Φ hm) inferInstance235 236end237 238section239 240variable (O : Type) [CommRing O] [MeasurableSpace O] (Φ : Polynomial O) (hm : Φ.Monic)241 242set_option warn.classDefReducibility false in243/-- The σ-algebra of `O_δ` transported from the product σ-algebra of `O^δ` along the power244basis. -/245noncomputable def unramifiedMeasurableSpace : MeasurableSpace (AdjoinRoot Φ) :=246  MeasurableSpace.comap (powerCoordinates O Φ hm) inferInstance247 248end249 250section251 252variable (O : Type) [CommRing O] [IsDomain O]253  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]254  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (Φ : Polynomial O) (hm : Φ.Monic)255 256/-- The coefficient measure of `O_δ`: the pushforward of the normalized coefficient Haar measure257of `O^δ` along the inverse of the power-basis coordinates. It is stated for an arbitrary ambient258σ-algebra on `AdjoinRoot Φ`; the theorems assume the transported one. -/259noncomputable def unramifiedCoefficientMeasure [MeasurableSpace (AdjoinRoot Φ)] :260    Measure (AdjoinRoot Φ) :=261  Measure.map (powerCoordinates O Φ hm).symm (coefficientMeasure O Φ.natDegree)262 263end264 265/-! ### Polynomial zero sets are null -/266 267/-- The zero set of a nonzero multivariate polynomial over a domain is null for any finite268product of copies of an atomless finite measure. -/269theorem mvPolynomial_zero_null {R : Type} [CommRing R] [IsDomain R]Discriminant locus is null270    [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] [SecondCountableTopology R]271    [MeasurableSpace R] [BorelSpace R]272    (ν : Measure R) [IsFiniteMeasure ν] [NullSingletonClass ν] :273    ∀ (n : ℕ) (P : MvPolynomial (Fin n) R), P ≠ 0 →274      Measure.pi (fun _ : Fin n => ν) {x | MvPolynomial.eval x P = 0} = 0 := by275  classical276  intro n277  induction n with278  | zero =>279    intro P hP280    rw [MvPolynomial.eq_C_of_isEmpty P] at hP ⊢281    simp_all282  | succ n ih =>283    intro P hP284    set Q := MvPolynomial.finSuccEquiv R n P285    have hQ : Q ≠ 0 := (map_ne_zero_iff _ (MvPolynomial.finSuccEquiv R n).injective).2 hP286    have hZ : MeasurableSet {x : Fin (n+1) → R | MvPolynomial.eval x P = 0} :=287      (isClosed_eq (MvPolynomial.continuous_eval P) continuous_const).measurableSet288    let e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n+1) => R) 0289    set T : Set (R × (Fin n → R)) := e.symm ⁻¹' {x | MvPolynomial.eval x P = 0} with hT290    rw [← (measurePreserving_piFinSuccAbove (fun _ : Fin (n+1) => ν) 0).symm.measure_preimage291      hZ.nullMeasurableSet, Measure.prod_apply_symm (e.symm.measurable hZ)]292    have hae := measure_eq_zero_iff_ae_notMem.1 (ih _ (Polynomial.leadingCoeff_ne_zero.mpr hQ))293    have hzero : (fun s : Fin n → R => ν ((fun y => (y, s)) ⁻¹' T))294        =ᵐ[Measure.pi fun _ : Fin n => ν] 0 := by295      filter_upwards [hae] with s hs296      have hne : Polynomial.map (MvPolynomial.eval s) Q ≠ 0 := fun h => hs <| by297        simpa using congrArg (Polynomial.coeff · Q.natDegree) h298      refine measure_mono_null (fun y hy => ?_) ((Finset.finite_toSet299        (Polynomial.map (MvPolynomial.eval s) Q).roots.toFinset).measure_zero ν)300      simp only [hT, Set.mem_preimage, Set.mem_ofPred_eq] at hy301      have key : e.symm (y, s) = Fin.cons y s := by302        ext i303        refine Fin.cases ?_ (fun j => ?_) i <;> simp [e, MeasurableEquiv.piFinSuccAbove_symm_apply,304          Fin.insertNthEquiv]305      rw [key, MvPolynomial.eval_eq_eval_mv_eval'] at hy306      simpa using (Polynomial.mem_roots hne).2 hy307    rw [lintegral_congr_ae hzero]; simp308 309/-! ### Adic congruences -/310 311/-- Adic congruences in an `O`-algebra are compatible with multiplication. -/312theorem algebra_product_congruence (O R : Type) [CommRing O] [CommRing R] [Algebra O R]313    (I : Ideal O) (j : ℕ) (x x2 y y2 : R) (hx : adicCongr I j x x2) (hy : adicCongr I j y y2) :314    adicCongr I j (x*y) (x2*y2) := by315  have key : ∀ r : R, ∀ z ∈ (I ^ j • ⊤ : Submodule O R), r * z ∈ (I ^ j • ⊤ : Submodule O R) :=316    fun r z hz => Submodule.smul_induction_on hz317      (fun a ha m _ => mul_smul_comm a r m ▸ Submodule.smul_mem_smul ha Submodule.mem_top)318      (fun u v hu hv => (mul_add r u v).symm ▸ add_mem hu hv)319  unfold adicCongr at *320  rw [show x * y - x2 * y2 = y * (x - x2) + x2 * (y - y2) by ring]321  exact add_mem (key _ _ hx) (key _ _ hy)322 323/-! ### Local volume recursion -/324 325private lemma expr_eval_pow (x : ℚ) (e : Expr) (n : ℕ) :326    (Expr.pow e n).eval x = (e.eval x)^n := by327  induction n with328  | zero => simp [Expr.pow, Expr.eval]329  | succ n ih => simp [Expr.pow, Expr.eval, ih, pow_succ]330 331private lemma otherChildren_volume_prod (x : ℚ) (n a : ℕ) (m : Pattern n) :332    ((otherChildren a m).map fun z => (stateVolume z.2).eval (x^z.1)).prod333      = (x^(patternWeight m))⁻¹ := by334  unfold otherChildren patternWeight335  rw [List.map_flatMap, List.flatMap_def, List.prod_flatten, List.map_map]336  simp only [Function.comp_def, List.map_replicate, List.prod_replicate, stateVolume,337    Expr.eval, expr_eval_pow]338  rw [Finset.prod_map_toList, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_inv_distrib]339  refine Finset.prod_congr rfl fun ij _ => ?_340  rw [inv_pow, ← pow_mul, ← pow_mul, mul_assoc]341 342/-- The volume recursion: the children of an allowed tangent pattern `P` at a state `s`,343weighted by `q^(-tri d)`, have total volume `divisorProbability s d · stateVolume s`. -/344theorem child_volume_ratio (s : State) (hs : s.Valid) (P : TangentPattern s.degree)Proposition 6.1345    (hP : Allowed s P) (q : ℕ) (hq : 2 ≤ q) :346    ((q:ℚ)⁻¹^(tri P.d.val))347        * (((children s P).map fun z => (stateVolume z.2).eval ((q:ℚ)^z.1)).prod)348      / (stateVolume s).eval q = (divisorProbability s P.d.val).eval q := by349  have h2 : (2:ℚ) ≤ q := by exact_mod_cast hq350  have hq0 : (q:ℚ) ≠ 0 := by linarith351  have hq1 : (q:ℚ) - 1 ≠ 0 := by linarith352  have hq1' : -1 + (q:ℚ) ≠ 0 := by linarith353  have hq1'' : (q:ℚ) + -1 ≠ 0 := by linarith354  obtain ⟨hd0, hsum, hP⟩ := hP355  cases s with356  | single a c =>357    obtain ⟨hdc, hrx, hrt⟩ := hP358    simp only [children, List.map_append, List.prod_append]359    rw [otherChildren_volume_prod]360    simp only [stateVolume, divisorProbability, Expr.eval, expr_eval_pow, eminusOne, Expr.sub,361      Expr.neg]362    by_cases h0 : P.rt.val = 0363    · have hdc' : ¬ P.d.val < c := fun h => by have := hrt.2 h; omega364      have hc : c = P.d.val := by omega365      have hw : patternWeight P.other = P.d.val := by omega366      simp only [h0, if_true, hdc', if_false, List.map_nil, List.prod_nil, hw, inv_pow]367      rw [show (q:ℚ)^c = (q:ℚ)^P.d.val from congrArg _ hc]368      field_simp369    · have hdc' : P.d.val < c := hrt.1 (by omega)370      have hc : (q:ℚ)^c = (q:ℚ)^(P.rt.val + (c - P.d.val)) * (q:ℚ)^(patternWeight P.other) := by371        rw [← pow_add]; congr 1; omega372      simp only [h0, if_false, hdc', if_true, List.map_cons, List.map_nil, List.prod_cons,373        List.prod_nil, Expr.eval, expr_eval_pow, hc, pow_one, inv_pow]374      field_simp375  | crossing a b c h =>376    obtain ⟨hdc, hdh, hrt, hrx⟩ := hP377    simp only [children, List.map_append, List.prod_append]378    rw [otherChildren_volume_prod]379    simp only [stateVolume, divisorProbability, Expr.eval, expr_eval_pow, eminusOne, Expr.sub,380      Expr.neg]381    have htri : tri P.d.val = chooseTwo P.d.val + P.d.val := by382      unfold tri chooseTwo383      obtain ⟨n, hn⟩ : ∃ n, P.d.val = n+1 := ⟨_, (Nat.succ_pred_eq_of_pos hd0).symm⟩384      rw [hn, Nat.add_sub_cancel, show (n+1)*(n+1+1) = (n+1)*n + (n+1)*2 by ring,385        Nat.add_mul_div_right _ _ two_pos]386    have hch : (q:ℚ)^(c+h) = (q:ℚ)^(P.rt.val + (c - P.d.val)) * (q:ℚ)^(P.rx.val + (h - P.d.val))387        * (q:ℚ)^(patternWeight P.other) * (q:ℚ)^P.d.val := by388      rw [← pow_add, ← pow_add, ← pow_add]; congr 1; omega389    rw [htri, hch]390    have hc' : P.d.val < c ↔ P.rt.val ≠ 0 := ⟨fun h => by have := hrt.2 h; omega, hrt.1 ∘ by omega⟩391    have hh' : P.d.val < h ↔ P.rx.val ≠ 0 := ⟨fun h => by have := hrx.2 h; omega, hrx.1 ∘ by omega⟩392    have e1 : P.rt.val = 0 → c - P.d.val = 0 := fun h => by have := hrt.2; omega393    have e2 : P.rx.val = 0 → h - P.d.val = 0 := fun h => by have := hrx.2; omega394    by_cases h0 : P.rt.val = 0 <;> by_cases h1 : P.rx.val = 0 <;>395    · simp only [h0, h1, hc', hh', e1, e2, ne_eq, not_true_eq_false, not_false_eq_true, if_true,396        if_false, List.map_nil, List.prod_nil, Expr.eval, inv_pow, List.map_cons, List.prod_cons,397        expr_eval_pow]398      norm_num [Expr.eval, expr_eval_pow, pow_add]399      field_simp400 401/-! ### Counting coloured maps -/402 403private theorem card_fiber_succ {r n : ℕ} (f : Fin (n + 1) → Option (Fin r)) (y : Option (Fin r)) :404    Nat.card {x : Fin (n+1) // f x = y} =405      Nat.card {x : Fin n // f x.succ = y} + if f 0 = y then 1 else 0 := by406  simp only [Nat.card_eq_fintype_card, Fintype.card_subtype, Finset.card_filter, Fin.sum_univ_succ]407  ring408 409/-- The number of maps `Fin n → Option (Fin r)` with exactly `m i` points coloured `i`. -/410private noncomputable def coloredCount (r n : ℕ) (m : Fin r → ℕ) : ℕ :=411  Nat.card {f : Fin n → Option (Fin r) // ∀ i : Fin r, Nat.card {x : Fin n // f x = some i} = m i}412 413private theorem coloredCount_succ (r n : ℕ) (m : Fin r → ℕ) :414    coloredCount r (n+1) m = ∑ c : Option (Fin r), Nat.card {g : Fin n → Option (Fin r) //415      ∀ i : Fin r, Nat.card {x : Fin n // g x = some i} + (if c = some i then 1 else 0) = m i} := by416  unfold coloredCount417  rw [Nat.card_congr (Equiv.sigmaFiberEquiv418    (fun f : {f : Fin (n+1) → Option (Fin r) // ∀ i : Fin r,419      Nat.card {x : Fin (n+1) // f x = some i} = m i} => f.1 0)).symm, Nat.card_sigma]420  refine Finset.sum_congr rfl fun c _ => Nat.card_congr421    { toFun := fun p => ⟨Fin.tail p.1.1, fun i => by rw [← p.1.2 i, card_fiber_succ, p.2]; rfl⟩422      invFun := fun g => ⟨⟨Fin.cons c g.1, fun i => by rw [← g.2 i, card_fiber_succ]; simp⟩,423        by simp⟩424      left_inv := fun ⟨⟨f, hf⟩, hc⟩ => by subst hc; simp [Fin.cons_self_tail]425      right_inv := fun g => by simp }426 427private theorem coloredCount_term (r n : ℕ) (m : Fin r → ℕ) (i : Fin r) :428    Nat.card {g : Fin n → Option (Fin r) //429      ∀ j : Fin r, Nat.card {x : Fin n // g x = some j} + (if some i = some j then 1 else 0) = m j}430      = if m i = 0 then 0 else coloredCount r n (Function.update m i (m i - 1)) := by431  split_ifs with h432  · rw [Nat.card_eq_zero]; left433    constructor; rintro ⟨g, hg⟩434    have := hg i; simp at this; omega435  · refine Nat.card_congr (Equiv.subtypeEquivRight fun g => forall_congr' fun j => ?_)436    by_cases hj : j = i437    · subst hj; simp; omega438    · simp [Ne.symm hj, hj]439 440private theorem descFactorial_succ_left (n M : ℕ) :441    (n+1).descFactorial M = n.descFactorial M + M * n.descFactorial (M-1) := by442  cases M with443  | zero => simp444  | succ k =>445    rw [Nat.succ_descFactorial_succ, Nat.descFactorial_succ, Nat.add_sub_cancel]446    by_cases hk : k ≤ n447    · rw [show n + 1 = (n - k) + (k + 1) by omega, add_mul]448    · simp [Nat.descFactorial_eq_zero_iff_lt.mpr (show n < k by omega)]449 450private theorem coloredCount_eq (r n : ℕ) : ∀ m : Fin r → ℕ,451    (coloredCount r n m : ℚ) = (n.descFactorial (∑ i, m i) : ℚ) / ∏ i, ((m i).factorial : ℚ) := by452  induction n with453  | zero =>454    intro m455    by_cases h : ∀ i, m i = 0456    · have hP : ∀ f : Fin 0 → Option (Fin r),457          ∀ i : Fin r, Nat.card {x : Fin 0 // f x = some i} = m i := by458        intro f i; simp [h]459      unfold coloredCount460      rw [Nat.card_congr (Equiv.subtypeUnivEquiv hP)]461      simp [h]462    · push Not at h463      obtain ⟨i, hi⟩ := h464      have hC : coloredCount r 0 m = 0 := by465        unfold coloredCount466        rw [Nat.card_eq_zero]; left467        constructor; rintro ⟨g, hg⟩468        have := hg i; simp at this; omega469      have hle : m i ≤ ∑ j, m j :=470        Finset.single_le_sum (fun j _ => Nat.zero_le _) (Finset.mem_univ i)471      rw [hC, Nat.descFactorial_eq_zero_iff_lt.mpr (show 0 < ∑ j, m j by omega)]; simp472  | succ n ih =>473    intro m474    have hnone : Nat.card {g : Fin n → Option (Fin r) // ∀ i, Nat.card {x : Fin n // g x = some i}475        + (if (none : Option (Fin r)) = some i then 1 else 0) = m i} = coloredCount r n m := by476      simp [coloredCount]477    have key : ∀ i, ((if m i = 0 then 0 else coloredCount r n (Function.update m i (m i - 1)) : ℕ)478        : ℚ) = (m i : ℚ) * n.descFactorial (∑ j, m j - 1) / ∏ j, ((m j).factorial : ℚ) := by479      intro i480      split_ifs with h481      · simp [h]482      rw [ih]483      have hs : ∑ j, Function.update m i (m i - 1) j = ∑ j, m j - 1 := by484        rw [Finset.sum_update_of_mem (Finset.mem_univ _), Finset.sdiff_singleton_eq_erase,485          ← Finset.add_sum_erase _ _ (Finset.mem_univ i)]486        omega487      have hp : (∏ j, ((Function.update m i (m i - 1) j).factorial : ℚ)) * m i488          = ∏ j, ((m j).factorial : ℚ) := by489        rw [← Finset.mul_prod_erase _ _ (Finset.mem_univ i),490          ← Finset.mul_prod_erase _ (fun j => ((m j).factorial : ℚ)) (Finset.mem_univ i),491          Finset.prod_congr rfl (fun j hj => by492            rw [Function.update_of_ne (Finset.ne_of_mem_erase hj)])]493        simp only [Function.update_self]494        rw [← Nat.mul_factorial_pred h]; push_cast; ring495      have hmi : (m i : ℚ) ≠ 0 := by exact_mod_cast h496      rw [hs, ← hp]497      have : (∏ j, ((Function.update m i (m i - 1) j).factorial : ℚ)) ≠ 0 :=498        Finset.prod_ne_zero_iff.mpr fun j _ => by positivity499      field_simp500    rw [coloredCount_succ, Fintype.sum_option, hnone]501    simp only [coloredCount_term]502    rw [Nat.cast_add, Nat.cast_sum, ih]503    simp only [key]504    rw [← Finset.sum_div, ← Finset.sum_mul, ← Nat.cast_sum, descFactorial_succ_left]505    push_cast; ring506 507private theorem prod_range_sub_eq_descFactorial (Q M : ℕ) :508    ((List.range M).map fun j => (Q:ℚ)-j).prod = (Q.descFactorial M : ℚ) := by509  induction M with510  | zero => simp511  | succ k ih =>512    simp only [List.range_succ, List.pure_def, List.bind_eq_flatMap, List.flatMap_append,513      List.flatMap_cons, List.flatMap_nil, List.append_nil, List.map_append, List.map_cons,514      List.map_nil, List.prod_append, List.prod_cons, List.prod_nil, mul_one,515      Nat.descFactorial_succ, Nat.cast_mul] at ih ⊢516    rw [ih]517    by_cases hk : k ≤ Q518    · rw [Nat.cast_sub hk]; ring519    · simp [Nat.descFactorial_eq_zero_iff_lt.mpr (show Q < k by omega)]520 521/-- The number of maps `Fin Q → Option (Fin r)` with exactly `m i` points of colour `i` is522`Q (Q-1) ⋯ (Q - ∑ m + 1) / ∏ (m i)!`. -/523theorem colored_subset_count (Q r : ℕ) (m : Fin r → ℕ) :524    ((Nat.card {f : Fin Q→Option (Fin r) //525      ∀ i : Fin r, Nat.card {x : Fin Q // f x=some i}=m i} : ℕ) : ℚ) =526      ((List.range (∑ i : Fin r, m i)).map fun j => (Q:ℚ)-j).prod527        / ∏ i : Fin r, (Nat.factorial (m i):ℚ) := by528  rw [prod_range_sub_eq_descFactorial]529  exact coloredCount_eq r Q m530 531/-! ### Assorted coordinate lemmas -/532 533/-- If each component `e j` divides a power of `π` up to `d`-th powers, then a single exponent534`s ≥ s₀` works for all components of the finite product simultaneously. -/535theorem common_vertical_exponent (O : Type) [CommRing O] (ι : Type) [Finite ι] (C : ι → Type)536    [∀ j, CommRing (C j)] [∀ j, Algebra O (C j)] (pi : O) (e : ∀ j, C j) (d : ℕ)537    (hvert : ∀ j, ∃ (s : ℕ) (cj : C j), algebraMap O (C j) pi ^ s = e j ^ d * cj) (s₀ : ℕ) :538    ∃ (s : ℕ) (cc : ∀ j, C j), s₀ ≤ s ∧ (algebraMap O (∀ j, C j) pi) ^ s = e ^ d * cc := by539  have := Fintype.ofFinite ι540  choose sj cj h using hvert541  refine ⟨s₀ + ∑ i, sj i, fun j => cj j * algebraMap O (C j) pi ^ (s₀ + ∑ i, sj i - sj j),542    Nat.le_add_right _ _, funext fun j => ?_⟩543  have : sj j ≤ s₀ + ∑ i, sj i :=544    (Finset.single_le_sum (fun i _ => Nat.zero_le (sj i)) (Finset.mem_univ j)).trans545      (Nat.le_add_left _ _)546  simp only [Pi.algebraMap_apply, Pi.pow_apply, Pi.mul_apply]547  conv_lhs => rw [← Nat.add_sub_cancel' this, pow_add, h j]548  rw [mul_assoc]549 550/-- A surjection preserving and reflecting all adic congruences is measurable for the adic551cylinder σ-algebra. -/552theorem congruence_bijection_measurable (O V : Type) [CommRing O] [AddCommGroup V] [Module O V]553    (I : Ideal O) [MeasurableSpace V] (hgen : ‹MeasurableSpace V› = adicCylinderSpace I V)554    (F : V → V) (honto : Function.Surjective F)555    (hcong : ∀ j x y, adicCongr I j (F x) (F y) ↔ adicCongr I j x y) :556    Measurable F := by557  rw [hgen]558  let _ : MeasurableSpace V := adicCylinderSpace I V559  refine measurable_generateFrom fun s hs => ?_560  rcases hs with rfl | ⟨j, a, rfl⟩561  · simp562  · obtain ⟨b, rfl⟩ := honto a563    have : F ⁻¹' {y | adicCongr I j y (F b)} = {y | adicCongr I j y b} := by564      ext y; simp [hcong]565    exact this ▸ MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, b, rfl⟩)566 567/-- Over a finite field `k`, the number of `f : ι → k` vanishing on `A` and nonvanishing on a568disjoint `B` is `(|k| - 1)^|B| · |k|^(|ι| - |A| - |B|)`. -/569theorem coordinate_constraint_count (k ι : Type) [Field k] [Fintype k] [Fintype ι]570    (A B : Finset ι) (hAB : Disjoint A B) :571    Nat.card {f : ι→k // (∀ i∈A, f i=0) ∧ (∀ i∈B, f i≠0)}572      = (Fintype.card k-1)^B.card * (Fintype.card k)^(Fintype.card ι-A.card-B.card) := by573  classical574  let S : ι → Finset k := fun i =>575    if i ∈ A then {0} else if i ∈ B then Finset.univ.erase 0 else Finset.univ576  have hset : (Finset.univ.filter577      (fun f : ι → k => (∀ i∈A, f i=0) ∧ (∀ i∈B, f i≠0))) = Fintype.piFinset S := by578    ext f579    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Fintype.mem_piFinset, S]580    constructor581    · rintro ⟨h1, h2⟩ i582      by_cases hA : i ∈ A583      · simp [hA, h1 i hA]584      · by_cases hB : i ∈ B585        · simp [hA, hB, h2 i hB]586        · simp [hA, hB]587    · intro h588      refine ⟨fun i hi => by simpa [hi] using h i, fun i hi => ?_⟩589      simpa [Finset.disjoint_right.mp hAB hi, hi] using h i590  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, hset, Fintype.card_piFinset]591  have hcard : ∀ i, (S i).card =592      if i ∈ A then 1 else if i ∈ B then Fintype.card k - 1 else Fintype.card k := by593    intro i594    by_cases hA : i ∈ A595    · simp [S, hA]596    · by_cases hB : i ∈ B <;> simp [S, hA, hB, Finset.card_erase_of_mem]597  simp only [hcard]598  rw [Finset.prod_ite, Finset.prod_const_one, one_mul, Finset.prod_ite,599    Finset.prod_const, Finset.prod_const, Finset.filter_filter, Finset.filter_filter]600  have h1 : Finset.univ.filter (fun i => i ∉ A ∧ i ∈ B) = B := by601    ext i602    simpa using fun h => Finset.disjoint_right.mp hAB h603  have h2 : Finset.univ.filter (fun i => i ∉ A ∧ i ∉ B) = (A ∪ B)ᶜ := by604    ext i; simp605  rw [h1, h2, Finset.card_compl, Finset.card_union_of_disjoint hAB, Nat.sub_sub]606 607/-- The curve ideal `(f + π ∑ zᵢ bᵢ)` lies in the residue cell of `f`. -/608theorem coordinate_ideal_in_residue_cell (O R : Type) [CommRing O] [CommRing R] [Algebra O R]609    (n : ℕ) (pi : O) (b : Fin n → R) (f : R) (z : Fin n → O) :610    coordinateIdeal pi f b z ∈ residueIdealCell (algebraMap O R pi) f := by611  refine ⟨⟨_, rfl⟩, ?_⟩612  unfold coordinateIdeal normalizedIdeal613  rw [Ideal.map_span, Set.image_singleton]614  congr 2615  rw [normalizedGenerator, map_add, add_eq_left, Ideal.Quotient.eq_zero_iff_mem,616    coordinateLift_smul_eq_mul]617  exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)618 619/-- For a free module `V ≅ O^n` over a DVR with uniformizer `π`, multiplication by `π` is620injective and `V / πV` has length `n`. -/621theorem coordinate_module_pi_quotient_length (O : Type) [CommRing O] [IsDomain O]622    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (pi : O)623    (hpi : Irreducible pi) (n : ℕ) (V : Type) [AddCommGroup V] [Module O V]624    (EV : V ≃ₗ[O] (Fin n → O)) :625    Function.Injective (fun v : V => pi • v) ∧626      Module.length O (V ⧸ LinearMap.range (pi • (LinearMap.id : V →ₗ[O] V))) = (n : ℕ∞) := by627  refine ⟨fun v w h => EV.injective <| funext fun i => mul_left_cancel₀ hpi.ne_zero ?_, ?_⟩628  · simpa using congrArg (fun x => EV x i) h629  set I : Ideal O := Ideal.span {pi} with hI630  have hsimple : IsSimpleModule O (O ⧸ I) := by631    have hImax : I.IsMaximal := by632      rw [hI, hpi.maximalIdeal_eq.symm]; exact IsLocalRing.maximalIdeal.isMaximal O633    rw [Ideal.isMaximal_def] at hImax634    exact isSimpleModule_iff_isCoatom.mpr hImax635  let f : V →ₗ[O] (Fin n → O ⧸ I) :=636    LinearMap.pi (fun i => I.mkQ ∘ₗ LinearMap.proj i ∘ₗ EV.toLinearMap)637  have hsurj : Function.Surjective f := by638    intro y639    choose x hx using fun i => Ideal.Quotient.mk_surjective (y i)640    exact ⟨EV.symm x, funext fun i => by simp [f, hx]⟩641  have hker : LinearMap.ker f = LinearMap.range (pi • (LinearMap.id : V →ₗ[O] V)) := by642    ext v643    simp only [LinearMap.mem_ker, LinearMap.mem_range, f]644    constructor645    · intro h646      have h' : ∀ i, EV v i ∈ I := fun i => by647        simpa [Ideal.Quotient.eq_zero_iff_mem] using congrFun h i648      choose y hy using fun i => Ideal.mem_span_singleton'.mp (h' i)649      exact ⟨EV.symm y, EV.injective <| funext fun i => by simp [← hy i, mul_comm]⟩650    · rintro ⟨w, rfl⟩651      funext i652      simp only [LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe,653        LinearMap.smul_apply, LinearMap.id_apply, map_smul, LinearMap.coe_proj,654        Function.eval, Submodule.mkQ_apply, Pi.zero_apply]655      rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero, hI, smul_eq_mul]656      exact Ideal.mem_span_singleton'.mpr ⟨EV w i, mul_comm _ _⟩657  let e := (Submodule.quotEquivOfEq _ _ hker).symm.trans (f.quotKerEquivOfSurjective hsurj)658  rw [e.length_eq, Module.length_pi, Module.length_eq_one]659  simp660 661/-- The coordinate remainder `(z, v) ↦ π • E (v ∑ zᵢ bᵢ)` raises `π`-adic order. -/662theorem coordinate_remainder_raises_order (O R : Type) [CommRing O] [CommRing R] [Algebra O R]663    (n : ℕ) (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R)) :664    RaisesAdicOrder (Ideal.span {pi}) (coordinateRemainder pi b E) := by665  set I : Ideal O := Ideal.span {pi}666  have key : ∀ (j : ℕ) {M N : Type} [AddCommGroup M] [Module O M] [AddCommGroup N] [Module O N]667      (f : M →ₗ[O] N) (x : M), x ∈ (I ^ j • ⊤ : Submodule O M) →668        f x ∈ (I ^ j • ⊤ : Submodule O N) := by669    intro j M N _ _ _ _ f x hx670    have hle : (I ^ j • ⊤ : Submodule O M) ≤ (I ^ j • ⊤ : Submodule O N).comap f := by671      rw [Submodule.smul_le]672      intro r hr m _673      simpa using Submodule.smul_mem_smul hr Submodule.mem_top674    exact hle hx675  intro j x y hxy676  unfold adicCongr at hxy ⊢677  have h2 : x.2 - y.2 ∈ (I ^ j • ⊤ : Submodule O R) := by678    simpa using key j (LinearMap.snd O (Fin n → O) R) _ hxy679  have hL : coordinateLift b x.1 - coordinateLift b y.1 ∈ (I ^ j • ⊤ : Submodule O R) := by680    simpa [coordinateLift, Fintype.linearCombination_apply, sub_smul, Finset.sum_sub_distrib]681      using key j ((Fintype.linearCombination O b).comp (LinearMap.fst O (Fin n → O) R)) _ hxy682  have hprod : x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1683      ∈ (I ^ j • ⊤ : Submodule O R) := by684    rw [show x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1685        = x.2 * (coordinateLift b x.1 - coordinateLift b y.1)686          + (x.2 - y.2) * coordinateLift b y.1 by ring]687    exact Submodule.add_mem _ (key j (LinearMap.mulLeft O x.2) _ hL)688      (key j (LinearMap.mulRight O (coordinateLift b y.1)) _ h2)689  have hE := key j E.toLinearMap _ hprod690  simp only [LinearEquiv.coe_coe, map_sub] at hE691  unfold coordinateRemainder692  rw [← smul_sub, pow_succ', Submodule.mul_smul]693  exact Submodule.smul_mem_smul (Ideal.mem_span_singleton_self pi) hE694 695/-! ### Rank of a division chart -/696 697private theorem card_quot_eq_of_surjective (R M : Type) [CommRing R] [AddCommGroup M] (J : Ideal R)698    (φ : R →+ M) (hφ : Function.Surjective φ) (hker : ∀ r, φ r = 0 ↔ r ∈ J) :699    Nat.card (R ⧸ J) = Nat.card M := by700  have hs := Ideal.Quotient.mk_surjective (I := J)701  let s := Function.surjInv hs702  have hmk : ∀ x, Ideal.Quotient.mk J (s x) = x := Function.surjInv_eq hs703  refine Nat.card_congr (Equiv.ofBijective (fun x => φ (s x)) ⟨fun x y hxy => ?_, fun m => ?_⟩)704  · rwa [← hmk x, ← hmk y, Ideal.Quotient.eq, ← hker, map_sub, sub_eq_zero]705  · obtain ⟨r, rfl⟩ := hφ m706    have h1 : Ideal.Quotient.mk J (s (Ideal.Quotient.mk J r)) = Ideal.Quotient.mk J r := hmk _707    rw [Ideal.Quotient.eq, ← hker, map_sub, sub_eq_zero] at h1708    exact ⟨Ideal.Quotient.mk J r, h1⟩709 710private theorem card_quot_divisionChart (O R : Type) [CommRing O] [IsDomain O]711    [IsDiscreteValuationRing O] [CommRing R] [Algebra O R] (pi : O) (hpi : Irreducible pi) (n : ℕ)712    (f : R) (b : Fin n → R) (hb : IsDivisionChart O R pi f b) :713    Nat.card (R ⧸ Ideal.comap (Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}))714      (Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f})) =715      Nat.card (Fin n → IsLocalRing.ResidueField O) := by716  obtain ⟨E, hE⟩ := hb.1717  have hmax : IsLocalRing.maximalIdeal O = Ideal.span {pi} := hpi.maximalIdeal_eq718  let φ : R →+ (Fin n → IsLocalRing.ResidueField O) :=719    { toFun := fun r i => IsLocalRing.residue O ((E r).1 i)720      map_zero' := by ext i; simp721      map_add' := by intro x y; ext i; simp }722  apply card_quot_eq_of_surjective R _ _ φ723  · intro m724    choose z hz using fun i => IsLocalRing.residue_surjective (R := O) (m i)725    exact ⟨E.symm (z, 0), by ext i; simp [φ, hz]⟩726  · intro r727    have hEf : ∀ a : R, E (f * a) = (0, a) := fun a => E.symm.injective <| by728      rw [E.symm_apply_apply, hE]729      simp [divisionMap, coordinateLift]730    constructor731    · intro h732      have hi : ∀ i, ∃ y, pi * y = (E r).1 i := fun i ↦ by733        have : IsLocalRing.residue O ((E r).1 i) = 0 := congrFun h i734        rw [IsLocalRing.residue_eq_zero_iff, hmax, Ideal.mem_span_singleton'] at this735        obtain ⟨y, hy⟩ := this736        exact ⟨y, by rw [← hy, mul_comm]⟩737      choose z hz using hi738      have hr : r = algebraMap O R pi * coordinateLift b z + f * (E r).2 := by739        have := hE (E r)740        rw [E.symm_apply_apply] at this741        refine this.trans ?_742        rw [divisionMap, ← coordinateLift_smul_eq_mul]743        congr 2; ext i; exact (hz i).symm744      rw [Ideal.mem_comap, Ideal.mem_span_singleton']745      refine ⟨Ideal.Quotient.mk _ (E r).2, ?_⟩746      rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton']747      exact ⟨-coordinateLift b z, by linear_combination hr⟩748    · intro h749      obtain ⟨a, ha⟩ := Ideal.mem_span_singleton'.1 (Ideal.mem_comap.1 h)750      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a751      rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at ha752      obtain ⟨t, ht⟩ := ha753      have hr : r = f * a + pi • (-t) := by754        rw [Algebra.smul_def]; linear_combination ht755      ext i756      simp only [φ, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.zero_apply]757      rw [hr, map_add, map_smul, hEf]758      simp only [Prod.fst_add, Prod.smul_fst, Pi.add_apply, Pi.smul_apply, Pi.zero_apply,759        zero_add, smul_eq_mul]760      rw [IsLocalRing.residue_eq_zero_iff, hmax]761      exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)762 763/-- Two division charts whose centres generate the same ideal modulo `π` have the same rank. -/764theorem division_chart_rank_eq_of_residue_ideal_eq (O R : Type) [CommRing O] [IsDomain O]765    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] [CommRing R] [Algebra O R]766    (pi : O) (hpi : Irreducible pi) (n n' : ℕ) (f g : R) (b : Fin n → R) (c : Fin n' → R)767    (hb : IsDivisionChart O R pi f b) (hc : IsDivisionChart O R pi g c)768    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =769      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :770    n = n' := by771  have h1 := card_quot_divisionChart O R pi hpi n f b hb772  rw [hres, card_quot_divisionChart O R pi hpi n' g c hc] at h1773  have := Fintype.ofFinite (IsLocalRing.ResidueField O)774  simp only [Nat.card_pi, Finset.prod_const, Finset.card_univ, Fintype.card_fin] at h1775  exact (Nat.pow_right_injective (Finite.one_lt_card_iff_nontrivial.mpr inferInstance) h1).symm776 777/-! ### Division coordinates -/778 779/-- If `b` lifts an `O`-basis of `R/(f)` and `f` is a nonzerodivisor, the division map780`(z, v) ↦ ∑ zᵢ bᵢ + f v` is injective. -/781private theorem division_coordinates_injective (O R : Type) [CommRing O] [CommRing R] [Algebra O R]782    (n : ℕ)783    (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)784    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) [IsDomain R] (hf : f ≠ 0) :785    Function.Injective (divisionMap (O := O) f b) := by786  have key : ∀ z : Fin n → O,787      Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z) = ∑ i, z i • B i := by788    intro z789    rw [← Ideal.Quotient.mkₐ_eq_mk O, coordinateLift, map_sum]790    refine Finset.sum_congr rfl fun i _ => ?_791    rw [map_smul, Ideal.Quotient.mkₐ_eq_mk, hb]792  rintro ⟨z, v⟩ ⟨z', v'⟩ h793  simp only [divisionMap] at h794  have hq := congrArg (Ideal.Quotient.mk (Ideal.span {f})) h795  have hf0 : Ideal.Quotient.mk (Ideal.span {f}) f = 0 :=796    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self f)797  simp only [map_add, map_mul, hf0, zero_mul, add_zero, key] at hq798  obtain rfl : z = z' := funext fun i => by799    simpa [Finsupp.finsetSum_apply, Finsupp.single_apply] using congrArg (fun x => B.repr x i) hq800  rw [mul_left_cancel₀ hf (add_left_cancel h)]801 802/-- If `b` lifts an `O`-basis of `R/(f)`, the division map `(z, v) ↦ ∑ zᵢ bᵢ + f v` is803surjective. -/804private theorem division_coordinates_surjective (O R : Type) [CommRing O] [CommRing R] [Algebra O R]805    (n : ℕ) (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)806    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) :807    Function.Surjective (divisionMap (O := O) f b) := by808  intro h809  set z : Fin n → O := fun i => B.repr (Ideal.Quotient.mk (Ideal.span {f}) h) i810  have hz : Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z)811      = Ideal.Quotient.mk (Ideal.span {f}) h := by812    unfold coordinateLift813    rw [map_sum]814    conv_rhs => rw [← B.sum_repr (Ideal.Quotient.mk (Ideal.span {f}) h)]815    refine Finset.sum_congr rfl fun i _ => ?_816    rw [Algebra.smul_def, map_mul, hb i, Algebra.smul_def]817    rfl818  obtain ⟨v, hv⟩ := Ideal.mem_span_singleton'.mp (Ideal.Quotient.eq.1 hz.symm)819  exact ⟨(z, v), by simp only [divisionMap]; rw [mul_comm, hv]; ring⟩820 821/-- Recentring: if the regular element `f` and the chart centre `g` (with division equivalence822`Ec`) generate the same ideal modulo `π`, then the chart can be rescaled by a unit so that its new823centre `g'` satisfies `f = g' + π h₀`, with the same curve ideals. -/824theorem division_data_same_cell_recenter (O R : Type) [CommRing O] [CommRing R] [Algebra O R]825    [IsLocalRing R] (pi : O) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n : ℕ)826    (f g : R) (c : Fin n → R)827    (hf : Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>828      y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))829    (Ec : R ≃ₗ[O] ((Fin n → O) × R)) (hEc : ∀ s, Ec.symm s = divisionMap g c s)830    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =831      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :832    ∃ (g' : R) (c' : Fin n → R) (F : R ≃ₗ[O] ((Fin n → O) × R)) (h₀ : R),833      (∀ s, F.symm s = divisionMap g' c' s) ∧ f = g' + pi • h₀ ∧834      Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>835        y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g') ∧836      ∀ z : Fin n → O, coordinateIdeal pi g c z = coordinateIdeal pi g' c' z := by837  set I : Ideal R := Ideal.span {algebraMap O R pi} with hI838  set mk := Ideal.Quotient.mk I839  have hIm : I ≤ IsLocalRing.maximalIdeal R := by840    rw [hI, Ideal.span_le]; simpa using hpm841  obtain ⟨a, ha⟩ := Ideal.mem_span_singleton'.1 (hres ▸ Ideal.mem_span_singleton_self (mk g))842  obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 (hres ▸ Ideal.mem_span_singleton_self (mk f))843  have hba : b * a = 1 := hf <| by simp only; rw [one_mul, mul_assoc, ha, hb]844  obtain ⟨a', rfl⟩ := Ideal.Quotient.mk_surjective a845  obtain ⟨b', rfl⟩ := Ideal.Quotient.mk_surjective b846  have hunit : IsUnit a' := by847    by_contra hna848    have h2 : b' * a' - 1 ∈ I := by849      rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_one]850      exact sub_eq_zero.2 hba851    have := (IsLocalRing.maximalIdeal R).sub_mem ((IsLocalRing.maximalIdeal R).mul_mem_left b'852      ((IsLocalRing.mem_maximalIdeal _).2 hna)) (hIm h2)853    simp at this854  obtain ⟨u, rfl⟩ := hunit855  -- multiplication by `u` as an `O`-linear equivalence856  let M : R ≃ₗ[O] R :=857    { toFun := fun x => (u : R) * x858      invFun := fun x => ((u⁻¹ : Rˣ) : R) * x859      map_add' := fun x y => mul_add _ _ _860      map_smul' := fun r x => by simp [Algebra.mul_smul_comm]861      left_inv := fun x => Units.inv_mul_cancel_left u x862      right_inv := fun x => Units.mul_inv_cancel_left u x }863  have hlift : ∀ (w : R) (z : Fin n → O),864      w * coordinateLift c z = coordinateLift (fun i => w * c i) z := by865    intro w z866    simp only [coordinateLift, Finset.mul_sum, mul_smul_comm]867  have hg' : mk (((u⁻¹ : Rˣ) : R) * g) = mk f := by868    rw [map_mul, ← ha, ← mul_assoc, ← map_mul, Units.inv_mul, map_one, one_mul]869  obtain ⟨h, hh⟩ := Ideal.mem_span_singleton'.1 (Ideal.Quotient.eq.1 hg')870  refine ⟨((u⁻¹ : Rˣ) : R) * g, fun i => ((u⁻¹ : Rˣ) : R) * c i, M.trans Ec, -h, fun s => ?_, ?_,871    ?_, fun z => ?_⟩872  · rw [LinearEquiv.trans_symm, LinearEquiv.trans_apply, hEc]873    change ((u⁻¹ : Rˣ) : R) * divisionMap g c s = _874    simp only [divisionMap, mul_add, hlift, mul_assoc]875  · rw [smul_neg, Algebra.smul_def, mul_comm (algebraMap O R pi), hh]; ring876  · simpa only [show mk (((u⁻¹ : Rˣ) : R) * g) = mk f from hg'] using hf877  · simp only [coordinateIdeal, normalizedIdeal, normalizedGenerator]878    rw [← hlift, ← mul_add, Ideal.span_singleton_mul_left_unit (Units.isUnit _)]879 880/-- Recentring for two division charts of the same rank whose centres generate the same ideal881modulo `π` (see `division_data_same_cell_recenter`). -/882theorem division_chart_same_cell_recenter (O R : Type) [CommRing O] [CommRing R] [Algebra O R]883    [IsLocalRing R] (pi : O) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n : ℕ)884    (f g : R) (b c : Fin n → R) (hb : IsDivisionChart O R pi f b) (hc : IsDivisionChart O R pi g c)885    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =886      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :887    ∃ (g' : R) (c' : Fin n → R) (F : R ≃ₗ[O] ((Fin n → O) × R)) (h₀ : R),888      (∀ s, F.symm s = divisionMap g' c' s) ∧ f = g' + pi • h₀ ∧889      Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>890        y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g') ∧891      ∀ z : Fin n → O, coordinateIdeal pi g c z = coordinateIdeal pi g' c' z :=892  let ⟨Ec, hEc⟩ := hc.1893  division_data_same_cell_recenter O R pi hpm n f g c hb.2 Ec hEc hres894 895/-- If `b` lifts an `O`-basis of `R/(f)` with `f ≠ 0` in a domain, the division map is the896inverse of an `O`-linear equivalence `R ≃ O^n × R`. -/897theorem division_linear_equivalence (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)Lemma 3.1898    (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)899    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) [IsDomain R] (hf : f ≠ 0) :900    ∃ E : R ≃ₗ[O] ((Fin n → O) × R), ∀ s, E.symm s = divisionMap f b s := by901  let L : ((Fin n → O) × R) →ₗ[O] R :=902    { toFun := divisionMap f b903      map_add' := by904        intro x y905        simp only [divisionMap, coordinateLift, Prod.fst_add, Prod.snd_add, Pi.add_apply,906          add_smul, Finset.sum_add_distrib, mul_add]907        ring908      map_smul' := by909        intro c x910        simp only [divisionMap, coordinateLift, Prod.smul_fst, Prod.smul_snd, Pi.smul_apply,911          smul_eq_mul, RingHom.id_apply, smul_add, Finset.smul_sum, mul_smul]912        rw [mul_smul_comm] }913  exact ⟨(LinearEquiv.ofBijective L ⟨division_coordinates_injective O R n f B b hb hf,914    division_coordinates_surjective O R n f B b hb⟩).symm, fun _ => rfl⟩915 916/-! ### Finite coordinate spaces -/917 918/-- On `O^n`, `x ≡ y (mod I^j)` holds iff it holds coordinatewise. -/919theorem finite_coordinate_adic_congruence (O : Type) [CommRing O] (n : ℕ) (I : Ideal O) (j : ℕ)920    (x y : Fin n → O) :921    adicCongr I j x y ↔ ∀ i, x i - y i ∈ I^j := by922  unfold adicCongr923  constructor924  · intro h925    have : ∀ i, (x - y) i ∈ I ^ j :=926      Submodule.smul_induction_on h927        (fun r hr m _ i => by simpa using Ideal.mul_mem_right (m i) _ hr)928        (fun a b ha hb i => by simpa using Ideal.add_mem _ (ha i) (hb i))929    simpa using this930  · intro h931    have hv : x - y = ∑ i, (x i - y i) • (Pi.single i 1 : Fin n → O) := by932      funext k933      simp [Finset.sum_apply, Pi.single_apply]934    rw [hv]935    exact Submodule.sum_mem _ fun i _ => Submodule.smul_mem_smul (h i) Submodule.mem_top936 937/-- For the `I`-adic topology on `O`, the adic cylinders form a basis of the product topology938of `O^n`. -/939theorem finite_coordinate_cylinder_basis (O : Type) [CommRing O] [TopologicalSpace O]940    [IsTopologicalRing O] (I : Ideal O) (htop : IsAdic I) (n : ℕ) :941    TopologicalSpace.IsTopologicalBasis (adicCylinders I (Fin n → O)) := by942  have hball : ∀ (j : ℕ) (x : Fin n → O),943      {y : Fin n → O | adicCongr I j y x} = {y | ∀ i, y i - x i ∈ I ^ j} := fun j x =>944    Set.ext fun y => finite_coordinate_adic_congruence O n I j y x945  have hring : ∀ (j : ℕ) (a b : O), b - a ∈ I ^ j → {t : O | t - a ∈ I ^ j} ∈ nhds b := by946    intro j a b hb947    refine Filter.mem_of_superset ((htop.hasBasis_nhds b).mem_of_mem (i := j) trivial) ?_948    rintro _ ⟨k, hk, rfl⟩949    change b + k - a ∈ I ^ j950    rw [show b + k - a = (b - a) + k by ring]; exact Ideal.add_mem _ hb hk951  refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_952  · rintro s (rfl | ⟨j, x, rfl⟩)953    · exact isOpen_empty954    rw [hball, isOpen_iff_mem_nhds]955    intro y hy956    refine Filter.mem_of_superset (Filter.iInter_mem.2 fun i =>957      (continuous_apply i).continuousAt.preimage_mem_nhds (hring j (x i) (y i) (hy i))) ?_958    intro z hz959    simpa only [Set.mem_iInter, Set.mem_preimage, Set.mem_ofPred_eq] using hz960  · intro x U hxU hU961    obtain ⟨F, u, hu, hFU⟩ := isOpen_pi_iff.1 hU x hxU962    have hj : ∀ i ∈ F, ∃ j : ℕ, ∀ t : O, t - x i ∈ I ^ j → t ∈ u i := by963      intro i hi964      obtain ⟨j, -, hj⟩ := (htop.hasBasis_nhds (x i)).mem_iff.1965        ((hu i hi).1.mem_nhds (hu i hi).2)966      exact ⟨j, fun t ht => hj ⟨t - x i, ht, by simp⟩⟩967    choose! J hJ using hj968    refine ⟨{y | adicCongr I (F.sup J) y x}, Or.inr ⟨F.sup J, x, rfl⟩, ?_, ?_⟩969    · rw [hball]; intro i; simp970    · rw [hball]971      exact fun y hy => hFU fun i hi =>972        hJ i hi (y i) (Ideal.pow_le_pow_right (Finset.le_sup hi) (hy i))973 974/-- For the `I`-adic topology on `O`, the Borel σ-algebra of `O^n` is generated by the adic975cylinders. -/976theorem finite_coordinate_borel_cylinders (O : Type) [CommRing O] [TopologicalSpace O]977    [IsTopologicalRing O] (I : Ideal O) (htop : IsAdic I) (n : ℕ) [SecondCountableTopology O]978    [MeasurableSpace O] [BorelSpace O] :979    (inferInstance : MeasurableSpace (Fin n → O)) = adicCylinderSpace I (Fin n → O) := by980  rw [BorelSpace.measurable_eq (α := Fin n → O)]981  exact (finite_coordinate_cylinder_basis O I htop n).borel_eq_generateFrom982 983/-- Every `O`-linear map `O^m → O^n` is continuous. -/984theorem finite_coordinate_linear_continuous (O : Type) [CommRing O] [TopologicalSpace O]985    [IsTopologicalRing O] (m n : ℕ) (L : (Fin m → O) →ₗ[O] (Fin n → O)) :986    Continuous L :=987  LinearMap.continuous_on_pi L988 989end SurfaceBlowup