/-
Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)
-/
import SurfaceBlowup.Basic
import Mathlib.Topology.Algebra.MvPolynomial

/-!
# Adic congruences, adic cylinders and division charts

This file sets up the adic language used by the measure-theoretic part of the development.
For an ideal `I` of a ring `R` and an `R`-module `M`, `x ≡ y (mod I^j M)` is `adicCongr I j x y`;
the adic cylinders `{y | y ≡ x (mod I^j M)}` generate the σ-algebra `adicCylinderSpace I M`.
We then introduce the coordinates attached to a division chart (an `O`-linear equivalence
`R ≃ (Fin n → O) × R` inverse to `(z, v) ↦ ∑ zᵢ bᵢ + f v`), the curve ideals
`(f + π ∑ zᵢ bᵢ)` they parametrize, ideal atlases and their measures, and the power-basis
coordinates of an unramified extension `O[X]/(Φ)`.

## Main results

* `mvPolynomial_zero_null`: zero sets of nonzero multivariate polynomials are null for products
  of atomless finite measures.
* `child_volume_ratio`: the local volume recursion for the children of a tangent pattern.
* `colored_subset_count`: the multinomial count of partially coloured maps `Fin Q → Option (Fin r)`.
* `division_linear_equivalence`: a lifted basis of `R/(f)` yields a division equivalence.
* `division_chart_rank_eq_of_residue_ideal_eq`: division charts with the same residue ideal
  have the same rank.
* `finite_coordinate_cylinder_basis`, `finite_coordinate_borel_cylinders`: on `O^n` with the
  `I`-adic topology, adic cylinders form a basis and generate the Borel σ-algebra.

Provenance: `Def_SurfaceBlowupV2_{AdicDigits, CylinderFamily, IdealCoordinates, Normalizer,
IdealAtlas, IdealChartSigma, UnramifiedMeasure}`, `Thm_Gen_PolyZeroNull`, `Thm_SurfaceBlowupV2_*`:
`algebra_product_congruence`, `child_volume_ratio`, `colored_subset_count`,
`common_vertical_exponent`, `congruence_bijection_measurable`, `coordinate_constraint_count`,
`coordinate_ideal_in_residue_cell`, `coordinate_module_pi_quotient_length`,
`coordinate_remainder_raises_order`, `division_chart_rank_eq_of_residue_ideal_eq`,
`division_coordinates_{injective, surjective}`, `division_{data, chart}_same_cell_recenter`,
`division_linear_equivalence`, `finite_coordinate_{adic_congruence, cylinder_basis,
borel_cylinders, linear_continuous}`.
-/

noncomputable section

open MeasureTheory
open scoped BigOperators ENNReal

namespace SurfaceBlowup

/-! ### Adic congruences and cylinders -/

section

variable {R M : Type} [CommRing R] [AddCommGroup M] [Module R M]

/-- `x ≡ y` modulo `I ^ j • M`. -/
def adicCongr (I : Ideal R) (j : ℕ) (x y : M) : Prop :=
  x - y ∈ (I ^ j • ⊤ : Submodule R M)

/-- A self-map `r` of `M` raises adic order: `x ≡ y (mod I^j)` implies `r x ≡ r y (mod I^(j+1))`. -/
def RaisesAdicOrder (I : Ideal R) (r : M → M) : Prop :=
  ∀ j x y, adicCongr I j x y → adicCongr I (j+1) (r x) (r y)

/-- The perturbation `x ↦ x + r x` of the identity by `r`. -/
def adicPerturb (r : M → M) (x : M) : M := x + r x

/-- The fixed-point iteration `x₀ = 0`, `x_{j+1} = y - r xⱼ` solving `x + r x = y`. -/
def digitIter (r : M → M) (y : M) : ℕ → M
  | 0 => 0
  | j+1 => y - r (digitIter r y j)

/-- The quotient `M / I ^ j M`. -/
abbrev AdicQuotient (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M]
    (j : ℕ) := M ⧸ (I ^ j • ⊤ : Submodule R M)

/-- The reduction map `M → M / I ^ j M`. -/
def adicReduce (I : Ideal R) (j : ℕ) : M →ₗ[R] AdicQuotient I M j :=
  (I ^ j • ⊤ : Submodule R M).mkQ

/-- The adic cylinders of `M`: the empty set and the congruence classes modulo `I ^ j M`. -/
def adicCylinders (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M] : Set (Set M) :=
  {s | s = ∅ ∨ ∃ j x, s = {y | adicCongr I j y x}}

set_option warn.classDefReducibility false in
/-- The σ-algebra on `M` generated by the adic cylinders. -/
def adicCylinderSpace (I : Ideal R) (M : Type) [AddCommGroup M] [Module R M] :
    MeasurableSpace M :=
  MeasurableSpace.generateFrom (adicCylinders I M)

end

/-! ### Division coordinates and curve ideals -/

section

variable {O R : Type} [CommRing O] [CommRing R] [Algebra O R]

/-- The lift `∑ i, zᵢ • bᵢ` of coordinates `z ∈ O^n` along representatives `b`. -/
def coordinateLift {n : ℕ} (b : Fin n → R) (z : Fin n → O) : R := ∑ i, z i • b i

/-- Scaling the coordinates by `a ∈ O` multiplies their lift by the image of `a`. -/
theorem coordinateLift_smul_eq_mul {n : ℕ} (b : Fin n → R) (a : O) (z : Fin n → O) :
    coordinateLift b (a • z) = algebraMap O R a * coordinateLift b z := by
  simp only [coordinateLift, Finset.mul_sum, Pi.smul_apply, smul_eq_mul, Algebra.smul_def, map_mul,
    mul_assoc]

/-- The division map `(z, v) ↦ ∑ zᵢ bᵢ + f v`. -/
def divisionMap {n : ℕ} (f : R) (b : Fin n → R) (s : (Fin n → O) × R) : R :=
  coordinateLift b s.1 + f * s.2

/-- The generator `f + ∑ zᵢ bᵢ`. -/
def normalizedGenerator {n : ℕ} (f : R) (b : Fin n → R) (z : Fin n → O) : R :=
  f + coordinateLift b z

/-- The remainder map `(z, v) ↦ π • E (v · ∑ zᵢ bᵢ)` of the normalization fixed-point problem. -/
def coordinateRemainder {n : ℕ} (pi : O) (b : Fin n → R)
    (E : R ≃ₗ[O] ((Fin n → O) × R)) (s : (Fin n → O) × R) : (Fin n → O) × R :=
  pi • E (s.2 * coordinateLift b s.1)

/-- The residue cell of `f`: principal ideals whose image modulo `π` is `(f mod π)`. -/
def residueIdealCell (pi f : R) : Set (Ideal R) :=
  {J | (∃ g : R, J = Ideal.span {g}) ∧
    Ideal.map (Ideal.Quotient.mk (Ideal.span {pi})) J =
      Ideal.span {Ideal.Quotient.mk (Ideal.span {pi}) f}}

/-- The principal ideal `(f + ∑ zᵢ bᵢ)`. -/
def normalizedIdeal {n : ℕ} (f : R) (b : Fin n → R) (z : Fin n → O) : Ideal R :=
  Ideal.span {normalizedGenerator f b z}

/-- The normal form of `h`: the solution `s` of `s + coordinateRemainder s = E h` (by choice). -/
def generatorNormalForm {n : ℕ} (pi : O) (b : Fin n → R)
    (E : R ≃ₗ[O] ((Fin n → O) × R)) (h : R) : (Fin n → O) × R :=
  Function.invFun (adicPerturb (coordinateRemainder pi b E)) (E h)

/-- The curve ideal `(f + π ∑ zᵢ bᵢ)` of the chart `(f, b)` at the coordinates `z`. -/
def coordinateIdeal {n : ℕ} (pi : O) (f : R) (b : Fin n → R) (z : Fin n → O) : Ideal R :=
  normalizedIdeal f b (pi • z)

/-- The transition map between two charts with the same residue cell. -/
def idealTransition {n : ℕ} (pi : O) (b c : Fin n → R)
    (F : R ≃ₗ[O] ((Fin n → O) × R)) (h0 : R) (z : Fin n → O) : Fin n → O :=
  (generatorNormalForm pi c F (h0 + coordinateLift b z)).1

end

/-! ### Ideal charts, atlases and their measures -/

section

variable (O R : Type) [CommRing O] [CommRing R] [Algebra O R]

/-- A division chart of rank `n`: a generator `f` regular modulo `π` with representatives `b`
and an `O`-linear equivalence `E` inverse to the division map. -/
structure IdealChart (pi : O) (n : ℕ) where
  /-- The centre generator. -/
  f : R
  /-- The coordinate representatives. -/
  b : Fin n → R
  /-- The division equivalence. -/
  E : R ≃ₗ[O] ((Fin n → O) × R)
  division : ∀ s, E.symm s = divisionMap f b s
  regular : Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>
    y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f)

/-- A finite atlas of `X` by charts of rank `n` whose residue cells partition `X`. -/
structure IdealAtlas (pi : O) (n : ℕ) (X : Set (Ideal R)) where
  /-- The chart index type. -/
  ι : Type
  [fin : Fintype ι]
  /-- The charts. -/
  chart : ι → IdealChart O R pi n
  cover : X = ⋃ i, residueIdealCell (algebraMap O R pi) (chart i).f
  disjoint : Pairwise fun i j =>
    Disjoint (residueIdealCell (algebraMap O R pi) (chart i).f)
      (residueIdealCell (algebraMap O R pi) (chart j).f)

attribute [instance] IdealAtlas.fin

/-- Division-chart data for the chart `z ↦ (f + pi·b(z))`: the representatives `b` carry an
`O`-linear division equivalence for `f` and `f` is regular modulo `pi`. -/
def IsDivisionChart (pi : O) {n : ℕ} (f : R) (b : Fin n → R) : Prop :=
  (∃ E : R ≃ₗ[O] ((Fin n → O) × R), ∀ s, E.symm s = divisionMap f b s) ∧
    Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>
      y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f)

variable {O R} in
/-- The centre and representatives of an ideal chart form a division chart. -/
theorem IdealChart.isDivisionChart {pi : O} {n : ℕ} (C : IdealChart O R pi n) :
    IsDivisionChart O R pi C.f C.b :=
  ⟨⟨C.E, C.division⟩, C.regular⟩

set_option warn.classDefReducibility false in
/-- The intrinsic σ-algebra on curve ideals: generated by the images of the Borel sets of `O^n`
under all division charts of all ranks `n`. -/
def idealChartSigma [MeasurableSpace O] (pi : O) : MeasurableSpace (Ideal R) :=
  MeasurableSpace.generateFrom
    {T : Set (Ideal R) | ∃ (n : ℕ) (f : R) (b : Fin n → R) (S : Set (Fin n → O)),
      IsDivisionChart O R pi f b ∧ MeasurableSet S ∧ T = coordinateIdeal pi f b '' S}

variable [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]
  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] [IsDomain O]
  [MeasurableSpace (Ideal R)]

/-- The pushforward of the coefficient measure of `O^n` along the chart's curve-ideal map. -/
noncomputable def chartMeasure (pi : O) (n : ℕ) (c : IdealChart O R pi n) : Measure (Ideal R) :=
  (coefficientMeasure O n).map (coordinateIdeal pi c.f c.b)

/-- The measure `q^(-n) ∑ᵢ chartMeasure (chart i)` of an atlas. -/
noncomputable def stateMeasure (pi : O) (n : ℕ) (q : ℕ) {X : Set (Ideal R)}
    (A : IdealAtlas O R pi n X) : Measure (Ideal R) :=
  ((q : ℝ≥0∞)⁻¹^n) • ∑ i : A.ι, chartMeasure O R pi n (A.chart i)

end

/-! ### Unramified extensions -/

section

variable (O : Type) [CommRing O] (Φ : Polynomial O) (hm : Φ.Monic)

/-- Coordinates of `O_δ = O[X]/(Φ)` in the power basis `1, θ, …, θ^(δ-1)` (`δ = natDegree Φ`). -/
noncomputable def powerCoordinates : AdjoinRoot Φ ≃ₗ[O] (Fin Φ.natDegree → O) :=
  (AdjoinRoot.powerBasis' hm).basis.equivFun

end

section

variable (O : Type) [CommRing O] [TopologicalSpace O] (Φ : Polynomial O) (hm : Φ.Monic)

set_option warn.classDefReducibility false in
/-- The topology of `O_δ` transported from the product topology of `O^δ` along the power basis. -/
noncomputable def unramifiedTopology : TopologicalSpace (AdjoinRoot Φ) :=
  TopologicalSpace.induced (powerCoordinates O Φ hm) inferInstance

end

section

variable (O : Type) [CommRing O] [MeasurableSpace O] (Φ : Polynomial O) (hm : Φ.Monic)

set_option warn.classDefReducibility false in
/-- The σ-algebra of `O_δ` transported from the product σ-algebra of `O^δ` along the power
basis. -/
noncomputable def unramifiedMeasurableSpace : MeasurableSpace (AdjoinRoot Φ) :=
  MeasurableSpace.comap (powerCoordinates O Φ hm) inferInstance

end

section

variable (O : Type) [CommRing O] [IsDomain O]
  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]
  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (Φ : Polynomial O) (hm : Φ.Monic)

/-- The coefficient measure of `O_δ`: the pushforward of the normalized coefficient Haar measure
of `O^δ` along the inverse of the power-basis coordinates. It is stated for an arbitrary ambient
σ-algebra on `AdjoinRoot Φ`; the theorems assume the transported one. -/
noncomputable def unramifiedCoefficientMeasure [MeasurableSpace (AdjoinRoot Φ)] :
    Measure (AdjoinRoot Φ) :=
  Measure.map (powerCoordinates O Φ hm).symm (coefficientMeasure O Φ.natDegree)

end

/-! ### Polynomial zero sets are null -/

/-- The zero set of a nonzero multivariate polynomial over a domain is null for any finite
product of copies of an atomless finite measure. -/
theorem mvPolynomial_zero_null {R : Type} [CommRing R] [IsDomain R]
    [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] [SecondCountableTopology R]
    [MeasurableSpace R] [BorelSpace R]
    (ν : Measure R) [IsFiniteMeasure ν] [NullSingletonClass ν] :
    ∀ (n : ℕ) (P : MvPolynomial (Fin n) R), P ≠ 0 →
      Measure.pi (fun _ : Fin n => ν) {x | MvPolynomial.eval x P = 0} = 0 := by
  classical
  intro n
  induction n with
  | zero =>
    intro P hP
    rw [MvPolynomial.eq_C_of_isEmpty P] at hP ⊢
    simp_all
  | succ n ih =>
    intro P hP
    set Q := MvPolynomial.finSuccEquiv R n P
    have hQ : Q ≠ 0 := (map_ne_zero_iff _ (MvPolynomial.finSuccEquiv R n).injective).2 hP
    have hZ : MeasurableSet {x : Fin (n+1) → R | MvPolynomial.eval x P = 0} :=
      (isClosed_eq (MvPolynomial.continuous_eval P) continuous_const).measurableSet
    let e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n+1) => R) 0
    set T : Set (R × (Fin n → R)) := e.symm ⁻¹' {x | MvPolynomial.eval x P = 0} with hT
    rw [← (measurePreserving_piFinSuccAbove (fun _ : Fin (n+1) => ν) 0).symm.measure_preimage
      hZ.nullMeasurableSet, Measure.prod_apply_symm (e.symm.measurable hZ)]
    have hae := measure_eq_zero_iff_ae_notMem.1 (ih _ (Polynomial.leadingCoeff_ne_zero.mpr hQ))
    have hzero : (fun s : Fin n → R => ν ((fun y => (y, s)) ⁻¹' T))
        =ᵐ[Measure.pi fun _ : Fin n => ν] 0 := by
      filter_upwards [hae] with s hs
      have hne : Polynomial.map (MvPolynomial.eval s) Q ≠ 0 := fun h => hs <| by
        simpa using congrArg (Polynomial.coeff · Q.natDegree) h
      refine measure_mono_null (fun y hy => ?_) ((Finset.finite_toSet
        (Polynomial.map (MvPolynomial.eval s) Q).roots.toFinset).measure_zero ν)
      simp only [hT, Set.mem_preimage, Set.mem_ofPred_eq] at hy
      have key : e.symm (y, s) = Fin.cons y s := by
        ext i
        refine Fin.cases ?_ (fun j => ?_) i <;> simp [e, MeasurableEquiv.piFinSuccAbove_symm_apply,
          Fin.insertNthEquiv]
      rw [key, MvPolynomial.eval_eq_eval_mv_eval'] at hy
      simpa using (Polynomial.mem_roots hne).2 hy
    rw [lintegral_congr_ae hzero]; simp

/-! ### Adic congruences -/

/-- Adic congruences in an `O`-algebra are compatible with multiplication. -/
theorem algebra_product_congruence (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    (I : Ideal O) (j : ℕ) (x x2 y y2 : R) (hx : adicCongr I j x x2) (hy : adicCongr I j y y2) :
    adicCongr I j (x*y) (x2*y2) := by
  have key : ∀ r : R, ∀ z ∈ (I ^ j • ⊤ : Submodule O R), r * z ∈ (I ^ j • ⊤ : Submodule O R) :=
    fun r z hz => Submodule.smul_induction_on hz
      (fun a ha m _ => mul_smul_comm a r m ▸ Submodule.smul_mem_smul ha Submodule.mem_top)
      (fun u v hu hv => (mul_add r u v).symm ▸ add_mem hu hv)
  unfold adicCongr at *
  rw [show x * y - x2 * y2 = y * (x - x2) + x2 * (y - y2) by ring]
  exact add_mem (key _ _ hx) (key _ _ hy)

/-! ### Local volume recursion -/

private lemma expr_eval_pow (x : ℚ) (e : Expr) (n : ℕ) :
    (Expr.pow e n).eval x = (e.eval x)^n := by
  induction n with
  | zero => simp [Expr.pow, Expr.eval]
  | succ n ih => simp [Expr.pow, Expr.eval, ih, pow_succ]

private lemma otherChildren_volume_prod (x : ℚ) (n a : ℕ) (m : Pattern n) :
    ((otherChildren a m).map fun z => (stateVolume z.2).eval (x^z.1)).prod
      = (x^(patternWeight m))⁻¹ := by
  unfold otherChildren patternWeight
  rw [List.map_flatMap, List.flatMap_def, List.prod_flatten, List.map_map]
  simp only [Function.comp_def, List.map_replicate, List.prod_replicate, stateVolume,
    Expr.eval, expr_eval_pow]
  rw [Finset.prod_map_toList, ← Finset.prod_pow_eq_pow_sum, ← Finset.prod_inv_distrib]
  refine Finset.prod_congr rfl fun ij _ => ?_
  rw [inv_pow, ← pow_mul, ← pow_mul, mul_assoc]

/-- The volume recursion: the children of an allowed tangent pattern `P` at a state `s`,
weighted by `q^(-tri d)`, have total volume `divisorProbability s d · stateVolume s`. -/
theorem child_volume_ratio (s : State) (hs : s.Valid) (P : TangentPattern s.degree)
    (hP : Allowed s P) (q : ℕ) (hq : 2 ≤ q) :
    ((q:ℚ)⁻¹^(tri P.d.val))
        * (((children s P).map fun z => (stateVolume z.2).eval ((q:ℚ)^z.1)).prod)
      / (stateVolume s).eval q = (divisorProbability s P.d.val).eval q := by
  have h2 : (2:ℚ) ≤ q := by exact_mod_cast hq
  have hq0 : (q:ℚ) ≠ 0 := by linarith
  have hq1 : (q:ℚ) - 1 ≠ 0 := by linarith
  have hq1' : -1 + (q:ℚ) ≠ 0 := by linarith
  have hq1'' : (q:ℚ) + -1 ≠ 0 := by linarith
  obtain ⟨hd0, hsum, hP⟩ := hP
  cases s with
  | single a c =>
    obtain ⟨hdc, hrx, hrt⟩ := hP
    simp only [children, List.map_append, List.prod_append]
    rw [otherChildren_volume_prod]
    simp only [stateVolume, divisorProbability, Expr.eval, expr_eval_pow, eminusOne, Expr.sub,
      Expr.neg]
    by_cases h0 : P.rt.val = 0
    · have hdc' : ¬ P.d.val < c := fun h => by have := hrt.2 h; omega
      have hc : c = P.d.val := by omega
      have hw : patternWeight P.other = P.d.val := by omega
      simp only [h0, if_true, hdc', if_false, List.map_nil, List.prod_nil, hw, inv_pow]
      rw [show (q:ℚ)^c = (q:ℚ)^P.d.val from congrArg _ hc]
      field_simp
    · have hdc' : P.d.val < c := hrt.1 (by omega)
      have hc : (q:ℚ)^c = (q:ℚ)^(P.rt.val + (c - P.d.val)) * (q:ℚ)^(patternWeight P.other) := by
        rw [← pow_add]; congr 1; omega
      simp only [h0, if_false, hdc', if_true, List.map_cons, List.map_nil, List.prod_cons,
        List.prod_nil, Expr.eval, expr_eval_pow, hc, pow_one, inv_pow]
      field_simp
  | crossing a b c h =>
    obtain ⟨hdc, hdh, hrt, hrx⟩ := hP
    simp only [children, List.map_append, List.prod_append]
    rw [otherChildren_volume_prod]
    simp only [stateVolume, divisorProbability, Expr.eval, expr_eval_pow, eminusOne, Expr.sub,
      Expr.neg]
    have htri : tri P.d.val = chooseTwo P.d.val + P.d.val := by
      unfold tri chooseTwo
      obtain ⟨n, hn⟩ : ∃ n, P.d.val = n+1 := ⟨_, (Nat.succ_pred_eq_of_pos hd0).symm⟩
      rw [hn, Nat.add_sub_cancel, show (n+1)*(n+1+1) = (n+1)*n + (n+1)*2 by ring,
        Nat.add_mul_div_right _ _ two_pos]
    have hch : (q:ℚ)^(c+h) = (q:ℚ)^(P.rt.val + (c - P.d.val)) * (q:ℚ)^(P.rx.val + (h - P.d.val))
        * (q:ℚ)^(patternWeight P.other) * (q:ℚ)^P.d.val := by
      rw [← pow_add, ← pow_add, ← pow_add]; congr 1; omega
    rw [htri, hch]
    have hc' : P.d.val < c ↔ P.rt.val ≠ 0 := ⟨fun h => by have := hrt.2 h; omega, hrt.1 ∘ by omega⟩
    have hh' : P.d.val < h ↔ P.rx.val ≠ 0 := ⟨fun h => by have := hrx.2 h; omega, hrx.1 ∘ by omega⟩
    have e1 : P.rt.val = 0 → c - P.d.val = 0 := fun h => by have := hrt.2; omega
    have e2 : P.rx.val = 0 → h - P.d.val = 0 := fun h => by have := hrx.2; omega
    by_cases h0 : P.rt.val = 0 <;> by_cases h1 : P.rx.val = 0 <;>
    · simp only [h0, h1, hc', hh', e1, e2, ne_eq, not_true_eq_false, not_false_eq_true, if_true,
        if_false, List.map_nil, List.prod_nil, Expr.eval, inv_pow, List.map_cons, List.prod_cons,
        expr_eval_pow]
      norm_num [Expr.eval, expr_eval_pow, pow_add]
      field_simp

/-! ### Counting coloured maps -/

private theorem card_fiber_succ {r n : ℕ} (f : Fin (n + 1) → Option (Fin r)) (y : Option (Fin r)) :
    Nat.card {x : Fin (n+1) // f x = y} =
      Nat.card {x : Fin n // f x.succ = y} + if f 0 = y then 1 else 0 := by
  simp only [Nat.card_eq_fintype_card, Fintype.card_subtype, Finset.card_filter, Fin.sum_univ_succ]
  ring

/-- The number of maps `Fin n → Option (Fin r)` with exactly `m i` points coloured `i`. -/
private noncomputable def coloredCount (r n : ℕ) (m : Fin r → ℕ) : ℕ :=
  Nat.card {f : Fin n → Option (Fin r) // ∀ i : Fin r, Nat.card {x : Fin n // f x = some i} = m i}

private theorem coloredCount_succ (r n : ℕ) (m : Fin r → ℕ) :
    coloredCount r (n+1) m = ∑ c : Option (Fin r), Nat.card {g : Fin n → Option (Fin r) //
      ∀ i : Fin r, Nat.card {x : Fin n // g x = some i} + (if c = some i then 1 else 0) = m i} := by
  unfold coloredCount
  rw [Nat.card_congr (Equiv.sigmaFiberEquiv
    (fun f : {f : Fin (n+1) → Option (Fin r) // ∀ i : Fin r,
      Nat.card {x : Fin (n+1) // f x = some i} = m i} => f.1 0)).symm, Nat.card_sigma]
  refine Finset.sum_congr rfl fun c _ => Nat.card_congr
    { toFun := fun p => ⟨Fin.tail p.1.1, fun i => by rw [← p.1.2 i, card_fiber_succ, p.2]; rfl⟩
      invFun := fun g => ⟨⟨Fin.cons c g.1, fun i => by rw [← g.2 i, card_fiber_succ]; simp⟩,
        by simp⟩
      left_inv := fun ⟨⟨f, hf⟩, hc⟩ => by subst hc; simp [Fin.cons_self_tail]
      right_inv := fun g => by simp }

private theorem coloredCount_term (r n : ℕ) (m : Fin r → ℕ) (i : Fin r) :
    Nat.card {g : Fin n → Option (Fin r) //
      ∀ j : Fin r, Nat.card {x : Fin n // g x = some j} + (if some i = some j then 1 else 0) = m j}
      = if m i = 0 then 0 else coloredCount r n (Function.update m i (m i - 1)) := by
  split_ifs with h
  · rw [Nat.card_eq_zero]; left
    constructor; rintro ⟨g, hg⟩
    have := hg i; simp at this; omega
  · refine Nat.card_congr (Equiv.subtypeEquivRight fun g => forall_congr' fun j => ?_)
    by_cases hj : j = i
    · subst hj; simp; omega
    · simp [Ne.symm hj, hj]

private theorem descFactorial_succ_left (n M : ℕ) :
    (n+1).descFactorial M = n.descFactorial M + M * n.descFactorial (M-1) := by
  cases M with
  | zero => simp
  | succ k =>
    rw [Nat.succ_descFactorial_succ, Nat.descFactorial_succ, Nat.add_sub_cancel]
    by_cases hk : k ≤ n
    · rw [show n + 1 = (n - k) + (k + 1) by omega, add_mul]
    · simp [Nat.descFactorial_eq_zero_iff_lt.mpr (show n < k by omega)]

private theorem coloredCount_eq (r n : ℕ) : ∀ m : Fin r → ℕ,
    (coloredCount r n m : ℚ) = (n.descFactorial (∑ i, m i) : ℚ) / ∏ i, ((m i).factorial : ℚ) := by
  induction n with
  | zero =>
    intro m
    by_cases h : ∀ i, m i = 0
    · have hP : ∀ f : Fin 0 → Option (Fin r),
          ∀ i : Fin r, Nat.card {x : Fin 0 // f x = some i} = m i := by
        intro f i; simp [h]
      unfold coloredCount
      rw [Nat.card_congr (Equiv.subtypeUnivEquiv hP)]
      simp [h]
    · push Not at h
      obtain ⟨i, hi⟩ := h
      have hC : coloredCount r 0 m = 0 := by
        unfold coloredCount
        rw [Nat.card_eq_zero]; left
        constructor; rintro ⟨g, hg⟩
        have := hg i; simp at this; omega
      have hle : m i ≤ ∑ j, m j :=
        Finset.single_le_sum (fun j _ => Nat.zero_le _) (Finset.mem_univ i)
      rw [hC, Nat.descFactorial_eq_zero_iff_lt.mpr (show 0 < ∑ j, m j by omega)]; simp
  | succ n ih =>
    intro m
    have hnone : Nat.card {g : Fin n → Option (Fin r) // ∀ i, Nat.card {x : Fin n // g x = some i}
        + (if (none : Option (Fin r)) = some i then 1 else 0) = m i} = coloredCount r n m := by
      simp [coloredCount]
    have key : ∀ i, ((if m i = 0 then 0 else coloredCount r n (Function.update m i (m i - 1)) : ℕ)
        : ℚ) = (m i : ℚ) * n.descFactorial (∑ j, m j - 1) / ∏ j, ((m j).factorial : ℚ) := by
      intro i
      split_ifs with h
      · simp [h]
      rw [ih]
      have hs : ∑ j, Function.update m i (m i - 1) j = ∑ j, m j - 1 := by
        rw [Finset.sum_update_of_mem (Finset.mem_univ _), Finset.sdiff_singleton_eq_erase,
          ← Finset.add_sum_erase _ _ (Finset.mem_univ i)]
        omega
      have hp : (∏ j, ((Function.update m i (m i - 1) j).factorial : ℚ)) * m i
          = ∏ j, ((m j).factorial : ℚ) := by
        rw [← Finset.mul_prod_erase _ _ (Finset.mem_univ i),
          ← Finset.mul_prod_erase _ (fun j => ((m j).factorial : ℚ)) (Finset.mem_univ i),
          Finset.prod_congr rfl (fun j hj => by
            rw [Function.update_of_ne (Finset.ne_of_mem_erase hj)])]
        simp only [Function.update_self]
        rw [← Nat.mul_factorial_pred h]; push_cast; ring
      have hmi : (m i : ℚ) ≠ 0 := by exact_mod_cast h
      rw [hs, ← hp]
      have : (∏ j, ((Function.update m i (m i - 1) j).factorial : ℚ)) ≠ 0 :=
        Finset.prod_ne_zero_iff.mpr fun j _ => by positivity
      field_simp
    rw [coloredCount_succ, Fintype.sum_option, hnone]
    simp only [coloredCount_term]
    rw [Nat.cast_add, Nat.cast_sum, ih]
    simp only [key]
    rw [← Finset.sum_div, ← Finset.sum_mul, ← Nat.cast_sum, descFactorial_succ_left]
    push_cast; ring

private theorem prod_range_sub_eq_descFactorial (Q M : ℕ) :
    ((List.range M).map fun j => (Q:ℚ)-j).prod = (Q.descFactorial M : ℚ) := by
  induction M with
  | zero => simp
  | succ k ih =>
    simp only [List.range_succ, List.pure_def, List.bind_eq_flatMap, List.flatMap_append,
      List.flatMap_cons, List.flatMap_nil, List.append_nil, List.map_append, List.map_cons,
      List.map_nil, List.prod_append, List.prod_cons, List.prod_nil, mul_one,
      Nat.descFactorial_succ, Nat.cast_mul] at ih ⊢
    rw [ih]
    by_cases hk : k ≤ Q
    · rw [Nat.cast_sub hk]; ring
    · simp [Nat.descFactorial_eq_zero_iff_lt.mpr (show Q < k by omega)]

/-- The number of maps `Fin Q → Option (Fin r)` with exactly `m i` points of colour `i` is
`Q (Q-1) ⋯ (Q - ∑ m + 1) / ∏ (m i)!`. -/
theorem colored_subset_count (Q r : ℕ) (m : Fin r → ℕ) :
    ((Nat.card {f : Fin Q→Option (Fin r) //
      ∀ i : Fin r, Nat.card {x : Fin Q // f x=some i}=m i} : ℕ) : ℚ) =
      ((List.range (∑ i : Fin r, m i)).map fun j => (Q:ℚ)-j).prod
        / ∏ i : Fin r, (Nat.factorial (m i):ℚ) := by
  rw [prod_range_sub_eq_descFactorial]
  exact coloredCount_eq r Q m

/-! ### Assorted coordinate lemmas -/

/-- If each component `e j` divides a power of `π` up to `d`-th powers, then a single exponent
`s ≥ s₀` works for all components of the finite product simultaneously. -/
theorem common_vertical_exponent (O : Type) [CommRing O] (ι : Type) [Finite ι] (C : ι → Type)
    [∀ j, CommRing (C j)] [∀ j, Algebra O (C j)] (pi : O) (e : ∀ j, C j) (d : ℕ)
    (hvert : ∀ j, ∃ (s : ℕ) (cj : C j), algebraMap O (C j) pi ^ s = e j ^ d * cj) (s₀ : ℕ) :
    ∃ (s : ℕ) (cc : ∀ j, C j), s₀ ≤ s ∧ (algebraMap O (∀ j, C j) pi) ^ s = e ^ d * cc := by
  have := Fintype.ofFinite ι
  choose sj cj h using hvert
  refine ⟨s₀ + ∑ i, sj i, fun j => cj j * algebraMap O (C j) pi ^ (s₀ + ∑ i, sj i - sj j),
    Nat.le_add_right _ _, funext fun j => ?_⟩
  have : sj j ≤ s₀ + ∑ i, sj i :=
    (Finset.single_le_sum (fun i _ => Nat.zero_le (sj i)) (Finset.mem_univ j)).trans
      (Nat.le_add_left _ _)
  simp only [Pi.algebraMap_apply, Pi.pow_apply, Pi.mul_apply]
  conv_lhs => rw [← Nat.add_sub_cancel' this, pow_add, h j]
  rw [mul_assoc]

/-- A surjection preserving and reflecting all adic congruences is measurable for the adic
cylinder σ-algebra. -/
theorem congruence_bijection_measurable (O V : Type) [CommRing O] [AddCommGroup V] [Module O V]
    (I : Ideal O) [MeasurableSpace V] (hgen : ‹MeasurableSpace V› = adicCylinderSpace I V)
    (F : V → V) (honto : Function.Surjective F)
    (hcong : ∀ j x y, adicCongr I j (F x) (F y) ↔ adicCongr I j x y) :
    Measurable F := by
  rw [hgen]
  let _ : MeasurableSpace V := adicCylinderSpace I V
  refine measurable_generateFrom fun s hs => ?_
  rcases hs with rfl | ⟨j, a, rfl⟩
  · simp
  · obtain ⟨b, rfl⟩ := honto a
    have : F ⁻¹' {y | adicCongr I j y (F b)} = {y | adicCongr I j y b} := by
      ext y; simp [hcong]
    exact this ▸ MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, b, rfl⟩)

/-- Over a finite field `k`, the number of `f : ι → k` vanishing on `A` and nonvanishing on a
disjoint `B` is `(|k| - 1)^|B| · |k|^(|ι| - |A| - |B|)`. -/
theorem coordinate_constraint_count (k ι : Type) [Field k] [Fintype k] [Fintype ι]
    (A B : Finset ι) (hAB : Disjoint A B) :
    Nat.card {f : ι→k // (∀ i∈A, f i=0) ∧ (∀ i∈B, f i≠0)}
      = (Fintype.card k-1)^B.card * (Fintype.card k)^(Fintype.card ι-A.card-B.card) := by
  classical
  let S : ι → Finset k := fun i =>
    if i ∈ A then {0} else if i ∈ B then Finset.univ.erase 0 else Finset.univ
  have hset : (Finset.univ.filter
      (fun f : ι → k => (∀ i∈A, f i=0) ∧ (∀ i∈B, f i≠0))) = Fintype.piFinset S := by
    ext f
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Fintype.mem_piFinset, S]
    constructor
    · rintro ⟨h1, h2⟩ i
      by_cases hA : i ∈ A
      · simp [hA, h1 i hA]
      · by_cases hB : i ∈ B
        · simp [hA, hB, h2 i hB]
        · simp [hA, hB]
    · intro h
      refine ⟨fun i hi => by simpa [hi] using h i, fun i hi => ?_⟩
      simpa [Finset.disjoint_right.mp hAB hi, hi] using h i
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, hset, Fintype.card_piFinset]
  have hcard : ∀ i, (S i).card =
      if i ∈ A then 1 else if i ∈ B then Fintype.card k - 1 else Fintype.card k := by
    intro i
    by_cases hA : i ∈ A
    · simp [S, hA]
    · by_cases hB : i ∈ B <;> simp [S, hA, hB, Finset.card_erase_of_mem]
  simp only [hcard]
  rw [Finset.prod_ite, Finset.prod_const_one, one_mul, Finset.prod_ite,
    Finset.prod_const, Finset.prod_const, Finset.filter_filter, Finset.filter_filter]
  have h1 : Finset.univ.filter (fun i => i ∉ A ∧ i ∈ B) = B := by
    ext i
    simpa using fun h => Finset.disjoint_right.mp hAB h
  have h2 : Finset.univ.filter (fun i => i ∉ A ∧ i ∉ B) = (A ∪ B)ᶜ := by
    ext i; simp
  rw [h1, h2, Finset.card_compl, Finset.card_union_of_disjoint hAB, Nat.sub_sub]

/-- The curve ideal `(f + π ∑ zᵢ bᵢ)` lies in the residue cell of `f`. -/
theorem coordinate_ideal_in_residue_cell (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    (n : ℕ) (pi : O) (b : Fin n → R) (f : R) (z : Fin n → O) :
    coordinateIdeal pi f b z ∈ residueIdealCell (algebraMap O R pi) f := by
  refine ⟨⟨_, rfl⟩, ?_⟩
  unfold coordinateIdeal normalizedIdeal
  rw [Ideal.map_span, Set.image_singleton]
  congr 2
  rw [normalizedGenerator, map_add, add_eq_left, Ideal.Quotient.eq_zero_iff_mem,
    coordinateLift_smul_eq_mul]
  exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)

/-- For a free module `V ≅ O^n` over a DVR with uniformizer `π`, multiplication by `π` is
injective and `V / πV` has length `n`. -/
theorem coordinate_module_pi_quotient_length (O : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (pi : O)
    (hpi : Irreducible pi) (n : ℕ) (V : Type) [AddCommGroup V] [Module O V]
    (EV : V ≃ₗ[O] (Fin n → O)) :
    Function.Injective (fun v : V => pi • v) ∧
      Module.length O (V ⧸ LinearMap.range (pi • (LinearMap.id : V →ₗ[O] V))) = (n : ℕ∞) := by
  refine ⟨fun v w h => EV.injective <| funext fun i => mul_left_cancel₀ hpi.ne_zero ?_, ?_⟩
  · simpa using congrArg (fun x => EV x i) h
  set I : Ideal O := Ideal.span {pi} with hI
  have hsimple : IsSimpleModule O (O ⧸ I) := by
    have hImax : I.IsMaximal := by
      rw [hI, hpi.maximalIdeal_eq.symm]; exact IsLocalRing.maximalIdeal.isMaximal O
    rw [Ideal.isMaximal_def] at hImax
    exact isSimpleModule_iff_isCoatom.mpr hImax
  let f : V →ₗ[O] (Fin n → O ⧸ I) :=
    LinearMap.pi (fun i => I.mkQ ∘ₗ LinearMap.proj i ∘ₗ EV.toLinearMap)
  have hsurj : Function.Surjective f := by
    intro y
    choose x hx using fun i => Ideal.Quotient.mk_surjective (y i)
    exact ⟨EV.symm x, funext fun i => by simp [f, hx]⟩
  have hker : LinearMap.ker f = LinearMap.range (pi • (LinearMap.id : V →ₗ[O] V)) := by
    ext v
    simp only [LinearMap.mem_ker, LinearMap.mem_range, f]
    constructor
    · intro h
      have h' : ∀ i, EV v i ∈ I := fun i => by
        simpa [Ideal.Quotient.eq_zero_iff_mem] using congrFun h i
      choose y hy using fun i => Ideal.mem_span_singleton'.mp (h' i)
      exact ⟨EV.symm y, EV.injective <| funext fun i => by simp [← hy i, mul_comm]⟩
    · rintro ⟨w, rfl⟩
      funext i
      simp only [LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe,
        LinearMap.smul_apply, LinearMap.id_apply, map_smul, LinearMap.coe_proj,
        Function.eval, Submodule.mkQ_apply, Pi.zero_apply]
      rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero, hI, smul_eq_mul]
      exact Ideal.mem_span_singleton'.mpr ⟨EV w i, mul_comm _ _⟩
  let e := (Submodule.quotEquivOfEq _ _ hker).symm.trans (f.quotKerEquivOfSurjective hsurj)
  rw [e.length_eq, Module.length_pi, Module.length_eq_one]
  simp

/-- The coordinate remainder `(z, v) ↦ π • E (v ∑ zᵢ bᵢ)` raises `π`-adic order. -/
theorem coordinate_remainder_raises_order (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    (n : ℕ) (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R)) :
    RaisesAdicOrder (Ideal.span {pi}) (coordinateRemainder pi b E) := by
  set I : Ideal O := Ideal.span {pi}
  have key : ∀ (j : ℕ) {M N : Type} [AddCommGroup M] [Module O M] [AddCommGroup N] [Module O N]
      (f : M →ₗ[O] N) (x : M), x ∈ (I ^ j • ⊤ : Submodule O M) →
        f x ∈ (I ^ j • ⊤ : Submodule O N) := by
    intro j M N _ _ _ _ f x hx
    have hle : (I ^ j • ⊤ : Submodule O M) ≤ (I ^ j • ⊤ : Submodule O N).comap f := by
      rw [Submodule.smul_le]
      intro r hr m _
      simpa using Submodule.smul_mem_smul hr Submodule.mem_top
    exact hle hx
  intro j x y hxy
  unfold adicCongr at hxy ⊢
  have h2 : x.2 - y.2 ∈ (I ^ j • ⊤ : Submodule O R) := by
    simpa using key j (LinearMap.snd O (Fin n → O) R) _ hxy
  have hL : coordinateLift b x.1 - coordinateLift b y.1 ∈ (I ^ j • ⊤ : Submodule O R) := by
    simpa [coordinateLift, Fintype.linearCombination_apply, sub_smul, Finset.sum_sub_distrib]
      using key j ((Fintype.linearCombination O b).comp (LinearMap.fst O (Fin n → O) R)) _ hxy
  have hprod : x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1
      ∈ (I ^ j • ⊤ : Submodule O R) := by
    rw [show x.2 * coordinateLift b x.1 - y.2 * coordinateLift b y.1
        = x.2 * (coordinateLift b x.1 - coordinateLift b y.1)
          + (x.2 - y.2) * coordinateLift b y.1 by ring]
    exact Submodule.add_mem _ (key j (LinearMap.mulLeft O x.2) _ hL)
      (key j (LinearMap.mulRight O (coordinateLift b y.1)) _ h2)
  have hE := key j E.toLinearMap _ hprod
  simp only [LinearEquiv.coe_coe, map_sub] at hE
  unfold coordinateRemainder
  rw [← smul_sub, pow_succ', Submodule.mul_smul]
  exact Submodule.smul_mem_smul (Ideal.mem_span_singleton_self pi) hE

/-! ### Rank of a division chart -/

private theorem card_quot_eq_of_surjective (R M : Type) [CommRing R] [AddCommGroup M] (J : Ideal R)
    (φ : R →+ M) (hφ : Function.Surjective φ) (hker : ∀ r, φ r = 0 ↔ r ∈ J) :
    Nat.card (R ⧸ J) = Nat.card M := by
  have hs := Ideal.Quotient.mk_surjective (I := J)
  let s := Function.surjInv hs
  have hmk : ∀ x, Ideal.Quotient.mk J (s x) = x := Function.surjInv_eq hs
  refine Nat.card_congr (Equiv.ofBijective (fun x => φ (s x)) ⟨fun x y hxy => ?_, fun m => ?_⟩)
  · rwa [← hmk x, ← hmk y, Ideal.Quotient.eq, ← hker, map_sub, sub_eq_zero]
  · obtain ⟨r, rfl⟩ := hφ m
    have h1 : Ideal.Quotient.mk J (s (Ideal.Quotient.mk J r)) = Ideal.Quotient.mk J r := hmk _
    rw [Ideal.Quotient.eq, ← hker, map_sub, sub_eq_zero] at h1
    exact ⟨Ideal.Quotient.mk J r, h1⟩

private theorem card_quot_divisionChart (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [CommRing R] [Algebra O R] (pi : O) (hpi : Irreducible pi) (n : ℕ)
    (f : R) (b : Fin n → R) (hb : IsDivisionChart O R pi f b) :
    Nat.card (R ⧸ Ideal.comap (Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}))
      (Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f})) =
      Nat.card (Fin n → IsLocalRing.ResidueField O) := by
  obtain ⟨E, hE⟩ := hb.1
  have hmax : IsLocalRing.maximalIdeal O = Ideal.span {pi} := hpi.maximalIdeal_eq
  let φ : R →+ (Fin n → IsLocalRing.ResidueField O) :=
    { toFun := fun r i => IsLocalRing.residue O ((E r).1 i)
      map_zero' := by ext i; simp
      map_add' := by intro x y; ext i; simp }
  apply card_quot_eq_of_surjective R _ _ φ
  · intro m
    choose z hz using fun i => IsLocalRing.residue_surjective (R := O) (m i)
    exact ⟨E.symm (z, 0), by ext i; simp [φ, hz]⟩
  · intro r
    have hEf : ∀ a : R, E (f * a) = (0, a) := fun a => E.symm.injective <| by
      rw [E.symm_apply_apply, hE]
      simp [divisionMap, coordinateLift]
    constructor
    · intro h
      have hi : ∀ i, ∃ y, pi * y = (E r).1 i := fun i ↦ by
        have : IsLocalRing.residue O ((E r).1 i) = 0 := congrFun h i
        rw [IsLocalRing.residue_eq_zero_iff, hmax, Ideal.mem_span_singleton'] at this
        obtain ⟨y, hy⟩ := this
        exact ⟨y, by rw [← hy, mul_comm]⟩
      choose z hz using hi
      have hr : r = algebraMap O R pi * coordinateLift b z + f * (E r).2 := by
        have := hE (E r)
        rw [E.symm_apply_apply] at this
        refine this.trans ?_
        rw [divisionMap, ← coordinateLift_smul_eq_mul]
        congr 2; ext i; exact (hz i).symm
      rw [Ideal.mem_comap, Ideal.mem_span_singleton']
      refine ⟨Ideal.Quotient.mk _ (E r).2, ?_⟩
      rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton']
      exact ⟨-coordinateLift b z, by linear_combination hr⟩
    · intro h
      obtain ⟨a, ha⟩ := Ideal.mem_span_singleton'.1 (Ideal.mem_comap.1 h)
      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective a
      rw [← map_mul, Ideal.Quotient.eq, Ideal.mem_span_singleton'] at ha
      obtain ⟨t, ht⟩ := ha
      have hr : r = f * a + pi • (-t) := by
        rw [Algebra.smul_def]; linear_combination ht
      ext i
      simp only [φ, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.zero_apply]
      rw [hr, map_add, map_smul, hEf]
      simp only [Prod.fst_add, Prod.smul_fst, Pi.add_apply, Pi.smul_apply, Pi.zero_apply,
        zero_add, smul_eq_mul]
      rw [IsLocalRing.residue_eq_zero_iff, hmax]
      exact Ideal.mul_mem_right _ _ (Ideal.subset_span rfl)

/-- Two division charts whose centres generate the same ideal modulo `π` have the same rank. -/
theorem division_chart_rank_eq_of_residue_ideal_eq (O R : Type) [CommRing O] [IsDomain O]
    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] [CommRing R] [Algebra O R]
    (pi : O) (hpi : Irreducible pi) (n n' : ℕ) (f g : R) (b : Fin n → R) (c : Fin n' → R)
    (hb : IsDivisionChart O R pi f b) (hc : IsDivisionChart O R pi g c)
    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =
      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :
    n = n' := by
  have h1 := card_quot_divisionChart O R pi hpi n f b hb
  rw [hres, card_quot_divisionChart O R pi hpi n' g c hc] at h1
  have := Fintype.ofFinite (IsLocalRing.ResidueField O)
  simp only [Nat.card_pi, Finset.prod_const, Finset.card_univ, Fintype.card_fin] at h1
  exact (Nat.pow_right_injective (Finite.one_lt_card_iff_nontrivial.mpr inferInstance) h1).symm

/-! ### Division coordinates -/

/-- If `b` lifts an `O`-basis of `R/(f)` and `f` is a nonzerodivisor, the division map
`(z, v) ↦ ∑ zᵢ bᵢ + f v` is injective. -/
private theorem division_coordinates_injective (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    (n : ℕ)
    (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)
    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) [IsDomain R] (hf : f ≠ 0) :
    Function.Injective (divisionMap (O := O) f b) := by
  have key : ∀ z : Fin n → O,
      Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z) = ∑ i, z i • B i := by
    intro z
    rw [← Ideal.Quotient.mkₐ_eq_mk O, coordinateLift, map_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [map_smul, Ideal.Quotient.mkₐ_eq_mk, hb]
  rintro ⟨z, v⟩ ⟨z', v'⟩ h
  simp only [divisionMap] at h
  have hq := congrArg (Ideal.Quotient.mk (Ideal.span {f})) h
  have hf0 : Ideal.Quotient.mk (Ideal.span {f}) f = 0 :=
    Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self f)
  simp only [map_add, map_mul, hf0, zero_mul, add_zero, key] at hq
  obtain rfl : z = z' := funext fun i => by
    simpa [Finsupp.finsetSum_apply, Finsupp.single_apply] using congrArg (fun x => B.repr x i) hq
  rw [mul_left_cancel₀ hf (add_left_cancel h)]

/-- If `b` lifts an `O`-basis of `R/(f)`, the division map `(z, v) ↦ ∑ zᵢ bᵢ + f v` is
surjective. -/
private theorem division_coordinates_surjective (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    (n : ℕ) (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)
    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) :
    Function.Surjective (divisionMap (O := O) f b) := by
  intro h
  set z : Fin n → O := fun i => B.repr (Ideal.Quotient.mk (Ideal.span {f}) h) i
  have hz : Ideal.Quotient.mk (Ideal.span {f}) (coordinateLift b z)
      = Ideal.Quotient.mk (Ideal.span {f}) h := by
    unfold coordinateLift
    rw [map_sum]
    conv_rhs => rw [← B.sum_repr (Ideal.Quotient.mk (Ideal.span {f}) h)]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Algebra.smul_def, map_mul, hb i, Algebra.smul_def]
    rfl
  obtain ⟨v, hv⟩ := Ideal.mem_span_singleton'.mp (Ideal.Quotient.eq.1 hz.symm)
  exact ⟨(z, v), by simp only [divisionMap]; rw [mul_comm, hv]; ring⟩

/-- Recentring: if the regular element `f` and the chart centre `g` (with division equivalence
`Ec`) generate the same ideal modulo `π`, then the chart can be rescaled by a unit so that its new
centre `g'` satisfies `f = g' + π h₀`, with the same curve ideals. -/
theorem division_data_same_cell_recenter (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    [IsLocalRing R] (pi : O) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n : ℕ)
    (f g : R) (c : Fin n → R)
    (hf : Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>
      y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))
    (Ec : R ≃ₗ[O] ((Fin n → O) × R)) (hEc : ∀ s, Ec.symm s = divisionMap g c s)
    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =
      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :
    ∃ (g' : R) (c' : Fin n → R) (F : R ≃ₗ[O] ((Fin n → O) × R)) (h₀ : R),
      (∀ s, F.symm s = divisionMap g' c' s) ∧ f = g' + pi • h₀ ∧
      Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>
        y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g') ∧
      ∀ z : Fin n → O, coordinateIdeal pi g c z = coordinateIdeal pi g' c' z := by
  set I : Ideal R := Ideal.span {algebraMap O R pi} with hI
  set mk := Ideal.Quotient.mk I
  have hIm : I ≤ IsLocalRing.maximalIdeal R := by
    rw [hI, Ideal.span_le]; simpa using hpm
  obtain ⟨a, ha⟩ := Ideal.mem_span_singleton'.1 (hres ▸ Ideal.mem_span_singleton_self (mk g))
  obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 (hres ▸ Ideal.mem_span_singleton_self (mk f))
  have hba : b * a = 1 := hf <| by simp only; rw [one_mul, mul_assoc, ha, hb]
  obtain ⟨a', rfl⟩ := Ideal.Quotient.mk_surjective a
  obtain ⟨b', rfl⟩ := Ideal.Quotient.mk_surjective b
  have hunit : IsUnit a' := by
    by_contra hna
    have h2 : b' * a' - 1 ∈ I := by
      rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_one]
      exact sub_eq_zero.2 hba
    have := (IsLocalRing.maximalIdeal R).sub_mem ((IsLocalRing.maximalIdeal R).mul_mem_left b'
      ((IsLocalRing.mem_maximalIdeal _).2 hna)) (hIm h2)
    simp at this
  obtain ⟨u, rfl⟩ := hunit
  -- multiplication by `u` as an `O`-linear equivalence
  let M : R ≃ₗ[O] R :=
    { toFun := fun x => (u : R) * x
      invFun := fun x => ((u⁻¹ : Rˣ) : R) * x
      map_add' := fun x y => mul_add _ _ _
      map_smul' := fun r x => by simp [Algebra.mul_smul_comm]
      left_inv := fun x => Units.inv_mul_cancel_left u x
      right_inv := fun x => Units.mul_inv_cancel_left u x }
  have hlift : ∀ (w : R) (z : Fin n → O),
      w * coordinateLift c z = coordinateLift (fun i => w * c i) z := by
    intro w z
    simp only [coordinateLift, Finset.mul_sum, mul_smul_comm]
  have hg' : mk (((u⁻¹ : Rˣ) : R) * g) = mk f := by
    rw [map_mul, ← ha, ← mul_assoc, ← map_mul, Units.inv_mul, map_one, one_mul]
  obtain ⟨h, hh⟩ := Ideal.mem_span_singleton'.1 (Ideal.Quotient.eq.1 hg')
  refine ⟨((u⁻¹ : Rˣ) : R) * g, fun i => ((u⁻¹ : Rˣ) : R) * c i, M.trans Ec, -h, fun s => ?_, ?_,
    ?_, fun z => ?_⟩
  · rw [LinearEquiv.trans_symm, LinearEquiv.trans_apply, hEc]
    change ((u⁻¹ : Rˣ) : R) * divisionMap g c s = _
    simp only [divisionMap, mul_add, hlift, mul_assoc]
  · rw [smul_neg, Algebra.smul_def, mul_comm (algebraMap O R pi), hh]; ring
  · simpa only [show mk (((u⁻¹ : Rˣ) : R) * g) = mk f from hg'] using hf
  · simp only [coordinateIdeal, normalizedIdeal, normalizedGenerator]
    rw [← hlift, ← mul_add, Ideal.span_singleton_mul_left_unit (Units.isUnit _)]

/-- Recentring for two division charts of the same rank whose centres generate the same ideal
modulo `π` (see `division_data_same_cell_recenter`). -/
theorem division_chart_same_cell_recenter (O R : Type) [CommRing O] [CommRing R] [Algebra O R]
    [IsLocalRing R] (pi : O) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n : ℕ)
    (f g : R) (b c : Fin n → R) (hb : IsDivisionChart O R pi f b) (hc : IsDivisionChart O R pi g c)
    (hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =
      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}) :
    ∃ (g' : R) (c' : Fin n → R) (F : R ≃ₗ[O] ((Fin n → O) × R)) (h₀ : R),
      (∀ s, F.symm s = divisionMap g' c' s) ∧ f = g' + pi • h₀ ∧
      Function.Injective (fun y : R ⧸ Ideal.span {algebraMap O R pi} =>
        y * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g') ∧
      ∀ z : Fin n → O, coordinateIdeal pi g c z = coordinateIdeal pi g' c' z :=
  let ⟨Ec, hEc⟩ := hc.1
  division_data_same_cell_recenter O R pi hpm n f g c hb.2 Ec hEc hres

/-- If `b` lifts an `O`-basis of `R/(f)` with `f ≠ 0` in a domain, the division map is the
inverse of an `O`-linear equivalence `R ≃ O^n × R`. -/
theorem division_linear_equivalence (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)
    (f : R) (B : Module.Basis (Fin n) O (R ⧸ Ideal.span {f})) (b : Fin n → R)
    (hb : ∀ i, Ideal.Quotient.mk (Ideal.span {f}) (b i) = B i) [IsDomain R] (hf : f ≠ 0) :
    ∃ E : R ≃ₗ[O] ((Fin n → O) × R), ∀ s, E.symm s = divisionMap f b s := by
  let L : ((Fin n → O) × R) →ₗ[O] R :=
    { toFun := divisionMap f b
      map_add' := by
        intro x y
        simp only [divisionMap, coordinateLift, Prod.fst_add, Prod.snd_add, Pi.add_apply,
          add_smul, Finset.sum_add_distrib, mul_add]
        ring
      map_smul' := by
        intro c x
        simp only [divisionMap, coordinateLift, Prod.smul_fst, Prod.smul_snd, Pi.smul_apply,
          smul_eq_mul, RingHom.id_apply, smul_add, Finset.smul_sum, mul_smul]
        rw [mul_smul_comm] }
  exact ⟨(LinearEquiv.ofBijective L ⟨division_coordinates_injective O R n f B b hb hf,
    division_coordinates_surjective O R n f B b hb⟩).symm, fun _ => rfl⟩

/-! ### Finite coordinate spaces -/

/-- On `O^n`, `x ≡ y (mod I^j)` holds iff it holds coordinatewise. -/
theorem finite_coordinate_adic_congruence (O : Type) [CommRing O] (n : ℕ) (I : Ideal O) (j : ℕ)
    (x y : Fin n → O) :
    adicCongr I j x y ↔ ∀ i, x i - y i ∈ I^j := by
  unfold adicCongr
  constructor
  · intro h
    have : ∀ i, (x - y) i ∈ I ^ j :=
      Submodule.smul_induction_on h
        (fun r hr m _ i => by simpa using Ideal.mul_mem_right (m i) _ hr)
        (fun a b ha hb i => by simpa using Ideal.add_mem _ (ha i) (hb i))
    simpa using this
  · intro h
    have hv : x - y = ∑ i, (x i - y i) • (Pi.single i 1 : Fin n → O) := by
      funext k
      simp [Finset.sum_apply, Pi.single_apply]
    rw [hv]
    exact Submodule.sum_mem _ fun i _ => Submodule.smul_mem_smul (h i) Submodule.mem_top

/-- For the `I`-adic topology on `O`, the adic cylinders form a basis of the product topology
of `O^n`. -/
theorem finite_coordinate_cylinder_basis (O : Type) [CommRing O] [TopologicalSpace O]
    [IsTopologicalRing O] (I : Ideal O) (htop : IsAdic I) (n : ℕ) :
    TopologicalSpace.IsTopologicalBasis (adicCylinders I (Fin n → O)) := by
  have hball : ∀ (j : ℕ) (x : Fin n → O),
      {y : Fin n → O | adicCongr I j y x} = {y | ∀ i, y i - x i ∈ I ^ j} := fun j x =>
    Set.ext fun y => finite_coordinate_adic_congruence O n I j y x
  have hring : ∀ (j : ℕ) (a b : O), b - a ∈ I ^ j → {t : O | t - a ∈ I ^ j} ∈ nhds b := by
    intro j a b hb
    refine Filter.mem_of_superset ((htop.hasBasis_nhds b).mem_of_mem (i := j) trivial) ?_
    rintro _ ⟨k, hk, rfl⟩
    change b + k - a ∈ I ^ j
    rw [show b + k - a = (b - a) + k by ring]; exact Ideal.add_mem _ hb hk
  refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
  · rintro s (rfl | ⟨j, x, rfl⟩)
    · exact isOpen_empty
    rw [hball, isOpen_iff_mem_nhds]
    intro y hy
    refine Filter.mem_of_superset (Filter.iInter_mem.2 fun i =>
      (continuous_apply i).continuousAt.preimage_mem_nhds (hring j (x i) (y i) (hy i))) ?_
    intro z hz
    simpa only [Set.mem_iInter, Set.mem_preimage, Set.mem_ofPred_eq] using hz
  · intro x U hxU hU
    obtain ⟨F, u, hu, hFU⟩ := isOpen_pi_iff.1 hU x hxU
    have hj : ∀ i ∈ F, ∃ j : ℕ, ∀ t : O, t - x i ∈ I ^ j → t ∈ u i := by
      intro i hi
      obtain ⟨j, -, hj⟩ := (htop.hasBasis_nhds (x i)).mem_iff.1
        ((hu i hi).1.mem_nhds (hu i hi).2)
      exact ⟨j, fun t ht => hj ⟨t - x i, ht, by simp⟩⟩
    choose! J hJ using hj
    refine ⟨{y | adicCongr I (F.sup J) y x}, Or.inr ⟨F.sup J, x, rfl⟩, ?_, ?_⟩
    · rw [hball]; intro i; simp
    · rw [hball]
      exact fun y hy => hFU fun i hi =>
        hJ i hi (y i) (Ideal.pow_le_pow_right (Finset.le_sup hi) (hy i))

/-- For the `I`-adic topology on `O`, the Borel σ-algebra of `O^n` is generated by the adic
cylinders. -/
theorem finite_coordinate_borel_cylinders (O : Type) [CommRing O] [TopologicalSpace O]
    [IsTopologicalRing O] (I : Ideal O) (htop : IsAdic I) (n : ℕ) [SecondCountableTopology O]
    [MeasurableSpace O] [BorelSpace O] :
    (inferInstance : MeasurableSpace (Fin n → O)) = adicCylinderSpace I (Fin n → O) := by
  rw [BorelSpace.measurable_eq (α := Fin n → O)]
  exact (finite_coordinate_cylinder_basis O I htop n).borel_eq_generateFrom

/-- Every `O`-linear map `O^m → O^n` is continuous. -/
theorem finite_coordinate_linear_continuous (O : Type) [CommRing O] [TopologicalSpace O]
    [IsTopologicalRing O] (m n : ℕ) (L : (Fin m → O) →ₗ[O] (Fin n → O)) :
    Continuous L :=
  LinearMap.continuous_on_pi L

end SurfaceBlowup