Divided powers

Let A be a commutative (semi)ring and I be an ideal of A. A divided power structure on I is the datum of operations a n ↦ dpow a n satisfying relations that model the intuitive formula dpow n a = a ^ n / n ! and collected by the structure DividedPowers. The list of axioms is embedded in the structure: To avoid coercions, we rather consider DividedPowers.dpow : ℕ → A → A, extended by 0.

• DividedPowers.dpow_null asserts that dpow n x = 0 for x ∉ I

• DividedPowers.dpow_mem : dpow n x ∈ I for n ≠ 0 For x y : A and m n : ℕ such that x ∈ I and y ∈ I, one has

• DividedPowers.dpow_zero : dpow 0 x = 1

• DividedPowers.dpow_one : dpow 1 x = 1

• DividedPowers.dpow_add : dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y, this is the binomial theorem without binomial coefficients.

• DividedPowers.dpow_mul: dpow n (a * x) = a ^ n * dpow n x

• DividedPowers.mul_dpow : dpow m x * dpow n x = choose (m + n) m * dpow (m + n) x

• DividedPowers.dpow_comp : dpow m (dpow n x) = uniformBell m n * dpow (m * n) x

• DividedPowers.dividedPowersBot : the trivial divided powers structure on the zero ideal

• DividedPowers.prod_dpow: a product of divided powers is a multinomial coefficients times a divided power

• DividedPowers.dpow_sum: the multinomial theorem for divided powers, without multinomial coefficients.

• DividedPowers.ofRingEquiv: transfer divided powers along RingEquiv

• DividedPowers.equiv: the equivalence DividedPowers I ≃ DividedPowers J, for e : R ≃+* S, and I : Ideal R, J : Ideal S such that I.map e = J

• DividedPowers.exp: the power series Σ (dpow n a) X ^n

• DividedPowers.exp_add: its multiplicativity

References

• [P. Berthelot (1974), Cohomologie cristalline des schémas de caractéristique $p$ > 0][Berthelot-1974]

• [P. Berthelot and A. Ogus (1978), Notes on crystalline cohomology][BerthelotOgus-1978]

• [N. Roby (1963), Lois polynomes et lois formelles en théorie des modules][Roby-1963]

• [N. Roby (1965), Les algèbres à puissances dividées][Roby-1965]

Discussion

• In practice, one often has a single such structure to handle on a given ideal, but several ideals of the same ring might be considered. Without any explicit mention of the ideal, it is not clear whether such structures should be provided as instances.

• We do not provide any notation such as a ^[n] for dpow a n.

structure DividedPowers {A : Type u_1} [CommSemiring A] (I : Ideal A) : Type u_1

The divided power structure on an ideal I of a commutative ring A

• dpow : ℕ → A → A

  The divided power function underlying a divided power structure

• dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → self.dpow n x = 0
• dpow_zero : ∀ {x : A}, x ∈ I → self.dpow 0 x = 1
• dpow_one : ∀ {x : A}, x ∈ I → self.dpow 1 x = x
• dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → self.dpow n x ∈ I
• dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → self.dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, self.dpow k.1 x * self.dpow k.2 y
• dpow_mul : ∀ (n : ℕ) {a x : A}, x ∈ I → self.dpow n (a * x) = a ^ n * self.dpow n x
• mul_dpow : ∀ (m n : ℕ) {x : A}, x ∈ I → self.dpow m x * self.dpow n x = ↑((m + n).choose m) * self.dpow (m + n) x
• dpow_comp : ∀ (m : ℕ) {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → self.dpow m (self.dpow n x) = ↑(m.uniformBell n) * self.dpow (m * n) x

def dividedPowersBot (A : Type u_1) [CommSemiring A] [DecidableEq A] : DividedPowers ⊥

The canonical DividedPowers structure on the zero ideal

Equations

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

instance instInhabitedDividedPowersBotIdealOfDecidableEq {A : Type u_1} [CommSemiring A] [DecidableEq A] : Inhabited (DividedPowers ⊥)

Equations

• instInhabitedDividedPowersBotIdealOfDecidableEq = { default := dividedPowersBot A }

instance instCoeFunDividedPowersForallNatForall {A : Type u_1} [CommSemiring A] (I : Ideal A) : CoeFun (DividedPowers I) fun (x : DividedPowers I) => ℕ → A → A

The coercion from the divided powers structures to functions

Equations

• instCoeFunDividedPowersForallNatForall I = { coe := fun (hI : DividedPowers I) => hI.dpow }

theorem DividedPowers.ext {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI hI' : DividedPowers I) (h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x) : hI = hI'

theorem DividedPowers.coe_injective {A : Type u_1} [CommSemiring A] (I : Ideal A) : Function.Injective fun (h : DividedPowers I) => h.dpow

theorem DividedPowers.dpow_add' {A : Type u_1} [CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) (hb : b ∈ I) : hI.dpow n (a + b) = ∑ k ∈ Finset.range (n + 1), hI.dpow k a * hI.dpow (n - k) b

Variant of DividedPowers.dpow_add with a sum on range (n + 1)

def DividedPowers.exp {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) (a : A) : PowerSeries A

The exponential series of an element in the context of divided powers, Σ (dpow n a) X ^ n

Equations

• hI.exp a = PowerSeries.mk fun (n : ℕ) => hI.dpow n a

theorem DividedPowers.exp_add' {A : Type u_1} [CommSemiring A] {a b : A} (dp : ℕ → A → A) (dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ Finset.antidiagonal n, dp k.1 a * dp k.2 b) : (PowerSeries.mk fun (n : ℕ) => dp n (a + b)) = (PowerSeries.mk fun (n : ℕ) => dp n a) * PowerSeries.mk fun (n : ℕ) => dp n b

A more general of DividedPowers.exp_add

theorem DividedPowers.exp_add {A : Type u_1} [CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) (ha : a ∈ I) (hb : b ∈ I) : hI.exp (a + b) = hI.exp a * hI.exp b

theorem DividedPowers.dpow_smul {A : Type u_1} [CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) : hI.dpow n (b • a) = b ^ n • hI.dpow n a

theorem DividedPowers.dpow_mul_right {A : Type u_1} [CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) : hI.dpow n (a * b) = hI.dpow n a * b ^ n

theorem DividedPowers.dpow_smul_right {A : Type u_1} [CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) : hI.dpow n (a • b) = hI.dpow n a • b ^ n

theorem DividedPowers.factorial_mul_dpow_eq_pow {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) (n : ℕ) (ha : a ∈ I) : ↑n.factorial * hI.dpow n a = a ^ n

theorem DividedPowers.dpow_eval_zero {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {n : ℕ} (hn : n ≠ 0) : hI.dpow n 0 = 0

theorem DividedPowers.nilpotent_of_mem_dpIdeal {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} {n : ℕ} (hn : n ≠ 0) (hnI : ∀ {y : A}, y ∈ I → n • y = 0) (hI : DividedPowers I) (ha : a ∈ I) : a ^ n = 0

If an element of a divided power ideal is killed by multiplication by some nonzero integer n, then its nth power is zero.

Proposition 1.2.7 of [Berthelot-1974], part (i).

theorem DividedPowers.coincide_on_smul {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) {J : Ideal A} (hJ : DividedPowers J) {n : ℕ} (ha : a ∈ I • J) : hI.dpow n a = hJ.dpow n a

If J is another ideal of A with divided powers, then the divided powers of I and J coincide on I • J

[Berthelot-1974], 1.6.1 (ii)

theorem DividedPowers.prod_dpow {A : Type u_1} [CommSemiring A] {I : Ideal A} {a : A} (hI : DividedPowers I) {ι : Type u_2} {s : Finset ι} (n : ι → ℕ) (ha : a ∈ I) : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a

A product of divided powers is a multinomial coefficient times the divided power

[Roby-1965], formula (III')

theorem DividedPowers.dpow_sum' {A : Type u_1} [CommSemiring A] {M : Type u_2} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ → M → A) (dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1) (dpow_add : ∀ (n : ℕ) {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) (dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0) {ι : Type u_3} [DecidableEq ι] {s : Finset ι} {x : ι → M} (hx : ∀ i ∈ s, x i ∈ I) (n : ℕ) : dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)

Lemma towards dpow_sum when we only have partial information on a divided power ideal

theorem DividedPowers.dpow_sum {A : Type u_1} [CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {x : ι → A} (hx : ∀ i ∈ s, x i ∈ I) (n : ℕ) : hI.dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, hI.dpow (Multiset.count i ↑k) (x i)

A “multinomial” theorem for divided powers — without multinomial coefficients

def DividedPowers.ofRingEquiv {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) : DividedPowers J

Transfer divided powers under an equivalence

Equations

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

@[simp]

theorem DividedPowers.ofRingEquiv_dpow {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) (n : ℕ) (b : B) : (DividedPowers.ofRingEquiv h hI).dpow n b = e (hI.dpow n (e.symm b))

theorem DividedPowers.ofRingEquiv_dpow_apply {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) (n : ℕ) (a : A) : (DividedPowers.ofRingEquiv h hI).dpow n (e a) = e (hI.dpow n a)

def DividedPowers.equiv {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) : DividedPowers I ≃ DividedPowers J

Transfer divided powers under an equivalence (Equiv version)

Equations

• DividedPowers.equiv h = { toFun := DividedPowers.ofRingEquiv h, invFun := DividedPowers.ofRingEquiv ⋯, left_inv := ⋯, right_inv := ⋯ }

theorem DividedPowers.equiv_apply {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) (n : ℕ) (b : B) : ((DividedPowers.equiv h) hI).dpow n b = e (hI.dpow n (e.symm b))

theorem DividedPowers.equiv_apply' {A : Type u_1} {B : Type u_2} [CommSemiring A] {I : Ideal A} [CommSemiring B] {J : Ideal B} {e : A ≃+* B} (h : Ideal.map e I = J) (hI : DividedPowers I) (n : ℕ) (a : A) : ((DividedPowers.equiv h) hI).dpow n (e a) = e (hI.dpow n a)

Variant of DividedPowers.equiv_apply