Marked ideals and their cosupport

A marked ideal [Kol07, Definitions 48 and 59] is a pair (I, m) of an ideal and a natural number, the mark being the order one pretends I has; a marked element (Kollár: marked function) is a pair (f, m). This file gives the local, ring-level forms: the cosupport predicate says m ≤ ord I ("the closed point lies in cosupp (I, m)"); products add the marks and sums are defined for equal marks only; the four elementary properties of the cosupport listed in [Kol07, Definition 59] are restatements of the calculus of the order (Hironaka/Algebra/Local/Order.lean). The marked derivative D(I, m) = (D(I), m - 1) acts on this structure in Hironaka/Algebra/Local/Derivative.lean.

structure IsLocalRing.MarkedIdeal (R : Type u_1) [CommRing R] : Type u_1

A marked ideal [Kol07, Definitions 48 and 59]: an ideal I together with a mark m : ℕ.

• I : Ideal R

  The ideal.

• m : ℕ

  The mark.

theorem IsLocalRing.MarkedIdeal.ext {R : Type u_1} {inst✝ : CommRing R} {x y : MarkedIdeal R} (I : x.I = y.I) (m : x.m = y.m) : x = y

theorem IsLocalRing.MarkedIdeal.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : MarkedIdeal R} : x = y ↔ x.I = y.I ∧ x.m = y.m

structure IsLocalRing.MarkedElem (R : Type u_1) : Type u_1

A marked element (Kollár's "marked function", [Kol07, Definition 59]): an element f together with a mark m : ℕ.

• f : R

  The element.

• m : ℕ

  The mark.

theorem IsLocalRing.MarkedElem.ext {R : Type u_1} {x y : MarkedElem R} (f : x.f = y.f) (m : x.m = y.m) : x = y

theorem IsLocalRing.MarkedElem.ext_iff {R : Type u_1} {x y : MarkedElem R} : x = y ↔ x.f = y.f ∧ x.m = y.m

@[instance_reducible]

instance IsLocalRing.MarkedIdeal.instMul {R : Type u_1} [CommRing R] : Mul (MarkedIdeal R)

The product (I₁, m₁) · (I₂, m₂) = (I₁ I₂, m₁ + m₂) [Kol07, Definition 59].

Equations

• IsLocalRing.MarkedIdeal.instMul = { mul := fun (J K : IsLocalRing.MarkedIdeal R) => { I := J.I * K.I, m := J.m + K.m } }

@[simp]

theorem IsLocalRing.MarkedIdeal.mul_I {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) : (J * K).I = J.I * K.I

@[simp]

theorem IsLocalRing.MarkedIdeal.mul_m {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) : (J * K).m = J.m + K.m

theorem IsLocalRing.MarkedIdeal.mul_def {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) : J * K = { I := J.I * K.I, m := J.m + K.m }

def IsLocalRing.MarkedIdeal.add {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) (_h : J.m = K.m) : MarkedIdeal R

The sum (I₁, m) + (I₂, m) = (I₁ + I₂, m), "only sensible when the markings are the same" [Kol07, Definition 59].

Equations

• J.add K _h = { I := J.I ⊔ K.I, m := J.m }

@[simp]

theorem IsLocalRing.MarkedIdeal.add_I {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) (h : J.m = K.m) : (J.add K h).I = J.I ⊔ K.I

@[simp]

theorem IsLocalRing.MarkedIdeal.add_m {R : Type u_1} [CommRing R] (J K : MarkedIdeal R) (h : J.m = K.m) : (J.add K h).m = J.m

def IsLocalRing.MarkedIdeal.InCosupp {R : Type u_1} [CommRing R] [IsLocalRing R] (J : MarkedIdeal R) : Prop

The local cosupport predicate: "the closed point lies in cosupp (I, m)" [Kol07, Definition 59], i.e. m ≤ ord I.

Equations

• J.InCosupp = (↑J.m ≤ IsLocalRing.ord J.I)

theorem IsLocalRing.MarkedIdeal.inCosupp_iff_le_pow {R : Type u_1} [CommRing R] [IsLocalRing R] (J : MarkedIdeal R) : J.InCosupp ↔ J.I ≤ maximalIdeal R ^ J.m

theorem IsLocalRing.MarkedIdeal.inCosupp_anti {R : Type u_1} [CommRing R] [IsLocalRing R] {I J : Ideal R} {m : ℕ} (h : I ≤ J) (hJ : { I := J, m := m }.InCosupp) : { I := I, m := m }.InCosupp

cosupp (J, m) ⊆ cosupp (I, m) for I ≤ J (property (1) of [Kol07, Definition 59]).

theorem IsLocalRing.MarkedIdeal.inCosupp_mul {R : Type u_1} [CommRing R] [IsLocalRing R] {J K : MarkedIdeal R} (hJ : J.InCosupp) (hK : K.InCosupp) : (J * K).InCosupp

cosupp (I₁, m₁) ∩ cosupp (I₂, m₂) ⊆ cosupp (I₁ I₂, m₁ + m₂) (property (2) of [Kol07, Definition 59]).

theorem IsLocalRing.MarkedIdeal.inCosupp_pow {R : Type u_1} [CommRing R] [IsLocalRing R] {J : MarkedIdeal R} (c : ℕ) (h : J.InCosupp) : { I := J.I ^ c, m := J.m * c }.InCosupp

cosupp (I, m) ⊆ cosupp (I^c, mc): the inclusion of property (3) of [Kol07, Definition 59] valid in every local ring.

theorem IsLocalRing.MarkedIdeal.inCosupp_add_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {J K : MarkedIdeal R} (h : J.m = K.m) : (J.add K h).InCosupp ↔ J.InCosupp ∧ K.InCosupp

cosupp (I₁ + I₂, m) = cosupp (I₁, m) ∩ cosupp (I₂, m) (property (4) of [Kol07, Definition 59]).

theorem IsLocalRing.MarkedIdeal.inCosupp_pow_iff_of_ordElem_mul {R : Type u_1} [CommRing R] [IsRegularLocalRing R] (hmul : ∀ (f g : R), ordElem (f * g) = ordElem f + ordElem g) (J : MarkedIdeal R) {c : ℕ} (hc : 1 ≤ c) : J.InCosupp ↔ { I := J.I ^ c, m := J.m * c }.InCosupp

cosupp (I, m) = cosupp (I^c, mc) for c ≥ 1 (property (3) of [Kol07, Definition 59]), given multiplicativity of the order on elements (through ord (I^c) = c · ord I, ord_pow_of_ordElem_mul).

@[instance_reducible]

instance IsLocalRing.MarkedElem.instMul {R : Type u_1} [Mul R] : Mul (MarkedElem R)

(f₁, m₁) · (f₂, m₂) = (f₁ f₂, m₁ + m₂) [Kol07, Definition 59].

Equations

• IsLocalRing.MarkedElem.instMul = { mul := fun (a b : IsLocalRing.MarkedElem R) => { f := a.f * b.f, m := a.m + b.m } }

@[simp]

theorem IsLocalRing.MarkedElem.mul_f {R : Type u_1} [Mul R] (a b : MarkedElem R) : (a * b).f = a.f * b.f

@[simp]

theorem IsLocalRing.MarkedElem.mul_m {R : Type u_1} [Mul R] (a b : MarkedElem R) : (a * b).m = a.m + b.m

theorem IsLocalRing.MarkedElem.mul_def {R : Type u_1} [Mul R] (a b : MarkedElem R) : a * b = { f := a.f * b.f, m := a.m + b.m }

def IsLocalRing.MarkedElem.add {R : Type u_1} [Add R] (a b : MarkedElem R) (_h : a.m = b.m) : MarkedElem R

(f₁, m) + (f₂, m) = (f₁ + f₂, m) for equal marks [Kol07, Definition 59].

Equations

• a.add b _h = { f := a.f + b.f, m := a.m }

@[simp]

theorem IsLocalRing.MarkedElem.add_f {R : Type u_1} [Add R] (a b : MarkedElem R) (h : a.m = b.m) : (a.add b h).f = a.f + b.f

@[simp]

theorem IsLocalRing.MarkedElem.add_m {R : Type u_1} [Add R] (a b : MarkedElem R) (h : a.m = b.m) : (a.add b h).m = a.m

def IsLocalRing.MarkedElem.toMarkedIdeal {R : Type u_1} [CommRing R] (a : MarkedElem R) : MarkedIdeal R

The marked ideal (⟨f⟩, m) of a marked element (f, m).

Equations

• a.toMarkedIdeal = { I := Ideal.span {a.f}, m := a.m }

@[simp]

theorem IsLocalRing.MarkedElem.toMarkedIdeal_I {R : Type u_1} [CommRing R] (a : MarkedElem R) : a.toMarkedIdeal.I = Ideal.span {a.f}

@[simp]

theorem IsLocalRing.MarkedElem.toMarkedIdeal_m {R : Type u_1} [CommRing R] (a : MarkedElem R) : a.toMarkedIdeal.m = a.m

theorem IsLocalRing.MarkedElem.toMarkedIdeal_mul {R : Type u_1} [CommRing R] (a b : MarkedElem R) : (a * b).toMarkedIdeal = a.toMarkedIdeal * b.toMarkedIdeal

def IsLocalRing.MarkedElem.InCosupp {R : Type u_1} [CommRing R] [IsLocalRing R] (a : MarkedElem R) : Prop

The cosupport predicate for marked elements: m ≤ ord f.

Equations

• a.InCosupp = (↑a.m ≤ IsLocalRing.ordElem a.f)

theorem IsLocalRing.MarkedElem.inCosupp_toMarkedIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (a : MarkedElem R) : a.toMarkedIdeal.InCosupp ↔ a.InCosupp

theorem IsLocalRing.MarkedElem.inCosupp_iff_mem_pow {R : Type u_1} [CommRing R] [IsLocalRing R] (a : MarkedElem R) : a.InCosupp ↔ a.f ∈ maximalIdeal R ^ a.m