Examples of divided power structures

In this file we show that, for certain choices of a commutative (semi)ring A and an ideal I of A, the family of maps ℕ → A → A given by fun n x ↦ x^n/n! is a divided power structure on I.

Main Definitions

• DividedPowers.OfInvertibleFactorial.dpow : the family of functions ℕ → A → A given by x^n/n!.
• DividedPowers.OfInvertibleFactorial.dividedPowers : the divided power structure on I given by fun x n ↦ x^n/n!, assuming that there exists a natural number n such that f (n-1)! is invertible in A and I^n = 0.
• DividedPowers.OfSquareZero.dividedPowers : given an ideal I such that I^2 =0, this is the divided power structure on I given by fun x n ↦ x^n/n!.
• DividedPowers.CharP.dividedPowers : if A is a commutative ring of prime characteristic p and I is an ideal such that I^p = 0, , this is the divided power structure on I given by fun x n ↦ x^n/n!.
• DividedPowers.RatAlgebra.dividedPowers : if I is any ideal in a ℚ-algebra, this is the divided power structure on I given by fun x n ↦ x^n/n!.

Main Results

• DividedPowers.RatAlgebra.dividedPowers_unique: there are no other divided power structures on an ideal of a ℚ-algebra.

References

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

• P. Berthelot and A. Ogus (1978), Notes on crystalline cohomology

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

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

noncomputable def DividedPowers.OfInvertibleFactorial.dpow {A : Type u_1} [CommSemiring A] (I : Ideal A) [DecidablePred fun (x : A) => x ∈ I] : ℕ → A → A

The family of functions ℕ → A → A given by x^n/n!.

Equations

• DividedPowers.OfInvertibleFactorial.dpow I m x = if x ∈ I then Ring.inverse ↑m.factorial * x ^ m else 0

theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {m : ℕ} {x : A} (hx : x ∈ I) : dpow I m x = Ring.inverse ↑m.factorial * x ^ m

theorem DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {m : ℕ} {x : A} (hx : x ∉ I) : dpow I m x = 0

theorem DividedPowers.OfInvertibleFactorial.dpow_null {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {m : ℕ} {x : A} (hx : x ∉ I) : dpow I m x = 0

theorem DividedPowers.OfInvertibleFactorial.dpow_zero {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {x : A} (hx : x ∈ I) : dpow I 0 x = 1

theorem DividedPowers.OfInvertibleFactorial.dpow_one {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {x : A} (hx : x ∈ I) : dpow I 1 x = x

theorem DividedPowers.OfInvertibleFactorial.dpow_mem {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {m : ℕ} (hm : m ≠ 0) {x : A} (hx : x ∈ I) : dpow I m x ∈ I

theorem DividedPowers.OfInvertibleFactorial.dpow_add_of_lt {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) {m : ℕ} (hmn : m < n) {x y : A} (hx : x ∈ I) (hy : y ∈ I) : dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

theorem DividedPowers.OfInvertibleFactorial.dpow_add {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m : ℕ} {x : A} (hx : x ∈ I) {y : A} (hy : y ∈ I) : dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

theorem DividedPowers.OfInvertibleFactorial.dpow_mul {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {m : ℕ} {a x : A} (hx : x ∈ I) : dpow I m (a * x) = a ^ m * dpow I m x

theorem DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_lt {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) {m k : ℕ} (hkm : m + k < n) {x : A} (hx : x ∈ I) : dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

theorem DividedPowers.OfInvertibleFactorial.mul_dpow {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m k : ℕ} {x : A} (hx : x ∈ I) : dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

theorem DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) {m k : ℕ} (hk : k ≠ 0) (hkm : m * k < n) {x : A} (hx : x ∈ I) : dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

theorem DividedPowers.OfInvertibleFactorial.dpow_comp {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m k : ℕ} (hk : k ≠ 0) {x : A} (hx : x ∈ I) : dpow I m (dpow I k x) = ↑(m.uniformBell k) * dpow I (m * k) x

noncomputable def DividedPowers.OfInvertibleFactorial.dividedPowers {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) : DividedPowers I

If (n-1)! is invertible in A and I^n = 0, then I admits a divided power structure. Proposition 1.2.7 of [B74], part (ii).

Equations

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

theorem DividedPowers.OfInvertibleFactorial.dpow_apply {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] {n : ℕ} (hn_fac : IsUnit ↑(n - 1).factorial) (hnI : I ^ n = 0) {m : ℕ} {x : A} : (dividedPowers hn_fac hnI).dpow m x = if x ∈ I then Ring.inverse ↑m.factorial * x ^ m else 0

noncomputable def DividedPowers.OfSquareZero.dividedPowers {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hI2 : I ^ 2 = 0) : DividedPowers I

If I^2 = 0, then I admits a divided power structure.

Equations

• DividedPowers.OfSquareZero.dividedPowers hI2 = DividedPowers.OfInvertibleFactorial.dividedPowers ⋯ hI2

theorem DividedPowers.OfSquareZero.dpow_of_two_le {A : Type u_1} [CommSemiring A] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hI2 : I ^ 2 = 0) {n : ℕ} (hn : 2 ≤ n) (a : A) : (dividedPowers hI2).dpow n a = 0

noncomputable def DividedPowers.IsNilpotent.dividedPowers {A : Type u_1} [CommRing A] {p : ℕ} [Fact (Nat.Prime p)] (hp : IsNilpotent ↑p) {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hIp : I ^ p = 0) : DividedPowers I

If A is a commutative ring of prime characteristic p and I is an ideal such that I^p = 0, then I admits a divided power structure.

Equations

• DividedPowers.IsNilpotent.dividedPowers hp hIp = DividedPowers.OfInvertibleFactorial.dividedPowers ⋯ hIp

theorem DividedPowers.IsNilpotent.dpow_of_prime_le {A : Type u_1} [CommRing A] {p : ℕ} [Fact (Nat.Prime p)] (hp : IsNilpotent ↑p) {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hIp : I ^ p = 0) {n : ℕ} (hn : p ≤ n) (a : A) : (dividedPowers hp hIp).dpow n a = 0

noncomputable def DividedPowers.CharP.dividedPowers (A : Type u_1) [CommRing A] (p : ℕ) [CharP A p] [Fact (Nat.Prime p)] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hIp : I ^ p = 0) : DividedPowers I

If A is a commutative ring of prime characteristic p and I is an ideal such that I^p = 0, then I admits a divided power structure.

Equations

• DividedPowers.CharP.dividedPowers A p hIp = DividedPowers.IsNilpotent.dividedPowers ⋯ hIp

theorem DividedPowers.CharP.dpow_of_prime_le (A : Type u_1) [CommRing A] (p : ℕ) [CharP A p] [Fact (Nat.Prime p)] {I : Ideal A} [DecidablePred fun (x : A) => x ∈ I] (hIp : I ^ p = 0) {n : ℕ} (hn : p ≤ n) (a : A) : (dividedPowers A p hIp).dpow n a = 0

noncomputable def DividedPowers.RatAlgebra.dpow {R : Type u_1} [CommSemiring R] (I : Ideal R) [DecidablePred fun (x : R) => x ∈ I] : ℕ → R → R

The family ℕ → R → R given by dpow n x = x ^ n / n!.

Equations

• DividedPowers.RatAlgebra.dpow I = DividedPowers.OfInvertibleFactorial.dpow I

theorem DividedPowers.RatAlgebra.dpow_eq_of_mem {R : Type u_1} [CommSemiring R] {I : Ideal R} [DecidablePred fun (x : R) => x ∈ I] (n : ℕ) {x : R} (hx : x ∈ I) : dpow I n x = Ring.inverse ↑n.factorial * x ^ n

noncomputable def DividedPowers.RatAlgebra.dividedPowers {R : Type u_1} [CommSemiring R] (I : Ideal R) [DecidablePred fun (x : R) => x ∈ I] [Algebra ℚ R] : DividedPowers I

If I is an ideal in a ℚ-algebra A, then I admits a unique divided power structure, given by dpow n x = x ^ n / n!.

Equations

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

@[simp]

theorem DividedPowers.RatAlgebra.dpow_apply {R : Type u_1} [CommSemiring R] (I : Ideal R) [DecidablePred fun (x : R) => x ∈ I] [Algebra ℚ R] {n : ℕ} {x : R} : (dividedPowers I).dpow n x = if x ∈ I then Ring.inverse ↑n.factorial * x ^ n else 0

theorem DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul {R : Type u_1} [CommSemiring R] (I : Ideal R) [Algebra ℚ R] (hI : DividedPowers I) {n : ℕ} {x : R} (hx : x ∈ I) : hI.dpow n x = Ring.inverse ↑n.factorial • x ^ n

If I is an ideal in a ℚ-algebra A, then the divided power structure on I given by dpow n x = x ^ n / n! is the only possible one.

theorem DividedPowers.RatAlgebra.dividedPowers_unique {R : Type u_1} [CommSemiring R] {I : Ideal R} [DecidablePred fun (x : R) => x ∈ I] [Algebra ℚ R] (hI : DividedPowers I) : hI = dividedPowers I

There are no other divided power structures on an ideal of a ℚ-algebra.