Dilatations of commutative rings and semirings

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

§5.0.2 : Dilatations of commutative rings and semirings

The ring-theoretic dilatation A[{Mᵢ/aᵢ}] from [M], matching Multicenter A below to the paper's {[Mᵢ, aᵢ]}ᵢ∈I (ported from ProjConstruction/Proj).

Vendored from Project/Dilatation/lemma.lean

theorem CategoryTheory.Dilatations.Ideal.prod_span' {ι : Type u_1} {A' : Type u_2} [CommSemiring A'] (f : ι → A') (s : Finset ι) : Ideal.span {∏ i ∈ s, f i} = ∏ i ∈ s, Ideal.span {f i}

theorem CategoryTheory.Dilatations.Ideal.prod_map {ι : Type u_1} {A' : Type u_2} {B' : Type u_3} {F' : Type u_4} [CommSemiring A'] [CommSemiring B'] [FunLike F' A' B'] [RingHomClass F' A' B'] (f : ι → Ideal A') (s : Finset ι) (χ : F') : Ideal.map χ (∏ i ∈ s, f i) = ∏ i ∈ s, Ideal.map χ (f i)

Vendored from Project/Dilatation/Family.lean

def CategoryTheory.Dilatations.familyPow {A' : Type u_5} {G : Type u_6} [CommMonoid A'] [Zero G] [Pow A' G] {ι : Type u_7} (f : ι → A') (v : ι →₀ G) : A'

The finite product of a family raised to finitely supported exponents.

Equations

• CategoryTheory.Dilatations.familyPow f v = v.prod fun (i : ι) (k : G) => f i ^ k

@[instance_reducible]

def CategoryTheory.Dilatations.instFamilyPow {A' : Type u_5} {G : Type u_6} [CommMonoid A'] [Zero G] [Pow A' G] {ι : Type u_7} : HPow (ι → A') (ι →₀ G) A'

Scoped exponent notation for finite products of a family.

Equations

• CategoryTheory.Dilatations.instFamilyPow = { hPow := fun (f : ι → A') (v : ι →₀ G) => CategoryTheory.Dilatations.familyPow f v }

theorem CategoryTheory.Dilatations.familyPow_def {A' : Type u_5} {G : Type u_6} [CommMonoid A'] [Zero G] [Pow A' G] {ι : Type u_7} (f : ι → A') (v : ι →₀ G) : f ^ v = v.prod fun (i : ι) (k : G) => f i ^ k

theorem CategoryTheory.Dilatations.familyPow_add {A' : Type u_5} [CommMonoid A'] {ι : Type u_7} (f : ι → A') (v w : ι →₀ ℕ) : f ^ (v + w) = f ^ v * f ^ w

@[simp]

theorem CategoryTheory.Dilatations.familyPow_zero {A' : Type u_5} [CommMonoid A'] {ι : Type u_7} (f : ι → A') : f ^ 0 = 1

theorem CategoryTheory.Dilatations.familyPow_nsmul {A' : Type u_5} [CommMonoid A'] {ι : Type u_7} (f : ι → A') (ν : ι →₀ ℕ) (k : ℕ) : (f ^ ν) ^ k = f ^ (k • ν)

A family-power raised to an ordinary ℕ-power is the family-power at the scaled exponent : (f ^ ν) ^ k = f ^ (k•ν). Used to relate a "power of a power" to a single flattened exponent.

theorem CategoryTheory.Dilatations.family_pow_flatten {A' : Type u_5} [CommMonoid A'] {ι : Type u_7} (f : ι → A') (μ : (ι →₀ ℕ) →₀ ℕ) : (μ.prod fun (ν : ι →₀ ℕ) (k : ℕ) => (f ^ ν) ^ k) = f ^ μ.sum fun (ν : ι →₀ ℕ) (k : ℕ) => k • ν

Flattening a finite ℕ-combination μ of exponent profiles and taking a single family-power agrees with taking the family-power at each profile first and combining : μ.prod (fun ν k ↦ (f ^ ν) ^ k) = f ^ (μ.sum fun ν k ↦ k•ν). This is the key identity behind reindexing a multi-center by exponent profiles (Multicenter.reindex_LargeIdeal_pow, Multicenter.reindex_elem_pow below).

theorem CategoryTheory.Dilatations.Ideal.familyPow_def {A' : Type u_5} [CommSemiring A'] {ι : Type u_6} (M : ι → Ideal A') (v : ι →₀ ℕ) : M ^ v = v.prod fun (i : ι) (k : ℕ) => M i ^ k

theorem CategoryTheory.Dilatations.Ideal.mem_familyPow_add {A' : Type u_5} [CommSemiring A'] {ι : Type u_6} {M : ι → Ideal A'} {v w : ι →₀ ℕ} {x y : A'} (hx : x ∈ M ^ v) (hy : y ∈ M ^ w) : x * y ∈ M ^ (v + w)

theorem CategoryTheory.Dilatations.Ideal.mem_familyPow_of_mem {A' : Type u_5} [CommSemiring A'] {ι : Type u_6} {M : ι → Ideal A'} {a : ι → A'} {v : ι →₀ ℕ} (mem : ∀ i ∈ v.support, a i ∈ M i) : a ^ v ∈ M ^ v

Vendored from Project/Dilatation/Multicenter.lean (live, non-commented-out part only)

structure CategoryTheory.Dilatations.Multicenter (A' : Type u_5) [CommSemiring A'] : Type (max u_5 (u_6 + 1))

A family of ideals and corresponding denominator elements in a commutative semiring.

• index : Type u_6

  The index type of the ideal-denominator pairs.

• ideal : self.index → Ideal A'

  The ideal of permitted numerators at each index.

• elem : self.index → A'

  The denominator element at each index.

def CategoryTheory.Dilatations.Multicenter.«term_^ℕ» : Lean.TrailingParserDescr

Finitely supported natural-number exponent profiles on a multicenter.

Equations

• CategoryTheory.Dilatations.Multicenter.«term_^ℕ» = Lean.ParserDescr.trailingNode `CategoryTheory.Dilatations.Multicenter.«term_^ℕ» 1024 0 (Lean.ParserDescr.symbol "^ℕ")

def CategoryTheory.Dilatations.Multicenter.LargeIdeal {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (i : M.index) : Ideal A'

Enlarge the numerator ideal by the principal ideal of its denominator.

Equations

• M.LargeIdeal i = M.ideal i + Ideal.span {M.elem i}

theorem CategoryTheory.Dilatations.Multicenter.elem_mem_LargeIdeal {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (i : M.index) : M.elem i ∈ M.LargeIdeal i

@[reducible, inline]

abbrev CategoryTheory.Dilatations.Multicenter.prodLargeIdealPower {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (v : M.index →₀ ℕ) : Ideal A'

The product of enlarged numerator ideals at an exponent profile.

Equations

• M.prodLargeIdealPower v = v.prod fun (i : M.index) (k : ℕ) => M.LargeIdeal i ^ k

theorem CategoryTheory.Dilatations.Multicenter.elem_pow_mem_LargeIdealPow {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (ν : M.index →₀ ℕ) : M.elem ^ ν ∈ M.LargeIdeal ^ ν

@[reducible]

def CategoryTheory.Dilatations.Multicenter.reindex {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : Multicenter A'

The ν-indexed reindexing of M: index type M^ℕ (exponent profiles), ideal L ^ ν at ν, element a ^ ν at ν. Dilating by this center gives back the same ring as dilating by M directly (reindexRingEquiv below, inside Dilatation).

Equations

• M.reindex = { index := M.index →₀ ℕ, ideal := M.prodLargeIdealPower, elem := fun (ν : M.index →₀ ℕ) => M.elem ^ ν }

theorem CategoryTheory.Dilatations.Multicenter.reindex_LargeIdeal {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (ν : M.index →₀ ℕ) : M.reindex.LargeIdeal ν = M.LargeIdeal ^ ν

reindex's large ideal at ν is just L ^ ν itself : the +span{a ^ ν} correction is already absorbed, since a ^ ν ∈ L ^ ν (elem_pow_mem_LargeIdealPow).

noncomputable def CategoryTheory.Dilatations.Multicenter.flatten {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (μ : (M.index →₀ ℕ) →₀ ℕ) : M.index →₀ ℕ

Flatten a finite ℕ-combination of exponent profiles into a single exponent profile : μ ↦ Σ_ν μ(ν)•ν. This is the comparison map between reindex's own exponent profiles ((M^ℕ) →₀ ℕ) and M's (M^ℕ).

Equations

• M.flatten μ = μ.sum fun (ν : M.index →₀ ℕ) (k : ℕ) => k • ν

theorem CategoryTheory.Dilatations.Multicenter.flatten_add {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (μ μ' : (M.index →₀ ℕ) →₀ ℕ) : M.flatten (μ + μ') = M.flatten μ + M.flatten μ'

theorem CategoryTheory.Dilatations.Multicenter.flatten_zero {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : M.flatten 0 = 0

theorem CategoryTheory.Dilatations.Multicenter.flatten_single {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (ν0 : M.index →₀ ℕ) : M.flatten (Finsupp.single ν0 1) = ν0

theorem CategoryTheory.Dilatations.Multicenter.flatten_surjective {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : Function.Surjective M.flatten

theorem CategoryTheory.Dilatations.Multicenter.reindex_LargeIdeal_pow {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (μ : (M.index →₀ ℕ) →₀ ℕ) : M.reindex.LargeIdeal ^ μ = M.LargeIdeal ^ M.flatten μ

theorem CategoryTheory.Dilatations.Multicenter.reindex_elem_pow {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (μ : (M.index →₀ ℕ) →₀ ℕ) : M.reindex.elem ^ μ = M.elem ^ M.flatten μ

structure CategoryTheory.Dilatations.Multicenter.PreDil {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : Type (max u_5 u_6)

A fraction representative with numerator in the corresponding product ideal.

• pow : M.index →₀ ℕ

  The finitely supported exponent profile of the denominator.

• num : A'

  The numerator of the representative.

• num_mem : self.num ∈ M.LargeIdeal ^ self.pow

def CategoryTheory.Dilatations.Multicenter.r {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : M.PreDil → M.PreDil → Prop

Equality after cross-multiplication and multiplication by another denominator.

Equations

• M.r x y = ∃ (β : M.index →₀ ℕ), x.num * M.elem ^ (β + y.pow) = y.num * M.elem ^ (β + x.pow)

theorem CategoryTheory.Dilatations.Multicenter.r_refl {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.PreDil) : M.r x x

theorem CategoryTheory.Dilatations.Multicenter.r_symm {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : M.r x y → M.r y x

theorem CategoryTheory.Dilatations.Multicenter.r_trans {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y z : M.PreDil) : M.r x y → M.r y z → M.r x z

def CategoryTheory.Dilatations.Multicenter.setoid {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Setoid M.PreDil

The equivalence relation on fraction representatives.

Equations

• CategoryTheory.Dilatations.Multicenter.setoid = { r := M.r, iseqv := ⋯ }

def CategoryTheory.Dilatations.Multicenter.Dilatation {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : Type (max u_5 u_6)

The quotient of permitted fraction representatives by cross-multiplication.

Equations

• M.Dilatation = Quotient CategoryTheory.Dilatations.Multicenter.setoid

def CategoryTheory.Dilatations.Multicenter.«term_[_]» : Lean.TrailingParserDescr

The dilatation of a commutative semiring at a multicenter.

Equations

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

def CategoryTheory.Dilatations.Multicenter.Dilatation.mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.PreDil) : M.Dilatation

Map a fraction representative to its class in the dilatation.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.mk x = ⟦x⟧

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mk_eq_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : mk x = mk y ↔ M.r x y

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.induction_on {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {P : M.Dilatation → Prop} (x : M.Dilatation) (h : ∀ (x : M.PreDil), P (mk x)) : P x

def CategoryTheory.Dilatations.Multicenter.Dilatation.descFun {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {B' : Type u_6} (f : M.PreDil → B') (hf : ∀ (x y : M.PreDil), M.r x y → f x = f y) : M.Dilatation → B'

Descend a relation-respecting function on representatives to the quotient.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.descFun f hf = Quotient.lift f hf

def CategoryTheory.Dilatations.Multicenter.Dilatation.descFun₂ {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {B' : Type u_6} (f : M.PreDil → M.PreDil → B') (hf : ∀ (a b x y : M.PreDil), M.r a b → M.r x y → f a x = f b y) : M.Dilatation → M.Dilatation → B'

Descend a binary function that respects equality of representatives.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.descFun₂ f hf = Quotient.lift₂ f ⋯

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.descFun_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {B' : Type u_6} (f : M.PreDil → B') (hf : ∀ (x y : M.PreDil), M.r x y → f x = f y) (x : M.PreDil) : descFun f hf (mk x) = f x

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.descFun₂_mk_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {B' : Type u_6} (f : M.PreDil → M.PreDil → B') (hf : ∀ (a b x y : M.PreDil), M.r a b → M.r x y → f a x = f b y) (x y : M.PreDil) : descFun₂ f hf (mk x) (mk y) = f x y

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.add' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : M.PreDil

Addition of representatives using a common denominator.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.add' x y = { pow := x.pow + y.pow, num := M.elem ^ y.pow * x.num + M.elem ^ x.pow * y.num, num_mem := ⋯ }

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.add'_pow {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : (add' x y).pow = x.pow + y.pow

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.add'_num {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : (add' x y).num = M.elem ^ y.pow * x.num + M.elem ^ x.pow * y.num

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.add'_respects {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {x x' y y' : M.PreDil} (hx : M.r x x') (hy : M.r y y') : M.r (add' x y) (add' x' y')

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instAdd {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Add M.Dilatation

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mk_add_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : mk x + mk y = mk (add' x y)

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.mul' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : M.PreDil

Multiplication of representatives by multiplying their numerators.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.mul' x y = { pow := x.pow + y.pow, num := x.num * y.num, num_mem := ⋯ }

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mul'_num {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : (mul' x y).num = x.num * y.num

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mul'_pow {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : (mul' x y).pow = x.pow + y.pow

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.dist' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y z : M.PreDil) : M.r (mul' x (add' y z)) (add' (mul' x y) (mul' x z))

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instMul {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Mul M.Dilatation

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mk_mul_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.PreDil) : mk x * mk y = mk (mul' x y)

@[instance_reducible]

instance CategoryTheory.Dilatations.Multicenter.Dilatation.instZero {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Zero M.Dilatation

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.instZero = { zero := CategoryTheory.Dilatations.Multicenter.Dilatation.mk { pow := 0, num := 0, num_mem := ⋯ } }

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.zero_def {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : 0 = mk { pow := 0, num := 0, num_mem := ⋯ }

@[instance_reducible]

instance CategoryTheory.Dilatations.Multicenter.Dilatation.instOne {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : One M.Dilatation

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.instOne = { one := CategoryTheory.Dilatations.Multicenter.Dilatation.mk { pow := 0, num := 1, num_mem := ⋯ } }

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.one_def {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : 1 = mk { pow := 0, num := 1, num_mem := ⋯ }

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instAddCommMonoid {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : AddCommMonoid M.Dilatation

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.monoid {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Monoid M.Dilatation

Equations

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

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instCommSemiring {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : CommSemiring M.Dilatation

Equations

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

def CategoryTheory.Dilatations.Multicenter.Dilatation.fromBaseRing {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') : A' →+* M.Dilatation

The canonical ring homomorphism sending a base element to denominator one.

Equations

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

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.fromBaseRing_apply {A' : Type u_5} [CommSemiring A'] (M : Multicenter A') (x : A') : (fromBaseRing M) x = mk { pow := 0, num := x, num_mem := ⋯ }

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instAlgebra {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : Algebra A' M.Dilatation

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.instAlgebra = (CategoryTheory.Dilatations.Multicenter.Dilatation.fromBaseRing M).toAlgebra

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.algebraMap_eq {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : algebraMap A' M.Dilatation = fromBaseRing M

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.algebraMap_apply {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : A') : (algebraMap A' M.Dilatation) x = mk { pow := 0, num := x, num_mem := ⋯ }

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.smul_mk {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : A') (y : M.PreDil) : x • mk y = mk { pow := y.pow, num := x * y.num, num_mem := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.Dilatations.Multicenter.Dilatation.frac {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (ν : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ ν)) : M.Dilatation

The fraction of a permitted numerator by a denominator exponent profile.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.frac ν m = CategoryTheory.Dilatations.Multicenter.Dilatation.mk { pow := ν, num := ↑m, num_mem := ⋯ }

def CategoryTheory.Dilatations.Multicenter.Dilatation.«term_/.[_]_» : Lean.TrailingParserDescr

Fraction notation with an explicit multicenter.

Equations

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

def CategoryTheory.Dilatations.Multicenter.Dilatation.«term_/._» : Lean.TrailingParserDescr

Fraction notation with the multicenter inferred from the numerator type.

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.frac_add_frac {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (v w : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (n : ↥(M.LargeIdeal ^ w)) : frac v m + frac w n = frac (v + w) ⟨↑m * M.elem ^ w + ↑n * M.elem ^ v, ⋯⟩

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.frac_mul_frac {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (v w : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (n : ↥(M.LargeIdeal ^ w)) : frac v m * frac w n = frac (v + w) ⟨↑m * ↑n, ⋯⟩

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.smul_frac {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (a : A') (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) : a • frac v m = frac v (a • m)

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.nonzerodiv_image {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (v : M.index →₀ ℕ) : (algebraMap A' M.Dilatation) (M.elem ^ v) ∈ nonZeroDivisors M.Dilatation

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

Each denominator becomes a non-zero-divisor in the dilatation.

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.image_elem_LargeIdeal_equal {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (v : M.index →₀ ℕ) : Ideal.span {(algebraMap A' M.Dilatation) (M.elem ^ v)} = Ideal.map (algebraMap A' M.Dilatation) (M.LargeIdeal ^ v)

Reindexing invariance : A'[M.reindex] ≃+* A'[M]

A purely ring-theoretic fact, independent of the comparison with categories : dilating by the ν-indexed reindexing of M (Multicenter.reindex) gives back the same ring as dilating by M directly. The forward map sends a ν-indexed generator ⟨μ,m,hm⟩ to ⟨flatten μ, m,_⟩; the backward map sends ⟨ν,m,hm⟩ to the singleton-profile generator ⟨single ν 1, m,_⟩.

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.reindex.PreDil) : M.PreDil

The forward direction on representatives : ⟨μ,m,hm⟩ ↦ ⟨flatten μ, m, _⟩.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil x = { pow := M.flatten x.pow, num := x.num, num_mem := ⋯ }

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil_respects {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {x y : M.reindex.PreDil} (h : M.reindex.r x y) : M.r (toPreDil x) (toPreDil y)

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : M.reindex.Dilatation → M.Dilatation

Flatten exponent profiles to map the reindexed dilatation to the original.

Equations

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

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.PreDil) : M.reindex.PreDil

The backward direction on representatives : ⟨ν,m,hm⟩ ↦ ⟨single ν 1, m, _⟩.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil' x = { pow := Finsupp.single x.pow 1, num := x.num, num_mem := ⋯ }

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil'_respects {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} {x y : M.PreDil} (h : M.r x y) : M.reindex.r (toPreDil' x) (toPreDil' y)

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : M.Dilatation → M.reindex.Dilatation

Embed representatives using singleton profiles in the reindexed dilatation.

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil_toPreDil' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.PreDil) : toPreDil (toPreDil' x) = x

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil'_toPreDil {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (y : M.reindex.PreDil) : M.reindex.r (toPreDil' (toPreDil y)) y

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_toDilatation' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x : M.Dilatation) : x.toDilatation'.toDilatation = x

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation'_toDilatation {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (y : M.reindex.Dilatation) : y.toDilatation.toDilatation' = y

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil_add' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.reindex.PreDil) : toPreDil (add' x y) = add' (toPreDil x) (toPreDil y)

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toPreDil_mul' {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.reindex.PreDil) : toPreDil (mul' x y) = mul' (toPreDil x) (toPreDil y)

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_zero {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : toDilatation 0 = 0

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_one {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : toDilatation 1 = 1

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_add {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.reindex.Dilatation) : (x + y).toDilatation = x.toDilatation + y.toDilatation

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_mul {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (x y : M.reindex.Dilatation) : (x * y).toDilatation = x.toDilatation * y.toDilatation

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.reindexRingEquiv {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : M.reindex.Dilatation ≃+* M.Dilatation

Ring-theoretic reindexing invariance. Dilating by the ν-indexed reindexing of M (Multicenter.reindex) gives back the same ring as dilating by M directly.

Equations

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

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.toDilatation_algebraMap {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} (a : A') : ((algebraMap A' M.reindex.Dilatation) a).toDilatation = (algebraMap A' M.Dilatation) a

Flattening exponent profiles fixes the image of each base element.

noncomputable def CategoryTheory.Dilatations.Multicenter.Dilatation.reindexAlgEquiv {A' : Type u_5} [CommSemiring A'] {M : Multicenter A'} : M.reindex.Dilatation ≃ₐ[A'] M.Dilatation

Reindexing is an isomorphism of algebras over the original commutative semiring.

Equations

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

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

def CategoryTheory.Dilatations.Multicenter.Dilatation.neg' {A' : Type u_5} [CommRing A'] {M : Multicenter A'} (x : M.PreDil) : M.PreDil

Negation of a representative by negating its numerator.

Equations

• CategoryTheory.Dilatations.Multicenter.Dilatation.neg' x = { pow := x.pow, num := -x.num, num_mem := ⋯ }

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.neg'_pow {A' : Type u_5} [CommRing A'] {M : Multicenter A'} (x : M.PreDil) : (neg' x).pow = x.pow

@[simp]

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.neg'_num {A' : Type u_5} [CommRing A'] {M : Multicenter A'} (x : M.PreDil) : (neg' x).num = -x.num

@[instance_reducible]

instance CategoryTheory.Dilatations.Multicenter.Dilatation.instNeg {A' : Type u_5} [CommRing A'] {M : Multicenter A'} : Neg M.Dilatation

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.mk_neg {A' : Type u_5} [CommRing A'] {M : Multicenter A'} (x : M.PreDil) : -mk x = mk (neg' x)

@[instance_reducible]

noncomputable instance CategoryTheory.Dilatations.Multicenter.Dilatation.instCommRing {A' : Type u_5} [CommRing A'] {M : Multicenter A'} : CommRing M.Dilatation

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.Dilatation.neg_frac {A' : Type u_5} [CommRing A'] {M : Multicenter A'} (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) : -frac v m = frac v (-m)

theorem CategoryTheory.Dilatations.Multicenter.cond_univ_implies_large_cond {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) (ν : M.index →₀ ℕ) : Ideal.span {(algebraMap A' B') (M.elem ^ ν)} = Ideal.map (algebraMap A' B') (M.LargeIdeal ^ ν)

theorem CategoryTheory.Dilatations.Multicenter.equ_trivial_image_divisor_ring {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (i : M.index) : Ideal.map (algebraMap A' B') (Ideal.span {M.elem i}) = Ideal.span {(algebraMap A' B') (M.elem i)}

theorem CategoryTheory.Dilatations.Multicenter.equiv_small_big_cond {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] : (∀ (i : M.index), Ideal.map (algebraMap A' B') (Ideal.span {M.elem i}) = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) ↔ ∀ (i : M.index), Ideal.map (algebraMap A' B') (Ideal.span {M.elem i}) ≥ Ideal.map (algebraMap A' B') (M.ideal i)

theorem CategoryTheory.Dilatations.Multicenter.lemma_exists_in_image {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) (ν : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ ν)) : ∃! bm : B', (algebraMap A' B') (M.elem ^ ν) * bm = (algebraMap A' B') ↑m

noncomputable def CategoryTheory.Dilatations.Multicenter.fractionValue {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) : B'

The unique quotient of a mapped numerator by its mapped denominator.

Equations

• M.fractionValue v m non_zero_divisor gen = Exists.choose ⋯

theorem CategoryTheory.Dilatations.Multicenter.fractionValue_spec {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) : (algebraMap A' B') (M.elem ^ v) * M.fractionValue v m non_zero_divisor gen = (algebraMap A' B') ↑m

theorem CategoryTheory.Dilatations.Multicenter.fractionValue_unique {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) (bm : B') : (algebraMap A' B') (M.elem ^ v) * bm = (algebraMap A' B') ↑m → M.fractionValue v m non_zero_divisor gen = bm

noncomputable def CategoryTheory.Dilatations.Multicenter.desc {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) : M.Dilatation →ₐ[A'] B'

The algebra homomorphism determined by the universal property of ring dilatations.

Equations

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

theorem CategoryTheory.Dilatations.Multicenter.dsc_spec {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (v : M.index →₀ ℕ) (m : ↥(M.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) : (algebraMap A' B') (M.elem ^ v) * (M.desc non_zero_divisor gen) (Dilatation.frac v m) = (algebraMap A' B') ↑m

theorem CategoryTheory.Dilatations.Multicenter.lemma_exists_unique_morphism {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] (M : Multicenter A') [Algebra A' B'] (non_zero_divisor : ∀ (i : M.index), (algebraMap A' B') (M.elem i) ∈ nonZeroDivisors B') (gen : ∀ (i : M.index), Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)) (χ' : M.Dilatation →ₐ[A'] B') : χ' = M.desc non_zero_divisor gen

theorem CategoryTheory.Dilatations.Multicenter.reciprocal_for_univ {A' : Type u_5} {B' : Type u_6} [CommRing A'] [CommRing B'] [Algebra A' B'] (M : Multicenter A') (χ' : M.Dilatation →ₐ[A'] B') (i : M.index) : Ideal.span {(algebraMap A' B') (M.elem i)} = Ideal.map (algebraMap A' B') (M.LargeIdeal i)