Invariance of factor invariants and uniqueness of algebra types

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.Measure.PrimitiveLocus7import SurfaceBlowup.Unramified.FactorCells8 9/-!10# Invariance of factor invariants and uniqueness of algebra types11 12Over a complete DVR `O` with finite residue field and fraction field `K = BaseField O`, the13invariants `(e, f)` of the integral closure of `O` in a finite extension `L/K` depend only on the14`K`-isomorphism class of `L`. Consequences: polynomial types are invariant under normalized15reversal `g ↦ g(0)⁻¹ · reverse g`, algebra types are unique, and a monic `F ∈ O[X]` has polynomial16type `σ` over `K` exactly when `O[X]/(F)` has algebra type `σ`.17 18## Main results19 20* `SurfaceBlowup.field_invariant_algEquiv`, `SurfaceBlowup.factor_invariant_algEquiv`21* `SurfaceBlowup.reverse_normalized_irreducible`, `SurfaceBlowup.reverse_polynomial_type_iff`22* `SurfaceBlowup.algebra_type_unique`, `SurfaceBlowup.polynomial_type_iff_algebra_type`23 24Provenance: Thm_SurfaceBlowupV2_{factor_invariant_algEquiv, reverse_normalized_irreducible,25reverse_polynomial_type_iff, field_invariant_algEquiv, algebra_type_unique,26polynomial_type_iff_algebra_type}.27-/28 29namespace SurfaceBlowup30 31open Polynomial32 33/-! ### Invariance under isomorphism -/34 35/-- The invariants `(e, f)` of the integral closure of `O` in a finite extension `L/K` (assumed36finite over `O`) depend only on the `K`-isomorphism class of `L`. -/37theorem field_invariant_algEquiv (O : Type) [CommRing O] [IsDomain O]38    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]39    [Finite (IsLocalRing.ResidueField O)] (L L' : Type) [Field L] [Field L']40    [Algebra (BaseField O) L] [Algebra O L] [IsScalarTower O (BaseField O) L]41    [FiniteDimensional (BaseField O) L] [Algebra (BaseField O) L'] [Algebra O L']42    [IsScalarTower O (BaseField O) L'] [FiniteDimensional (BaseField O) L']43    (e : L ≃ₐ[BaseField O] L') (hfin : Module.Finite O (integralClosure O L)) :44    fieldInvariant O L = fieldInvariant O L' := by45  obtain ⟨φ, -⟩ := integral_closure_algEquiv O L L' (e.restrictScalars O)46  have : Module.Finite O (integralClosure O L') := .equiv φ.toLinearEquiv47  have h1 := integral_closure_is_local O (BaseField O) L48  have h2 := integral_closure_is_local O (BaseField O) L'49  have := integral_closure_is_dvr O (BaseField O) L50  have := integral_closure_is_dvr O (BaseField O) L'51  obtain ⟨hr, hi⟩ := dvr_algEquiv_ramification_inertia O _ _52    (algebraMap_injective_of_tower O _ L) (algebraMap_injective_of_tower O _ L') φ53  unfold fieldInvariant54  rw [dif_pos h1, dif_pos h2, hr, hi]55 56/-- `K`-isomorphic root fields of monic irreducibles `g, g'` (with finite closure) have the same57factor invariant. -/58theorem factor_invariant_algEquiv (O : Type) [CommRing O] [IsDomain O]59    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]60    [Finite (IsLocalRing.ResidueField O)] (g g' : Polynomial (BaseField O)) (hg : g.Monic)61    (hirr : Irreducible g) (hg' : g'.Monic) (hirr' : Irreducible g')62    (e : AdjoinRoot g ≃ₐ[BaseField O] AdjoinRoot g')63    (hfin : Module.Finite O (integralClosure O (AdjoinRoot g))) :64    factorInvariant O g = factorInvariant O g' := by65  have : Fact (Irreducible g) := ⟨hirr⟩66  have : Fact (Irreducible g') := ⟨hirr'⟩67  have : Module.Finite (BaseField O) (AdjoinRoot g) := hg.finite_adjoinRoot68  have : Module.Finite (BaseField O) (AdjoinRoot g') := hg'.finite_adjoinRoot69  exact field_invariant_algEquiv O _ _ e hfin70 71/-! ### Normalized reversal -/72 73section Reverse74 75variable {K : Type} [Field K]76 77/-- The normalized reversal `f(0)⁻¹ · reverse f`. -/78private noncomputable def rho (f : K[X]) : K[X] := C (f.coeff 0)⁻¹ * f.reverse79 80private theorem rho_mul (f g : K[X]) : rho (f * g) = rho f * rho g := by81  unfold rho82  rw [mul_coeff_zero, reverse_mul_of_domain, mul_inv, C_mul]83  ring84 85private theorem rho_prod (gs : List K[X]) : rho gs.prod = (gs.map rho).prod := by86  induction gs with87  | nil => simp [rho, reverse]88  | cons g gs ih => rw [List.prod_cons, rho_mul, ih, List.map_cons, List.prod_cons]89 90private theorem reverse_reverse_of (f : K[X]) (h0 : f.coeff 0 ≠ 0) : f.reverse.reverse = f := by91  have hd : f.reverse.natDegree = f.natDegree := by92    rw [reverse_natDegree, natTrailingDegree_eq_zero_of_constantCoeff_ne_zero h0, Nat.sub_zero]93  ext n94  rw [coeff_reverse, coeff_reverse, hd, revAt_invol]95 96private theorem rho_coeff_zero {f : K[X]} (hf : f.Monic) : (rho f).coeff 0 = (f.coeff 0)⁻¹ := by97  rw [rho, coeff_C_mul, coeff_zero_reverse, hf.leadingCoeff, mul_one]98 99private theorem rho_rho (f : K[X]) (hf : f.Monic) (h0 : f.coeff 0 ≠ 0) : rho (rho f) = f := by100  rw [rho, rho_coeff_zero hf, inv_inv, rho, reverse_mul_of_domain, reverse_reverse_of f h0,101    show (C (f.coeff 0)⁻¹).reverse = C (f.coeff 0)⁻¹ by simp [reverse], ← mul_assoc, ← C_mul,102    mul_inv_cancel₀ h0, C_1, one_mul]103 104end Reverse105 106/-- For a monic irreducible `g` with `g(0) ≠ 0` and finite closure, its normalized reversal107`h = g(0)⁻¹ · reverse g` is monic irreducible of the same degree with `h(0) = g(0)⁻¹`, has the108same factor invariant and finite closure, and normalized reversal of `h` gives back `g`. -/109theorem reverse_normalized_irreducible (O : Type) [CommRing O] [IsDomain O]110    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]111    [Finite (IsLocalRing.ResidueField O)] (g : Polynomial (BaseField O)) (hg : g.Monic)112    (hgi : Irreducible g) (h0 : g.coeff 0 ≠ 0)113    (hfin : Module.Finite O (integralClosure O (AdjoinRoot g))) :114    (C (g.coeff 0)⁻¹ * g.reverse).Monic115      ∧ Irreducible (C (g.coeff 0)⁻¹ * g.reverse)116      ∧ (C (g.coeff 0)⁻¹ * g.reverse).natDegree = g.natDegree117      ∧ (C (g.coeff 0)⁻¹ * g.reverse).coeff 0 = (g.coeff 0)⁻¹118      ∧ factorInvariant O (C (g.coeff 0)⁻¹ * g.reverse) = factorInvariant O g119      ∧ C ((C (g.coeff 0)⁻¹ * g.reverse).coeff 0)⁻¹ * (C (g.coeff 0)⁻¹ * g.reverse).reverse =120        g121      ∧ Module.Finite O (integralClosure O (AdjoinRoot (C (g.coeff 0)⁻¹ * g.reverse))) := by122  set K := BaseField O123  set c := g.coeff 0124  set h := C c⁻¹ * g.reverse with hh125  have hr : 0 < g.natDegree := natDegree_pos_iff_degree_pos.mpr (degree_pos_of_irreducible hgi)126  have hrevdeg : g.reverse.natDegree = g.natDegree := by127    rw [reverse_natDegree, natTrailingDegree_eq_zero_of_constantCoeff_ne_zero h0, Nat.sub_zero]128  have hdeg : h.natDegree = g.natDegree := by rw [hh, natDegree_C_mul (inv_ne_zero h0), hrevdeg]129  have hmon : h.Monic := by130    rw [Monic, hh, leadingCoeff_mul, leadingCoeff_C, reverse_leadingCoeff,131      trailingCoeff_eq_coeff_zero h0, inv_mul_cancel₀ h0]132  have hcoeff0 : h.coeff 0 = c⁻¹ := rho_coeff_zero hg133  have hgrev : g.reverse = C c * h := by134    rw [hh, ← mul_assoc, ← C_mul, mul_inv_cancel₀ h0, C_1, one_mul]135  -- the root field `K[X]/(h)` is isomorphic to `K[X]/(g)`, via the inverse of the root of `h`136  have hne : h ≠ 0 := hmon.ne_zero137  have : Nontrivial (AdjoinRoot h) := AdjoinRoot.nontrivial h (by138    rw [degree_eq_natDegree hne, hdeg]; exact_mod_cast hr.ne')139  set L := AdjoinRoot h140  set β : L := AdjoinRoot.root h141  have hβ : h.eval₂ (algebraMap K L) β = 0 := AdjoinRoot.eval₂_root h142  have hβinv : β * (-(algebraMap K L c) * (divX h).eval₂ (algebraMap K L) β) = 1 := by143    have e1 := congrArg (fun p ↦ p.eval₂ (algebraMap K L) β) (X_mul_divX_add h)144    simp only [eval₂_add, eval₂_mul, eval₂_X, eval₂_C, hβ, hcoeff0] at e1145    calc β * (-(algebraMap K L c) * (divX h).eval₂ (algebraMap K L) β)146        = -(algebraMap K L c) * (β * (divX h).eval₂ (algebraMap K L) β) := by ring147      _ = algebraMap K L (c * c⁻¹) := by rw [eq_neg_of_add_eq_zero_left e1, map_mul]; ring148      _ = 1 := by rw [mul_inv_cancel₀ h0, map_one]149  let _ : Invertible β := invertibleOfRightInverse _ _ hβinv150  have hgβ : g.eval₂ (algebraMap K L) (⅟β) = 0 := by151    have : Invertible (⅟β) := invertibleInvOf152    rw [← eval₂_reverse_eq_zero_iff, invOf_invOf, hgrev, eval₂_mul, hβ, mul_zero]153  have : Fact (Irreducible g) := ⟨hgi⟩154  let φ : AdjoinRoot g →ₐ[K] L := AdjoinRoot.liftAlgHom g (Algebra.ofId K L) (⅟β) hgβ155  have hinj : Function.Injective φ := φ.toRingHom.injective156  have : FiniteDimensional K (AdjoinRoot g) := (AdjoinRoot.powerBasis hg.ne_zero).finite157  have : FiniteDimensional K L := (AdjoinRoot.powerBasis hne).finite158  have hsurj : Function.Surjective φ :=159    (LinearMap.injective_iff_surjective_of_finrank_eq_finrank (f := φ.toLinearMap) (by160      rw [(AdjoinRoot.powerBasis hg.ne_zero).finrank, AdjoinRoot.powerBasis_dim,161        (AdjoinRoot.powerBasis hne).finrank, AdjoinRoot.powerBasis_dim, hdeg])).mp hinj162  let e : AdjoinRoot g ≃ₐ[K] L := AlgEquiv.ofBijective φ ⟨hinj, hsurj⟩163  have hirr : Irreducible h := (Ideal.irreducible_iff_isMaximal_span_singleton hne).mpr164    (Ideal.Quotient.maximal_of_isField _165      (MulEquiv.isField (Field.toIsField (AdjoinRoot g)) e.symm.toMulEquiv))166  obtain ⟨φ', -⟩ := integral_closure_algEquiv O _ _ (e.restrictScalars O)167  exact ⟨hmon, hirr, hdeg, hcoeff0, (factor_invariant_algEquiv O g h hg hgi hmon hirr e hfin).symm,168    rho_rho g hg h0, .equiv φ'.toLinearEquiv⟩169 170private theorem rev_type_forward (O : Type) [CommRing O] [IsDomain O]171    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]172    [Finite (IsLocalRing.ResidueField O)] (P : Polynomial (BaseField O)) (h0 : P.coeff 0 ≠ 0)173    (τ : FactorType) : HasPolynomialTypeF O P τ → HasPolynomialTypeF O (rho P) τ := by174  rintro ⟨gs, hmem, hpw, hprod, hτ, hfin⟩175  have hg0 : ∀ g ∈ gs, g.coeff 0 ≠ 0 := fun g hg hz ↦ by176    obtain ⟨Q, hQ⟩ := List.dvd_prod hg177    exact h0 (by rw [hprod, hQ, mul_coeff_zero, hz, zero_mul])178  have hrev : ∀ g ∈ gs, _ := fun g hg ↦179    reverse_normalized_irreducible O g (hmem g hg).1 (hmem g hg).2 (hg0 g hg) (hfin g hg)180  refine ⟨gs.map rho, ?_, ?_, by rw [hprod, rho_prod], ?_, ?_⟩181  · simp only [List.mem_map]182    rintro _ ⟨g, hg, rfl⟩183    exact ⟨(hrev g hg).1, (hrev g hg).2.1⟩184  · refine List.Nodup.map_on (fun a ha b hb hab ↦ ?_) hpw185    rw [← (hrev a ha).2.2.2.2.2.1, ← (hrev b hb).2.2.2.2.2.1]186    exact congrArg rho hab187  · rw [hτ, List.map_map]188    exact congrArg _ (List.map_congr_left fun g hg ↦ ((hrev g hg).2.2.2.2.1).symm)189  · simp only [List.mem_map]190    rintro _ ⟨g, hg, rfl⟩191    exact (hrev g hg).2.2.2.2.2.2192 193/-- A monic `P` with `P(0) ≠ 0` has type `τ` iff its normalized reversal does. -/194theorem reverse_polynomial_type_iff (O : Type) [CommRing O] [IsDomain O]195    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]196    [Finite (IsLocalRing.ResidueField O)] (P : Polynomial (BaseField O)) (hP : P.Monic)197    (h0 : P.coeff 0 ≠ 0) (τ : FactorType) :198    HasPolynomialTypeF O P τ ↔ HasPolynomialTypeF O (Polynomial.C (P.coeff 0)⁻¹ * P.reverse) τ :=199  ⟨rev_type_forward O P h0 τ, fun h ↦ rho_rho P hP h0 ▸200    rev_type_forward O (rho P) (by rw [rho_coeff_zero hP]; exact inv_ne_zero h0) τ h⟩201 202/-! ### Uniqueness of algebra types -/203 204/-- A `K`-algebra isomorphism between finite products of fields `∏ Lᵢ ≃ ∏ L'ⱼ` yields an injection205`φ : ι → ι'` with `Lᵢ ≃ L'_{φ i}`. -/206private theorem pi_field_matching (K : Type) [Field K] (ι ι' : Type) [Finite ι] [Finite ι']207    (L : ι → Type) [∀ i, Field (L i)] [∀ i, Algebra K (L i)]208    (L' : ι' → Type) [∀ i, Field (L' i)] [∀ i, Algebra K (L' i)]209    (f : (∀ i, L i) ≃ₐ[K] (∀ j, L' j)) :210    ∃ φ : ι → ι', Function.Injective φ ∧ ∀ i, Nonempty (L i ≃ₐ[K] L' (φ i)) := by211  classical212  have := Fintype.ofFinite ι213  have := Fintype.ofFinite ι'214  have hs : ∀ i, Function.Surjective ((Pi.evalAlgHom K L i).comp f.symm.toAlgHom) :=215    fun i x ↦ ⟨f (Pi.single i x), by simp⟩216  have hker : ∀ i, ∃ j, RingHom.ker ((Pi.evalAlgHom K L i).comp f.symm.toAlgHom) =217      RingHom.ker (Pi.evalAlgHom K L' j) := fun i ↦218    (pi_field_maximal_ideals ι' L' _).1.1 (RingHom.ker_isMaximal_of_surjective _ (hs i))219  choose φ hφ using hker220  refine ⟨φ, fun i i' h ↦ ?_, fun i ↦ ?_⟩221  · have h1 := hφ i222    rw [h] at h1223    apply (pi_field_maximal_ideals ι L ⊥).2 i i'224    ext x225    simpa [RingHom.mem_ker] using Ideal.ext_iff.1 (h1.trans (hφ i').symm) (f x)226  · exact ⟨(Ideal.quotientKerAlgEquivOfSurjective (hs i)).symm.trans227      ((Ideal.quotientEquivAlgOfEq K (hφ i)).trans228        (Ideal.quotientKerAlgEquivOfSurjective fun x ↦ ⟨Pi.single (φ i) x, by simp⟩))⟩229 230/-- The algebra type of an `O`-algebra, if it exists, is unique. -/231theorem algebra_type_unique (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]232    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]233    (B : Type) [CommRing B] [Algebra O B] (σ τ : FactorType) (hσ : HasAlgebraType O B σ)234    (hτ : HasAlgebraType O B τ) : σ = τ := by235  obtain ⟨ι, _, L, _, _, _, _, _, e, rfl, hfinL⟩ := hσ236  obtain ⟨ι', _, L', _, _, _, _, _, e', rfl, -⟩ := hτ237  obtain ⟨φ, hφi, hφ⟩ := pi_field_matching _ ι ι' L L' (e.symm.trans e')238  obtain ⟨ψ, hψi, -⟩ := pi_field_matching _ ι' ι L' L (e'.symm.trans e)239  have hb : Function.Bijective φ := (Fintype.bijective_iff_injective_and_card φ).2240    ⟨hφi, le_antisymm (Fintype.card_le_of_injective φ hφi) (Fintype.card_le_of_injective ψ hψi)⟩241  refine (Finset.sum_congr rfl fun i _ ↦ ?_).trans (Fintype.sum_bijective φ hb _ _ fun _ ↦ rfl)242  obtain ⟨g⟩ := hφ i243  rw [field_invariant_algEquiv O (L i) (L' (φ i)) g (hfinL i)]244 245/-! ### Polynomial types versus algebra types -/246 247private theorem sum_singleton_get {α β : Type} (f : α → β) (l : List α) :248    ∑ i : Fin l.length, ({f (l.get i)} : Multiset β) = ((l.map f : List β) : Multiset β) := by249  induction l with250  | nil => simp251  | cons a l ih =>252    refine (Fin.sum_univ_succ253      (fun i : Fin (l.length + 1) ↦ ({f ((a :: l).get i)} : Multiset β))).trans ?_254    rw [show ∑ i : Fin l.length, ({f ((a :: l).get i.succ)} : Multiset β) = _ from ih]255    rfl256 257private theorem type_forward (O : Type) [CommRing O] [IsDomain O] (F : Polynomial O)258    (σ : FactorType) (h : HasPolynomialTypeF O (F.map (algebraMap O (BaseField O))) σ) :259    HasAlgebraType O (AdjoinRoot F) σ := by260  obtain ⟨gs, hgs, hd, hprod, hσ, hfinG⟩ := h261  obtain ⟨e₁, -⟩ := polynomial_quotient_product_equiv (BaseField O) gs hgs hd262  obtain ⟨e₀, -⟩ := adjoinRoot_base_change O F263  rw [hprod] at e₀264  have : ∀ i : Fin gs.length, Fact (Irreducible (gs.get i)) :=265    fun i ↦ ⟨(hgs _ (List.get_mem gs i)).2⟩266  refine ⟨Fin gs.length, inferInstance, fun i ↦ AdjoinRoot (gs.get i),267    fun i ↦ AdjoinRoot.instField, fun i ↦ inferInstance, fun i ↦ inferInstance,268    fun i ↦ inferInstance, fun i ↦ (hgs _ (List.get_mem gs i)).1.finite_adjoinRoot, e₀.trans e₁,269    ?_, fun i ↦ hfinG _ (List.get_mem gs i)⟩270  rw [hσ, ← sum_singleton_get]271  rfl272 273/-- For monic `F ∈ O[X]`, the image of `F` in `K[X]` has polynomial type `σ` iff `O[X]/(F)` has274algebra type `σ`. -/275theorem polynomial_type_iff_algebra_type (O : Type) [CommRing O] [IsDomain O]276    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]277    [Finite (IsLocalRing.ResidueField O)] (F : Polynomial O) (hF : F.Monic) (σ : FactorType) :278    HasPolynomialTypeF O (F.map (algebraMap O (BaseField O))) σ ↔279      HasAlgebraType O (AdjoinRoot F) σ := by280  classical281  open UniqueFactorizationMonoid in282  refine ⟨type_forward O F σ, fun h ↦ ?_⟩283  obtain ⟨e₀, -⟩ := adjoinRoot_base_change O F284  -- `K[X]/(F)` is reduced (a product of fields), so the image `G` of `F` is squarefree285  set G := F.map (algebraMap O (BaseField O))286  have hGm : G.Monic := hF.map _287  have h0 : G ≠ 0 := hGm.ne_zero288  have hsq : Squarefree G := by289    obtain ⟨ι, _, L, _, _, _, _, _, e, -, -⟩ := h290    exact squarefree_of_isReduced_adjoinRoot _ _ h0291      (isReduced_of_injective (e₀.symm.trans e).toRingHom (e₀.symm.trans e).injective)292  -- closure finiteness of each irreducible factor is read off by matching factors with the `Lᵢ`293  have hmon : ∀ g ∈ normalizedFactors G, g.Monic := fun g hg ↦ by294    rw [← normalize_normalized_factor g hg]295    exact monic_normalize (irreducible_of_normalized_factor g hg).ne_zero296  set l := (normalizedFactors G).toList with hl297  have hlm : ∀ g ∈ l, g.Monic ∧ Irreducible g := fun g hg ↦ by298    rw [hl, Multiset.mem_toList] at hg299    exact ⟨hmon g hg, irreducible_of_normalized_factor g hg⟩300  have hlnd : l.Pairwise (fun g h ↦ g ≠ h) := by301    change l.Nodup302    rw [hl, ← Multiset.coe_nodup, Multiset.coe_toList]303    exact (squarefree_iff_nodup_normalizedFactors h0).1 hsq304  have hlprod : G = l.prod := by305    rw [hl, Multiset.prod_toList]306    exact (eq_of_monic_of_associated (by simpa using monic_multiset_prod_of_monic _ id hmon) hGm307      (prod_normalizedFactors h0)).symm308  obtain ⟨e₁, -⟩ := polynomial_quotient_product_equiv (BaseField O) l hlm hlnd309  rw [hlprod] at e₀310  obtain ⟨ι, _, L, _, _, _, _, _, e, -, hfinL⟩ := id h311  have : ∀ i : Fin l.length, Fact (Irreducible (l.get i)) := fun i ↦ ⟨(hlm _ (List.get_mem l i)).2⟩312  obtain ⟨φ, -, hφ⟩ := pi_field_matching (BaseField O) (Fin l.length) ι313    (fun i ↦ AdjoinRoot (l.get i)) L (e₁.symm.trans (e₀.symm.trans e))314  have hfac : ∀ g ∈ normalizedFactors G, Module.Finite O (integralClosure O (AdjoinRoot g)) := by315    intro g hg316    obtain ⟨j, rfl⟩ := List.mem_iff_get.1 (show g ∈ l by rwa [hl, Multiset.mem_toList])317    obtain ⟨ψ⟩ := hφ j318    obtain ⟨χ, -⟩ := integral_closure_algEquiv O _ _ (ψ.restrictScalars O)319    have := hfinL (φ j)320    exact .equiv χ.symm.toLinearEquiv321  obtain ⟨τ, hτ⟩ := squarefree_monic_has_polynomial_type O G hGm hsq hfac322  rwa [algebra_type_unique O (AdjoinRoot F) σ τ h (type_forward O F τ hτ)]323 324end SurfaceBlowup