Ideal-chart atlases and atlas independence of the state measure

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.Blowup.PointTransport7import SurfaceBlowup.Measure.Normalizer8import SurfaceBlowup.Measure.StateVolumes9 10/-!11# Ideal-chart atlases and atlas independence of the state measure12 13A division chart parametrizes the residue-ideal cell of a generator `f` by the coordinate ideals14`(f + π Σ zᵢ bᵢ)`. We show that this parametrization is a bijection onto the cell, that the15transition map between two charts of the same cell is a congruence-preserving bijection and hence16preserves Haar measure, and conclude that the pushforward chart measures, and so the state measure17of an ideal atlas, do not depend on the choice of charts. We also record how strict transforms and18coordinate ideals decompose over finite products.19 20## Main results21 22* `pi_strict_transform_map_eval`, `product_chart_projection`: principal ideals, strict transforms23  and coordinate ideals over a finite product are computed componentwise.24* `coordinate_ideal_cell_bijection`: a division chart is a bijection onto its residue-ideal cell.25* `ideal_chart_transition_haar`: chart transitions preserve Haar measure on `O^n`.26* `ideal_chart_pushforward_independent`, `state_measure_atlas_independent`: the chart measures,27  hence the state measure, do not depend on the choice of charts.28 29Provenance: `Thm_SurfaceBlowupV2_*`: `pi_strict_transform_map_eval`, `product_chart_projection`,30`coordinate_ideal_{surjective, cell_bijection}`, `coordinate_transition_{ideal_identity, inverse,31congruence_iff, measure_preserving}`, `ideal_chart_transition_haar`,32`division_chart_preimage_image_measurable`, `ideal_chart_pushforward_independent`,33`state_measure_atlas_independent`.34-/35 36open scoped BigOperators ENNReal37 38namespace SurfaceBlowup39 40/-- Over a finite product `Π C_j`, principal ideals and strict transforms are computed41  componentwise. -/42theorem pi_strict_transform_map_eval (O : Type) [CommRing O] (R : Type) [CommRing R] [Algebra O R]43    (ι : Type) [Finite ι] (C : ι → Type) [∀ j, CommRing (C j)] [∀ j, Algebra O (C j)]44    (alpha : ∀ j, R →ₐ[O] C j) (e g : ∀ j, C j) (d : ℕ) (J : Ideal R) :45    (∀ x : ∀ j, C j, x ∈ Ideal.span {g} ↔ ∀ j, x j ∈ Ideal.span {g j}) ∧46      (∀ j, (Ideal.span {g}).map (Pi.evalRingHom C j) = Ideal.span {g j}) ∧47      (∀ x : ∀ j, C j, x ∈ strictTransformIdeal (AlgHom.pi alpha) e d J ↔ ∀ j,48      x j ∈ strictTransformIdeal (alpha j) (e j) d J) ∧ ∀ j,49      (strictTransformIdeal (AlgHom.pi alpha) e d J).map (Pi.evalRingHom C j) =50      strictTransformIdeal (alpha j) (e j) d J := by51  have := Fintype.ofFinite ι52  classical53  have hmap : ∀ j, (J.map (AlgHom.pi alpha).toRingHom).map (Pi.evalRingHom C j)54      = J.map (alpha j).toRingHom := fun j ↦ by rw [Ideal.map_map]; rfl55  have hpi := (pi_ideal_mem_iff_map_eval ι C (J.map (AlgHom.pi alpha).toRingHom)).156  have key : ∀ x : ∀ j, C j, x ∈ strictTransformIdeal (AlgHom.pi alpha) e d J ↔57      ∀ j, x j ∈ strictTransformIdeal (alpha j) (e j) d J := by58    intro x59    simp only [strictTransformIdeal, Submodule.mem_colon_singleton, Algebra.smul_def]60    rw [hpi]61    exact forall_congr' fun j ↦ by rw [hmap j]; simp62  refine ⟨fun x ↦ by rw [← Ideal.pi_span, Ideal.mem_pi], fun j ↦ by rw [principal_ideal_image]; rfl,63    key, fun j ↦ le_antisymm (Ideal.map_le_iff_le_comap.2 fun x hx ↦ (key x).1 hx j) fun y hy ↦ ?_⟩64  have : (Pi.single j y : ∀ j, C j) ∈ strictTransformIdeal (AlgHom.pi alpha) e d J :=65    (key _).2 fun k ↦ by66      by_cases h : k = j67      · subst h; simpa using hy68      · simp [Pi.single_eq_of_ne h]69  simpa using Ideal.mem_map_of_mem (Pi.evalRingHom C j) this70 71/-- A coordinate ideal of a product chart projects to the coordinate ideals of the component charts,72  membership is componentwise, and the chart is injective when all component charts are. -/73theorem product_chart_projection (O : Type) [CommRing O] (ι : Type) [Finite ι] (Oj : ι → Type)74    [∀ j, CommRing (Oj j)] [∀ j, Algebra O (Oj j)] (R : ι → Type) [∀ j, CommRing (R j)]75    [∀ j, Algebra O (R j)] [∀ j, Algebra (Oj j) (R j)] [∀ j, IsScalarTower O (Oj j) (R j)]76    (nn : ι → ℕ) (n : ℕ) (ρ : (Fin n → O) ≃ₗ[O] (∀ j, Fin (nn j) → Oj j))77    (bc' : ∀ j, Fin (nn j) → R j) (bc : Fin n → ∀ j, R j)78    (hcompat : ∀ (w : Fin n → O) (j : ι), coordinateLift bc w j = coordinateLift (bc' j) (ρ w j))79    (g : ∀ j, R j) (pi : O) (pij : ∀ j, Oj j) (hpi : ∀ j, algebraMap O (Oj j) pi = pij j) :80    (∀ (w : Fin n → O) (j : ι), (coordinateIdeal pi g bc w).map (Pi.evalRingHom R j) =81      coordinateIdeal (pij j) (g j) (bc' j) (ρ w j)) ∧82      (∀ (w : Fin n → O) (x : ∀ j, R j), x ∈ coordinateIdeal pi g bc w ↔ ∀ j,83      x j ∈ coordinateIdeal (pij j) (g j) (bc' j) (ρ w j)) ∧84      ((∀ j, Function.Injective (coordinateIdeal (pij j) (g j) (bc' j))) →85      Function.Injective (coordinateIdeal pi g bc)) := by86  have key : ∀ (w : Fin n → O) (j : ι),87      (g + coordinateLift bc (pi • w)) j = g j + coordinateLift (bc' j) (pij j • ρ w j) := by88    intro w j89    simp only [coordinateLift_smul_eq_mul, ← Algebra.smul_def]90    rw [← hpi, algebraMap_smul, Pi.add_apply, Pi.smul_apply, hcompat]91  have proj : ∀ (w : Fin n → O) (j : ι), (coordinateIdeal pi g bc w).map (Pi.evalRingHom R j) =92      coordinateIdeal (pij j) (g j) (bc' j) (ρ w j) := fun w j ↦93    (principal_ideal_image _ _ _ _).trans (congrArg (fun y ↦ Ideal.span {y}) (key w j))94  refine ⟨proj, fun w x ↦ ?_, fun hinj w w' h ↦ ρ.injective <| funext fun j ↦95    hinj j <| by rw [← proj, ← proj, h]⟩96  refine ((pi_strict_transform_map_eval O O ι R (fun j ↦ Algebra.ofId O (R j)) 097    (g + coordinateLift bc (pi • w)) 0 ⊥).1 x).trans (forall_congr' fun j ↦ ?_)98  rw [key]99  rfl100 101/-- Every ideal in the residue-ideal cell of `f` is a coordinate ideal of the division chart. -/102private theorem coordinate_ideal_surjective (O R : Type) [CommRing O] [CommRing R] [Algebra O R]103    (n : ℕ)104    (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))105    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] [IsDomain R] [IsLocalRing R]106    (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (f : R)107    (hE : ∀ s, E.symm s = divisionMap f b s)108    (hf : Function.Injective109      (fun x : R ⧸ Ideal.span {algebraMap O R pi} => x *110      Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))111    (J : Ideal R) (hJ : J ∈ residueIdealCell (algebraMap O R pi) f) :112    ∃ z : Fin n → O, coordinateIdeal pi f b z = J := by113  obtain ⟨h, rfl⟩ := residue_ideal_has_fixed_generator_lift R114    (algebraMap O R pi) f hpm hf J hJ115  refine ⟨(generatorNormalForm pi b E h).1, ?_⟩116  have key := normalizer_generator_equation O R n pi b E f hE h117  obtain ⟨u, hu⟩ := normalizing_factor_is_unit O R pi hpm118    (generatorNormalForm pi b E h).2119  unfold coordinateIdeal normalizedIdeal normalizedGenerator120  simp only [coordinateLift_smul_eq_mul, ← Algebra.smul_def]121  rw [← key, ← hu, principal_ideal_unit_invariance]122 123/-- The coordinate-ideal map of a division chart is a bijection onto the residue-ideal cell of124`f`. -/125theorem coordinate_ideal_cell_bijection (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)Proposition 3.2126    (pi : O) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))127    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] [IsDomain R] [IsLocalRing R]128    (hp0 : algebraMap O R pi ≠ 0) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (f : R)129    (hE : ∀ s, E.symm s = divisionMap f b s)130    (hf : Function.Injective131      (fun x : R ⧸ Ideal.span {algebraMap O R pi} => x *132      Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))133    :134    Function.Injective (coordinateIdeal pi f b) ∧ Set.range (coordinateIdeal pi f b) =135      residueIdealCell (algebraMap O R pi) f := by136  refine ⟨coordinate_ideal_injective O R n pi b E hp0 hpm f hE hf, Set.ext fun J ↦137    ⟨?_, coordinate_ideal_surjective O R n pi b E hpm f hE hf J⟩⟩138  rintro ⟨z, rfl⟩139  exact coordinate_ideal_in_residue_cell O R n pi b f z140 141/-- The transition map between two division charts of the same cell intertwines their142  coordinate-ideal maps. -/143private theorem coordinate_transition_ideal_identity (O R : Type) [CommRing O] [CommRing R]144    [Algebra O R]145    (n : ℕ) (pi : O) (b : Fin n → R)146    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] [IsLocalRing R]147    (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (f g : R) (c : Fin n → R)148    (F : R ≃ₗ[O] ((Fin n → O) × R)) (hF : ∀ s, F.symm s = divisionMap g c s) (h0 : R)149    (hfg : f = g + pi • h0) (z : Fin n → O) :150    coordinateIdeal pi g c (idealTransition pi b c F h0 z) = coordinateIdeal pi f b z := by151  have key := normalizer_generator_equation O R n pi c F g hF152    (h0 + coordinateLift b z)153  have hu := normalizing_factor_is_unit O R pi hpm154    (generatorNormalForm pi c F (h0 + coordinateLift b z)).2155  have hinv := principal_ideal_unit_invariance R156    (g + pi • coordinateLift c (generatorNormalForm pi c F (h0 + coordinateLift b z)).1) hu.unit157  simp only [coordinateIdeal, normalizedIdeal, normalizedGenerator, idealTransition,158    coordinateLift_smul_eq_mul, ← Algebra.smul_def]159  rw [← hinv, IsUnit.unit_spec, key, hfg, smul_add, add_assoc]160 161/-! ### Transition maps between two division charts of one cell -/162 163section Transition164 165variable (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ) (pi : O) (b : Fin n → R)166  (E : R ≃ₗ[O] ((Fin n → O) × R)) [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)]167  [IsDomain R] [IsLocalRing R] (hp0 : algebraMap O R pi ≠ 0)168  (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (f : R)169  (hE : ∀ s, E.symm s = divisionMap f b s)170  (hf : Function.Injective (fun x : R ⧸ Ideal.span {algebraMap O R pi} =>171    x * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f))172  (g : R) (c : Fin n → R) (F : R ≃ₗ[O] ((Fin n → O) × R)) (hF : ∀ s, F.symm s = divisionMap g c s)173  (hg : Function.Injective (fun x : R ⧸ Ideal.span {algebraMap O R pi} =>174    x * Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g))175  (h0 : R) (hfg : f = g + pi • h0)176 177include hp0 hpm hE hf hF hg hfg178 179/-- The coordinate transition map between two charts of the same cell is inverted by the reverse180  transition. -/181private theorem coordinate_transition_inverse :182    Function.LeftInverse (idealTransition pi c b E (-h0)) (idealTransition pi b c F h0) ∧183      Function.RightInverse (idealTransition pi c b E (-h0)) (idealTransition pi b c F h0) := by184  have hgf : g = f + pi • (-h0) := by rw [hfg, smul_neg]; abel185  have hfg' := coordinate_transition_ideal_identity O R n pi b hpm f g c F hF h0 hfg186  have hgf' := coordinate_transition_ideal_identity O R n pi c hpm g f b E hE (-h0) hgf187  exact ⟨fun z ↦ coordinate_ideal_injective O R n pi b E hp0 hpm f hE hf (by rw [hgf', hfg']),188    fun z ↦ coordinate_ideal_injective O R n pi c F hp0 hpm g hF hg (by rw [hfg', hgf'])⟩189 190/-- The coordinate transition map preserves and reflects congruence modulo `(π)^j`. -/191private theorem coordinate_transition_congruence_iff (j : ℕ) (z w : Fin n → O) :192    adicCongr (Ideal.span {pi}) j (idealTransition pi b c F h0 z) (idealTransition pi b c F h0 w) ↔193      adicCongr (Ideal.span {pi}) j z w := by194  refine ⟨fun h ↦ ?_, coordinate_transition_congruence O R n pi b c F h0 j z w⟩195  have hinv := (coordinate_transition_inverse O R n pi b E hp0 hpm f hE hf g c F hF hg h0 hfg).1196  simpa only [hinv z, hinv w] using coordinate_transition_congruence O R n pi c b E (-h0) j _ _ h197 198/-- The coordinate transition map preserves any probability measure that gives all `π`-adic balls of199  a given radius equal mass. -/200private theorem coordinate_transition_measure_preserving [MeasurableSpace (Fin n → O)]201    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))202    (mu : MeasureTheory.Measure (Fin n → O)) [MeasureTheory.IsProbabilityMeasure mu]203    (hball : ∀ j (x y : Fin n → O), mu {z | adicCongr (Ideal.span {pi}) j z x} =204      mu {z | adicCongr (Ideal.span {pi}) j z y}) :205    MeasureTheory.MeasurePreserving (idealTransition pi b c F h0) mu mu :=206  congruence_bijection_measure_preserving O (Fin n → O) (Ideal.span {pi}) hgen _207    (coordinate_transition_inverse O R n pi b E hp0 hpm f hE hf g c F hF hg h0 hfg).2.surjective208    (coordinate_transition_congruence_iff O R n pi b E hp0 hpm f hE hf g c F hF hg h0 hfg) mu hball209 210variable [IsDomain O] [IsDiscreteValuationRing O]211  [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]212  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]213  [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]214 215/-- The coordinate transition map preserves the Haar probability measure on `O^n`. -/216theorem ideal_chart_transition_haar (htop : IsAdic (IsLocalRing.maximalIdeal O))Proposition 3.2217    (hpi : Irreducible pi) :218    MeasureTheory.MeasurePreserving (idealTransition pi b c F h0) (coefficientMeasure O n)219      (coefficientMeasure O n) := by220  have := coefficient_measure_probability O htop n221  have hm : IsLocalRing.maximalIdeal O = Ideal.span {pi} :=222    (IsDiscreteValuationRing.irreducible_iff_uniformizer pi).mp hpi223  exact coordinate_transition_measure_preserving O R n pi b E hp0 hpm f hE hf g c F hF hg h0 hfg224    (finite_coordinate_borel_cylinders O (Ideal.span {pi}) (hm ▸ htop) n) _ fun j x y ↦ by225      rw [coefficient_uniformizer_cylinder_mass O htop n pi hpi j x,226        coefficient_uniformizer_cylinder_mass O htop n pi hpi j y]227 228/-- Two division charts of the same residue-ideal cell push Haar measure forward to the same measure229  on ideals. -/230theorem ideal_chart_pushforward_independent (htop : IsAdic (IsLocalRing.maximalIdeal O))Proposition 3.2231    (hpi : Irreducible pi) [MeasurableSpace (Ideal R)] (hc : Measurable (coordinateIdeal pi g c)) :232    (coefficientMeasure O n).map (coordinateIdeal pi f b) =233      (coefficientMeasure O n).map (coordinateIdeal pi g c) := by234  have hT := ideal_chart_transition_haar O R n pi b E hp0 hpm f hE hf g c F hF hg h0 hfg htop hpi235  have hfun : coordinateIdeal pi f b = coordinateIdeal pi g c ∘ idealTransition pi b c F h0 :=236    funext fun z ↦ (coordinate_transition_ideal_identity O R n pi b hpm f g c F hF h0 hfg z).symm237  rw [hfun, ← MeasureTheory.Measure.map_map hc hT.measurable, hT.map_eq]238 239end Transition240 241/-- For two division charts, the preimage under one of the image under the other of a measurable set242  is measurable. -/243theorem division_chart_preimage_image_measurable (O : Type) [CommRing O] [IsDomain O]244    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]245    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]246    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]247    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (R : Type) [CommRing R] [Algebra O R] [IsDomain R]248    [IsLocalRing R] (pi : O) (hpi : Irreducible pi) (hp0 : algebraMap O R pi ≠ 0)249    (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) (n n' : ℕ)250    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] (f g : R) (b : Fin n → R) (c : Fin n' → R)251    (hb : IsDivisionChart O R pi f b) (hc : IsDivisionChart O R pi g c) (S : Set (Fin n' → O))252    (hS : MeasurableSet S) :253    MeasurableSet (coordinateIdeal pi f b ⁻¹' (coordinateIdeal pi g c '' S)) := by254  obtain ⟨E, hE⟩ := hb.1255  by_cases hres : Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) f} =256      Ideal.span {Ideal.Quotient.mk (Ideal.span {algebraMap O R pi}) g}257  · obtain rfl := division_chart_rank_eq_of_residue_ideal_eq O R pi hpi n n' f g b c hb hc hres258    obtain ⟨g', c', F, h₀, hF, hfg, hg', hΨ⟩ :=259      division_chart_same_cell_recenter O R pi hpm n f g b c hb hc hres260    have himg : coordinateIdeal pi g c '' S = coordinateIdeal pi g' c' '' S :=261      Set.image_congr fun z _ ↦ hΨ z262    have hT := (ideal_chart_transition_haar O R n pi b E hp0 hpm f hE hb.2 g' c' F hF hg' h₀263      hfg htop hpi).measurable264    have hfun : coordinateIdeal pi f b = coordinateIdeal pi g' c' ∘ idealTransition pi b c' F h₀ :=265      funext fun z ↦266        (coordinate_transition_ideal_identity O R n pi b hpm f g' c' F hF h₀ hfg z).symm267    rw [himg, hfun, Set.preimage_comp,268      (coordinate_ideal_injective O R n pi c' F hp0 hpm g' hF hg').preimage_image]269    exact hT hS270  · convert MeasurableSet.empty271    rw [Set.eq_empty_iff_forall_notMem]272    rintro z ⟨s, _, hs⟩273    have h2 := coordinate_ideal_in_residue_cell O R n' pi c g s274    rw [hs] at h2275    exact hres ((coordinate_ideal_in_residue_cell O R n pi b f z).2.symm.trans h2.2)276 277/-- The state measure does not depend on the ideal atlas used to define it. -/278theorem state_measure_atlas_independent (O R : Type) [CommRing O] [IsDomain O]Proposition 3.2279    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]280    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]281    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]282    (htop : IsAdic (IsLocalRing.maximalIdeal O)) [CommRing R] [Algebra O R]283    [MeasurableSpace (Ideal R)] (pi : O) (hpi : Irreducible pi) (n : ℕ) (X : Set (Ideal R))284    (A B : IdealAtlas O R pi n X)285    (hB : ∀ j, Measurable (coordinateIdeal pi (B.chart j).f (B.chart j).b)) (e : A.ι ≃ B.ι)286    (hcell : ∀ i, residueIdealCell (algebraMap O R pi) (A.chart i).f =287      residueIdealCell (algebraMap O R pi) (B.chart (e i)).f)288    [IsAdicComplete (Ideal.span {pi}) ((Fin n → O) × R)] [IsDomain R] [IsLocalRing R]289    (hp0 : algebraMap O R pi ≠ 0) (hpm : algebraMap O R pi ∈ IsLocalRing.maximalIdeal R) :290    stateMeasure O R pi n (Nat.card (IsLocalRing.ResidueField O)) A =291      stateMeasure O R pi n (Nat.card (IsLocalRing.ResidueField O)) B := by292  have key : ∀ i, chartMeasure O R pi n (A.chart i) = chartMeasure O R pi n (B.chart (e i)) := by293    intro i294    set f := (A.chart i).f295    set g := (B.chart (e i)).f296    have hmem : Ideal.span {f} ∈ residueIdealCell (algebraMap O R pi) f :=297      ⟨⟨f, rfl⟩, by rw [Ideal.map_span, Set.image_singleton]⟩298    rw [hcell i] at hmem299    have hres := hmem.2300    rw [Ideal.map_span, Set.image_singleton] at hres301    obtain ⟨g', c', F, h₀, hF, hfg, hg', hΨ⟩ :=302      division_data_same_cell_recenter O R pi hpm n f g (B.chart (e i)).b (A.chart i).regular303        (B.chart (e i)).E (B.chart (e i)).division hres304    have hfun : coordinateIdeal pi g (B.chart (e i)).b = coordinateIdeal pi g' c' := funext hΨ305    have hc : Measurable (coordinateIdeal pi g' c') := hfun ▸ hB (e i)306    unfold chartMeasure307    rw [show (B.chart (e i)).f = g from rfl, hfun]308    exact ideal_chart_pushforward_independent O R n pi (A.chart i).b (A.chart i).E hp0 hpm f309      (A.chart i).division (A.chart i).regular g' c' F hF hg' h₀ hfg htop hpi hc310  unfold stateMeasure311  congr 1312  rw [← e.sum_comp]313  exact Finset.sum_congr rfl fun i _ ↦ key i314 315end SurfaceBlowup