A counterexample to the naive ring comparison

From Arnaud Mayeux, Dilatations of categories, via their Lean formalization, https://arxiv.org/abs/2608.09305, and rndmx/DilCat at commit 604559654c948566675da3f7709b8ad3126bd487 (Apache-2.0). The ring construction includes work by Arnaud Mayeux and Jujian Zhang from ProjConstruction/Proj (Apache-2.0).

Erratum to Proposition 5.1 : the naive I-indexed center is not the right one

The printed \citep[Proposition~5.1]{Mayeux} identifies 𝒞[{(aᵢ)⁻¹∘Mᵢ}ᵢ∈I] (dilating by the center indexed directly by i ∈ I, one generator per index) with A[M]. This identification is false : composition in SingleObj A' is multiplication, so the image of every morphism of this naive center's dilatation is a product c·∏ⱼ(mⱼ/aᵢⱼ), and not every element of A[M] has this form. The concrete witness below : A = ℤ[X], a = 2, M = (X), and (X+2)/2 ∈ A[M] is not reachable. See \S10.2 of the paper for the informal argument this formalizes.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Dilatations.NaiveCenterCounterexample.CEx : Multicenter (Polynomial ℤ)

The single-center example with ideal (X) and denominator 2 in ℤ[X].

Equations

• CategoryTheory.Dilatations.NaiveCenterCounterexample.CEx = { index := Unit, ideal := fun (x : Unit) => Ideal.span {Polynomial.X}, elem := fun (x : Unit) => 2 }

@[reducible, inline]

abbrev CategoryTheory.Dilatations.NaiveCenterCounterexample.Target : Type

The localization of the integers obtained by inverting 2.

Equations

• CategoryTheory.Dilatations.NaiveCenterCounterexample.Target = Localization (Submonoid.powers 2)

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.CEx_elem_pow_eval (ν : CEx.index →₀ ℕ) : Polynomial.eval 0 (CEx.elem ^ ν) = 2 ^ ν ()

noncomputable def CategoryTheory.Dilatations.NaiveCenterCounterexample.psiPreDil (x : CEx.PreDil) : Target

Evaluate a fraction representative at X = 0 in the localization of ℤ.

Equations

• CategoryTheory.Dilatations.NaiveCenterCounterexample.psiPreDil x = IsLocalization.mk' CategoryTheory.Dilatations.NaiveCenterCounterexample.Target (Polynomial.eval 0 x.num) ⟨2 ^ x.pow (), ⋯⟩

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psiPreDil_respects {x y : CEx.PreDil} (h : CEx.r x y) : psiPreDil x = psiPreDil y

noncomputable def CategoryTheory.Dilatations.NaiveCenterCounterexample.psi : CEx.Dilatation → Target

The evaluation-at-X=0 invariant ψ. Descends to the dilatation ring because it kills exactly what fraction-composition can produce from (X)-numerators.

Equations

• CategoryTheory.Dilatations.NaiveCenterCounterexample.psi = CategoryTheory.Dilatations.Multicenter.Dilatation.descFun CategoryTheory.Dilatations.NaiveCenterCounterexample.psiPreDil ⋯

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psi_algebraMap (c : Polynomial ℤ) : psi ((algebraMap (Polynomial ℤ) CEx.Dilatation) c) = (algebraMap ℤ Target) (Polynomial.eval 0 c)

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psi_mul (x y : CEx.Dilatation) : psi (x * y) = psi x * psi y

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.X_add_two_mem : Polynomial.X + 2 ∈ CEx.LargeIdeal ^ Finsupp.single () 1

noncomputable def CategoryTheory.Dilatations.NaiveCenterCounterexample.targetElement : CEx.Dilatation

The target element (X+2)/2 ∈ A[M], which we show is unreachable.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psi_target : psi targetElement = 1

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psi_frac_eq_zero (m : Polynomial ℤ) (hm : m ∈ Ideal.span {Polynomial.X}) (hL : m ∈ CEx.LargeIdeal ^ Finsupp.single () 1) : psi (Multicenter.Dilatation.frac (Finsupp.single () 1) ⟨m, hL⟩) = 0

noncomputable def CategoryTheory.Dilatations.NaiveCenterCounterexample.centerNaive : Center (SingleObj (Polynomial ℤ))

The naive I-indexed center {(a_i, M_i)} (here a single index): index Unit, morphism 2, sieve generated by (X) directly (not the large ideal).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.prop_naive : ∃! Φ : Functor (Dila centerNaive) (SingleObj CEx.Dilatation), (CatToDila centerNaive).comp Φ = Prop51.toDilatationFunctor CEx

The comparison functor for the naive center, built directly from the universal property (Dila_universal_property), exactly as the printed proof's Φ is meant to be.

noncomputable def CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive : Functor (Dila centerNaive) (SingleObj CEx.Dilatation)

The functor Φ_naive produced by prop_naive, matching the printed paper's Φ.

Equations

• CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive = Exists.choose CategoryTheory.Dilatations.NaiveCenterCounterexample.prop_naive

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive_spec : (CatToDila centerNaive).comp PhiNaive = Prop51.toDilatationFunctor CEx

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive_unique (G' : Functor (Dila centerNaive) (SingleObj CEx.Dilatation)) (hG' : (CatToDila centerNaive).comp G' = Prop51.toDilatationFunctor CEx) : G' = PhiNaive

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.CEx_elem_pow (ν : CEx.index →₀ ℕ) : CEx.elem ^ ν = 2 ^ ν ()

CEx.elem ^ ν = 2 ^ (ν ()) as a polynomial identity (no evaluation), for arbitrary ν.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.cXk_mem (c : Polynomial ℤ) (k : ℕ) : c * Polynomial.X ^ k ∈ CEx.LargeIdeal ^ Finsupp.single () k

c·Xᵏ always lies in the k-th large-ideal power, for every c and every k.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.psi_cXk_eq_zero (c : Polynomial ℤ) (k : ℕ) (hk : 1 ≤ k) : psi (Multicenter.Dilatation.frac (Finsupp.single () k) ⟨c * Polynomial.X ^ k, ⋯⟩) = 0

ψ kills every fraction (c·Xᵏ)/2ᵏ with k ≥ 1 (numerator divisible by X).

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.targetElement_ne_algebraMap (c : Polynomial ℤ) : (algebraMap (Polynomial ℤ) CEx.Dilatation) c ≠ targetElement

The key non-surjectivity fact. targetElement = (X+2)/2 is never algebraMap c for any c : ℤ[X]: cross-multiplying gives 2c = X+2 (up to a harmless common power of 2), and evaluating at X = 1 turns this into 2·c(1) = 3 in ℤ, which is false (2 does not divide 3).

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.mem_LargeIdeal_single1_of_mem_ideal {m : Polynomial ℤ} (hm : m ∈ Ideal.span {Polynomial.X}) : m ∈ CEx.LargeIdeal ^ Finsupp.single () 1

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.algebraMap_two_mul_frac (m : Polynomial ℤ) (hm : m ∈ CEx.LargeIdeal ^ Finsupp.single () 1) : (algebraMap (Polynomial ℤ) CEx.Dilatation) 2 * Multicenter.Dilatation.frac (Finsupp.single () 1) ⟨m, hm⟩ = (algebraMap (Polynomial ℤ) CEx.Dilatation) m

The defining identity for our specific [X,2] fraction, specialized from algebraMap_elem_pow_mul_frac.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive_map_fraction (X' : SingleObj (Polynomial ℤ)) (m : Polynomial ℤ) (hm : m ∈ Ideal.span {Polynomial.X}) : PhiNaive.map (fractionInDilatation centerNaive ⟨(), ⟨X', ⟨m, hm⟩⟩⟩) = Multicenter.Dilatation.frac (Finsupp.single () 1) ⟨m, ⋯⟩

The image of a fraction generator. Φ_naive sends the "m-over-2" generator (for m ∈ (X)) to the honest dilatation fraction m/2 — no more, no less. This is forced : composing with Θ(2) on both sides and cancelling the nonzerodivisor algebraMap 2 pins the value down uniquely (cf. Phi51_full, the analogous computation for the ν-indexed center).

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.exists_c_k {A B : GeneratedCategory centerNaive} (f : A ⟶ B) : ∃ (c : Polynomial ℤ) (k : ℕ) (hmem : c * Polynomial.X ^ k ∈ CEx.LargeIdeal ^ Finsupp.single () k), PhiNaive.map ((GeneratedToDila centerNaive).map f) = Multicenter.Dilatation.frac (Finsupp.single () k) ⟨c * Polynomial.X ^ k, hmem⟩

Every reachable morphism is c·Xᵏ/2ᵏ. Since Dila centerNaive's only generators are C's original morphisms (ring elements) and the single fraction generator X/2 (from the sieve (X)), and composition is multiplication, every morphism's Φ_naive-image is a product of these, hence of the stated shape.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.targetElement_not_in_range {A B : Dila centerNaive} (φ : A ⟶ B) : PhiNaive.map φ ≠ targetElement

targetElement = (X+2)/2 is not in the image of Φ_naive. Every morphism of Dila centerNaive lifts (via GeneratedToDila_full) to a path of generators, whose image under Φ_naive is c·Xᵏ/2ᵏ by exists_c_k. If k = 0 this is algebraMap c, ruled out by targetElement_ne_algebraMap; if k ≥ 1 the numerator c·Xᵏ is divisible by X, so ψ kills it (psi_cXk_eq_zero), while ψ (targetElement) = 1 ≠ 0.

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.PhiNaive_not_full : ¬PhiNaive.Full

Φ_naive itself is not full (its image on the relevant End misses targetElement).

theorem CategoryTheory.Dilatations.NaiveCenterCounterexample.no_C_compatible_equiv : ¬∃ (Φ' : Dila centerNaive ≌ SingleObj CEx.Dilatation), (CatToDila centerNaive).comp Φ'.functor = Prop51.toDilatationFunctor CEx

The main theorem. No functor Dila centerNaive ⥤ SingleObj ℤ[X][CEx] compatible with the two canonical inclusion functors (i.e. matching the printed paper's comparison functor Φ) can be part of an equivalence of categories : by prop_naive's uniqueness clause any such functor equals Φ_naive, and Φ_naive is not full (PhiNaive_not_full), while every equivalence functor is full. This refutes Proposition 5.1's claimed identification 𝒞[(aᵢ)⁻¹∘Mᵢ] ≅ A[M] for the naive I-indexed center.