Reciprocity: the quantum torus, dilations and reciprocal substitution

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.Reciprocity.Defs7 8/-!9# Reciprocity: the quantum torus, dilations and reciprocal substitution10 11Algebraic properties of the reciprocity setting of `SurfaceBlowup.Reciprocity.Defs`. We show that12`q ↦ q⁻¹` is an involution of `ℚ(q)` and of `Coef`, commuting with the Adams operations; that the13reciprocal substitution `recipSer` and the dilations `dilate`/`codilate` act coefficientwise and14commute with the plethystic powers; that the twisted product on contact series is associative and15compatible with `ι₊`, `ι₋`, the anti-involution `†` and the diagonal substitution; and we relate16the representation `qact` to its `q ↦ q⁻¹` conjugate through the Gauss twist `Φ`.17 18## Main results19 20* `recipRat_recipRat`, `recipCoef_recipCoef`, `recipCoef_adamsCoef`, `adamsCoef_adamsCoef`.21* `qmul_assoc`, `qdagger_qmul`, `qdagger_qplus`, `qdagger_qminus`, `qdiag_mul`,22  `qcongr_qdiag_mul_qdagger`.23* `recipSer_pPow`, `dilate_pPow`, `codilate_pPow`, `moebiusSum_plethSum`, `plethSum_moebiusSum`.24* `gaussPhi_qactRecip_gaussPhiInv`: `Φ ∘ ρ̄(v V) ∘ Φ⁻¹ = S⁻¹ ∘ ρ(V†) ∘ S` for symmetric `V`.25* `SCongr.mul`, `SCongr.of_mul_right`, `SCongr.expSer`, `SCongr.logSer`: congruences of series.26 27Provenance: `Thm_SurfaceBlowupV2_recip_{qplus_mul, qpositive_basic, recipRat_apply,28adamsCoef_recipCoef_single, adamsSer_exp_log, plethSum_moebiusSum, projectiveNormalizer_recip,29qact_recip, qpow_scalar_arith, qdagger_mul, qdagger_qplus_qminus, qmul_assoc, recipSer_hom,30dilate_hom, dilate_pleth, gaussPhi_inv, gauss_conjugation, qdiag_mul, qdiag_central, recipSer_pleth,31scalar_cancel, scongr_basic, scongr_cancel, scongr_exp_log}`.32-/33 34noncomputable section35 36namespace SurfaceBlowup37 38/-! ### The substitution `q ↦ q⁻¹` and Adams operations on coefficients -/39 40private theorem recipRat_recipPoly (g : Polynomial ℚ) :41    recipRat (recipPoly g) = algebraMap (Polynomial ℚ) (RatFunc ℚ) g := by42  change recipRat (g.eval₂ RatFunc.C (RatFunc.X : RatFunc ℚ)⁻¹) = _43  rw [Polynomial.hom_eval₂,44    show recipRat.comp (RatFunc.C : ℚ →+* RatFunc ℚ) = RatFunc.C from RingHom.ext recipRat_C,45    map_inv₀, recipRat_X, inv_inv]46  exact eval₂_C_X_eq_algebraMap g47 48/-- `q ↦ q⁻¹` is an involution of `ℚ(q)`. -/49theorem recipRat_recipRat (f : RatFunc ℚ) : recipRat (recipRat f) = f := by50  conv_lhs => rw [← RatFunc.num_div_denom f]51  rw [map_div₀, map_div₀, recipRat_algebraMap, recipRat_algebraMap, recipRat_recipPoly,52    recipRat_recipPoly, RatFunc.num_div_denom]53 54/-- `v(q^k) = q^{-k}` for integer `k`. -/55private theorem recipRat_zpow_X (k : ℤ) :56    recipRat ((RatFunc.X : RatFunc ℚ) ^ k) = (RatFunc.X : RatFunc ℚ) ^ (-k) := by57  rw [map_zpow₀, recipRat_X, zpow_neg, inv_zpow]58 59/-- `ψ_δ` on a monomial: `q ↦ q^δ` on the coefficient and `Z_{e,f} ↦ Z_{e,δf}` on the type. -/60theorem adamsCoef_single (δ : ℕ) (σ : FactorType) (f : RatFunc ℚ) :61    adamsCoef δ (AddMonoidAlgebra.single σ f) =62      AddMonoidAlgebra.single (scaleType δ σ) (adamsRat δ f) := by63  simp [adamsCoef, AddMonoidAlgebra.mapRingHom_single, scaleTypeHom]64  rfl65 66/-- `v` on a monomial acts on the coefficient only. -/67theorem recipCoef_single (σ : FactorType) (f : RatFunc ℚ) :68    recipCoef (AddMonoidAlgebra.single σ f) = AddMonoidAlgebra.single σ (recipRat f) := by69  simp [recipCoef, AddMonoidAlgebra.mapRingHom_single]70 71/-- `ψ_δ` on scalars is `q ↦ q^δ`. -/72theorem adamsCoef_scalar (δ : ℕ) (f : RatFunc ℚ) :73    adamsCoef δ (scalar f) = scalar (adamsRat δ f) := by74  simp only [scalar, adamsCoef_single, scaleType, Multiset.map_zero]75 76/-- `v` on scalars is `q ↦ q⁻¹`. -/77theorem recipCoef_scalar (f : RatFunc ℚ) : recipCoef (scalar f) = scalar (recipRat f) :=78  recipCoef_single 0 f79 80/-- `v` on coefficients: `(v x)_σ = v(x_σ)`. -/81theorem recipCoef_coeff (x : Coef) (σ : FactorType) :82    (recipCoef x).coeff σ = recipRat (x.coeff σ) := by83  simp [recipCoef, AddMonoidAlgebra.coeff_mapRingHom]84 85private theorem coef_ringHom_ext {F G : Coef →+* Coef}86    (h : ∀ σ g, F (AddMonoidAlgebra.single σ g) = G (AddMonoidAlgebra.single σ g)) (y : Coef) :87    F y = G y :=88  DFunLike.congr_fun (AddMonoidAlgebra.ringHom_ext (fun r ↦ h 0 r) (fun m ↦ h m 1)) y89 90/-- `v` is an involution of `Coef`. -/91theorem recipCoef_recipCoef (x : Coef) : recipCoef (recipCoef x) = x :=92  coef_ringHom_ext (F := recipCoef.comp recipCoef) (G := RingHom.id _) (fun σ g ↦ by93    simp only [RingHom.comp_apply, recipCoef_single, recipRat_recipRat, RingHom.id_apply]) x94 95/-- `v` commutes with the Adams operations on `Coef`. -/96theorem recipCoef_adamsCoef (δ : ℕ) (hδ : 0 < δ) (x : Coef) :97    recipCoef (adamsCoef δ x) = adamsCoef δ (recipCoef x) :=98  coef_ringHom_ext (F := recipCoef.comp (adamsCoef δ)) (G := (adamsCoef δ).comp recipCoef)99    (fun σ g ↦ by100      simp only [RingHom.comp_apply, recipCoef_single, adamsCoef_single, adamsRat_recipRat δ hδ]) x101 102/-- `ψ_δ ∘ ψ_k = ψ_{δk}` on `Coef`. -/103theorem adamsCoef_adamsCoef (δ k : ℕ) (hδ : 0 < δ) (hk : 0 < k) (x : Coef) :104    adamsCoef δ (adamsCoef k x) = adamsCoef (δ * k) x :=105  coef_ringHom_ext (F := (adamsCoef δ).comp (adamsCoef k)) (G := adamsCoef (δ * k))106    (fun σ g ↦ by107      simp only [RingHom.comp_apply, adamsCoef_single, adamsRat_adamsRat δ k hδ hk, scaleType,108        Multiset.map_map, Function.comp_def, mul_assoc]) x109 110/-- `ψ_1` is the identity of `Coef`. -/111theorem adamsCoef_one (x : Coef) : adamsCoef 1 x = x :=112  coef_ringHom_ext (F := adamsCoef 1) (G := RingHom.id _) (fun σ g ↦ by113    simp [adamsCoef_single, adamsRat_one, scaleType]) x114 115/-- `scalar : ℚ(q) → Coef` is multiplicative. -/116theorem scalar_mul (f g : RatFunc ℚ) : scalar (f * g) = scalar f * scalar g := by117  simp only [scalar, AddMonoidAlgebra.single_mul_single, add_zero]118 119/-- `scalar : ℚ(q) → Coef` is additive. -/120theorem scalar_add (f g : RatFunc ℚ) : scalar (f + g) = scalar f + scalar g :=121  AddMonoidAlgebra.single_add _ _ _122 123/-- `scalar 1 = 1`. -/124theorem scalar_one : scalar 1 = 1 := rfl125 126/-- `scalar` is the algebra map `ℚ(q) → Coef`. -/127theorem scalar_eq_algebraMap (f : RatFunc ℚ) : scalar f = algebraMap (RatFunc ℚ) Coef f := by128  ext i129  simp [scalar, AddMonoidAlgebra.coe_algebraMap]130 131/-- Multiplication by `scalar r` is the `ℚ(q)`-scalar action. -/132theorem scalar_mul_eq_smul (r : RatFunc ℚ) (x : Coef) : scalar r * x = r • x := by133  rw [scalar_eq_algebraMap, Algebra.smul_def]134 135/-- The `ℚ`-scalar action on `Coef` is multiplication by the constant scalar. -/136theorem rat_smul_eq_scalar_mul (q : ℚ) (x : Coef) : q • x = scalar (RatFunc.C q) * x := by137  rw [scalar_eq_algebraMap, Algebra.smul_def,138    IsScalarTower.algebraMap_apply ℚ (RatFunc ℚ) Coef, eq_ratCast (algebraMap ℚ _) q,139    eq_ratCast RatFunc.C q]140 141/-- `v(q^j) = q^{-j}`. -/142private theorem recipCoef_qpow (j : ℤ) : recipCoef (qpow j) = qpow (-j) := by143  rw [qpow, recipCoef_scalar, recipRat_zpow_X, qpow]144 145/-- `ψ_δ(q^j) = q^{δj}`. -/146private theorem adamsCoef_qpow (δ : ℕ) (hδ : 0 < δ) (j : ℤ) :147    adamsCoef δ (qpow j) = qpow ((δ : ℤ) * j) := by148  rw [qpow, adamsCoef_scalar, adamsRat_zpow_X δ hδ, qpow]149 150/-- `q^n` for natural `n` is the scalar `X^n`. -/151theorem qpow_natCast (n : ℕ) : qpow (n : ℤ) = scalar ((RatFunc.X : RatFunc ℚ) ^ n) := by152  simp [qpow]153 154/-- `q^1` is the scalar `X`. -/155theorem qpow_one : qpow 1 = scalar (RatFunc.X : RatFunc ℚ) := by simp [qpow]156 157/-- `q^{-j} q^j = 1`. -/158theorem qpow_neg_mul_qpow (j : ℤ) : qpow (-j) * qpow j = 1 := by159  rw [← qpow_add, neg_add_cancel, qpow_zero]160 161/-! ### The twisted product on contact series -/162 163/-- Positivity (vanishing on the axes away from `(0,0)`) is preserved by the twisted product. -/164theorem QPositive.qmul {U V : QSer} (hU : QPositive U) (hV : QPositive V) :165    QPositive (qmul U V) := by166  intro c h hc hn167  refine Finset.sum_eq_zero fun p hp ↦ Finset.sum_eq_zero fun r hr ↦ ?_168  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp hr169  have : U p.1 r.1 * V p.2 r.2 = 0 := by170    rcases hc with rfl | rfl171    · by_cases h1 : r.1 = 0172      · have : r.2 ≠ 0 := by omega173        have : p.1 = 0 := by omega174        have : p.2 = 0 := by omega175        rw [hV p.2 r.2 (Or.inl ‹_›) (by omega), mul_zero]176      · rw [hU p.1 r.1 (Or.inl (by omega)) (by omega), zero_mul]177    · by_cases h1 : p.1 = 0178      · have : p.2 ≠ 0 := by omega179        rw [hV p.2 r.2 (Or.inr (by omega)) (by omega), mul_zero]180      · rw [hU p.1 r.1 (Or.inr (by omega)) (by omega), zero_mul]181  rw [this, mul_zero]182 183/-- Positivity is preserved by `†`. -/184theorem QPositive.qdagger {U : QSer} (hU : QPositive U) : QPositive (qdagger U) :=185  fun c h hc hn ↦ by simp [SurfaceBlowup.qdagger, hU c h hc hn]186 187/-- Positivity is preserved by `ι₊`. -/188theorem QPositive.qplus {U : QSer} (hU : QPositive U) : QPositive (qplus U) := by189  intro c k hc hn190  unfold SurfaceBlowup.qplus191  split_ifs with h1192  · rw [hU c (k - c) (by omega) (by omega), mul_zero]193  · rfl194 195/-- Positivity is preserved by `ι₋`. -/196theorem QPositive.qminus {U : QSer} (hU : QPositive U) : QPositive (qminus U) := by197  intro k h hc hn198  unfold SurfaceBlowup.qminus199  split_ifs with h1200  · rw [hU (k - h) h (by omega) (by omega), mul_zero]201  · rfl202 203/-- The diagonal substitution of a series is positive. -/204theorem qPositive_qdiag (f : Ser) : QPositive (qdiag f) := fun c h hc hn ↦ by205  unfold qdiag206  rw [if_neg (by omega)]207 208/-- The constant term of a twisted product: `(U V)₀₀ = U₀₀ V₀₀`. -/209theorem qmul_zero_zero (U V : QSer) : (qmul U V) 0 0 = U 0 0 * V 0 0 := by210  simp [qmul, qpow_zero]211 212/-! ### Adams operations, `exp` and `log` -/213 214private theorem adamsSer_subst (k : ℕ) (hk : k ≠ 0) (φ : Ser)215    (hφ : PowerSeries.map (adamsCoef k) φ = φ) (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :216    adamsSer k (φ.subst f) = φ.subst (adamsSer k f) := by217  have hs' : PowerSeries.HasSubst (PowerSeries.map (adamsCoef k) f) :=218    PowerSeries.HasSubst.of_constantCoeff_zero' (by219      rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply, PowerSeries.coeff_map,220        PowerSeries.coeff_zero_eq_constantCoeff_apply, hf, map_zero])221  have hm : PowerSeries.map (adamsCoef k) (φ.subst f) =222      φ.subst (PowerSeries.map (adamsCoef k) f) := by223    have := PowerSeries.map_subst (h := adamsCoef k)224      (PowerSeries.HasSubst.of_constantCoeff_zero' hf) φ225    rwa [hφ] at this226  rw [adamsSer, adamsSer, dif_neg hk, dif_neg hk, hm]227  exact PowerSeries.expand_subst k hk hs' φ228 229/-- `ψ_k` on series commutes with the logarithm (`k ≠ 0`, `g(0) = 1`). -/230theorem adamsSer_logSer (k : ℕ) (hk : k ≠ 0) (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :231    adamsSer k (logSer g) = logSer (adamsSer k g) := by232  rw [logSer, logSer, PowerSeries.logOf_eq, PowerSeries.logOf_eq,233    adamsSer_subst k hk _ (PowerSeries.map_log _) _ (by simp [hg]), adamsSer_sub k hk,234    adamsSer_one k hk]235 236/-- Reindexing a double divisor sum: pairs `(k, j)` with `k ∣ n`, `j ∣ n/k` correspond to pairs237`(m, k)` with `m ∣ n`, `k ∣ m` via `m = kj`. -/238theorem sum_divisors_sum_divisors_div {M : Type*} [AddCommMonoid M] (n : ℕ)239    (F : ℕ → ℕ → M) :240    ∑ k ∈ n.divisors, ∑ j ∈ (n / k).divisors, F k j241      = ∑ m ∈ n.divisors, ∑ k ∈ m.divisors, F k (m / k) := by242  rw [Finset.sum_sigma', Finset.sum_sigma']243  refine Finset.sum_bij' (fun x _ ↦ ⟨x.1 * x.2, x.1⟩) (fun y _ ↦ ⟨y.2, y.1 / y.2⟩)244    ?_ ?_ ?_ ?_ ?_245  · rintro ⟨k, j⟩ h246    simp only [Finset.mem_sigma, Nat.mem_divisors] at h ⊢247    obtain ⟨⟨hk, hn⟩, hj, hnk⟩ := h248    refine ⟨⟨?_, hn⟩, Dvd.intro _ rfl, ?_⟩249    · obtain ⟨a, ha⟩ := hj250      exact ⟨a, by rw [mul_assoc, ← ha, Nat.mul_div_cancel' hk]⟩251    · have hk0 : k ≠ 0 := by rintro rfl; exact hn (zero_dvd_iff.1 hk)252      have hj0 : j ≠ 0 := by rintro rfl; exact hnk (zero_dvd_iff.1 hj)253      exact mul_ne_zero hk0 hj0254  · rintro ⟨m, k⟩ h255    simp only [Finset.mem_sigma, Nat.mem_divisors] at h ⊢256    obtain ⟨⟨hm, hn⟩, hk, hm0⟩ := h257    refine ⟨⟨dvd_trans hk hm, hn⟩, ?_, ?_⟩258    · obtain ⟨a, ha⟩ := hm259      obtain ⟨b, hb⟩ := hk260      have hk0 : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; exact hm0 (by simpa using hb))261      refine ⟨a, ?_⟩262      rw [ha, hb, mul_assoc, Nat.mul_div_cancel_left _ hk0, Nat.mul_div_cancel_left _ hk0]263    · have hk0 : 0 < k := Nat.pos_of_dvd_of_pos hk (Nat.pos_of_ne_zero hm0)264      have := Nat.div_pos (Nat.le_of_dvd (Nat.pos_of_ne_zero hn) (dvd_trans hk hm)) hk0265      omega266  · rintro ⟨k, j⟩ h267    simp only [Finset.mem_sigma, Nat.mem_divisors] at h268    have hk0 : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at h)269    simp [Nat.mul_div_cancel_left _ hk0]270  · rintro ⟨m, k⟩ h271    simp only [Finset.mem_sigma, Nat.mem_divisors] at h272    simp [Nat.mul_div_cancel' h.2.1]273  · rintro ⟨k, j⟩ h274    simp only [Finset.mem_sigma, Nat.mem_divisors] at h275    have hk0 : 0 < k := Nat.pos_of_ne_zero (by rintro rfl; simp at h)276    simp [Nat.mul_div_cancel_left _ hk0]277 278/-- The divisor transform `[xⁿ] ↦ Σ_{k ∣ n} w(k) ψ_k([x^{n/k}] f)`. -/279private def divisorTransform (w : ℕ → ℚ) (f : Ser) : Ser :=280  PowerSeries.mk fun n ↦ ∑ k ∈ n.divisors, w k • adamsCoef k (PowerSeries.coeff (n / k) f)281 282private theorem plethSum_eq (f : Ser) : plethSum f = divisorTransform (fun k ↦ (k : ℚ)⁻¹) f := rfl283 284private theorem moebiusSum_eq (f : Ser) :285    moebiusSum f = divisorTransform (fun k ↦ ((ArithmeticFunction.moebius k : ℤ) : ℚ) / k) f :=286  rfl287 288private theorem coeff_divisorTransform_comp (a b : ℕ → ℚ) (f : Ser) (n : ℕ) :289    PowerSeries.coeff n (divisorTransform a (divisorTransform b f)) =290      ∑ m ∈ n.divisors, (∑ k ∈ m.divisors, a k * b (m / k)) •291        adamsCoef m (PowerSeries.coeff (n / m) f) := by292  simp only [divisorTransform, PowerSeries.coeff_mk, map_sum, map_rat_smul, Finset.smul_sum]293  have h1 : ∀ k ∈ n.divisors, ∀ j ∈ (n / k).divisors,294      a k • b j • adamsCoef k (adamsCoef j (PowerSeries.coeff (n / k / j) f))295        = (fun k j ↦ (a k * b j) • adamsCoef (k * j) (PowerSeries.coeff (n / (k * j)) f)) k j := by296    intro k hk j hj297    have hk0 : 0 < k := Nat.pos_of_mem_divisors hk298    have hj0 : 0 < j := Nat.pos_of_mem_divisors hj299    simp only [smul_smul, adamsCoef_adamsCoef k j hk0 hj0, Nat.div_div_eq_div_mul]300  rw [Finset.sum_congr rfl fun k hk ↦ Finset.sum_congr rfl (h1 k hk),301    sum_divisors_sum_divisors_div]302  refine Finset.sum_congr rfl fun m hm ↦ ?_303  rw [Finset.sum_smul]304  refine Finset.sum_congr rfl fun k hk ↦ ?_305  rw [Nat.mul_div_cancel' (Nat.dvd_of_mem_divisors hk)]306 307/-- `Σ_{k ∣ m} μ(k)` is `1` for `m = 1` and `0` otherwise. -/308theorem sum_divisors_moebius (m : ℕ) :309    ∑ k ∈ m.divisors, ((ArithmeticFunction.moebius k : ℤ) : ℚ) = if m = 1 then 1 else 0 := by310  have := congrArg (fun F ↦ F m) (ArithmeticFunction.moebius_mul_coe_zeta)311  simp only [ArithmeticFunction.coe_mul_zeta_apply, ArithmeticFunction.one_apply] at this312  rw [← Int.cast_sum, this]313  split_ifs <;> simp314 315private theorem divisorTransform_inv (a b : ℕ → ℚ) (f : Ser) (hf : PowerSeries.constantCoeff f = 0)316    (hab : ∀ m, ∑ k ∈ m.divisors, a k * b (m / k) = if m = 1 then 1 else 0) :317    divisorTransform a (divisorTransform b f) = f := by318  ext n319  rw [coeff_divisorTransform_comp]320  rcases Nat.eq_zero_or_pos n with rfl | hn321  · simp [hf]322  · simp only [hab, ite_smul, one_smul, zero_smul]323    rw [Finset.sum_ite_eq']324    simp [Nat.ne_of_gt hn, adamsCoef_one]325 326private theorem moebius_weight_left (m : ℕ) :327    ∑ k ∈ m.divisors, (((ArithmeticFunction.moebius k : ℤ) : ℚ) / (k : ℚ)) * ((m / k : ℕ) : ℚ)⁻¹328      = if m = 1 then 1 else 0 := by329  rcases Nat.eq_zero_or_pos m with rfl | hm330  · simp331  have : ∀ k ∈ m.divisors,332      (((ArithmeticFunction.moebius k : ℤ) : ℚ) / (k : ℚ)) * ((m / k : ℕ) : ℚ)⁻¹333      = ((ArithmeticFunction.moebius k : ℤ) : ℚ) * (m : ℚ)⁻¹ := by334    intro k hk335    have hk0 : (k : ℚ) ≠ 0 := by exact_mod_cast (Nat.pos_of_mem_divisors hk).ne'336    rw [Nat.cast_div (Nat.dvd_of_mem_divisors hk) hk0]337    have : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne'338    field_simp339  rw [Finset.sum_congr rfl this, ← Finset.sum_mul, sum_divisors_moebius]340  split_ifs with h <;> simp [h]341 342private theorem moebius_weight_right (m : ℕ) :343    ∑ k ∈ m.divisors,344      ((k : ℚ))⁻¹ * (((ArithmeticFunction.moebius (m / k) : ℤ) : ℚ) / ((m / k : ℕ) : ℚ))345      = if m = 1 then 1 else 0 := by346  rcases Nat.eq_zero_or_pos m with rfl | hm347  · simp348  have : ∀ k ∈ m.divisors,349      ((k : ℚ))⁻¹ * (((ArithmeticFunction.moebius (m / k) : ℤ) : ℚ) / ((m / k : ℕ) : ℚ))350      = ((ArithmeticFunction.moebius (m / k) : ℤ) : ℚ) * (m : ℚ)⁻¹ := by351    intro k hk352    have hk0 : (k : ℚ) ≠ 0 := by exact_mod_cast (Nat.pos_of_mem_divisors hk).ne'353    rw [Nat.cast_div (Nat.dvd_of_mem_divisors hk) hk0]354    have : (m : ℚ) ≠ 0 := by exact_mod_cast hm.ne'355    field_simp356  rw [Finset.sum_congr rfl this, ← Finset.sum_mul,357    Nat.sum_div_divisors m (fun k ↦ ((ArithmeticFunction.moebius k : ℤ) : ℚ)),358    sum_divisors_moebius]359  split_ifs with h <;> simp [h]360 361/-- Möbius inversion: `moebiusSum (plethSum f) = f` for `f(0) = 0`. -/362theorem moebiusSum_plethSum (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :(7.6)363    moebiusSum (plethSum f) = f :=364  divisorTransform_inv _ _ f hf moebius_weight_left365 366/-- Möbius inversion: `plethSum (moebiusSum f) = f` for `f(0) = 0`. -/367theorem plethSum_moebiusSum (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :368    plethSum (moebiusSum f) = f :=369  divisorTransform_inv _ _ f hf moebius_weight_right370 371/-- `plethSum` is additive. -/372theorem plethSum_add (f g : Ser) : plethSum (f + g) = plethSum f + plethSum g := by373  ext n; simp [plethSum, Finset.sum_add_distrib]374 375/-- `plethSum f` has constant term `0`. -/376theorem constantCoeff_plethSum (f : Ser) : PowerSeries.constantCoeff (plethSum f) = 0 := by377  rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]; simp [plethSum]378 379/-- `moebiusSum f` has constant term `0`. -/380theorem constantCoeff_moebiusSum (f : Ser) : PowerSeries.constantCoeff (moebiusSum f) = 0 := by381  rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply]; simp [moebiusSum]382 383/-! ### The projective normalizer -/384 385private theorem fraction_pow_var (i : ℕ) :386    (Expr.pow Expr.var i).fraction = ((Polynomial.X : Polynomial ℚ) ^ i, 1) := by387  induction i with388  | zero => simp [Expr.pow, Expr.fraction]389  | succ k ih => simp [Expr.pow, Expr.fraction, ih, pow_succ]390 391private theorem fraction_sum_pow_var (L : List ℕ) :392    (Expr.sum (L.map fun i ↦ Expr.pow Expr.var i)).fraction393      = ((L.map fun i ↦ (Polynomial.X : Polynomial ℚ) ^ i).sum, 1) := by394  induction L with395  | nil => simp [Expr.sum, Expr.fraction]396  | cons a L ih =>397    simp only [List.map_cons, Expr.sum, List.foldr_cons] at ih ⊢398    rw [Expr.fraction, ih, fraction_pow_var]399    simp400 401/-- The projective normalizer is `[n+1]_q = 1 + q + ⋯ + qⁿ`. -/402private theorem rational_projectiveNormalizer (n : ℕ) :403    (projectiveNormalizer n).rational =404      ∑ i ∈ Finset.range (n + 1), (RatFunc.X : RatFunc ℚ) ^ i := by405  unfold projectiveNormalizer Expr.rational406  rw [fraction_sum_pow_var]407  simp only [map_one, div_one]408  have e (m : ℕ) (f : ℕ → Polynomial ℚ) :409      ((List.range m).map f).sum = ∑ i ∈ Finset.range m, f i := by410    induction m with411    | zero => simp412    | succ k ih =>413      rw [List.range_succ, List.map_append, List.sum_append, ih, Finset.sum_range_succ]; simp414  rw [e, map_sum]415  simp [map_pow, RatFunc.algebraMap_X]416 417/-- `v([n+1]_q) = q⁻ⁿ [n+1]_q`. -/418theorem recipRat_projectiveNormalizer (n : ℕ) :Lemma 9.2419    recipRat (projectiveNormalizer n).rational =420      (RatFunc.X ^ n)⁻¹ * (projectiveNormalizer n).rational := by421  rw [rational_projectiveNormalizer, map_sum]422  simp only [map_pow, recipRat_X, inv_pow]423  rw [← Finset.sum_range_reflect, Finset.mul_sum]424  refine Finset.sum_congr rfl fun i hi ↦ ?_425  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.lt_succ_iff.mp (Finset.mem_range.mp hi))426  rw [show i + k + 1 - 1 - i = k by omega, pow_add]427  have : (RatFunc.X : RatFunc ℚ) ^ i ≠ 0 := pow_ne_zero _ RatFunc.X_ne_zero428  field_simp429 430/-- The projective normalizer is a nonzero rational function. -/431theorem projectiveNormalizer_rational_ne_zero (n : ℕ) : (projectiveNormalizer n).rational ≠ 0 := by432  have : ∑ i ∈ Finset.range (n + 1), (RatFunc.X : RatFunc ℚ) ^ i = algebraMap (Polynomial ℚ)433      (RatFunc ℚ) (∑ i ∈ Finset.range (n + 1), (Polynomial.X : Polynomial ℚ) ^ i) := by434    simp [map_sum, RatFunc.algebraMap_X]435  rw [rational_projectiveNormalizer, this]436  refine RatFunc.algebraMap_ne_zero fun h ↦ ?_437  have := congrArg (fun p ↦ Polynomial.coeff p 0) h438  simp [Polynomial.finsetSum_coeff, Polynomial.coeff_X_pow] at this439 440/-! ### Reciprocal substitution and the quantum torus -/441 442/-- Conjugating `ρ(U)` by the reciprocal substitution gives `ρ̄(v U)`. -/443theorem recipSer_qact (U : QSer) (f : Ser) :444    recipSer (qact U f) = qactRecip (qrecip U) (recipSer f) := by445  refine PowerSeries.ext fun n ↦ ?_446  simp only [recipSer, qact, qactRecip, qrecip, PowerSeries.coeff_map, PowerSeries.coeff_mk,447    map_sum, map_mul, recipCoef_qpow]448  refine Finset.sum_congr rfl fun p _ ↦ Finset.sum_congr rfl fun r _ ↦ ?_449  congr 2; ring450 451/-- `†` is an anti-homomorphism of the twisted product. -/452theorem qdagger_qmul (U V : QSer) : qdagger (qmul U V) = qmul (qdagger V) (qdagger U) := byLemma 8.1453  funext c h454  simp only [qdagger, qmul, map_sum, map_mul, recipCoef_qpow, Finset.mul_sum]455  rw [← Finset.Nat.sum_antidiagonal_swap]456  refine Finset.sum_congr rfl fun p hp ↦ ?_457  rw [← Finset.Nat.sum_antidiagonal_swap]458  refine Finset.sum_congr rfl fun r hr ↦ ?_459  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp hr460  subst hp hr461  simp only [Prod.fst_swap, Prod.snd_swap, neg_neg]462  have e : qpow ((((p.1 + p.2 : ℕ) : ℤ) + ((r.1 + r.2 : ℕ) : ℤ) -463        ((p.1 + p.2 : ℕ) : ℤ) * ((r.1 + r.2 : ℕ) : ℤ))) * qpow ((p.2 : ℤ) * (r.1 : ℤ)) =464      qpow (-((p.1 : ℤ) * (r.2 : ℤ))) * (qpow ((p.1 : ℤ) + (r.1 : ℤ) - (p.1 : ℤ) * (r.1 : ℤ)) *465        qpow ((p.2 : ℤ) + (r.2 : ℤ) - (p.2 : ℤ) * (r.2 : ℤ))) := by466    rw [← qpow_add, ← qpow_add, ← qpow_add]467    congr 1468    push_cast469    ring470  linear_combination (recipCoef (U p.2 r.2) * recipCoef (V p.1 r.1)) * e471 472private theorem qdagger_twist (c k : ℕ) (x : Coef) (hck : c ≤ k) :473    qpow ((c : ℤ) + k - c * k) * (recipCoef (qpow (-(chooseTwo c : ℤ)) * x)) =474      qpow (-(chooseTwo c : ℤ)) *475        (qpow (((c : ℤ) + ((k - c : ℕ) : ℤ)) - c * ((k - c : ℕ) : ℤ)) * recipCoef x) := by476  rw [map_mul, recipCoef_qpow, neg_neg, ← mul_assoc, ← mul_assoc, ← qpow_add, ← qpow_add]477  have := two_mul_chooseTwo c478  congr 2479  push_cast [Nat.cast_sub hck]480  linarith481 482/-- `†` commutes with `ι₊`. -/483theorem qdagger_qplus (U : QSer) : qdagger (qplus U) = qplus (qdagger U) := byLemma 8.1484  funext c k485  simp only [qdagger, qplus]486  split_ifs with h487  · exact qdagger_twist c k _ h488  · simp489 490/-- `†` commutes with `ι₋`. -/491theorem qdagger_qminus (U : QSer) : qdagger (qminus U) = qminus (qdagger U) := byLemma 8.1492  funext k h493  simp only [qdagger, qminus]494  split_ifs with hh495  · rw [show ((k : ℤ) + h - k * h) = ((h : ℤ) + k - h * k) by ring,496      show (((k - h : ℕ) : ℤ) + h - ((k - h : ℕ) : ℤ) * h) =497        ((h : ℤ) + ((k - h : ℕ) : ℤ)) - h * ((k - h : ℕ) : ℤ) by ring]498    exact qdagger_twist h k (U (k - h) h) hh499  · simp500 501private theorem sum_antidiagonal_assoc (n : ℕ) (F : ℕ → ℕ → ℕ → Coef) :502    ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.1,503      F q.1 q.2 p.2 =504    ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.2,505      F p.1 q.1 q.2 := by506  rw [Finset.sum_sigma', Finset.sum_sigma']507  refine Finset.sum_bij' (fun x _ ↦ ⟨(x.2.1, x.2.2 + x.1.2), (x.2.2, x.1.2)⟩)508    (fun x _ ↦ ⟨(x.1.1 + x.2.1, x.2.2), (x.1.1, x.2.1)⟩) ?_ ?_ ?_ ?_ ?_509  all_goals rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ hx510  all_goals simp only [Finset.mem_sigma, Finset.HasAntidiagonal.mem_antidiagonal] at hx ⊢511  all_goals first512    | rfl513    | (constructor <;> first | trivial | omega)514    | (obtain ⟨h1, h2⟩ := hx; subst h2; simp)515 516/-- The twisted product is associative. -/517theorem qmul_assoc (U V W : QSer) :Lemma 8.1518    qmul (qmul U V) W = qmul U (qmul V W) := by519  funext c h520  let K : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Coef := fun a b e x y z ↦521    qpow (-((a : ℤ) * (y : ℤ)) - (a : ℤ) * (z : ℤ) - (b : ℤ) * (z : ℤ)) *522      (U a x * (V b y * W e z))523  have hL : qmul (qmul U V) W c h = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal c,524      ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.1,525      (fun a b e ↦ ∑ r ∈ Finset.HasAntidiagonal.antidiagonal h,526        ∑ s ∈ Finset.HasAntidiagonal.antidiagonal r.1, K a b e s.1 s.2 r.2) q.1 q.2 p.2 := by527    simp only [qmul, Finset.sum_mul, Finset.mul_sum]528    refine Finset.sum_congr rfl (fun p hp ↦ ?_)529    rw [Finset.sum_comm]530    refine Finset.sum_congr rfl (fun q hq' ↦ ?_)531    refine Finset.sum_congr rfl (fun r hr ↦ ?_)532    refine Finset.sum_congr rfl (fun s hs ↦ ?_)533    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hq'534    simp only [K]535    rw [show -((q.1 : ℤ) * (s.2 : ℤ)) - (q.1 : ℤ) * (r.2 : ℤ) - (q.2 : ℤ) * (r.2 : ℤ)536        = -((p.1 : ℤ) * (r.2 : ℤ)) + -((q.1 : ℤ) * (s.2 : ℤ)) by rw [← hq']; push_cast; ring,537      qpow_add]538    ring539  have hR : qmul U (qmul V W) c h = ∑ p ∈ Finset.HasAntidiagonal.antidiagonal c,540      ∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.2,541      (fun a b e ↦ ∑ r ∈ Finset.HasAntidiagonal.antidiagonal h,542        ∑ s ∈ Finset.HasAntidiagonal.antidiagonal r.2, K a b e r.1 s.1 s.2) p.1 q.1 q.2 := by543    simp only [qmul, Finset.mul_sum]544    refine Finset.sum_congr rfl (fun p hp ↦ ?_)545    rw [Finset.sum_comm]546    refine Finset.sum_congr rfl (fun q hq' ↦ ?_)547    refine Finset.sum_congr rfl (fun r hr ↦ ?_)548    refine Finset.sum_congr rfl (fun s hs ↦ ?_)549    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hs550    simp only [K, ← hs]551    rw [mul_left_comm (U _ _), ← mul_assoc, ← qpow_add, Nat.cast_add]552    congr 2; ring553  rw [hL, hR]554  refine (sum_antidiagonal_assoc c (fun a b e ↦ ∑ r ∈ Finset.HasAntidiagonal.antidiagonal h,555    ∑ s ∈ Finset.HasAntidiagonal.antidiagonal r.1, K a b e s.1 s.2 r.2)).trans ?_556  refine Finset.sum_congr rfl (fun p _ ↦ Finset.sum_congr rfl (fun q _ ↦ ?_))557  exact sum_antidiagonal_assoc h (fun x y z ↦ K p.1 q.1 q.2 x y z)558 559/-! ### Reciprocal substitution and dilations on series -/560 561/-- `recipSer` acts coefficientwise: `[xⁿ] fᵛ = v([xⁿ] f)`. -/562theorem coeff_recipSer (f : Ser) (n : ℕ) :563    PowerSeries.coeff n (recipSer f) = recipCoef (PowerSeries.coeff n f) :=564  PowerSeries.coeff_map _ _ _565 566/-- `recipSer` is multiplicative. -/567theorem recipSer_mul (f g : Ser) : recipSer (f * g) = recipSer f * recipSer g := map_mul _ f g568 569/-- `recipSer` is additive on differences. -/570private theorem recipSer_sub (f g : Ser) : recipSer571    (f - g) = recipSer f - recipSer g := map_sub _ f g572 573/-- `recipSer 1 = 1`. -/574private theorem recipSer_one : recipSer (1 : Ser) = 1 := map_one _575 576/-- `recipSer` is semilinear over `recipCoef`. -/577private theorem recipSer_C_mul (a : Coef) (f : Ser) :578    recipSer (PowerSeries.C a * f) = PowerSeries.C (recipCoef a) * recipSer f := by579  rw [recipSer, map_mul, PowerSeries.map_C]; rfl580 581/-- `recipSer` is an involution. -/582theorem recipSer_recipSer (f : Ser) : recipSer (recipSer f) = f := by583  ext m; simp [coeff_recipSer, recipCoef_recipCoef]584 585private theorem scalar_X_pow (m : ℕ) : (scalar (RatFunc.X : RatFunc ℚ)) ^ m = qpow (m : ℤ) := by586  simp [scalar, qpow, AddMonoidAlgebra.single_pow, zpow_natCast]587 588private theorem scalar_X_inv_pow (m : ℕ) :589    (scalar (RatFunc.X : RatFunc ℚ)⁻¹) ^ m = qpow (-(m : ℤ)) := by590  simp [scalar, qpow, AddMonoidAlgebra.single_pow, zpow_neg, zpow_natCast, inv_pow]591 592private theorem scalar_X_mul_scalar_X_inv :593    scalar (RatFunc.X : RatFunc ℚ) * scalar (RatFunc.X : RatFunc ℚ)⁻¹ = 1 := by594  rw [← scalar_mul, mul_inv_cancel₀ RatFunc.X_ne_zero, scalar_one]595 596private theorem rescale_C (a b : Coef) :597    PowerSeries.rescale b (PowerSeries.C a) = PowerSeries.C a := by598  ext m599  simp only [PowerSeries.coeff_rescale, PowerSeries.coeff_C]600  split_ifs with h <;> simp [h]601 602/-- `[xⁿ] S f = qⁿ [xⁿ] f`. -/603theorem coeff_dilate (f : Ser) (n : ℕ) :604    PowerSeries.coeff n (dilate f) = qpow (n : ℤ) * PowerSeries.coeff n f := by605  simp [dilate, PowerSeries.coeff_rescale, scalar_X_pow]606 607/-- `[xⁿ] S⁻¹ f = q⁻ⁿ [xⁿ] f`. -/608theorem coeff_codilate (f : Ser) (n : ℕ) :609    PowerSeries.coeff n (codilate f) = qpow (-(n : ℤ)) * PowerSeries.coeff n f := by610  simp [codilate, PowerSeries.coeff_rescale, scalar_X_inv_pow]611 612/-- The dilation is multiplicative. -/613theorem dilate_mul (f g : Ser) : dilate (f * g) = dilate f * dilate g := map_mul _ _ _614 615/-- The dilation is linear over `Coef`. -/616private theorem dilate_C_mul (a : Coef) (f : Ser) :617    dilate (PowerSeries.C a * f) = PowerSeries.C a * dilate f := by618  simp only [dilate, map_mul, rescale_C]619 620/-- `S⁻¹ ∘ S = id`. -/621theorem codilate_dilate (f : Ser) : codilate (dilate f) = f := by622  simp only [dilate, codilate, PowerSeries.rescale_rescale, scalar_X_mul_scalar_X_inv,623    PowerSeries.rescale_one, RingHom.id_apply]624 625/-- `S ∘ S⁻¹ = id`. -/626theorem dilate_codilate (f : Ser) : dilate (codilate f) = f := by627  simp only [dilate, codilate, PowerSeries.rescale_rescale, mul_comm (scalar RatFunc.X⁻¹),628    scalar_X_mul_scalar_X_inv, PowerSeries.rescale_one, RingHom.id_apply]629 630/-- The reciprocal substitution conjugates `S` to `S⁻¹`. -/631theorem recipSer_dilate (f : Ser) : recipSer (dilate f) = codilate (recipSer f) := by632  ext m633  rw [coeff_recipSer, coeff_dilate, coeff_codilate, coeff_recipSer, map_mul, recipCoef_qpow]634 635/-- The dilation preserves congruence through degree `n`. -/636theorem SCongr.dilate {n : ℕ} {f g : Ser} (h : SCongr n f g) :637    SCongr n (SurfaceBlowup.dilate f) (SurfaceBlowup.dilate g) := fun m hm ↦ by638  rw [coeff_dilate, coeff_dilate, h m hm]639 640private theorem rescale_subst (r : Coef) (h f : Ser) (hf : PowerSeries.constantCoeff f = 0) :641    PowerSeries.rescale r (h.subst f) = h.subst (PowerSeries.rescale r f) := by642  rw [PowerSeries.rescale_eq_subst, PowerSeries.rescale_eq_subst,643    PowerSeries.subst_comp_subst_apply (PowerSeries.HasSubst.of_constantCoeff_zero' hf)644      (PowerSeries.HasSubst.smul_X' r)]645 646private theorem constantCoeff_codilate (f : Ser) :647    PowerSeries.constantCoeff (codilate f) = PowerSeries.constantCoeff f := by648  rw [← PowerSeries.coeff_zero_eq_constantCoeff_apply,649    ← PowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_codilate]650  simp [qpow_zero]651 652private theorem dilate_expSer (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :653    dilate (expSer f) = expSer (dilate f) :=654  rescale_subst _ _ _ hf655 656private theorem dilate_logSer (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :657    dilate (logSer g) = logSer (dilate g) := by658  rw [logSer, logSer, PowerSeries.logOf_eq, PowerSeries.logOf_eq, dilate,659    rescale_subst _ _ _ (by simp [hg]), map_sub, map_one]660  rfl661 662private theorem dilate_divisorTransform (w : ℕ → ℚ) (f : Ser) :663    dilate (divisorTransform w f) = divisorTransform w (dilate f) := by664  refine PowerSeries.ext fun n ↦ ?_665  simp only [coeff_dilate, divisorTransform, PowerSeries.coeff_mk, Finset.mul_sum]666  refine Finset.sum_congr rfl fun k hk ↦ ?_667  rw [map_mul, adamsCoef_qpow k (Nat.pos_of_mem_divisors hk), mul_smul_comm,668    ← Nat.cast_mul, Nat.mul_div_cancel' (Nat.dvd_of_mem_divisors hk)]669 670private theorem dilate_pLog (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :671    dilate (pLog g) = pLog (dilate g) := by672  rw [pLog, pLog, ← dilate_logSer g hg]673  exact dilate_divisorTransform _ _674 675/-- The dilation commutes with the plethystic powers `P_w` (for `g(0) = 1`). -/676theorem dilate_pPow (w : RatFunc ℚ) (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :(7.6)677    dilate (pPow w g) = pPow w (dilate g) := by678  rw [pPow, pPow, pExp, pExp, dilate_expSer _ (constantCoeff_plethSum _), plethSum_eq,679    plethSum_eq, dilate_divisorTransform, dilate_C_mul, dilate_pLog g hg]680 681/-- The inverse dilation commutes with the plethystic powers `P_w` (for `g(0) = 1`). -/682theorem codilate_pPow (w : RatFunc ℚ) (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :683    codilate (pPow w g) = pPow w (codilate g) := by684  conv_lhs => rw [← dilate_codilate g]685  rw [← dilate_pPow w _ (by rw [constantCoeff_codilate, hg]), codilate_dilate]686 687/-! ### The Gauss twist -/688 689/-- The reciprocal substitution conjugates `Φ` to `Φ⁻¹`. -/690theorem recipSer_gaussPhi (f : Ser) : recipSer (gaussPhi f) = gaussPhiInv (recipSer f) := by691  ext n692  simp only [gaussPhi, gaussPhiInv, coeff_recipSer, PowerSeries.coeff_mk, map_mul,693    recipCoef_qpow, neg_neg]694 695/-- `Φ` commutes with the dilation. -/696theorem gaussPhi_dilate (f : Ser) : gaussPhi (dilate f) = dilate (gaussPhi f) := by697  ext n : 1698  simp only [gaussPhi, coeff_dilate, PowerSeries.coeff_mk, mul_left_comm]699 700/-- `Φ` is additive on differences. -/701theorem gaussPhi_sub (f g : Ser) : gaussPhi (f - g) = gaussPhi f - gaussPhi g := by702  ext n703  simp only [gaussPhi, map_sub, mul_sub, PowerSeries.coeff_mk]704 705/-- For symmetric `V`, the Gauss twist conjugates `ρ̄(v V)` to `S⁻¹ ∘ ρ(V†) ∘ S`. -/706theorem gaussPhi_qactRecip_gaussPhiInv (V : QSer) (hV : ∀ c h : ℕ, V c h = V h c) (f : Ser) :Lemma 9.1707    gaussPhi (qactRecip (qrecip V) (gaussPhiInv f)) = codilate (qact (qdagger V) (dilate f)) := by708  have hL (a b c : ℤ) (x y : Coef) :709      qpow a * (qpow b * (x * (qpow c * y))) = qpow (a + b + c) * (x * y) := by710    rw [qpow_add, qpow_add]; ring711  have hR (a b c d : ℤ) (x y : Coef) :712      qpow a * (qpow b * (qpow c * x * (qpow d * y))) = qpow (a + b + c + d) * (x * y) := by713    rw [qpow_add, qpow_add, qpow_add]; ring714  refine PowerSeries.ext fun n ↦ ?_715  rw [coeff_codilate]716  simp only [gaussPhi, gaussPhiInv, qactRecip, qact, qrecip, qdagger, PowerSeries.coeff_mk,717    coeff_dilate]718  rw [Finset.mul_sum, Finset.mul_sum]719  refine Finset.sum_congr rfl fun p hp ↦ ?_720  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp721  rw [← Finset.Nat.sum_antidiagonal_swap, Finset.mul_sum, Finset.mul_sum]722  refine Finset.sum_congr rfl fun r hr ↦ ?_723  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hr724  simp only [Prod.fst_swap, Prod.snd_swap]725  rw [hV r.2 r.1, hL, hR]726  congr 2727  have e1 := two_mul_tri (r.1 + r.2 + p.2)728  have e2 := two_mul_tri r.1729  have e3 := two_mul_tri r.2730  have e4 := two_mul_tri p.2731  have hn : n = r.1 + r.2 + p.2 := by omega732  subst hn733  push_cast at e1 ⊢734  linarith735 736/-! ### Diagonal substitution -/737 738/-- Diagonal substitution `x ↦ E_{1,1}` is multiplicative into the quantum torus. -/739theorem qdiag_mul (f g : Ser) : qdiag (f * g) = qmul (qdiag f) (qdiag g) := byLemma 8.1740  funext c h741  simp only [qmul, qdiag]742  by_cases hch : c = h743  · subst hch744    rw [if_pos rfl, PowerSeries.coeff_mul, Finset.mul_sum]745    refine Finset.sum_congr rfl fun p hp ↦ ?_746    rw [Finset.sum_eq_single p]747    · rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp748      simp only [if_true]749      rw [← hp, show (-(((chooseTwo (p.1 + p.2) : ℕ) : ℤ))) =750        -((p.1 : ℤ) * p.2) + (-(chooseTwo p.1 : ℤ) + -(chooseTwo p.2 : ℤ)) by751          rw [chooseTwo_add]; ring,752        qpow_add, qpow_add]753      ring754    · intro r _ hr755      by_cases h1 : p.1 = r.1756      · have h2 : p.2 ≠ r.2 := fun h2 ↦ hr (Prod.ext h1.symm h2.symm)757        simp [h2]758      · simp [h1]759    · intro hp'; exact absurd hp hp'760  · rw [if_neg hch]761    symm762    refine Finset.sum_eq_zero fun p hp ↦ Finset.sum_eq_zero fun r hr ↦ ?_763    rw [Finset.HasAntidiagonal.mem_antidiagonal] at hp hr764    by_cases h1 : p.1 = r.1765    · have h2 : p.2 ≠ r.2 := by omega766      simp [h2]767    · simp [h1]768 769/-- Diagonal substitution sends `1` to the unit `E_{0,0}`. -/770private theorem qdiag_one : qdiag 1 = qone := by771  funext c h772  simp only [qdiag, qone, PowerSeries.coeff_one]773  by_cases hch : c = h774  · subst hch775    rcases eq_or_ne c 0 with rfl | hc776    · simp [chooseTwo, qpow_zero]777    · simp [hc]778  · simp only [if_neg hch]779    split_ifs with h' <;> first | rfl | omega780 781/-- `qdiag(f)† = qdiag(S(v f))`. -/782private theorem qdagger_qdiag (f : Ser) : qdagger (qdiag f) = qdiag (dilate (recipSer f)) := by783  funext c h784  simp only [qdagger, qdiag]785  by_cases hch : c = h786  · subst hch787    simp only [if_true, map_mul, recipCoef_qpow, coeff_dilate, coeff_recipSer]788    have e := two_mul_chooseTwo c789    rw [← mul_assoc, ← mul_assoc, ← qpow_add, ← qpow_add]790    congr 2791    linarith792  · simp [hch]793 794/-- If `S(v P_s) P_s ≡ 1` through degree `M`, then `qdiag(P_s) qdiag(P_s)† ≡ 1` through total795degree `2M + 1`. -/796theorem qcongr_qdiag_mul_qdagger (M s : ℕ)Lemma 8.3797    (h : SCongr M (dilate (recipSer (eulerSer (-1) s)) * eulerSer (-1) s) 1) :798    QCongr (2 * M + 1) (qmul (qdiag (eulerSer (-1) s)) (qdagger (qdiag (eulerSer (-1) s))))799      qone := by800  rw [qdagger_qdiag, ← qdiag_mul, mul_comm (eulerSer (-1) s), ← qdiag_one]801  exact h.qdiag802 803/-- The reciprocal substitution commutes with the plethystic powers, twisting the exponent by804`q ↦ q⁻¹`: `P_w(g)ᵛ = P_{v(w)}(gᵛ)` for `g(0) = 1`. -/805theorem recipSer_pPow (w : RatFunc ℚ) (g : Ser) (hg : PowerSeries.constantCoeff g = 1) :(7.6)806    recipSer (pPow w g) = pPow (recipRat w) (recipSer g) := by807  have hexp (f : Ser) (hf : PowerSeries.constantCoeff f = 0) :808      recipSer (expSer f) = expSer (recipSer f) :=809    (PowerSeries.map_subst (PowerSeries.HasSubst.of_constantCoeff_zero' hf)810      (PowerSeries.exp Coef)).trans (by rw [PowerSeries.map_exp]; rfl)811  have hlog : recipSer (logSer g) = logSer (recipSer g) := by812    have h1 : recipSer (g - 1) = recipSer g - 1 := by rw [recipSer_sub, recipSer_one]813    unfold recipSer at h1 ⊢814    rw [logSer, logSer, PowerSeries.logOf_eq, PowerSeries.logOf_eq, ← h1]815    exact (PowerSeries.map_subst (PowerSeries.HasSubst.of_constantCoeff_zero' (by simp [hg]))816      (PowerSeries.log Coef)).trans (by rw [PowerSeries.map_log]; rfl)817  have hdt (u : ℕ → ℚ) (f : Ser) :818      recipSer (divisorTransform u f) = divisorTransform u (recipSer f) := by819    refine PowerSeries.ext fun n ↦ ?_820    simp only [coeff_recipSer, divisorTransform, PowerSeries.coeff_mk, map_sum, map_rat_smul]821    exact Finset.sum_congr rfl fun k hk ↦ by822      rw [recipCoef_adamsCoef k (Nat.pos_of_mem_divisors hk)]823  rw [pPow, pPow, pExp, pExp, hexp _ (constantCoeff_plethSum _), plethSum_eq, plethSum_eq, hdt,824    recipSer_C_mul, recipCoef_scalar, pLog, pLog, moebiusSum_eq, moebiusSum_eq, hdt, hlog]825 826/-! ### Scalars and congruences of series -/827 828/-- Multiplication by a nonzero scalar `scalar w` is injective on `Coef`. -/829theorem scalar_mul_left_cancel {w : RatFunc ℚ} (hw : w ≠ 0) {x y : Coef}830    (h : scalar w * x = scalar w * y) : x = y := by831  have := congrArg (scalar w⁻¹ * ·) h832  simp only [← mul_assoc, ← scalar_mul, inv_mul_cancel₀ hw, scalar_one, one_mul] at this833  exact this834 835/-- `scalar w * x = 0` forces `x = 0` when `w ≠ 0`. -/836theorem eq_zero_of_scalar_mul_eq_zero {w : RatFunc ℚ} (hw : w ≠ 0) {x : Coef}837    (h : scalar w * x = 0) : x = 0 :=838  scalar_mul_left_cancel hw (by rw [h, mul_zero])839 840/-- Congruence of series is reflexive. -/841@[refl] theorem SCongr.refl (n : ℕ) (f : Ser) : SCongr n f f := fun _ _ ↦ rfl842 843/-- Equal series are congruent. -/844theorem SCongr.of_eq {n : ℕ} {f g : Ser} (h : f = g) : SCongr n f g := h ▸ SCongr.refl n f845 846/-- Congruence of series is symmetric. -/847theorem SCongr.symm {n : ℕ} {f g : Ser} (h : SCongr n f g) : SCongr n g f :=848  fun i hi ↦ (h i hi).symm849 850/-- Congruence of series is transitive. -/851theorem SCongr.trans {n : ℕ} {f g u : Ser} (h : SCongr n f g) (h' : SCongr n g u) :852    SCongr n f u :=853  fun i hi ↦ (h i hi).trans (h' i hi)854 855/-- Congruence through degree `n` implies congruence through any `m ≤ n`. -/856theorem SCongr.mono {n m : ℕ} {f g : Ser} (h : SCongr n f g) (hmn : m ≤ n) : SCongr m f g :=857  fun i hi ↦ h i (hi.trans hmn)858 859/-- Congruence of series is compatible with multiplication. -/860theorem SCongr.mul {n : ℕ} {f g u v : Ser} (h : SCongr n f g) (h' : SCongr n u v) :861    SCongr n (f * u) (g * v) := by862  intro i hi863  rw [PowerSeries.coeff_mul, PowerSeries.coeff_mul]864  refine Finset.sum_congr rfl fun x hx ↦ ?_865  rw [Finset.HasAntidiagonal.mem_antidiagonal] at hx866  rw [h x.1 (by omega), h' x.2 (by omega)]867 868/-- Congruence of series is compatible with multiplication by a constant. -/869theorem SCongr.C_mul {n : ℕ} {f g : Ser} (h : SCongr n f g) (a : Coef) :870    SCongr n (PowerSeries.C a * f) (PowerSeries.C a * g) := fun i hi ↦ by871  rw [PowerSeries.coeff_C_mul, PowerSeries.coeff_C_mul, h i hi]872 873/-- Congruence of series is compatible with powers. -/874theorem SCongr.pow {n : ℕ} {f g : Ser} (h : SCongr n f g) (p : ℕ) : SCongr n (f ^ p) (g ^ p) := by875  induction p with876  | zero => exact SCongr.refl n 1877  | succ p ih => rw [pow_succ, pow_succ]; exact ih.mul h878 879/-- Congruences can be cancelled by a series with constant term `1`. -/880theorem SCongr.of_mul_right {n : ℕ} {f g u : Ser} (hu : PowerSeries.constantCoeff u = 1)881    (h : SCongr n (f * u) (g * u)) : SCongr n f g := by882  obtain ⟨v, hv⟩ :=883    (PowerSeries.isUnit_iff_constantCoeff.mpr (by rw [hu]; exact isUnit_one)).exists_right_inv884  simpa [mul_assoc, hv] using h.mul (SCongr.refl n v)885 886private theorem scongr_subst (n : ℕ) (a : Ser) (f g : Ser)887    (hf : PowerSeries.constantCoeff f = 0) (hg : PowerSeries.constantCoeff g = 0)888    (h : SCongr n f g) : SCongr n (a.subst f) (a.subst g) := by889  have ht : PowerSeries.trunc (n+1) f = PowerSeries.trunc (n+1) g := by890    refine Polynomial.ext fun m ↦ ?_891    rw [PowerSeries.coeff_trunc, PowerSeries.coeff_trunc]892    split_ifs with hm893    · exact h m (by omega)894    · rfl895  intro m hm896  rw [PowerSeries.coeff_subst' (PowerSeries.HasSubst.of_constantCoeff_zero' hf),897    PowerSeries.coeff_subst' (PowerSeries.HasSubst.of_constantCoeff_zero' hg)]898  congr 1899  funext d900  congr 1901  have h1 := PowerSeries.trunc_trunc_pow f (n+1) d902  have h2 := PowerSeries.trunc_trunc_pow g (n+1) d903  rw [ht] at h1904  have := congrArg (fun p ↦ Polynomial.coeff p m) (h1.symm.trans h2)905  simpa [PowerSeries.coeff_trunc, show m < n + 1 by omega] using this906 907/-- `exp` preserves congruence through degree `n` (on series with zero constant term). -/908theorem SCongr.expSer {n : ℕ} {f g : Ser} (hf : PowerSeries.constantCoeff f = 0)909    (hg : PowerSeries.constantCoeff g = 0) (h : SCongr n f g) :910    SCongr n (SurfaceBlowup.expSer f) (SurfaceBlowup.expSer g) :=911  scongr_subst n (PowerSeries.exp Coef) f g hf hg h912 913/-- `log` preserves congruence through degree `n` (on series with constant term `1`). -/914theorem SCongr.logSer {n : ℕ} {u v : Ser} (hu : PowerSeries.constantCoeff u = 1)915    (hv : PowerSeries.constantCoeff v = 1) (huv : SCongr n u v) :916    SCongr n (SurfaceBlowup.logSer u) (SurfaceBlowup.logSer v) :=917  scongr_subst n (PowerSeries.log Coef) (u - 1) (v - 1) (by simp [hu]) (by simp [hv])918    fun m hm ↦ by simp [huv m hm]919 920end SurfaceBlowup