structure Multicenter (A : Type u_1) [CommSemiring A] : Type (max u_1 (u_2 + 1))

• index : Type u_2
• ideal : self.index → Ideal A
• elem : self.index → A

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

Equations

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

noncomputable def Multicenter.LargeIdeal {A : Type u_1} [CommSemiring A] (F : Multicenter A) (i : F.index) : Ideal A

Equations

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

theorem Multicenter.elem_mem_LargeIdeal {A : Type u_1} [CommSemiring A] (F : Multicenter A) (i : F.index) : F.elem i ∈ F.LargeIdeal i

@[reducible, inline]

noncomputable abbrev Multicenter.prodLargeIdealPower {A : Type u_1} [CommSemiring A] (F : Multicenter A) (v : F.index →₀ ℕ) : Ideal A

Equations

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

structure Multicenter.PreDil {A : Type u_1} [CommSemiring A] (F : Multicenter A) : Type (max u_1 u_2)

• pow : F.index →₀ ℕ
• num : A
• num_mem : self.num ∈ F.LargeIdeal ^ self.pow

noncomputable def Multicenter.r {A : Type u_1} [CommSemiring A] (F : Multicenter A) : F.PreDil → F.PreDil → Prop

Equations

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

theorem Multicenter.r_refl {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x : F.PreDil) : F.r x x

theorem Multicenter.r_symm {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : F.r x y → F.r y x

theorem Multicenter.r_trans {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y z : F.PreDil) : F.r x y → F.r y z → F.r x z

noncomputable def Multicenter.setoid {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Setoid F.PreDil

Equations

• Multicenter.setoid = { r := F.r, iseqv := ⋯ }

noncomputable def Multicenter.Dilatation {A : Type u_1} [CommSemiring A] (F : Multicenter A) : Type (max u_1 u_2)

Equations

• F.Dilatation = Quotient Multicenter.setoid

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

Equations

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

noncomputable def Multicenter.Dilatation.mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x : F.PreDil) : F.Dilatation

Equations

• Multicenter.Dilatation.mk x = ⟦x⟧

theorem Multicenter.Dilatation.mk_eq_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : Multicenter.Dilatation.mk x = Multicenter.Dilatation.mk y ↔ F.r x y

theorem Multicenter.Dilatation.induction_on {A : Type u_1} [CommSemiring A] {F : Multicenter A} {C : F.Dilatation → Prop} (x : F.Dilatation) (h : ∀ (x : F.PreDil), C (Multicenter.Dilatation.mk x)) : C x

noncomputable def Multicenter.Dilatation.descFun {A : Type u_1} [CommSemiring A] {F : Multicenter A} {B : Type u_2} (f : F.PreDil → B) (hf : ∀ (x y : F.PreDil), F.r x y → f x = f y) : F.Dilatation → B

Equations

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

noncomputable def Multicenter.Dilatation.descFun₂ {A : Type u_1} [CommSemiring A] {F : Multicenter A} {B : Type u_2} (f : F.PreDil → F.PreDil → B) (hf : ∀ (a b x y : F.PreDil), F.r a b → F.r x y → f a x = f b y) : F.Dilatation → F.Dilatation → B

Equations

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

@[simp]

theorem Multicenter.Dilatation.descFun_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} {B : Type u_2} (f : F.PreDil → B) (hf : ∀ (x y : F.PreDil), F.r x y → f x = f y) (x : F.PreDil) : Multicenter.Dilatation.descFun f hf (Multicenter.Dilatation.mk x) = f x

@[simp]

theorem Multicenter.Dilatation.descFun₂_mk_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} {B : Type u_2} (f : F.PreDil → F.PreDil → B) (hf : ∀ (a b x y : F.PreDil), F.r a b → F.r x y → f a x = f b y) (x y : F.PreDil) : Multicenter.Dilatation.descFun₂ f hf (Multicenter.Dilatation.mk x) (Multicenter.Dilatation.mk y) = f x y

noncomputable def Multicenter.Dilatation.add' {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : F.PreDil

Equations

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

@[simp]

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

@[simp]

theorem Multicenter.Dilatation.add'_pow {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : (Multicenter.Dilatation.add' x y).pow = x.pow + y.pow

noncomputable instance Multicenter.Dilatation.instAdd {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Add F.Dilatation

Equations

• Multicenter.Dilatation.instAdd = { add := Multicenter.Dilatation.descFun₂ (fun (x y : F.PreDil) => Multicenter.Dilatation.mk (Multicenter.Dilatation.add' x y)) ⋯ }

theorem Multicenter.Dilatation.mk_add_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : Multicenter.Dilatation.mk x + Multicenter.Dilatation.mk y = Multicenter.Dilatation.mk (Multicenter.Dilatation.add' x y)

noncomputable def Multicenter.Dilatation.mul' {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : F.PreDil

Equations

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

@[simp]

theorem Multicenter.Dilatation.mul'_pow {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : (Multicenter.Dilatation.mul' x y).pow = x.pow + y.pow

@[simp]

theorem Multicenter.Dilatation.mul'_num {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : (Multicenter.Dilatation.mul' x y).num = x.num * y.num

theorem Multicenter.Dilatation.dist' {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y z : F.PreDil) : F.r (Multicenter.Dilatation.mul' x (Multicenter.Dilatation.add' y z)) (Multicenter.Dilatation.add' (Multicenter.Dilatation.mul' x y) (Multicenter.Dilatation.mul' x z))

noncomputable instance Multicenter.Dilatation.instMul {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Mul F.Dilatation

Equations

• Multicenter.Dilatation.instMul = { mul := Multicenter.Dilatation.descFun₂ (fun (x y : F.PreDil) => Multicenter.Dilatation.mk (Multicenter.Dilatation.mul' x y)) ⋯ }

theorem Multicenter.Dilatation.mk_mul_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x y : F.PreDil) : Multicenter.Dilatation.mk x * Multicenter.Dilatation.mk y = Multicenter.Dilatation.mk (Multicenter.Dilatation.mul' x y)

noncomputable instance Multicenter.Dilatation.instZero {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Zero F.Dilatation

Equations

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

theorem Multicenter.Dilatation.zero_def {A : Type u_1} [CommSemiring A] {F : Multicenter A} : 0 = Multicenter.Dilatation.mk { pow := 0, num := 0, num_mem := ⋯ }

noncomputable instance Multicenter.Dilatation.instOne {A : Type u_1} [CommSemiring A] {F : Multicenter A} : One F.Dilatation

Equations

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

theorem Multicenter.Dilatation.one_def {A : Type u_1} [CommSemiring A] {F : Multicenter A} : 1 = Multicenter.Dilatation.mk { pow := 0, num := 1, num_mem := ⋯ }

noncomputable instance Multicenter.Dilatation.instAddCommMonoid {A : Type u_1} [CommSemiring A] {F : Multicenter A} : AddCommMonoid F.Dilatation

Equations

• Multicenter.Dilatation.instAddCommMonoid = AddCommMonoid.mk ⋯

noncomputable instance Multicenter.Dilatation.monoid {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Monoid F.Dilatation

Equations

• Multicenter.Dilatation.monoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

noncomputable instance Multicenter.Dilatation.instCommSemiring {A : Type u_1} [CommSemiring A] {F : Multicenter A} : CommSemiring F.Dilatation

Equations

• Multicenter.Dilatation.instCommSemiring = CommSemiring.mk ⋯

noncomputable def Multicenter.Dilatation.fromBaseRing {A : Type u_1} [CommSemiring A] (F : Multicenter A) : A →+* F.Dilatation

Equations

• Multicenter.Dilatation.fromBaseRing F = { toFun := fun (x : A) => Multicenter.Dilatation.mk { pow := 0, num := x, num_mem := ⋯ }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Multicenter.Dilatation.fromBaseRing_apply {A : Type u_1} [CommSemiring A] (F : Multicenter A) (x : A) : (Multicenter.Dilatation.fromBaseRing F) x = Multicenter.Dilatation.mk { pow := 0, num := x, num_mem := ⋯ }

noncomputable instance Multicenter.Dilatation.instAlgebra {A : Type u_1} [CommSemiring A] {F : Multicenter A} : Algebra A F.Dilatation

Equations

• Multicenter.Dilatation.instAlgebra = (Multicenter.Dilatation.fromBaseRing F).toAlgebra

theorem Multicenter.Dilatation.algebraMap_eq {A : Type u_1} [CommSemiring A] {F : Multicenter A} : algebraMap A F.Dilatation = Multicenter.Dilatation.fromBaseRing F

theorem Multicenter.Dilatation.algebraMap_apply {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x : A) : (algebraMap A F.Dilatation) x = Multicenter.Dilatation.mk { pow := 0, num := x, num_mem := ⋯ }

theorem Multicenter.Dilatation.smul_mk {A : Type u_1} [CommSemiring A] {F : Multicenter A} (x : A) (y : F.PreDil) : x • Multicenter.Dilatation.mk y = Multicenter.Dilatation.mk { pow := y.pow, num := x * y.num, num_mem := ⋯ }

@[reducible, inline]

noncomputable abbrev Multicenter.Dilatation.frac {A : Type u_1} [CommSemiring A] {F : Multicenter A} (ν : F.index →₀ ℕ) (m : ↥(F.LargeIdeal ^ ν)) : F.Dilatation

Equations

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

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

Equations

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

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

Equations

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

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

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

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

theorem Multicenter.Dilatation.nonzerodiv_image {A : Type u_1} [CommSemiring A] {F : Multicenter A} (v : F.index →₀ ℕ) : (algebraMap A F.Dilatation) (F.elem ^ v) ∈ nonZeroDivisors F.Dilatation

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

noncomputable def Multicenter.Dilatation.neg' {A : Type u_1} [CommRing A] {F : Multicenter A} (x : F.PreDil) : F.PreDil

Equations

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

@[simp]

theorem Multicenter.Dilatation.neg'_num {A : Type u_1} [CommRing A] {F : Multicenter A} (x : F.PreDil) : (Multicenter.Dilatation.neg' x).num = -x.num

@[simp]

theorem Multicenter.Dilatation.neg'_pow {A : Type u_1} [CommRing A] {F : Multicenter A} (x : F.PreDil) : (Multicenter.Dilatation.neg' x).pow = x.pow

noncomputable instance Multicenter.Dilatation.instNeg {A : Type u_1} [CommRing A] {F : Multicenter A} : Neg F.Dilatation

Equations

• Multicenter.Dilatation.instNeg = { neg := Multicenter.Dilatation.descFun (Multicenter.Dilatation.mk ∘ Multicenter.Dilatation.neg') ⋯ }

theorem Multicenter.Dilatation.mk_neg {A : Type u_1} [CommRing A] {F : Multicenter A} (x : F.PreDil) : -Multicenter.Dilatation.mk x = Multicenter.Dilatation.mk (Multicenter.Dilatation.neg' x)

noncomputable instance Multicenter.Dilatation.instCommRing {A : Type u_1} [CommRing A] {F : Multicenter A} : CommRing F.Dilatation

Equations

• Multicenter.Dilatation.instCommRing = CommRing.mk ⋯

theorem Multicenter.Dilatation.neg_frac {A : Type u_1} [CommRing A] {F : Multicenter A} (v : F.index →₀ ℕ) (m : ↥(F.LargeIdeal ^ v)) : -Multicenter.Dilatation.frac v m = Multicenter.Dilatation.frac v (-m)

theorem Multicenter.cond_univ_implies_large_cond {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (gen : ∀ (i : F.index), Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)) (ν : F.index →₀ ℕ) : Ideal.span {(algebraMap A B) (F.elem ^ ν)} = Ideal.map (algebraMap A B) (F.LargeIdeal ^ ν)

theorem Multicenter.equ_trivial_image_divisor_ring {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (i : F.index) : Ideal.map (algebraMap A B) (Ideal.span {F.elem i}) = Ideal.span {(algebraMap A B) (F.elem i)}

theorem Multicenter.equiv_small_big_cond {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] : (∀ (i : F.index), Ideal.map (algebraMap A B) (Ideal.span {F.elem i}) = Ideal.map (algebraMap A B) (F.LargeIdeal i)) ↔ ∀ (i : F.index), Ideal.map (algebraMap A B) (Ideal.span {F.elem i}) ≥ Ideal.map (algebraMap A B) (F.ideal i)

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

noncomputable def Multicenter.def_unique_elem {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (v : F.index →₀ ℕ) (m : ↥(F.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : F.index), (algebraMap A B) (F.elem i) ∈ nonZeroDivisors B) (gen : ∀ (i : F.index), Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)) : B

Equations

• F.def_unique_elem v m non_zero_divisor gen = Exists.choose ⋯

theorem Multicenter.def_unique_elem_spec {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (v : F.index →₀ ℕ) (m : ↥(F.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : F.index), (algebraMap A B) (F.elem i) ∈ nonZeroDivisors B) (gen : ∀ (i : F.index), Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)) : (algebraMap A B) (F.elem ^ v) * F.def_unique_elem v m non_zero_divisor gen = (algebraMap A B) ↑m

theorem Multicenter.def_unique_elem_unique {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (v : F.index →₀ ℕ) (m : ↥(F.LargeIdeal ^ v)) (non_zero_divisor : ∀ (i : F.index), (algebraMap A B) (F.elem i) ∈ nonZeroDivisors B) (gen : ∀ (i : F.index), Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)) (bm : B) : (algebraMap A B) (F.elem ^ v) * bm = (algebraMap A B) ↑m → F.def_unique_elem v m non_zero_divisor gen = bm

noncomputable def Multicenter.desc {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (non_zero_divisor : ∀ (i : F.index), (algebraMap A B) (F.elem i) ∈ nonZeroDivisors B) (gen : ∀ (i : F.index), Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)) : F.Dilatation →ₐ[A] B

Equations

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

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

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

theorem Multicenter.reciprocal_for_univ {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (F : Multicenter A) (χ' : F.Dilatation →ₐ[A] B) (i : F.index) : Ideal.span {(algebraMap A B) (F.elem i)} = Ideal.map (algebraMap A B) (F.LargeIdeal i)

noncomputable def Multicenter.image_mult {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] : Multicenter B

/ def cat_dil_test_reg (F: Multicenter A) fullsubcategory of Cat A-alg , Objects := {f:A→+* B | f (F.elem i) ∈ nonZeroDivisors B } := by sorry

lemma dil_representable_functor (F: Multicenter A) : A[F] represents the functor cat_dil_test_reg A F → Set, f ↦ singleton if ∀ i, Ideal.span {f (F.elem i)} ⊇ f (F.LargeIdeal i) emptyset else := by sorry

Equations

• F.image_mult = { index := F.index, ideal := fun (i : F.index) => Ideal.map (algebraMap A B) (F.ideal i), elem := fun (i : F.index) => (algebraMap A B) (F.elem i) }

@[simp]

theorem Multicenter.image_mult_index {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] : F.image_mult.index = F.index

@[simp]

theorem Multicenter.image_mult_elem {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (i : F.index) : F.image_mult.elem i = (algebraMap A B) (F.elem i)

@[simp]

theorem Multicenter.image_mult_ideal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (F : Multicenter A) [Algebra A B] (i : F.index) : F.image_mult.ideal i = Ideal.map (algebraMap A B) (F.ideal i)