Exponent-profile centers recover ring dilatations

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).

The corrected ring comparison

The one-object category SingleObj A' has the elements of the commutative ring A' as morphisms, with composition given by multiplication. A multicenter supplies a categorical center indexed by finitely supported exponent profiles ν: the denominator is M.elem ^ ν, and the numerator sieve comes from M.LargeIdeal ^ ν. Each enlarged ideal is M.LargeIdeal i = M.ideal i + (M.elem i).

The resulting dilatation is isomorphic to SingleObj A'[M] (Theorem 10.1 of the source). This replaces the naive single-index identification in the original Proposition 5.1; NaiveCenterCounterexample gives the explicit obstruction to that earlier statement.

def CategoryTheory.Dilatations.Prop51.Sieve.ofIdeal {A' : Type u} [CommRing A'] (I : Ideal A') : Sieve (SingleObj.star A')

An ideal of A', regarded as a sieve over the unique object of SingleObj A': ideals absorb multiplication by arbitrary ring elements, which is exactly a sieve's stability under precomposition, since composition in SingleObj A' is ring multiplication.

Equations

• CategoryTheory.Dilatations.Prop51.Sieve.ofIdeal I = { arrows := fun {x : CategoryTheory.SingleObj A'} (f : x ⟶ CategoryTheory.SingleObj.star A') => f ∈ I, downward_closed := ⋯ }

def CategoryTheory.Dilatations.Prop51.centerOfMulticenter {A' : Type u} [CommRing A'] (M : Multicenter A') : Center (SingleObj A')

A Multicenter A' as a Center (SingleObj A'), indexed by exponent profiles ν : M^ℕ: the generator at ν divides by aᵢ ^ ν := M.elem ^ ν with numerator ranging over M.LargeIdeal ^ ν, matching Dilatation.frac exactly (needed for Phi51 to be surjective — a single-index generator only reaches products, not sums, of LargeIdeal elements).

Equations

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

noncomputable def CategoryTheory.Dilatations.Prop51.toDilatationFunctor {A' : Type u} [CommRing A'] (M : Multicenter A') : Functor (SingleObj A') (SingleObj M.Dilatation)

The functor SingleObj A' ⥤ SingleObj A'[M] induced by the canonical ring map A' → A'[M] (CategoryTheory.SingleObj.mapHom turns any monoid hom into a functor between the attached one-object categories). This plays the role of Θ on the "attached-to-a-ring" side.

Equations

• CategoryTheory.Dilatations.Prop51.toDilatationFunctor M = (CategoryTheory.SingleObj.mapHom A' M.Dilatation) ↑(algebraMap A' M.Dilatation)

theorem CategoryTheory.Dilatations.Prop51.isIso_iff_isUnit {R : Type u_1} [Monoid R] (x : SingleObj.star R ⟶ SingleObj.star R) : IsIso x ↔ IsUnit x

General fact: in the one-object category SingleObj R attached to a monoid R, a morphism is an isomorphism iff it is a unit of R — composition unwinds to multiplication (SingleObj.comp_as_mul), so a two-sided categorical inverse is exactly a two-sided multiplicative inverse.

theorem CategoryTheory.Dilatations.Prop51.faithful_Q_of_isInvertedBy_of_faithful {E : Type u} [Category.{v', u} E] (W : MorphismProperty E) {E' : Type u} [Category.{v', u} E'] (e : Functor E E') (he : W.IsInvertedBy e) (hefaith : e.Faithful) : W.Q.Faithful

General fact: if W.IsInvertedBy e for some faithful e, then W.Q is faithful — e factors as W.Q ⋙ (lift of e) (universal property of the localization), and a functor whose composite with something else is faithful is itself faithful (faithful_of_comp_faithful_gen, applied to the lift, not e itself : here we need the reverse composition order, so we go via e's own factorization instead).

theorem CategoryTheory.Dilatations.Prop51.nonzerodiv_image_single {A' : Type u} [CommRing A'] (M : Multicenter A') (i : M.index) : (algebraMap A' M.Dilatation) (M.elem i) ∈ nonZeroDivisors M.Dilatation

The images of M's generators in A'[M] are non-zero-divisors — an unconditional structural fact about dilatations (Multicenter.Dilatation.nonzerodiv_image, specialized to a single generator).

theorem CategoryTheory.Dilatations.Prop51.prop_5_1 {A' : Type u} [CommRing A'] (M : Multicenter A') : ∃! Φ : Functor (Dila (centerOfMulticenter M)) (SingleObj M.Dilatation), (CatToDila (centerOfMulticenter M)).comp Φ = toDilatationFunctor M

Proposition 5.1, universal-property half. Dila (centerOfMulticenter M) is the unique factorization of toDilatationFunctor M through CatToDila (centerOfMulticenter M).

noncomputable def CategoryTheory.Dilatations.Prop51.Phi51 {A' : Type u} [CommRing A'] (M : Multicenter A') : Functor (Dila (centerOfMulticenter M)) (SingleObj M.Dilatation)

The functor Φ from Proposition 5.1 (the functor produced by prop_5_1's existence claim), matching the paper's own naming (cf. Alpha315 for the analogous functor in Proposition 3.15).

Equations

• CategoryTheory.Dilatations.Prop51.Phi51 M = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Prop51.Phi51_spec {A' : Type u} [CommRing A'] (M : Multicenter A') : (CatToDila (centerOfMulticenter M)).comp (Phi51 M) = toDilatationFunctor M

theorem CategoryTheory.Dilatations.Prop51.Phi51_unique {A' : Type u} [CommRing A'] (M : Multicenter A') (G : Functor (Dila (centerOfMulticenter M)) (SingleObj M.Dilatation)) (hG : (CatToDila (centerOfMulticenter M)).comp G = toDilatationFunctor M) : G = Phi51 M

Injectivity of Φ

Compare both Φ and the (unconditionally faithful) raw-localization comparison DilaToLoc against a common target : the categorical localization (CenterMorphismProperty (centerOfMulticenter M)).Localization, reached from SingleObj A'[M] via the ring-theoretic localization of A' at M's generators (using the monoid-level universal property of Localization, since the target's endomorphism monoid need not be a ring).

def CategoryTheory.Dilatations.Prop51.genSubmonoid {A' : Type u} [CommRing A'] (M : Multicenter A') : Submonoid A'

M's generators, viewed as a submonoid of A' itself (not of A'[M]).

Equations

• CategoryTheory.Dilatations.Prop51.genSubmonoid M = Submonoid.closure (Set.range M.elem)

theorem CategoryTheory.Dilatations.Prop51.genSubmonoid_nonZeroDivisors {A' : Type u} [CommRing A'] (M : Multicenter A') (i : M.index) : (algebraMap A' (Localization (genSubmonoid M))) (M.elem i) ∈ nonZeroDivisors (Localization (genSubmonoid M))

theorem CategoryTheory.Dilatations.Prop51.genSubmonoid_gen {A' : Type u} [CommRing A'] (M : Multicenter A') (i : M.index) : Ideal.span {(algebraMap A' (Localization (genSubmonoid M))) (M.elem i)} = Ideal.map (algebraMap A' (Localization (genSubmonoid M))) (M.LargeIdeal i)

noncomputable def CategoryTheory.Dilatations.Prop51.descToLoc {A' : Type u} [CommRing A'] (M : Multicenter A') : M.Dilatation →ₐ[A'] Localization (genSubmonoid M)

The canonical map from A'[M] into the full localization of A' at the generators — trivial to build via desc, since generators become units there.

Equations

• CategoryTheory.Dilatations.Prop51.descToLoc M = M.desc ⋯ ⋯

def CategoryTheory.Dilatations.Prop51.toLocEnd {A' : Type u} [CommRing A'] (M : Multicenter A') : A' →* End ((LocalizationFunctor (centerOfMulticenter M)).obj (SingleObj.star A'))

A', as a monoid hom into the endomorphism monoid of the raw localization (CenterMorphismProperty (centerOfMulticenter M)).Localization, matching LocalizationFunctor (centerOfMulticenter M).

Equations

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

theorem CategoryTheory.Dilatations.Prop51.toLocEnd_inverts_gen {A' : Type u} [CommRing A'] (M : Multicenter A') (y : ↥(genSubmonoid M)) : IsUnit ((toLocEnd M) ↑y)

theorem CategoryTheory.Dilatations.Prop51.genImage_central {A' : Type u} [CommRing A'] (M : Multicenter A') (a : A') ⦃X Y : (CenterMorphismProperty (centerOfMulticenter M)).Localization⦄ (v : X ⟶ Y) : CategoryStruct.comp ((toLocEnd M) a) v = CategoryStruct.comp v ((toLocEnd M) a)

Key structural fact: since A' is commutative, every image toLocEnd M a is central in the raw localization's endomorphism monoid — it commutes with everything. Proved via Localization.Construction.morphismProperty_eq_top: a MorphismProperty stable under composition, containing every generator-image and every formal inverse, is everything.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Dilatations.Prop51.localizationPoint {A' : Type u} [CommRing A'] (M : Multicenter A') : (CenterMorphismProperty (centerOfMulticenter M)).Localization

The single object of the raw localization, viewed as an object of (CenterMorphismProperty (centerOfMulticenter M)).Localization.

Equations

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

theorem CategoryTheory.Dilatations.Prop51.isoObj_eq_localizationPoint {A' : Type u} [CommRing A'] (M : Multicenter A') (X : (CenterMorphismProperty (centerOfMulticenter M)).Localization) : X = localizationPoint M

Every object of the raw localization is (canonically, but non-computably) equal to localizationPoint, since the localization of a single-object category is again single-object.

noncomputable def CategoryTheory.Dilatations.Prop51.castEndomorphism {A' : Type u} [CommRing A'] (M : Multicenter A') ⦃X Y : (CenterMorphismProperty (centerOfMulticenter M)).Localization⦄ (u : X ⟶ Y) : End (localizationPoint M)

Cast a morphism between arbitrary objects of the raw localization into an endomorphism of localizationPoint, using that the localization has (up to equality) a single object.

Equations

• CategoryTheory.Dilatations.Prop51.castEndomorphism M u = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp u (CategoryTheory.eqToHom ⋯))

theorem CategoryTheory.Dilatations.Prop51.allCentral {A' : Type u} [CommRing A'] (M : Multicenter A') (v : End (localizationPoint M)) ⦃X Y : (CenterMorphismProperty (centerOfMulticenter M)).Localization⦄ (u : X ⟶ Y) : CategoryStruct.comp (castEndomorphism M u) v = CategoryStruct.comp v (castEndomorphism M u)

Key structural fact, part 2: every endomorphism of the raw localization is central (commutes with everything) — same argument as genImage_central, one level up : generator-images are central by genImage_central, and formal inverses of central elements are central too.

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Prop51.commEnd {A' : Type u} [CommRing A'] (M : Multicenter A') : CommMonoid (End (localizationPoint M))

The endomorphism monoid of the raw localization's single object is commutative : this is what makes LocEndLift (a monoid-localization universal-property construction) type-check.

Equations

• CategoryTheory.Dilatations.Prop51.commEnd M = { toMonoid := CategoryTheory.End.monoid, mul_comm := ⋯ }

noncomputable def CategoryTheory.Dilatations.Prop51.LocEndLift {A' : Type u} [CommRing A'] (M : Multicenter A') : Localization (genSubmonoid M) →* End ((LocalizationFunctor (centerOfMulticenter M)).obj (SingleObj.star A'))

The universal monoid-level extension of toLocEnd along A' → Localization (genSubmonoid M) (the generators already become units under toLocEnd, so the monoid-localization universal property applies unconditionally).

Equations

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

noncomputable def CategoryTheory.Dilatations.Prop51.kappaHom {A' : Type u} [CommRing A'] (M : Multicenter A') : M.Dilatation →* End ((LocalizationFunctor (centerOfMulticenter M)).obj (SingleObj.star A'))

The comparison map A'[M] → (CenterMorphismProperty (centerOfMulticenter M)).Localization, as a monoid hom on the (single) Hom-set.

Equations

• CategoryTheory.Dilatations.Prop51.kappaHom M = (CategoryTheory.Dilatations.Prop51.LocEndLift M).comp ↑(CategoryTheory.Dilatations.Prop51.descToLoc M).toRingHom

noncomputable def CategoryTheory.Dilatations.Prop51.kappaFunctor {A' : Type u} [CommRing A'] (M : Multicenter A') : Functor (SingleObj M.Dilatation) (CenterMorphismProperty (centerOfMulticenter M)).Localization

kappaHom as a functor SingleObj A'[M] ⥤ (CenterMorphismProperty (centerOfMulticenter M)).Localization.

Equations

• CategoryTheory.Dilatations.Prop51.kappaFunctor M = CategoryTheory.SingleObj.functor (CategoryTheory.Dilatations.Prop51.kappaHom M)

theorem CategoryTheory.Dilatations.Prop51.toDilatationFunctor_comp_kappaFunctor {A' : Type u} [CommRing A'] (M : Multicenter A') : (toDilatationFunctor M).comp (kappaFunctor M) = LocalizationFunctor (centerOfMulticenter M)

theorem CategoryTheory.Dilatations.Prop51.Phi51_comp_kappaFunctor {A' : Type u} [CommRing A'] (M : Multicenter A') : (Phi51 M).comp (kappaFunctor M) = DilaToLoc (centerOfMulticenter M)

theorem CategoryTheory.Dilatations.Prop51.Phi51_faithful {A' : Type u} [CommRing A'] (M : Multicenter A') : (Phi51 M).Faithful

Surjectivity of Φ

With the ν-indexed sieve, a single fraction-generator edge at profile ν already reaches an arbitrary element of LargeIdeal ^ ν (the whole ideal, not just a product of simpler pieces), so every Dilatation.frac fraction — hence every element of A'[M], by induction_on — is directly the Φ-image of one such generator. No path/product induction is needed at all.

theorem CategoryTheory.Dilatations.Prop51.algebraMap_elem_pow_mul_frac {A' : Type u} [CommRing A'] (M : Multicenter A') (ν : M.index →₀ ℕ) (num : A') (hnum : num ∈ M.LargeIdeal ^ ν) : (algebraMap A' M.Dilatation) (M.elem ^ ν) * Multicenter.Dilatation.frac ν ⟨num, hnum⟩ = (algebraMap A' M.Dilatation) num

The defining fraction identity aᵢ ^ ν · (num/aᵢ ^ ν) = num inside A'[M] itself (as opposed to Multicenter.Dilatation.image_elem_LargeIdeal_equal's span/map statement) — the same computation, extracted as a reusable equation.

theorem CategoryTheory.Dilatations.Prop51.Phi51_full {A' : Type u} [CommRing A'] (M : Multicenter A') : (Phi51 M).Full

Packaging Φ into an isomorphism of categories

Phi51 is full and faithful, and both Dila (centerOfMulticenter M) and SingleObj A'[M] have a single object, so Φ restricts to a bijection on the (unique) Hom-set — a MonoidHom inverse to Phi51.map builds the inverse functor Psi51 directly, mirroring Iso315 in Proposition 3.15.

noncomputable def CategoryTheory.Dilatations.Prop51.Phi51Equiv {A' : Type u} [CommRing A'] (M : Multicenter A') : End ((CatToDila (centerOfMulticenter M)).obj (SingleObj.star A')) ≃ M.Dilatation

Φ, restricted to the single Hom-set, as a bijection (using that Phi51 is full and faithful).

Equations

• CategoryTheory.Dilatations.Prop51.Phi51Equiv M = Equiv.ofBijective (CategoryTheory.Dilatations.Prop51.Phi51 M).map ⋯

theorem CategoryTheory.Dilatations.Prop51.Phi51Equiv_apply {A' : Type u} [CommRing A'] (M : Multicenter A') (x : End ((CatToDila (centerOfMulticenter M)).obj (SingleObj.star A'))) : (Phi51Equiv M) x = (Phi51 M).map x

theorem CategoryTheory.Dilatations.Prop51.Phi51Equiv_one {A' : Type u} [CommRing A'] (M : Multicenter A') : (Phi51Equiv M) 1 = 1

theorem CategoryTheory.Dilatations.Prop51.Phi51Equiv_mul {A' : Type u} [CommRing A'] (M : Multicenter A') (x y : End ((CatToDila (centerOfMulticenter M)).obj (SingleObj.star A'))) : (Phi51Equiv M) (x * y) = (Phi51Equiv M) x * (Phi51Equiv M) y

noncomputable def CategoryTheory.Dilatations.Prop51.psi51Hom {A' : Type u} [CommRing A'] (M : Multicenter A') : M.Dilatation →* End ((CatToDila (centerOfMulticenter M)).obj (SingleObj.star A'))

The inverse of Phi51Equiv, as a MonoidHom — the data needed to build Psi51.

Equations

• CategoryTheory.Dilatations.Prop51.psi51Hom M = { toFun := ⇑(CategoryTheory.Dilatations.Prop51.Phi51Equiv M).symm, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def CategoryTheory.Dilatations.Prop51.Psi51 {A' : Type u} [CommRing A'] (M : Multicenter A') : Functor (SingleObj M.Dilatation) (Dila (centerOfMulticenter M))

The inverse functor to Phi51.

Equations

• CategoryTheory.Dilatations.Prop51.Psi51 M = CategoryTheory.SingleObj.functor (CategoryTheory.Dilatations.Prop51.psi51Hom M)

instance CategoryTheory.Dilatations.Prop51.dila51_subsingleton {A' : Type u} [CommRing A'] (M : Multicenter A') : Subsingleton (Dila (centerOfMulticenter M))

Dila (centerOfMulticenter M) has a single object, since C = SingleObj A' does (CatToDila_obj_surjective and Subsingleton.elim on C).

theorem CategoryTheory.Dilatations.Prop51.Phi51_comp_Psi51 {A' : Type u} [CommRing A'] (M : Multicenter A') : (Phi51 M).comp (Psi51 M) = Functor.id (Dila (centerOfMulticenter M))

theorem CategoryTheory.Dilatations.Prop51.Psi51_comp_Phi51 {A' : Type u} [CommRing A'] (M : Multicenter A') : (Psi51 M).comp (Phi51 M) = Functor.id (SingleObj M.Dilatation)

noncomputable def CategoryTheory.Dilatations.Prop51.Iso51 {A' : Type u} [CommRing A'] (M : Multicenter A') : ↧(Dila (centerOfMulticenter M)) ≅ ↧(SingleObj M.Dilatation)

Proposition 5.1, full statement. Φ assembles Phi51/Psi51 into an isomorphism of categories Dila (centerOfMulticenter M) ≅ SingleObj A'[M], matching the paper's "provides the desired identification."

Equations

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