Iterated dilatations of rings

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

Appendix C : Elementary Properties of Dilatations of Rings

Formalizing statements of A. Mayeux, Multi-centered Dilatations, Congruent Isomorphisms and Rost Double Deformation Space, Transformation Groups 31 (2026), 1801-1850, SS2.2 ("Elementary Properties of Dilatations"), on top of the Multicenter/Dilatation API above.

def CategoryTheory.Dilatations.Multicenter.restrict {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : Multicenter A'

Restriction of a multicenter to a subset K ⊆ I of the index set, matching the notation {[Mᵢ,aᵢ]}_{i∈K} of §2.2 of the printed paper.

Equations

• M.restrict K = { index := ↑K, ideal := fun (i : ↑K) => M.ideal ↑i, elem := fun (i : ↑K) => M.elem ↑i }

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.restrict_ideal {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (i : ↑K) : (M.restrict K).ideal i = M.ideal ↑i

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.restrict_elem {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (i : ↑K) : (M.restrict K).elem i = M.elem ↑i

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.restrict_LargeIdeal {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (i : ↑K) : (M.restrict K).LargeIdeal i = M.LargeIdeal ↑i

noncomputable def CategoryTheory.Dilatations.Multicenter.complement {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : Multicenter (M.restrict K).Dilatation

The second-stage multicenter of Proposition 2.24. Over B := A'[M.restrict K], the complementary indices j ∈ I ∖ K carry the ideal B·(Mⱼ) (the image of M.ideal j) and the element aⱼ/1 (the image of M.elem j).

Equations

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

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.complement_ideal {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (j : ↑Kᶜ) : (M.complement K).ideal j = Ideal.map (algebraMap A' (M.restrict K).Dilatation) (M.ideal ↑j)

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.complement_elem {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (j : ↑Kᶜ) : (M.complement K).elem j = (algebraMap A' (M.restrict K).Dilatation) (M.elem ↑j)

theorem CategoryTheory.Dilatations.Multicenter.gen_iff_le {A' : Type u_1} {B' : Type u_2} [CommRing A'] [CommRing B'] [Algebra A' B'] (M : Multicenter A') (i : M.index) : Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i) ↔ Ideal.map (algebraMap A' B') (M.ideal i) ≤ Ideal.span {(algebraMap A' B') (M.elem i)}

Reformulation of the gen hypothesis of the universal property. For an A'-algebra B', the condition span {φ(aᵢ)} = map φ (Lᵢ) appearing in Multicenter.desc is equivalent to the plain containment map φ (Mᵢ) ≤ span {φ(aᵢ)}, since Lᵢ = Mᵢ + (aᵢ). This is the working form used throughout Appendix C.

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.nonzerodiv_algebraMap_of_mem_nonZeroDivisors {A' : Type u_1} [CommRing A'] {M : Multicenter A'} {c : A'} (hc : c ∈ nonZeroDivisors A') : (algebraMap A' M.Dilatation) c ∈ nonZeroDivisors M.Dilatation

The canonical map of a dilatation preserves non-zero-divisors of the base ring: if c ∈ A' is a non-zero-divisor, so is its image in A'[M]. (Unlike Proposition 2.20's injectivity, which genuinely needs an extra hypothesis, this direction always holds; it is what makes the i ∈ K branch of Proposition 2.24 unconditional.)

noncomputable def CategoryTheory.Dilatations.psi224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : (M.restrict K).Dilatation →ₐ[A'] M.Dilatation

First stage of Proposition 2.24: the canonical A'-algebra map A'[M|_K] → A'[M].

Equations

• CategoryTheory.Dilatations.psi224 M K = (M.restrict K).desc ⋯ ⋯

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.algebra224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : Algebra (M.restrict K).Dilatation M.Dilatation

Equations

• CategoryTheory.Dilatations.algebra224 M K = (CategoryTheory.Dilatations.psi224 M K).toAlgebra

theorem CategoryTheory.Dilatations.algebraMap224_eq {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : algebraMap (M.restrict K).Dilatation M.Dilatation = (psi224 M K).toRingHom

instance CategoryTheory.Dilatations.scalarTower224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : IsScalarTower A' (M.restrict K).Dilatation M.Dilatation

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.algebra224' {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : Algebra A' (M.complement K).Dilatation

The A'-algebra structure on the second stage C224, obtained by composing A' → B224 with B224 → C224.

Equations

• CategoryTheory.Dilatations.algebra224' M K = ((algebraMap (M.restrict K).Dilatation (M.complement K).Dilatation).comp (algebraMap A' (M.restrict K).Dilatation)).toAlgebra

instance CategoryTheory.Dilatations.scalarTower224' {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : IsScalarTower A' (M.restrict K).Dilatation (M.complement K).Dilatation

The four hypotheses feeding the universal property.

theorem CategoryTheory.Dilatations.hnzd_chi {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (j : (M.complement K).index) : (algebraMap (M.restrict K).Dilatation M.Dilatation) ((M.complement K).elem j) ∈ nonZeroDivisors M.Dilatation

theorem CategoryTheory.Dilatations.hgen_chi {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (j : (M.complement K).index) : Ideal.span {(algebraMap (M.restrict K).Dilatation M.Dilatation) ((M.complement K).elem j)} = Ideal.map (algebraMap (M.restrict K).Dilatation M.Dilatation) ((M.complement K).LargeIdeal j)

theorem CategoryTheory.Dilatations.hnzd_rho {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (i : M.index) : (algebraMap A' (M.complement K).Dilatation) (M.elem i) ∈ nonZeroDivisors (M.complement K).Dilatation

theorem CategoryTheory.Dilatations.hgen_rho {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (i : M.index) : Ideal.span {(algebraMap A' (M.complement K).Dilatation) (M.elem i)} = Ideal.map (algebraMap A' (M.complement K).Dilatation) (M.LargeIdeal i)

The two comparison maps and the isomorphism.

noncomputable def CategoryTheory.Dilatations.chi224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : (M.complement K).Dilatation →ₐ[(M.restrict K).Dilatation] M.Dilatation

Second stage of Proposition 2.24: the canonical B224-algebra map C224 →ₐ A'[M].

Equations

• CategoryTheory.Dilatations.chi224 M K = (M.complement K).desc ⋯ ⋯

noncomputable def CategoryTheory.Dilatations.rho224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : M.Dilatation →ₐ[A'] (M.complement K).Dilatation

Reverse direction of Proposition 2.24: the canonical A'-algebra map A'[M] →ₐ C224.

Equations

• CategoryTheory.Dilatations.rho224 M K = M.desc ⋯ ⋯

theorem CategoryTheory.Dilatations.rho224_psi224 {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (b : (M.restrict K).Dilatation) : (rho224 M K) ((psi224 M K) b) = (algebraMap (M.restrict K).Dilatation (M.complement K).Dilatation) b

noncomputable def CategoryTheory.Dilatations.iteratedDilatationEquiv {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : (M.complement K).Dilatation ≃ₐ[(M.restrict K).Dilatation] M.Dilatation

Proposition 2.24. The full dilatation A'[M] is canonically isomorphic, as an A'[M|_K]-algebra, to the second-stage dilatation (A'[M|_K])[complement M K].

Equations

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

Uniqueness in Proposition 2.24

theorem CategoryTheory.Dilatations.chi224_unique {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (f : (M.complement K).Dilatation →ₐ[(M.restrict K).Dilatation] M.Dilatation) : f = chi224 M K

Uniqueness of the comparison map of Proposition 2.24. Any A[M|_K]-algebra map from the two-stage dilatation to A[M] equals chi224. This is the uniqueness half of the universal property of dilatations of rings, applied to the multicenter complement M K.

theorem CategoryTheory.Dilatations.iteratedDilatationEquiv_unique {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) (e : (M.complement K).Dilatation ≃ₐ[(M.restrict K).Dilatation] M.Dilatation) : e = iteratedDilatationEquiv M K

The isomorphism of Proposition 2.24 is unique. Any isomorphism of A[M|_K]-algebras between the two-stage dilatation and A[M] equals iteratedDilatationEquiv.

theorem CategoryTheory.Dilatations.iteratedDilatationEquiv_existsUnique {A' : Type u_1} [CommRing A'] (M : Multicenter A') (K : Set M.index) : ∃! e : (M.complement K).Dilatation ≃ₐ[(M.restrict K).Dilatation] M.Dilatation, ∀ (b : (M.restrict K).Dilatation), e ((algebraMap (M.restrict K).Dilatation (M.complement K).Dilatation) b) = (algebraMap (M.restrict K).Dilatation M.Dilatation) b

Proposition 2.24, existence and uniqueness together. There is exactly one isomorphism from the two-stage dilatation to A[M] compatible with the canonical maps out of the first-stage ring A[M|_K].