The universal divided power algebra

Let R be a (commutative) semiring and M be an R-module. In this file we define Γ_R(M), the universal divided power algebra of M, as the ring quotient of the polynomial ring in the variables ℕ × M by the relation DividedPowerAlgebra.Rel.

DividedPowerAlgebra R M satisfies a weak universal property for morphisms to rings with divided powers.

Main definitions

• DividedPowerAlgebra.Rel: the type coding the basic relations that will give rise to the divided power algebra.

• DividedPowerAlgebra R M: the universal divided power algebra of the R-module M, defined as RingQuot of DividedPowerAlgebra.Rel R M.

• DividedPowerAlgebra.dp R n m: for n : ℕ and m : M, this is the equivalence class of MvPolynomial.X (⟨n, m⟩) in DividedPowerAlgebra R M.

  When that algebra is endowed with its canonical divided power structure (to be defined), the image of MvPolynomial.X (n, m), for any n : ℕ and m : M, is equal to the nth divided power of the image of m.

  The API will be setup so that it is never (never say never…) necessary to lift to MvPolynomial.

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

TODO

• Add the weak universal property of DividedPowerAlgebra R M.
• Show in upcoming files that DividedPowerAlgebra R M has divided powers.

inductive DividedPowerAlgebra.Rel (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : MvPolynomial (ℕ × M) R → MvPolynomial (ℕ × M) R → Prop

The type coding the basic relations that will give rise to the divided power algebra. The class of MvPolynomial.X (n, a) will be equal to dpow n a, for a ∈ M.

• rfl_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Rel R M 0 0
• zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {a : M} : Rel R M (MvPolynomial.X (0, a)) 1
• smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} {n : ℕ} {a : M} : Rel R M (MvPolynomial.X (n, r • a)) (r ^ n • MvPolynomial.X (n, a))
• mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : ℕ} {a : M} : Rel R M (MvPolynomial.X (m, a) * MvPolynomial.X (n, a)) ((m + n).choose m • MvPolynomial.X (m + n, a))
• add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {a b : M} : Rel R M (MvPolynomial.X (n, a + b)) (∑ k ∈ Finset.antidiagonal n, MvPolynomial.X (k.1, a) * MvPolynomial.X (k.2, b))

noncomputable def DividedPowerAlgebra.RelI (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Ideal (MvPolynomial (ℕ × M) R)

The ideal of MvPolynomial (ℕ × M) R generated by Rel.

Equations

• DividedPowerAlgebra.RelI R M = Ideal.ofRel (DividedPowerAlgebra.Rel R M)

@[reducible, inline]

abbrev DividedPowerAlgebra (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Type (max u_1 u_2)

The divided power algebra of a module M is defined as the ring quotient of the polynomial ring in the variables ℕ × M by the ring relation defined by DividedPowerAlgebra.Rel. We will later show that that DividedPowerAlgebra R M has divided powers. It satisfies a weak universal property for morphisms to rings with divided powers.

Equations

• DividedPowerAlgebra R M = RingQuot (DividedPowerAlgebra.Rel R M)

theorem DividedPowerAlgebra.mkAlgHom_surjective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Function.Surjective ⇑(RingQuot.mkAlgHom R (Rel R M))

theorem DividedPowerAlgebra.mkAlgHom_C {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : (RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a

theorem DividedPowerAlgebra.mkRingHom_C {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : R) : (RingQuot.mkRingHom (Rel R M)) (MvPolynomial.C a) = (algebraMap R (DividedPowerAlgebra R M)) a

noncomputable def DividedPowerAlgebra.dp (R : Type u_1) {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : DividedPowerAlgebra R M

dp R n m is the equivalence class of X (⟨n, m⟩) in DividedPowerAlgebra R M.

Equations

• DividedPowerAlgebra.dp R n m = (RingQuot.mkAlgHom R (DividedPowerAlgebra.Rel R M)) (MvPolynomial.X (n, m))

theorem DividedPowerAlgebra.dp_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : dp R n m = (RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.X (n, m))

theorem DividedPowerAlgebra.induction_on' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M) (h_C : ∀ (a : R), P ((RingQuot.mkAlgHom R (Rel R M)) (MvPolynomial.C a))) (h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)) (h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)) : P f

theorem DividedPowerAlgebra.induction_on {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {P : DividedPowerAlgebra R M → Prop} (f : DividedPowerAlgebra R M) (C : ∀ (a : R), P ((algebraMap R (DividedPowerAlgebra R M)) a)) (add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)) (dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)) : P f

theorem DividedPowerAlgebra.dp_eq_mkRingHom {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (m : M) : dp R n m = (RingQuot.mkRingHom (Rel R M)) (MvPolynomial.X (n, m))

@[simp]

theorem DividedPowerAlgebra.dp_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {m : M} : dp R 0 m = 1

theorem DividedPowerAlgebra.dp_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {r : R} {n : ℕ} {m : M} : dp R n (r • m) = r ^ n • dp R n m

theorem DividedPowerAlgebra.dp_null {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} : dp R n 0 = if n = 0 then 1 else 0

theorem DividedPowerAlgebra.dp_null_of_ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (hn : n ≠ 0) : dp R n 0 = 0

theorem DividedPowerAlgebra.dp_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n p : ℕ} {m : M} : dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m

theorem DividedPowerAlgebra.dp_add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} {x y : M} : dp R n (x + y) = ∑ k ∈ Finset.antidiagonal n, dp R k.1 x * dp R k.2 y

theorem DividedPowerAlgebra.dp_sum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (q : ℕ) (x : ι → M) : dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

theorem DividedPowerAlgebra.dp_sum_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} [DecidableEq ι] (s : Finset ι) (q : ℕ) (a : ι → R) (x : ι → M) : dp R q (∑ i ∈ s, a i • x i) = ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

theorem DividedPowerAlgebra.prod_dp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {s : Finset ι} {n : ι → ℕ} {m : M} : ∏ i ∈ s, dp R (n i) m = ↑(Nat.multinomial s n) * dp R (s.sum n) m

theorem DividedPowerAlgebra.natFactorial_mul_dp_eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : M) : ↑n.factorial * dp R n x = dp R 1 x ^ n

noncomputable def DividedPowerAlgebra.embed (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : M →ₗ[R] DividedPowerAlgebra R M

The canonical linear map M →ₗ[R] DividedPowerAlgebra R M.

Equations

• DividedPowerAlgebra.embed R M = { toFun := fun (m : M) => DividedPowerAlgebra.dp R 1 m, map_add' := ⋯, map_smul' := ⋯ }

theorem DividedPowerAlgebra.embed_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) : (embed R M) m = dp R 1 m

theorem DividedPowerAlgebra.algHom_ext_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A} : f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

theorem DividedPowerAlgebra.algHom_ext {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_3} [CommSemiring A] [Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A} (h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) : f = g

theorem DividedPowerAlgebra.submodule_span_prod_dp_eq_top {R : Type u_3} {M : Type u_4} {ι : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) : Submodule.span R (Set.range fun (n : ι →₀ ℕ) => n.prod fun (i : ι) (k : ℕ) => dp R k (v i)) = ⊤